machine-code/garbage-collectors/lisp_gcScript.sml

16 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
26   E5957000 (* ldr r7,[r5] *)
27   E2078003 (* and r8,r7,#3 *)
30   14847004 (* strne r7,[r4],#4 *)
32   12447007 (* subne r7,r4,#7 *)
33   15857000 (* strne r7,[r5] *)
34   E2475001 (* sub r5,r7,#1 *)`;
39   E5967000 (* ldr r7,[r6] *)
40   E2078003 (* and r8,r7,#3 *)
43   14847004 (* strne r7,[r4],#4 *)
45   12447007 (* subne r7,r4,#7 *)
46   15867000 (* strne r7,[r6] *)
47   E2476001 (* sub r6,r7,#1 *)`;
97   E5197018 (* NO_GC:ldr r7,[r9,#-24] *)
101   14837004 (* strne r7,[r3],#4 *)
103   03A07002 (* moveq r7,#2 *)
104   05097018 (* streq r7,[r9,#-24] *)
118   E5097008 (* str r7,[r9,#-8] *)
125   E5197008 (* ldr r7,[r9,#-8] *)
268     (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8,d,xs) = (j2,x2,r7_2,r8_2,d2,xs2)) ==>
270     arm_move_pre(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs)``,
338   ``!a b b' i j j2 j3 e m m2 w ww r x xj2 xx2 xs xs2 d x2 xx  r7 r8 r7_2 r8_2 d2.
341     (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs) = (xj2,xx2,r7_2,r8_2,d2,xs2)) ==>
346     arm_move_pre(ref_addr a j,ref_field a (x,xx), r7,r8, d, xs)``,
373     (arm_cheney_step (r3,r4,r7,r8,d,xs) = (r3',r4',r5',r6',r7',r8',d',xs')) ==>
375     arm_cheney_step_pre (r3,r4,r7,r8,d,xs)``,
380   \\ Q.UNDISCH_TAC `arm_cheney_step (r3,r4,r7,r8,d,xs) = (r3',r4',r5',r6',r7',r8',d',xs')`
385   \\ `?r41 r52 r71 r81 d1 xs1. arm_move (ref_addr a j,r51,r7,r8,d,xs) = (r41,r52,r71,r81,d1,xs1)` by METIS_TAC [PAIR]
420        Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j2`,`j`,`e`,`m`,`m2`,`x`,`xx`,`r`,`ax`,`r41`,`r52`,`xs`,`xs1`,`d`,`x2`,`ad`,`r7`,`r8`,`r71`,`r81`,`d1`]) ref_cheney_move
457   ``!b i j e m x y r r3 r4 r5 r6 r7 r8 d xs i' m' r3' r4' r5' r6' r7' r8' d2 xs'.
460       (arm_cheney_loop (r3,r4,r5,r6,r7,r8,d,xs) = (r3',r4',r5',r6',r7',r8',d2,xs')) ==>
462       arm_cheney_loop_pre (r3,r4,r5,r6,r7,r8,d,xs)``,
479   \\ `?r31 r41 r51 r61 r71 r81 d1 xs1. arm_cheney_step (ref_addr a i,ref_addr a j,r7,r8,d,xs) =
488       arm_cheney_step_pre (r3,r4,r7,r8,d,xs)` by METIS_TAC [ref_cheney_step_thm]
538   ``!rs zs ds j m r4 r5 r7 r8 xs r12 ys jn mn.
544       (arm_move_roots(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) = (r4n,r5n,r6n,r7n,r8n,r12n,xn,xsn)) /\
546       arm_move_roots_pre(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) /\
562   \\ `?r41 r51 r71 r81 x1 xs1. arm_move (r4,xs r12,r7,r8,x,xs) = (r41,r51,r71,r81,x1,xs1)` by METIS_TAC [PAIR]
573   \\ `arm_move (ref_addr a j,ref_field a (h',h),r7,r8,x,xs) = (r41,r51,r71,r81,x1,xs1)` by METIS_TAC [WORD_ADD_0]
577     `w`,`ww`,`r`,`h'`,`r41`,`r51`,`xs`,`xs1`,`x`,`y1`,`h`,`r7`,`r8`,`r71`,`r81`,`x1`] o Q.INST [`ys`|->`xs`]) (INST_TYPE [``:'a``|->``:((bool[30] # bool) # bool[30] # bool)``] ref_cheney_move)
646     (arm_collect (r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
647     arm_collect_pre (r7,r8,a,x,xs) /\
660         arm_move_roots (r4l,r4l + n2w (8 * l),6w,r7,r8,a - 24w,x,xs2) =
721     (Q.SPECL [`b`,`m`,`r4l`,`r4l + n2w (8 * l)`,`r7`,`r8`,`xs2`,`a - 24w`,`ys`,`j2`,`m2`]
777     (arm_alloc_aux (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs) =
778                    (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
781     arm_alloc_aux_pre (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs)``,
790   \\ `?r3i r4i r5i r6i r7i r8i r9i xi xsi. arm_collect (r7,r8,a,x,xs) =
923     (arm_alloc_mem (r5,r6,r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
925     arm_alloc_mem_pre (r5,r6,r7,r8,a,x,xs)``,
937         arm_alloc_aux (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs) =
1049     (arm_alloc_mem (r5,r6,r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
1051     arm_alloc_mem_pre (r5,r6,r7,r8,a,x,xs) /\ arm_coll_inv (a,x,xs) (i,e,rs,rs2,l,u,m)``,
2193   ppc_move (r4:word32,r5:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
2195        (let r7 = f r5 in
2196         let r8 = r7 && 3w in
2198              (let r5 = r7 - 0x1w in (r4,r5,r7,r8,df,f))
2201               let f = (r4 =+ r7) f in
2205               let r7 = r4 - 0x7w in
2206               let f = (r5 =+ r7) f in
2207               let r5 = r7 - 0x1w in
2208                 (r4,r5,r7,r8,df,f))))
2210        (r4,r5,r7,r8,df,f))``
2213   ppc_move2 (r4:word32,r6:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
2215        (let r7 = f r6 in
2216         let r8 = 0x3w && r7 in
2218              (let r6 = r7 - 0x1w in (r4,r6,r7,r8,df,f))
2221               let f = (r4 =+ r7) f in
2225               let r7 = r4 - 0x7w in
2226               let f = (r6 =+ r7) f in
2227               let r6 = r7 - 0x1w in
2228                 (r4,r6,r7,r8,df,f))))
2230        (r4,r6,r7,r8,df,f))``
2233   ppc_cheney_step (r3:word32,r4:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
2236      let (r4,r5,r7,r8,df,f) = ppc_move (r4,r5,r7,r8,df,f) in
2237      let (r4,r6,r7,r8,df,f) = ppc_move2 (r4,r6,r7,r8,df,f) in
2242        (r3,r4,r5,r6,r7,r8,df,f))``;
2245   ppc_cheney_loop (r3,r4,r5,r6,r7,r8,df,f) =
2247        (r3,r4,r5,r6,r7,r8,df,f)
2249        (let (r3,r4,r5,r6,r7,r8,df,f) = ppc_cheney_step (r3,r4,r7,r8,df,f) in
2250           ppc_cheney_loop (r3,r4,r5,r6,r7,r8,df,f)))``;
2253   ppc_move_roots (r4,r5,r6:word32,r7,r8,r9,df,f) =
2255        (r4,r5,r6,r7,r8,r9,df,f)
2258         let (r4,r5,r7,r8,df,f) = ppc_move (r4,r5,r7,r8,df,f) in
2262           ppc_move_roots (r4,r5,r6,r7,r8,r9,df,f)))``
2274   ppc_collect (r7,r8,r9,df,f) =
2284      let (r4,r5,r6,r7,r8,r9,df,f) = ppc_move_roots (r4,r5,r6,r7,r8,r9,df,f) in
2285      let (r3,r4,r5,r6,r7,r8,df,f) = ppc_cheney_loop (r3,r4,r5,r6,r7,r8,df,f) in
2287        (r3,r4,r5,r6,r7,r8,r9,df,f))``;
2290   ppc_alloc_aux (r3,r4,r5,r6,r7,r8,r9,df,f) =
2292        (let (r3,r4,r5,r6,r7,r8,r9,df,f) = ppc_collect (r7,r8,r9,df,f) in
2293           (r3,r4,r5,r6,r7,r8,r9,df,f))
2295        (r3,r4,r5,r6,r7,r8,r9,df,f))``;
2299     (let r7 = f (r9 - 0x18w) in
2302           (let r7 = 0x2w in
2303            let f = (r9 - 0x18w =+ r7) f in
2304            let f = (r9 =+ r3) f in (r3,r4,r7,r8,r9,df,f))
2307            let f = (r3 =+ r7) f in
2312              (r3,r4,r7,r8,r9,df,f))))``;
2315   ppc_alloc_mem (r5,r6,r7,r8,r9,df,f) =
2318      let (r3,r4,r5,r6,r7,r8,r9,df,f) = ppc_alloc_aux (r3,r4,r5,r6,r7,r8,r9,df,f) in
2319      let (r3,r4,r7,r8,r9,df,f) = ppc_alloc_aux2 (r3,r4,r9,df,f) in
2320        (r3,r4,r5,r6,r7,r8,r9,df,f))``;
2323   ppc_alloc (r3,r4,r5,r6,r7,r8,r9,df,f) =
2328      let f = (r9 - 0x8w =+ r7) f in
2330      let (r3,r4,r5,r6,r7,r8,r9,df,f) = ppc_alloc_mem (r5,r6,r7,r8,r9,df,f) in
2335      let r7 = f (r9 - 0x8w) in
2337        (r3,r4,r5,r6,r7,r8,r9,df,f)``;