machine-code/just-in-time/jit_incrementalScript.sml

38   r7 ebp - pointer to j map and temp memory
180   r7 ebp - unchanged (pointer to j map and temp memory)
204   x86_access_j (r5,r7:word32,dh:word32 set,h:word32->word32) =
206     let r2 = r2 + r7 in
209       (r1,r2,r5,r7,dh,h)``;
329   x86_newcode (r1:word32,r5:word32,r7:word32,df:word32 set,f:word32->word8,dg:word32 set,g:word32->word8,dh:word32 set,h:word32->word32) =
330     if ~(r1 = 0w) then (r7,df,f,dg,g,dh,h) else
332       let r6 = h (r7 - 4w) in (* pointer to start of bytecode *)
337       let r5 = h (r7 - 32w) in
340       let r3 = h (r7 - 8w) in
342       let r4 = r7 + r1 in
344       let h = ((r7 - 8w) =+ r3) h in
345         (r7,df,f,dg,g,dh,h)``
370   x86_inc (r1,r2,r3,r4,r5,r6,r7,dh,h,df,f,dg,g) =
371     let h = (r7 - 12w =+ r1) h in
372     let h = (r7 - 16w =+ r2) h in
373     let h = (r7 - 20w =+ r3) h in
374     let h = (r7 - 24w =+ r4) h in (* address from which we got here *)
375     let h = (r7 - 28w =+ r6) h in
376     let h = (r7 - 32w =+ r5) h in
378     let (r1,r2,r5,r7,dh,h) = x86_access_j (r5,r7,dh,h) in
379     let (r7,df,f,dg,g,dh,h) = x86_newcode (r1,r5,r7,df,f,dg,g,dh,h) in
380     let r5 = h (r7 - 32w) in
381     let (r1,r2,r5,r7,dh,h) = x86_access_j (r5,r7,dh,h) in
382     let r4 = h (r7 - 24w) in
383     let r1 = h (r7 - 0x24w) in
388     let r1 = h (r7 - 12w) in
389     let r2 = h (r7 - 16w) in
390     let r3 = h (r7 - 20w) in
392     let r6 = h (r7 - 28w) in
393     let h = (r7 - 0x24w =+ r5) h in
394       (r1,r2,r3,r4,r5,r6,r7,dh,h,df,f,dg,g)``
422   ``i < LENGTH cs /\ LENGTH cs <= 128 /\ ALIGNED r7 /\
423     (r * MAP_INV r7 0 j cs) (fun2set (h,dh)) ==>
424     x86_access_j_pre (n2w i,r7,dh,h) /\
425     (x86_access_j (n2w i,r7,dh,h) =
427         if j i = NONE then 0w else THE (j i),n2w i,r7,dh,h))``,
432   \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`j`,`r7`])
1557   ``  LENGTH cs < 128 /\ ALIGNED r7 /\ n < LENGTH cs /\
1559       (pp * one (r7 - 0x20w,n2w n) * one (r7 - 8w,r3) * one (r7 - 4w,r6) * MAP_INV r7 0 j cs) (fun2set (h,dh)) /\
1564         x86_newcode_pre (r1,n2w n,r7,df,f,dg,g,dh,h) /\
1565         (x86_newcode (r1,n2w n,r7,df,f,dg,g,dh,h) =
1566            (r7,df,f2,dg,g,dh,h2)) /\
1569         (pp * one (r7 - 0x20w,n2w n) * one (r7 - 8w,r3i) * one (r7 - 4w,r6) * MAP_INV r7 0 j2 cs) (fun2set (h2,dh)) /\
1576   \\ `(h (r7 - 4w) = r6) /\ (r7 - 4w) IN dh` by SEP_READ_TAC
1577   \\ `(h (r7 - 8w) = r3) /\ (r7 - 8w) IN dh` by SEP_READ_TAC
1582   \\ `r7 - 0x20w IN dh /\ (h (r7 - 0x20w) = n2w n)` by SEP_READ_TAC
1587   \\ `ALIGNED (r7 + n2w (8 * (n - ji)))` by
1590   \\ STRIP_ASSUME_TAC (Q.SPECL [`n - ji`,`0`,`j`,`r7`,`cs`] MAP_INV_DROP_THM)
1592   \\ MP_TAC (Q.INST [`q`|->`qi`,`pp`|->`pp * one (r7 - 0x20w,n2w n) * one (r7 - 0x8w,r3) * one (r7 - 0x4w,r6) * MAP_INV r7 0 j (TAKE (n - ji) cs)`]
1594         ``x86_writecode (r3,r7 + 0x8w * n2w (n - ji),n2w (n - ji),r6i,df,f,dg,g,dh,h)``))
1598   \\ `r7 - 0x8w IN dh` by SEP_READ_TAC
1604   \\ STRIP_ASSUME_TAC (Q.SPECL [`n - ji`,`0`,`j2`,`r7`,`cs`] MAP_INV_DROP_THM)
1617   ``state_inv cs dh h dg g df f r7 j /\ n < LENGTH cs /\
1618     ((h (r7 - 0x24w) = 0w) ==> cont_jump j p cs r4 (n2w n)) ==>
1620        x86_inc_pre (r1,r2,r3,r4,n2w n,r6,r7,dh,h,df,f,dg,g) /\
1621        (x86_inc (r1,r2,r3,r4,n2w n,r6,r7,dh,h,df,f,dg,g) =
1622           (r1,r2,r3,w,0w,r6,r7,dh,h2,df,f2,dg,g)) /\
1623        state_inv cs dh h2 dg g df f2 r7 j2 /\ (j2 n = SOME w)``,
1626   \\ Q.PAT_ABBREV_TAC `h3 = (r7 - 0x20w:word32 =+ (n2w n):word32) fff`
1627   \\ `?ww. (SEP_T * one (r7 - 0xCw,r1) * one (r7 - 0x10w,r2) * one (r7 - 0x14w,r3) *
1628             one (r7 - 0x18w,r4) * one (r7 - 0x1Cw,r6) * one (r7 - 0x24w,ww) *
1629             one (r7 - 0x20w,n2w n) * one (r7 - 0x8w,a) * one (r7 - 0x4w,b) *
1630             MAP_INV r7 0 j cs) (fun2set (h3,dh))` by
1634   \\ `h (r7 - 0x24w) = ww` by
1635    (`h (r7 - 0x24w) = h3 (r7 - 0x24w)` by (Q.UNABBREV_TAC `h3`
1647    Q.INST [`r3`|->`a`,`r6`|->`b`,`pp`|->`SEP_T * one (r7 - 0xCw,r1) * one (r7 - 0x10w,r2) *
1648        one (r7 - 0x14w,r3) * one (r7 - 0x18w,r4) * one (r7 - 0x1Cw,r6) * one (r7 - 0x24w,ww)`,`q`|->`emp`] o
1651         then 0x0w else 0x1w,n2w n,r7,df,f,dg,g,dh,h3)``
1655   \\ `h2 (r7 - 0x20w) = n2w n` by SEP_READ_TAC
1662   \\ `h2 (r7 - 0x18w) = r4` by SEP_READ_TAC
1673   \\ `h2 (r7 - 0x24w) = ww` by SEP_READ_TAC
2342   x86_inc_init (r2:word32,r4:word32,r7:word32,dh:word32 set,h:word32->word32) =
2344     let h = (r7 =+ r5) h in
2345     let r7 = r7 + 36w in
2346     let h = (r7 - 4w =+ r2) h in
2347     let h = (r7 - 8w =+ r4) h in
2349     let r2 = r7 in
2352       (r7,dh,h)``