1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_ops"; 2 3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 4open combinTheory finite_mapTheory addressTheory; 5 6open decompilerLib progTheory set_sepTheory helperLib; 7open lisp_typeTheory lisp_invTheory lisp_gcTheory lisp_equalTheory; 8open ppc_encodeLib x86_encodeLib; 9open prog_armLib prog_ppcLib prog_x86Lib; 10 11val decompile_arm = decompile prog_armLib.arm_tools; 12val decompile_ppc = decompile prog_ppcLib.ppc_tools; 13val decompile_x86 = decompile prog_x86Lib.x86_tools; 14 15infix \\ 16val op \\ = op THEN; 17val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"]; 18val RW = REWRITE_RULE; 19val RW1 = ONCE_REWRITE_RULE; 20 21val aLISP_def = Define ` 22 aLISP (x1,x2,x3,x4,x5,x6,limit) = 23 SEP_EXISTS a r3 r4 r5 r6 r7 r8 df f dm m dg g s. 24 ~(aR 2w) * aR 3w r3 * aR 4w r4 * aR 5w r5 * aR 6w r6 * aR 7w r7 * aR 8w r8 * aR 9w a * 25 aMEMORY df f * aMEMORY dm m * aBYTE_MEMORY dg g * 26 cond (lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g))`; 27 28val pLISP_def = Define ` 29 pLISP (x1,x2,x3,x4,x5,x6,limit) = 30 SEP_EXISTS a r3 r4 r5 r6 r7 r8 df f dm m dg g s. 31 ~(pR 0w) * ~(pR 2w) * pR 3w r3 * pR 4w r4 * pR 5w r5 * pR 6w r6 * pR 7w r7 * pR 8w r8 * pR 9w a * 32 pMEMORY df f * pMEMORY dm m * pBYTE_MEMORY dg g * 33 cond (lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g))`; 34 35val xLISP_def = Define ` 36 xLISP (x1,x2,x3,x4,x5,x6,limit) = 37 SEP_EXISTS a r3 r4 r5 r6 r7 r8 df f dm m dg g s. 38 xR EAX r3 * xR ECX r4 * xR EDX r5 * xR EBX r6 * xR EDI r7 * xR ESI r8 * xR EBP a * 39 xMEMORY df f * xMEMORY dm m * xBYTE_MEMORY dg g * 40 cond (lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g))`; 41 42fun x86_reg 1 = "eax" | x86_reg 2 = "ecx" | x86_reg 3 = "edx" 43 | x86_reg 4 = "ebx" | x86_reg 5 = "edi" | x86_reg 6 = "esi" | x86_reg _ = fail() 44 45val _ = set_echo 0; 46 47 48(* automation *) 49 50fun dest_sep_exists tm = let 51 val (x,y) = dest_comb tm 52 val _ = if (fst o dest_const) x = "SEP_EXISTS" then () else fail() 53 in dest_abs y end; 54 55fun dest_sep_cond tm = 56 if (fst o dest_const o fst o dest_comb) tm = "cond" 57 then snd (dest_comb tm) else fail(); 58 59fun prove_spec th imp def pre_tm post_tm = let 60 val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) th 61 val tm = (cdr o concl o SPEC_ALL) def 62 val tm = repeat (snd o dest_sep_exists) tm 63 val fill = list_dest dest_star tm 64 val res = list_dest dest_star p 65 val res2 = filter (not o can dest_sep_cond) res 66 val fill2 = filter (not o can dest_sep_cond) fill 67 val res3 = map dest_comb (filter (not o can dest_sep_hide) res2) 68 val fill3 = map dest_comb (filter (not o can dest_sep_hide) fill2) 69 fun rename [] (y1,y2) = (y2,y2) 70 | rename ((x1,x2)::xs) (y1,y2) = if x1 ~~ y1 then (y2,x2) 71 else rename xs (y1,y2) 72 val s = map (fn (x,y) => x |-> y) (map (rename fill3) res3) 73 val th = INST s th 74 val th = UNDISCH_ALL (RW [SPEC_MOVE_COND] (SIMP_RULE (bool_ss++sep_cond_ss) [] th)) 75 val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) th 76 val fill = list_dest dest_star tm 77 val res = list_dest dest_star p 78 val f = list_mk_star (filter (fn x => not (tmem x res)) fill) (type_of (hd fill)) 79 val th = SPEC f (MATCH_MP SPEC_FRAME th) 80 val pre = (fst o dest_imp o snd o dest_imp) (concl imp) handle e => ``T:bool`` 81 val (_,p,_,_) = dest_spec (concl (PURE_REWRITE_RULE [GSYM SPEC_MOVE_COND] (DISCH pre th))) 82 val x = (snd o dest_star) p 83 val th = SPEC x (MATCH_MP SPEC_FRAME th) 84 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN th) 85 val goal = (cdr o car o concl) th 86 fun AUTO_EXISTS_TAC (asm,tm) = let 87 fun ex tm = let 88 val (v,tm) = dest_exists tm 89 in v :: ex tm end handle e => [] 90 val xs = ex tm 91 val x = hd (list_dest dest_conj (repeat (snd o dest_exists) tm)) 92 val assum = [``lisp_inv (Dot x1 x2,x2,x3,x4,x5,x6,limit) 93 (w1,w2,w3,w4,w5,w6,a',x',xs',s,dm,m,dg,g)``, 94 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) 95 (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g)``] 96 val tm2 = hd (filter (can (match_term x)) asm) 97 val (s,_) = match_term x tm2 98 val ys = map (subst s) xs 99 fun exx [] = ALL_TAC | exx (x::xs) = EXISTS_TAC x THEN exx xs 100 in exx ys (asm,tm) end 101 val lemma = prove(goal, 102 REWRITE_TAC [STAR_ASSOC] 103 \\ SIMP_TAC (std_ss++sep_cond_ss) [] 104 \\ REWRITE_TAC [SEP_IMP_MOVE_COND] 105 \\ REPEAT STRIP_TAC 106 \\ IMP_RES_TAC (SIMP_RULE std_ss [] imp) 107 \\ REPEAT (Q.PAT_X_ASSUM `xx ==> yy` (K ALL_TAC)) 108 \\ ASM_SIMP_TAC std_ss [LET_DEF] 109 \\ SIMP_TAC std_ss [def,SEP_CLAUSES] 110 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS] 111 \\ REPEAT STRIP_TAC 112 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 113 \\ AUTO_EXISTS_TAC 114 \\ FULL_SIMP_TAC std_ss [] 115 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_MULT_COMM WORD_MULT_ASSOC] 116 \\ METIS_TAC []) 117 val th = MATCH_MP th lemma 118 val th = RW [GSYM SPEC_MOVE_COND] (DISCH_ALL th) 119 val tm = (cdr o concl o SPEC_ALL) def 120 fun ff tm = let val (x,y) = dest_sep_exists tm in x :: ff y end handle e => [] 121 val zs = ff tm 122 fun gg [] th = th 123 | gg (x::xs) th = gg xs (EXISTS_PRE [ANTIQUOTE x] th) 124 val th = gg zs th 125 val th = MATCH_MP SPEC_STRENGTHEN th 126 val th = SPEC (mk_cond_star(pre_tm,pre)) th 127 val goal = (cdr o car o concl) th 128 val lemma = prove(goal, 129 SIMP_TAC std_ss [def,SEP_CLAUSES] 130 \\ SIMP_TAC (bool_ss++sep_cond_ss) [] 131 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS,cond_STAR] 132 \\ REPEAT STRIP_TAC 133 \\ AUTO_EXISTS_TAC 134 \\ FULL_SIMP_TAC std_ss [] 135 \\ IMP_RES_TAC (SIMP_RULE std_ss [] imp) 136 \\ REPEAT (Q.PAT_X_ASSUM `xx ==> yy` (K ALL_TAC)) 137 \\ FULL_SIMP_TAC std_ss [] 138 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ METIS_TAC []) 139 val th = MATCH_MP th lemma 140 val th = RW [SEP_CLAUSES] th 141 in th end; 142 143fun set_pc th = let 144 val (_,_,_,q) = (dest_spec o concl o UNDISCH_ALL) th 145 val tm = find_term (fn x => tmem (car x) [``xPC``,``aPC``,``pPC``] handle e => false) q 146 in subst [``p:word32``|->cdr tm] end 147 148 149(* cons *) 150 151val ARM_LISP_CONS = save_thm("ARM_LISP_CONS",let 152 val th = arm_alloc_thm 153 val imp = lisp_inv_cons 154 val def = aLISP_def 155 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 156 val post_tm = set_pc th ``aLISP (Dot x1 x2,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 157 val res = prove_spec th imp def pre_tm post_tm 158 val (_,_,c,_) = dest_spec (concl res) 159 val def = new_definition("arm_alloc_code",mk_eq(``(arm_alloc_code:word32->(word32 # word32) set) p``,c)) 160 val res = RW [GSYM def] res 161 in res end); 162 163val PPC_LISP_CONS = save_thm("PPC_LISP_CONS",let 164 val th = RW [ppc_alloc_EQ] ppc_alloc_thm 165 val imp = lisp_inv_cons 166 val def = pLISP_def 167 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 168 val post_tm = set_pc th ``pLISP (Dot x1 x2,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 169 val res = prove_spec th imp def pre_tm post_tm 170 val (_,_,c,_) = dest_spec (concl res) 171 val def = new_definition("ppc_alloc_code",mk_eq(``(ppc_alloc_code:word32->(word32 # word32) set) p``,c)) 172 val res = RW [GSYM def] res 173 in res end); 174 175val X86_LISP_CONS = save_thm("X86_LISP_CONS",let 176 val th = RW [x86_alloc_EQ] x86_alloc_thm 177 val imp = lisp_inv_cons 178 val def = xLISP_def 179 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 180 val post_tm = set_pc th ``xLISP (Dot x1 x2,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 181 val res = prove_spec th imp def pre_tm post_tm 182 val (_,_,c,_) = dest_spec (concl res) 183 val def = new_definition("x86_alloc_code",mk_eq(``(x86_alloc_code:word32->(word32 # word8 list # bool) set) p``,c)) 184 val res = RW [GSYM def] res 185 in res end); 186 187 188(* equal *) 189 190val ARM_LISP_EQUAL = save_thm("ARM_LISP_EQUAL",let 191 val th = arm_eq_thm 192 val imp = lisp_inv_equal 193 val def = aLISP_def 194 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 195 val post_tm = set_pc th ``aLISP (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 196 val res = prove_spec th imp def pre_tm post_tm 197 val (_,_,c,_) = dest_spec (concl res) 198 val def = new_definition("arm_equal_code",mk_eq(``(arm_equal_code:word32->(word32 # word32) set) p``,c)) 199 val res = RW [GSYM def] res 200 in res end); 201 202val PPC_LISP_EQUAL = save_thm("PPC_LISP_EQUAL",let 203 val th = ppc_eq_thm 204 val imp = lisp_inv_equal 205 val def = pLISP_def 206 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 207 val post_tm = set_pc th ``pLISP (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 208 val res = prove_spec th imp def pre_tm post_tm 209 val (_,_,c,_) = dest_spec (concl res) 210 val def = new_definition("ppc_equal_code",mk_eq(``(ppc_equal_code:word32->(word32 # word32) set) p``,c)) 211 val res = RW [GSYM def] res 212 in res end); 213 214val X86_LISP_EQUAL = save_thm("X86_LISP_EQUAL",let 215 val th = x86_eq_thm 216 val imp = lisp_inv_equal 217 val def = xLISP_def 218 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 219 val post_tm = set_pc th ``xLISP (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 220 val res = prove_spec th imp def pre_tm post_tm 221 val (_,_,c,_) = dest_spec (concl res) 222 val def = new_definition("x86_equal_code",mk_eq(``(x86_equal_code:word32->(word32 # word8 list # bool) set) p``,c)) 223 val res = RW [GSYM def] res 224 in res end); 225 226 227(* isDot and isSym *) 228 229fun ARM_LISP_ISDOT i = let 230 val _ = print "a" 231 val (arm_spec,_,sts,_) = arm_tools 232 val ((th,_,_),_) = arm_spec ("E31"^(int_to_string (i+2))^"0003") 233 val th = HIDE_POST_RULE ``aS1 psrN`` th 234 val th = HIDE_POST_RULE ``aS1 psrC`` th 235 val th = HIDE_POST_RULE ``aS1 psrV`` th 236 val th = HIDE_PRE_STATUS_RULE sts th 237 val def = aLISP_def 238 val imp = lisp_inv_test 239 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 240 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (isDot x) * ~(aS1 psrC) * ~(aS1 psrV)`` 241 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 242 val th = RW [ALIGNED_INTRO] th 243 val th = RW [ALIGNED_def] th 244 val result = prove_spec th imp def pre_tm post_tm 245 in save_thm("ARM_LISP_ISDOT" ^ int_to_string i,result) end; 246 247fun X86_LISP_ISDOT i = let 248 val _ = print "x" 249 val s = "test " ^ (x86_reg i) ^ ", 3" 250 val s = x86_encode s 251 val (spec,_,sts,_) = x86_tools 252 val ((th,_,_),_) = spec s 253 val th = HIDE_PRE_STATUS_RULE sts th 254 val th = HIDE_POST_RULE ``xS1 X_PF`` th 255 val th = HIDE_POST_RULE ``xS1 X_SF`` th 256 val th = HIDE_POST_RULE ``xS1 X_AF`` th 257 val th = HIDE_POST_RULE ``xS1 X_OF`` th 258 val th = HIDE_POST_RULE ``xS1 X_CF`` th 259 val def = xLISP_def 260 val imp = lisp_inv_test 261 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 262 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (isDot x)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF`` 263 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 264 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 265 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 266 val result = prove_spec th imp def pre_tm post_tm 267 in save_thm("X86_LISP_ISDOT" ^ int_to_string i,result) end; 268 269fun PPC_LISP_ISDOT i = let 270 val _ = print "p" 271 val s = "andi. 2, " ^ int_to_string (i+2) ^ ", 3" 272 val s = ppc_encode s 273 val (spec,_,sts,_) = ppc_tools 274 val ((th,_,_),_) = spec s 275 val th = HIDE_PRE_STATUS_RULE sts th 276 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th 277 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th 278 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th 279 val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th 280 val def = pLISP_def 281 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 282 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (isDot(x))) * ~(pS1 PPC_CARRY) * 283 ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)`` 284 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 285 val imp = lisp_inv_test 286 val th = HIDE_POST_RULE ``pR 2w`` th 287 val th = HIDE_PRE_RULE ``pR 2w`` th 288 val result = prove_spec th imp def pre_tm post_tm 289 in save_thm("PPC_LISP_ISDOT" ^ int_to_string i,result) end; 290 291val _ = map ARM_LISP_ISDOT [1,2,3,4,5,6] 292val _ = map X86_LISP_ISDOT [1,2,3,4,5,6] 293val _ = map PPC_LISP_ISDOT [1,2,3,4,5,6] 294 295fun ARM_LISP_ISSTR i = let 296 val (arm_spec,_,sts,_) = arm_tools 297 val ((th,_,_),_) = arm_spec ("E31"^(int_to_string (i+2))^"0001") 298 val th = HIDE_POST_RULE ``aS1 psrN`` th 299 val th = HIDE_POST_RULE ``aS1 psrC`` th 300 val th = HIDE_POST_RULE ``aS1 psrV`` th 301 val th = HIDE_PRE_STATUS_RULE sts th 302 val th = RW [Q.SPEC `n2w n` WORD_AND_COMM] th 303 val def = aLISP_def 304 val imp = lisp_inv_test 305 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 306 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ ~(isSym x) * ~(aS1 psrC) * ~(aS1 psrV)`` 307 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 308 val result = prove_spec th imp def pre_tm post_tm 309 in save_thm("ARM_LISP_ISSTR" ^ int_to_string i,result) end; 310 311fun X86_LISP_ISSTR i = let 312 val _ = print "x" 313 val s = "test " ^ (x86_reg i) ^ ", 1" 314 val s = x86_encode s 315 val (spec,_,sts,_) = x86_tools 316 val ((th,_,_),_) = spec s 317 val th = HIDE_PRE_STATUS_RULE sts th 318 val th = HIDE_POST_RULE ``xS1 X_PF`` th 319 val th = HIDE_POST_RULE ``xS1 X_SF`` th 320 val th = HIDE_POST_RULE ``xS1 X_AF`` th 321 val th = HIDE_POST_RULE ``xS1 X_OF`` th 322 val th = HIDE_POST_RULE ``xS1 X_CF`` th 323 val def = xLISP_def 324 val imp = lisp_inv_test 325 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 326 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME ~(isSym x)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF`` 327 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 328 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 329 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 330 val result = prove_spec th imp def pre_tm post_tm 331 in save_thm("X86_LISP_ISSTR" ^ int_to_string i,result) end; 332 333fun PPC_LISP_ISSTR i = let 334 val _ = print "p" 335 val s = "andi. 2, " ^ int_to_string (i+2) ^ ", 1" 336 val s = ppc_encode s 337 val (spec,_,sts,_) = ppc_tools 338 val ((th,_,_),_) = spec s 339 val th = HIDE_PRE_STATUS_RULE sts th 340 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th 341 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th 342 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th 343 val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th 344 val def = pLISP_def 345 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 346 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (~isSym(x))) * ~(pS1 PPC_CARRY) * 347 ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)`` 348 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 349 val imp = lisp_inv_test 350 val th = HIDE_POST_RULE ``pR 2w`` th 351 val th = HIDE_PRE_RULE ``pR 2w`` th 352 val result = prove_spec th imp def pre_tm post_tm 353 in save_thm("PPC_LISP_ISSTR" ^ int_to_string i,result) end; 354 355val _ = map ARM_LISP_ISSTR [1,2,3,4,5,6] 356val _ = map X86_LISP_ISSTR [1,2,3,4,5,6] 357val _ = map PPC_LISP_ISSTR [1,2,3,4,5,6] 358 359 360(* assign Sym "nil", Sym "t" *) 361 362fun swap_thm 1 = lisp_inv_swap1 363 | swap_thm 2 = lisp_inv_swap2 364 | swap_thm 3 = lisp_inv_swap3 365 | swap_thm 4 = lisp_inv_swap4 366 | swap_thm 5 = lisp_inv_swap5 367 | swap_thm 6 = lisp_inv_swap6 368 | swap_thm _ = fail() 369 370fun ARM_LISP_CONST (c,n,task,thc) i = let 371 val _ = print "a" 372 val s = "E3A0"^(int_to_string (i+2))^"0"^n 373 val (spec,_,_,_) = arm_tools 374 val ((th,_,_),_) = spec s 375 val imp = lisp_inv_move 376 val def = aLISP_def 377 val swap = swap_thm i 378 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 379 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 380 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 381 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)`` 382 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> c] 383 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]] 384 val post_tm = cdr (concl (INST s (REFL post_tm))) 385 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 386 val tm2 = cdr (concl (INST s (INST sw (REFL tm)))) 387 val result = prove_spec th imp def pre_tm post_tm 388 val r1 = save_thm("ARM_LISP_CONST" ^ int_to_string i ^ n,result) 389 val r2 = save_thm("ARM_LISP_CONST" ^ int_to_string i ^ "_" ^ task, 390 RW [GSYM TASK_EVAL_def,GSYM TASK_CONT_def,GSYM TASK_FUNC_def] result) 391 in (r1,r2) end 392 393val ARM_LISP_CONST_NIL = ARM_LISP_CONST (``(Sym "nil"):SExp``, "03", "EVAL", lisp_inv_nil) 394val ARM_LISP_CONST_T = ARM_LISP_CONST (``(Sym "t"):SExp``, "0F", "CONT", lisp_inv_t) 395val ARM_LISP_CONST_QUOTE = ARM_LISP_CONST (``(Sym "quote"):SExp``, "1B", "FUNC", lisp_inv_quote) 396 397val _ = map ARM_LISP_CONST_NIL [1,2,3,4,5,6] 398val _ = map ARM_LISP_CONST_T [1,2,3,4,5,6] 399val _ = map ARM_LISP_CONST_QUOTE [1,2,3,4,5,6] 400 401fun X86_LISP_CONST (c,n,task,thc) i = let 402 val _ = print "x" 403 val m = Arbnum.toString(Arbnum.fromHexString n) 404 val s = "mov " ^ x86_reg i ^ ", " ^ m 405 val s = x86_encode s 406 val (spec,_,_,_) = x86_tools 407 val ((th,_,_),_) = spec s 408 val imp = lisp_inv_move 409 val def = xLISP_def 410 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 411 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 412 val swap = swap_thm i 413 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 414 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 415 val pre_tm = mk_star(pre_tm, (snd o dest_star o cdr o car o car o concl) th) 416 val post_tm = mk_star(post_tm, (snd o dest_star o cdr o concl) th) 417 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> c] 418 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]] 419 val post_tm = cdr (concl (INST s (REFL post_tm))) 420 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 421 val tm2 = cdr (concl (INST s (INST sw (REFL tm)))) 422 val result = prove_spec th imp def pre_tm post_tm 423 val r1 = save_thm("X86_LISP_CONST" ^ int_to_string i ^ n,result) 424 val r2 = save_thm("X86_LISP_CONST" ^ int_to_string i ^ "_" ^ task, 425 RW [GSYM TASK_EVAL_def,GSYM TASK_CONT_def,GSYM TASK_FUNC_def] result) 426 in (r1,r2) end 427 428val X86_LISP_CONST_NIL = X86_LISP_CONST (``(Sym "nil"):SExp``, "03", "EVAL", lisp_inv_nil) 429val X86_LISP_CONST_T = X86_LISP_CONST (``(Sym "t"):SExp``, "0F", "CONT", lisp_inv_t) 430val X86_LISP_CONST_QUOTE = X86_LISP_CONST (``(Sym "quote"):SExp``, "1B", "FUNC", lisp_inv_quote) 431 432val _ = map X86_LISP_CONST_NIL [1,2,3,4,5,6] 433val _ = map X86_LISP_CONST_T [1,2,3,4,5,6] 434val _ = map X86_LISP_CONST_QUOTE [1,2,3,4,5,6] 435 436fun PPC_LISP_CONST (c,n,task,thc) i = let 437 val _ = print "p" 438 val m = Arbnum.toString(Arbnum.fromHexString n) 439 val s = "addi " ^ int_to_string (i+2) ^ ", 0, " ^ m 440 val s = ppc_encode s 441 val (spec,_,_,_) = ppc_tools 442 val ((th,_,_),_) = spec s 443 val th = RW [WORD_OR_CLAUSES] th 444 val def = pLISP_def 445 val swap = swap_thm i 446 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 447 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 448 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 449 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 4w)`` 450 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> c] 451 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]] 452 val post_tm = cdr (concl (INST s (REFL post_tm))) 453 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 454 val tm2 = cdr (concl (INST s (INST sw (REFL tm)))) 455 val result = prove_spec th imp def pre_tm post_tm 456 val r1 = save_thm("PPC_LISP_CONST" ^ int_to_string i ^ n,result) 457 val r2 = save_thm("PPC_LISP_CONST" ^ int_to_string i ^ "_" ^ task, 458 RW [GSYM TASK_EVAL_def,GSYM TASK_CONT_def,GSYM TASK_FUNC_def] result) 459 in (r1,r2) end 460 461val PPC_LISP_CONST_NIL = PPC_LISP_CONST (``(Sym "nil"):SExp``, "3", "EVAL", lisp_inv_nil) 462val PPC_LISP_CONST_T = PPC_LISP_CONST (``(Sym "t"):SExp``, "F", "CONT", lisp_inv_t) 463val PPC_LISP_CONST_QUOTE = PPC_LISP_CONST (``(Sym "quote"):SExp``, "1B", "FUNC", lisp_inv_quote) 464 465val _ = map PPC_LISP_CONST_NIL [1,2,3,4,5,6] 466val _ = map PPC_LISP_CONST_T [1,2,3,4,5,6] 467val _ = map PPC_LISP_CONST_QUOTE [1,2,3,4,5,6] 468 469 470(* assign 0 or 1 *) 471 472val lisp_inv_0 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `0` o UNDISCH) lisp_inv_Val 473val lisp_inv_1 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `1` o UNDISCH) lisp_inv_Val 474 475fun ARM_LISP_VAL thc i = let 476 val _ = print "a" 477 val v = find_term (can (match_term ``Val n``)) (concl thc) 478 val n = find_term (can (match_term ``(n2w n):word32``)) (concl thc) 479 val n = int_to_string (numSyntax.int_of_term (cdr n)) 480 val s = "E3A0"^(int_to_string (i+2))^"00"^n 481 val (spec,_,_,_) = arm_tools 482 val ((th,_,_),_) = spec s 483 val def = aLISP_def 484 val swap = swap_thm i 485 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 486 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 487 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 488 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)`` 489 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> v] 490 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]] 491 val post_tm = cdr (concl (INST s (REFL post_tm))) 492 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 493 val tm2 = cdr (concl (INST s (INST sw (REFL tm)))) 494 val result = prove_spec th imp def pre_tm post_tm 495 val r1 = save_thm("ARM_LISP_VAL_" ^ int_to_string i ^ "_" ^ n,result) 496 in r1 end 497 498val _ = map (ARM_LISP_VAL lisp_inv_0) [1,2,3,4,5,6] 499val _ = map (ARM_LISP_VAL lisp_inv_1) [1,2,3,4,5,6] 500 501fun X86_LISP_VAL thc i = let 502 val _ = print "x" 503 val v = find_term (can (match_term ``Val n``)) (concl thc) 504 val n = find_term (can (match_term ``(n2w n):word32``)) (concl thc) 505 val n = int_to_string (numSyntax.int_of_term (cdr n)) 506 val s = "mov " ^ x86_reg i ^ ", " ^ n 507 val s = x86_encode s 508 val (spec,_,_,_) = x86_tools 509 val ((th,_,_),_) = spec s 510 val def = xLISP_def 511 val swap = swap_thm i 512 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 513 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 514 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip`` 515 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip`` 516 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> v] 517 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]] 518 val post_tm = cdr (concl (INST s (REFL post_tm))) 519 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 520 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 521 val result = prove_spec th imp def pre_tm post_tm 522 val r1 = save_thm("X86_LISP_VAL_" ^ int_to_string i ^ "_" ^ n,result) 523 in r1 end 524 525val _ = map (X86_LISP_VAL lisp_inv_0) [1,2,3,4,5,6] 526val _ = map (X86_LISP_VAL lisp_inv_1) [1,2,3,4,5,6] 527 528fun PPC_LISP_VAL thc i = let 529 val _ = print "p" 530 val v = find_term (can (match_term ``Val n``)) (concl thc) 531 val n = find_term (can (match_term ``(n2w n):word32``)) (concl thc) 532 val n = int_to_string (numSyntax.int_of_term (cdr n)) 533 val s = "addi " ^ (int_to_string (i+2)) ^ ", 0, " ^ n 534 val s = ppc_encode s 535 val (spec,_,_,_) = ppc_tools 536 val ((th,_,_),_) = spec s 537 val def = pLISP_def 538 val swap = swap_thm i 539 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc)) 540 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap)) 541 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 542 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)`` 543 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> v] 544 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]] 545 val post_tm = cdr (concl (INST s (REFL post_tm))) 546 val result = prove_spec th imp def pre_tm post_tm 547 val r1 = save_thm("PPC_LISP_VAL_" ^ int_to_string i ^ "_" ^ n,result) 548 in r1 end 549 550val _ = map (PPC_LISP_VAL lisp_inv_0) [1,2,3,4,5,6] 551val _ = map (PPC_LISP_VAL lisp_inv_1) [1,2,3,4,5,6] 552 553 554(* move *) 555 556fun ARM_LISP_MOVE (i,j) = let 557 val _ = print "a" 558 val inst = "E1A0"^(int_to_string (i+2))^"00"^(int_to_string (j+2)) 559 val (spec,_,_,_) = arm_tools 560 val ((th,_,_),_) = spec inst 561 val imp = lisp_inv_move 562 val def = aLISP_def 563 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 564 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)`` 565 val s = [[QUOTE ("x" ^ int_to_string i)] |-> [QUOTE ("x" ^ int_to_string j)]] 566 val sw = [[QUOTE ("w" ^ int_to_string i)] |-> [QUOTE ("w" ^ int_to_string j)]] 567 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 568 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 569 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 570 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) 571 val result = prove_spec th imp def pre_tm post_tm 572 in save_thm("ARM_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end 573 574fun X86_LISP_MOVE (i,j) = let 575 val _ = print "x" 576 val s = "mov " ^ x86_reg i ^ ", " ^ x86_reg j 577 val s = x86_encode s 578 val (spec,_,_,_) = x86_tools 579 val ((th,_,_),_) = spec s 580 val imp = lisp_inv_move 581 val def = xLISP_def 582 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 583 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 584 val pre_tm = mk_star(pre_tm, (snd o dest_star o cdr o car o car o concl) th) 585 val post_tm = mk_star(post_tm, (snd o dest_star o cdr o concl) th) 586 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("x" ^ int_to_string j)]] 587 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("w" ^ int_to_string j)]] 588 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 589 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 590 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 591 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) 592 val result = prove_spec th imp def pre_tm post_tm 593 in save_thm("X86_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end 594 595fun PPC_LISP_MOVE (i,j) = let 596 val _ = print "p" 597 val s = "or " ^ int_to_string (i+2) ^ ", " ^ int_to_string (j+2) ^ ", " ^ int_to_string (j+2) 598 val s = ppc_encode s 599 val (spec,_,_,_) = ppc_tools 600 val ((th,_,_),_) = spec s 601 val th = RW [WORD_OR_CLAUSES] th 602 val imp = lisp_inv_move 603 val def = pLISP_def 604 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 605 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)`` 606 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("x" ^ int_to_string j)]] 607 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("w" ^ int_to_string j)]] 608 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 609 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 610 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 611 val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp]) 612 val result = prove_spec th imp def pre_tm post_tm 613 in save_thm("PPC_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end 614 615fun pairs x [] = [] | pairs x (y::ys) = (x,y) :: pairs x ys 616fun cross [] ys = [] | cross (x::xs) ys = pairs x ys @ cross xs ys 617val list = filter (fn (x,y) => not (x = y)) (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 618val _ = map ARM_LISP_MOVE list 619val _ = map X86_LISP_MOVE list 620val _ = map PPC_LISP_MOVE list 621 622 623(* car *) 624 625fun ARM_LISP_CAR (i,j) = let 626 val _ = print "a" 627 val inst = "E59"^(int_to_string (j+2))^(int_to_string (i+2))^"000" 628 val (spec,_,_,_) = arm_tools 629 val ((th,_,_),_) = spec inst 630 val def = aLISP_def 631 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 632 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)`` 633 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> Term [QUOTE ("CAR x" ^ int_to_string j ^ ":SExp")]] 634 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("(xs:word32->word32) w" ^ int_to_string j ^ ":word32")]] 635 val post_tm = subst s post_tm 636 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 637 val tm2 = subst s (subst sw tm) 638 val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)] 639 val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " IN (x:word32 set) /\\ (w" ^ int_to_string j ^ " && 3w = 0w)")] 640 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),METIS_TAC [lisp_inv_car,lisp_inv_address]) 641 val result = prove_spec th imp def pre_tm post_tm 642 in save_thm("ARM_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end 643 644fun X86_LISP_CAR (i,j) = let 645 val _ = print "x" 646 val s = "mov " ^ x86_reg i ^ ", [" ^ x86_reg j ^ "]" 647 val s = x86_encode s 648 val (spec,_,_,_) = x86_tools 649 val ((th,_,_),_) = spec s 650 val def = xLISP_def 651 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 652 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 653 val pc1 = find_term (can (match_term ``xPC p``)) ((cdr o car o car o concl) th) 654 val pc2 = find_term (can (match_term ``xPC p``)) ((cdr o concl) th) 655 val pre_tm = mk_star(pre_tm,pc1) 656 val post_tm = mk_star(post_tm,pc2) 657 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CAR x" ^ int_to_string j)]] 658 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 659 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) w" ^ int_to_string j)]] 660 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 661 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 662 val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)] 663 val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " IN (x:word32 set) /\\ (w" ^ int_to_string j ^ " && 3w = 0w)")] 664 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), 665 NTAC 2 STRIP_TAC 666 \\ IMP_RES_TAC lisp_inv_car 667 \\ IMP_RES_TAC lisp_inv_address 668 \\ ASM_SIMP_TAC std_ss []) 669 val result = prove_spec th imp def pre_tm post_tm 670 in save_thm("X86_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end 671 672fun PPC_LISP_CAR (i,j) = let 673 val _ = print "p" 674 val s = "lwz "^int_to_string(i+2)^",0("^int_to_string(j+2)^")" 675 val s = ppc_encode s 676 val (spec,_,_,_) = ppc_tools 677 val ((th,_,_),_) = spec s 678 val def = pLISP_def 679 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 680 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)`` 681 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CAR x" ^ int_to_string j)]] 682 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 683 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) w" ^ int_to_string j)]] 684 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 685 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 686 val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)] 687 val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " IN (x:word32 set) /\\ (w" ^ int_to_string j ^ " && 3w = 0w)")] 688 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), 689 NTAC 2 STRIP_TAC 690 \\ IMP_RES_TAC lisp_inv_car 691 \\ IMP_RES_TAC lisp_inv_address 692 \\ ASM_SIMP_TAC std_ss []) 693 val result = prove_spec th imp def pre_tm post_tm 694 in save_thm("PPC_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end 695 696val _ = map ARM_LISP_CAR (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 697val _ = map X86_LISP_CAR (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 698val _ = map PPC_LISP_CAR (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 699 700 701(* cdr *) 702 703fun ARM_LISP_CDR (i,j) = let 704 val _ = print "a" 705 val inst = "E59"^(int_to_string (j+2))^(int_to_string (i+2))^"004" 706 val (spec,_,_,_) = arm_tools 707 val ((th,_,_),_) = spec inst 708 val def = aLISP_def 709 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 710 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)`` 711 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> Term [QUOTE ("CDR x" ^ int_to_string j ^ ":SExp")]] 712 val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("(xs:word32->word32) (w" ^ int_to_string j ^ " + 4w):word32")]] 713 val post_tm = subst s post_tm 714 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 715 val tm2 = subst s (subst sw tm) 716 val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)] 717 val tm4 = Term [QUOTE ("(w" ^ int_to_string j ^ " + 4w) IN (x:word32 set) /\\ ((w" ^ int_to_string j ^ " + 4w) && 3w = 0w)")] 718 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), 719 REWRITE_TAC [ALIGNED_INTRO,ALIGNED_CLAUSES] 720 \\ REWRITE_TAC [ALIGNED_def] \\ METIS_TAC [lisp_inv_cdr,lisp_inv_address]) 721 val result = prove_spec th imp def pre_tm post_tm 722 in save_thm("ARM_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end 723 724fun X86_LISP_CDR (i,j) = let 725 val _ = print "x" 726 val s = "mov " ^ x86_reg i ^ ", [" ^ x86_reg j ^ "+4]" 727 val s = x86_encode s 728 val (spec,_,_,_) = x86_tools 729 val ((th,_,_),_) = spec s 730 val def = xLISP_def 731 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 732 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)`` 733 val pc1 = find_term (can (match_term ``xPC p``)) ((cdr o car o car o concl) th) 734 val pc2 = find_term (can (match_term ``xPC p``)) ((cdr o concl) th) 735 val pre_tm = mk_star(pre_tm,pc1) 736 val post_tm = mk_star(post_tm,pc2) 737 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CDR x" ^ int_to_string j)]] 738 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 739 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) (w" ^ int_to_string j ^ " + 4w)")]] 740 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 741 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 742 val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)] 743 val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " + 4w IN (x:word32 set) /\\ ((w" ^ int_to_string j ^ " + 4w) && 3w = 0w)")] 744 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), 745 NTAC 2 STRIP_TAC 746 \\ REWRITE_TAC [ALIGNED_INTRO,ALIGNED_CLAUSES] 747 \\ REWRITE_TAC [ALIGNED_def] 748 \\ IMP_RES_TAC lisp_inv_cdr 749 \\ IMP_RES_TAC lisp_inv_address 750 \\ ASM_SIMP_TAC std_ss []) 751 val result = prove_spec th imp def pre_tm post_tm 752 in save_thm("X86_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end 753 754fun PPC_LISP_CDR (i,j) = let 755 val _ = print "p" 756 val s = "lwz "^int_to_string(i+2)^",4("^int_to_string(j+2)^")" 757 val s = ppc_encode s 758 val (spec,_,_,_) = ppc_tools 759 val ((th,_,_),_) = spec s 760 val def = pLISP_def 761 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 762 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)`` 763 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CDR x" ^ int_to_string j)]] 764 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 765 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) (w" ^ int_to_string j ^ " + 4w)")]] 766 val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)`` 767 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 768 val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)] 769 val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " + 4w IN (x:word32 set) /\\ ((w" ^ int_to_string j ^ " + 4w) && 3w = 0w)")] 770 val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))), 771 NTAC 2 STRIP_TAC 772 \\ REWRITE_TAC [ALIGNED_INTRO,ALIGNED_CLAUSES] 773 \\ REWRITE_TAC [ALIGNED_def] 774 \\ IMP_RES_TAC lisp_inv_cdr 775 \\ IMP_RES_TAC lisp_inv_address 776 \\ ASM_SIMP_TAC std_ss []) 777 val result = prove_spec th imp def pre_tm post_tm 778 in save_thm("PPC_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end 779 780val _ = map ARM_LISP_CDR (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 781val _ = map X86_LISP_CDR (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 782val _ = map PPC_LISP_CDR (cross [1,2,3,4,5,6] [1,2,3,4,5,6]) 783 784 785(* add *) 786 787val ARM_LISP_ADD = let 788 val (th,def) = decompile_arm "ha" ` 789 E0833004 (* add r3,r3,r4 *) 790 E2433002 (* sub r3,r3,#2 *)` 791 val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th 792 val imp = lisp_inv_ADD 793 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 794 val def = aLISP_def 795 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 796 val post_tm = ``aLISP (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) * aPC (p + 0x8w)`` 797 val result = prove_spec th imp def pre_tm post_tm 798 in save_thm("ARM_LISP_ADD",result) end; 799 800val X86_LISP_ADD = let 801 val (th,def) = decompile_x86 "ha" ` 802 01C8 (* add eax,ecx *) 803 83E802 (* sub eax,2 *)` 804 val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th 805 val imp = lisp_inv_ADD 806 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 807 val def = xLISP_def 808 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 809 val post_tm = ``xLISP (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) * xPC (p + 0x5w) * ~xS`` 810 val result = prove_spec th imp def pre_tm post_tm 811 in save_thm("X86_LISP_ADD",result) end; 812 813val PPC_LISP_ADD = let 814 val (th,def) = decompile_ppc "ha" ` 815 7C632214 (* add 3,3,4 *) 816 3863FFFE (* addi 3,3,-2 *)` 817 val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th 818 val imp = lisp_inv_ADD 819 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 820 val def = pLISP_def 821 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 822 val post_tm = ``pLISP (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) * pPC (p + 0x8w)`` 823 val result = prove_spec th imp def pre_tm post_tm 824 in save_thm("PPC_LISP_ADD",result) end; 825 826 827(* sub *) 828 829val ARM_LISP_SUB = let 830 val (th,def) = decompile_arm "ha" ` 831 E0433004 (* sub r3,r3,r4 *) 832 E2833002 (* add r3,r3,#2 *)` 833 val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th 834 val imp = lisp_inv_SUB 835 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 836 val def = aLISP_def 837 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 838 val post_tm = ``aLISP (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) * aPC (p + 0x8w)`` 839 val result = prove_spec th imp def pre_tm post_tm 840 in save_thm("ARM_LISP_SUB",result) end; 841 842val X86_LISP_SUB = let 843 val (th,def) = decompile_x86 "ha" ` 844 29C8 (* sub eax,ecx *) 845 83C002 (* add eax,2 *)` 846 val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th 847 val imp = lisp_inv_SUB 848 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 849 val def = xLISP_def 850 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 851 val post_tm = ``xLISP (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) * xPC (p + 0x5w) * ~xS`` 852 val result = prove_spec th imp def pre_tm post_tm 853 in save_thm("X86_LISP_SUB",result) end; 854 855val PPC_LISP_SUB = let 856 val (th,def) = decompile_ppc "ha" ` 857 7C641810 (* subfc 3,4,3 *) 858 38630002 (* addi 3,3,2 *)` 859 val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th 860 val imp = lisp_inv_SUB 861 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 862 val def = pLISP_def 863 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 864 val post_tm = ``pLISP (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) * pPC (p + 0x8w) * ~pS`` 865 val result = prove_spec th imp def pre_tm post_tm 866 in save_thm("PPC_LISP_SUB",result) end; 867 868(* sub1 and add1 *) 869 870fun ARM_LISP_SUB1 i = let 871 val (arm_spec,_,sts,_) = arm_tools 872 val st = int_to_string (i+2) 873 val ((th,_,_),_) = arm_spec ("E24"^st^st^"004") 874 val imp = lisp_inv_SUB1 875 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 876 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 877 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) 878 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 879 val imp = RW1 [GSYM AND_IMP_INTRO] imp 880 val def = aLISP_def 881 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 882 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w)`` 883 val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")] 884 val tm = subst [``x:SExp``|->v] ``LISP_SUB x (Val 1)`` 885 val post_tm = subst [v|->tm] post_tm 886 val result = prove_spec th imp def pre_tm post_tm 887 in save_thm("ARM_LISP_SUB1_" ^ (int_to_string i),result) end; 888 889fun ARM_LISP_ADD1 i = let 890 val (arm_spec,_,sts,_) = arm_tools 891 val st = int_to_string (i+2) 892 val ((th,_,_),_) = arm_spec ("E28"^st^st^"004") 893 val imp = lisp_inv_ADD1 894 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 895 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 896 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) 897 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 898 val imp = RW1 [GSYM AND_IMP_INTRO] imp 899 val def = aLISP_def 900 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 901 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w)`` 902 val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")] 903 val tm = subst [``x:SExp``|->v] ``LISP_ADD x (Val 1)`` 904 val post_tm = subst [v|->tm] post_tm 905 val result = prove_spec th imp def pre_tm post_tm 906 in save_thm("ARM_LISP_ADD1_" ^ (int_to_string i),result) end; 907 908val _ = map ARM_LISP_SUB1 [1,2,3,4,5,6] 909val _ = map ARM_LISP_ADD1 [1,2,3,4,5,6] 910 911fun X86_LISP_SUB1 i = let 912 val st = x86_reg i 913 val s = x86_encode ("sub "^st^",4") 914 val (spec,_,sts,_) = x86_tools 915 val ((th,_,_),_) = spec s 916 val th = HIDE_STATUS_RULE true sts th 917 val imp = lisp_inv_SUB1 918 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 919 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 920 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) 921 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 922 val imp = RW1 [GSYM AND_IMP_INTRO] imp 923 val def = xLISP_def 924 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 925 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 926 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 927 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 928 val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")] 929 val tm = subst [``x:SExp``|->v] ``LISP_SUB x (Val 1)`` 930 val post_tm = subst [v|->tm] post_tm 931 val result = prove_spec th imp def pre_tm post_tm 932 in save_thm("X86_LISP_SUB1_" ^ (int_to_string i),result) end; 933 934fun X86_LISP_ADD1 i = let 935 val st = x86_reg i 936 val s = x86_encode ("add "^st^",4") 937 val (spec,_,sts,_) = x86_tools 938 val ((th,_,_),_) = spec s 939 val th = HIDE_STATUS_RULE true sts th 940 val imp = lisp_inv_ADD1 941 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 942 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 943 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) 944 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 945 val imp = RW1 [GSYM AND_IMP_INTRO] imp 946 val def = xLISP_def 947 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 948 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 949 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 950 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 951 val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")] 952 val tm = subst [``x:SExp``|->v] ``LISP_ADD x (Val 1)`` 953 val post_tm = subst [v|->tm] post_tm 954 val result = prove_spec th imp def pre_tm post_tm 955 in save_thm("X86_LISP_ADD1_" ^ (int_to_string i),result) end; 956 957val _ = map X86_LISP_SUB1 [1,2,3,4,5,6] 958val _ = map X86_LISP_ADD1 [1,2,3,4,5,6] 959 960fun PPC_LISP_SUB1 i = let 961 val st = int_to_string (i+2) 962 val s = ppc_encode ("addi "^st^","^st^",-4") 963 val (spec,_,sts,_) = ppc_tools 964 val ((th,_,_),_) = spec s 965 val imp = lisp_inv_SUB1 966 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 967 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 968 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) 969 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 970 val imp = RW1 [GSYM AND_IMP_INTRO] imp 971 val def = pLISP_def 972 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 973 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 0x4w)`` 974 val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")] 975 val tm = subst [``x:SExp``|->v] ``LISP_SUB x (Val 1)`` 976 val post_tm = subst [v|->tm] post_tm 977 val result = prove_spec th imp def pre_tm post_tm 978 in save_thm("PPC_LISP_SUB1_" ^ (int_to_string i),result) end; 979 980fun PPC_LISP_ADD1 i = let 981 val st = int_to_string (i+2) 982 val s = ppc_encode ("addi "^st^","^st^",4") 983 val (spec,_,sts,_) = ppc_tools 984 val ((th,_,_),_) = spec s 985 val imp = lisp_inv_ADD1 986 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 987 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 988 val imp = UNDISCH (RW [AND_IMP_INTRO] imp) 989 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 990 val imp = RW1 [GSYM AND_IMP_INTRO] imp 991 val def = pLISP_def 992 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p`` 993 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 0x4w)`` 994 val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")] 995 val tm = subst [``x:SExp``|->v] ``LISP_ADD x (Val 1)`` 996 val post_tm = subst [v|->tm] post_tm 997 val result = prove_spec th imp def pre_tm post_tm 998 in save_thm("PPC_LISP_ADD1_" ^ (int_to_string i),result) end; 999 1000val _ = map PPC_LISP_SUB1 [1,2,3,4,5,6] 1001val _ = map PPC_LISP_ADD1 [1,2,3,4,5,6] 1002 1003 1004(* less *) 1005 1006val ARM_LISP_LESS = let 1007 val (arm_spec,_,sts,_) = arm_tools 1008 val ((th,_,_),_) = arm_spec "E1530004" 1009 val imp = lisp_inv_LESS 1010 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1011 val imp = RW1 [EQ_SYM_EQ] imp 1012 val th = RW [GSYM WORD_NOT_LOWER] th 1013 val th = HIDE_PRE_STATUS_RULE sts th 1014 val th = HIDE_POST_RULE ``aS1 psrN`` th 1015 val th = HIDE_POST_RULE ``aS1 psrZ`` th 1016 val th = HIDE_POST_RULE ``aS1 psrV`` th 1017 val def = aLISP_def 1018 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 1019 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * ~(aS1 psrZ) * aS1 psrC ~(getVal x1 < getVal x2) * ~(aS1 psrV)`` 1020 val result = prove_spec th imp def pre_tm post_tm 1021 in save_thm("ARM_LISP_LESS",result) end; 1022 1023val X86_LISP_LESS = let 1024 val s = x86_encode "cmp eax,ecx" 1025 val (spec,_,sts,_) = x86_tools 1026 val ((th,_,_),_) = spec s 1027 val imp = lisp_inv_LESS 1028 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1029 val imp = RW1 [EQ_SYM_EQ] imp 1030 val th = RW [GSYM WORD_NOT_LOWER] th 1031 val th = HIDE_PRE_STATUS_RULE sts th 1032 val th = HIDE_POST_RULE ``xS1 X_PF`` th 1033 val th = HIDE_POST_RULE ``xS1 X_SF`` th 1034 val th = HIDE_POST_RULE ``xS1 X_AF`` th 1035 val th = HIDE_POST_RULE ``xS1 X_OF`` th 1036 val th = HIDE_POST_RULE ``xS1 X_ZF`` th 1037 val def = xLISP_def 1038 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 1039 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC (eip + 0x2w) * ~(xS1 X_AF) * ~(xS1 X_OF) * 1040 ~(xS1 X_SF) * ~(xS1 X_ZF) * ~(xS1 X_PF) * xS1 X_CF (SOME (getVal x1 < getVal x2))`` 1041 val result = prove_spec th imp def pre_tm post_tm 1042 in save_thm("X86_LISP_LESS",result) end; 1043 1044val PPC_LISP_LESS = let 1045 val s = ppc_encode "cmplw 3,4" 1046 val (spec,_,sts,_) = ppc_tools 1047 val ((th,_,_),_) = spec s 1048 val imp = lisp_inv_LESS 1049 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1050 val imp = RW1 [EQ_SYM_EQ] imp 1051 val th = RW [GSYM WORD_NOT_LOWER] th 1052 val th = HIDE_PRE_STATUS_RULE sts th 1053 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th 1054 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x2w)`` th 1055 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th 1056 val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th 1057 val def = pLISP_def 1058 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1059 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 0x4w) * 1060 pS1 (PPC_CR0 0x0w) (SOME (getVal x1 < getVal x2)) * ~pS1 PPC_CARRY * 1061 ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x2w) * ~pS1 (PPC_CR0 0x3w)`` 1062 val result = prove_spec th imp def pre_tm post_tm 1063 in save_thm("PPC_LISP_LESS",result) end; 1064 1065 1066(* mult, div and mod *) 1067 1068open divideTheory; 1069 1070val ARM_LISP_MULT = let 1071 val th = SIMP_RULE std_ss [lisp_word_mul_def,LET_DEF,SEP_CLAUSES] lisp_word_mul_arm_thm 1072 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th 1073 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1074 val th = SPEC (mk_var("r5",``:word32``)) th 1075 val imp = lisp_inv_MULT 1076 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1077 val def = aLISP_def 1078 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p`` 1079 val post_tm = set_pc th ``aLISP (LISP_MULT x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * aPC p`` 1080 val result = prove_spec th imp def pre_tm post_tm 1081 in save_thm("ARM_LISP_MULT",result) end; 1082 1083val PPC_LISP_MULT = let 1084 val th = SIMP_RULE std_ss [lisp_word_mul_def,LET_DEF,SEP_CLAUSES] lisp_word_mul_ppc_thm 1085 val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `pR 5w` SEP_HIDE_def])) th 1086 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1087 val th = SPEC (mk_var("r5",``:word32``)) th 1088 val imp = lisp_inv_MULT 1089 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1090 val def = pLISP_def 1091 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1092 val post_tm = set_pc th ``pLISP (LISP_MULT x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * pPC p * ~pS`` 1093 val result = prove_spec th imp def pre_tm post_tm 1094 in save_thm("PPC_LISP_MULT",result) end; 1095 1096val X86_LISP_MULT = let 1097 val th = SIMP_RULE std_ss [lisp_word_mul_def,LET_DEF,SEP_CLAUSES] lisp_word_mul_x86_thm 1098 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th 1099 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1100 val th = Q.SPEC `edx` th 1101 val imp = lisp_inv_MULT 1102 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1103 val def = xLISP_def 1104 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 1105 val post_tm = set_pc th ``xLISP (LISP_MULT x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * xPC p * ~xS`` 1106 val result = prove_spec th imp def pre_tm post_tm 1107 in save_thm("X86_LISP_MULT",result) end; 1108 1109val ARM_LISP_DIV = let 1110 val th = SIMP_RULE std_ss [lisp_word_div_def,LET_DEF,SEP_CLAUSES] lisp_word_div_arm_thm 1111 val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `aR 5w` SEP_HIDE_def])) th 1112 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1113 val th = SPEC (mk_var("r5",``:word32``)) th 1114 val imp = lisp_inv_DIV 1115 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1116 val def = aLISP_def 1117 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 1118 val post_tm = set_pc th ``aLISP (LISP_DIV x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * aPC p * ~aS`` 1119 val result = prove_spec th imp def pre_tm post_tm 1120 in save_thm("ARM_LISP_DIV",result) end; 1121 1122val PPC_LISP_DIV = let 1123 val th = SIMP_RULE std_ss [lisp_word_div_def,LET_DEF,SEP_CLAUSES] lisp_word_div_ppc_thm 1124 val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `pR 5w` SEP_HIDE_def])) th 1125 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1126 val th = SPEC (mk_var("r5",``:word32``)) th 1127 val imp = lisp_inv_DIV 1128 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1129 val def = pLISP_def 1130 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1131 val post_tm = set_pc th ``pLISP (LISP_DIV x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * pPC p * ~pS`` 1132 val result = prove_spec th imp def pre_tm post_tm 1133 in save_thm("PPC_LISP_DIV",result) end; 1134 1135val X86_LISP_DIV = let 1136 val th = SIMP_RULE std_ss [lisp_word_div_def,LET_DEF,SEP_CLAUSES] lisp_word_div_x86_thm 1137 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th 1138 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1139 val th = Q.SPEC `edx` th 1140 val imp = lisp_inv_DIV 1141 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1142 val def = xLISP_def 1143 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 1144 val post_tm = set_pc th ``xLISP (LISP_DIV x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * xPC p * ~xS`` 1145 val result = prove_spec th imp def pre_tm post_tm 1146 in save_thm("X86_LISP_DIV",result) end; 1147 1148val ARM_LISP_MOD = let 1149 val th = SIMP_RULE std_ss [lisp_word_mod_def,LET_DEF,SEP_CLAUSES] lisp_word_mod_arm_thm 1150 val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `aR 5w` SEP_HIDE_def])) th 1151 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1152 val th = SPEC (mk_var("r5",``:word32``)) th 1153 val imp = lisp_inv_MOD 1154 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1155 val def = aLISP_def 1156 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 1157 val post_tm = set_pc th ``aLISP (LISP_MOD x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * aPC p * ~aS`` 1158 val result = prove_spec th imp def pre_tm post_tm 1159 in save_thm("ARM_LISP_MOD",result) end; 1160 1161val PPC_LISP_MOD = let 1162 val th = SIMP_RULE std_ss [lisp_word_mod_def,LET_DEF,SEP_CLAUSES] lisp_word_mod_ppc_thm 1163 val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `pR 5w` SEP_HIDE_def])) th 1164 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1165 val th = SPEC (mk_var("r5",``:word32``)) th 1166 val imp = lisp_inv_MOD 1167 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1168 val def = pLISP_def 1169 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1170 val post_tm = set_pc th ``pLISP (LISP_MOD x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * pPC p * ~pS`` 1171 val result = prove_spec th imp def pre_tm post_tm 1172 in save_thm("PPC_LISP_MOD",result) end; 1173 1174val X86_LISP_MOD = let 1175 val th = SIMP_RULE std_ss [lisp_word_mod_def,LET_DEF,SEP_CLAUSES] lisp_word_mod_x86_thm 1176 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th 1177 val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th 1178 val th = Q.SPEC `edx` th 1179 val imp = lisp_inv_MOD 1180 val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1181 val def = xLISP_def 1182 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS`` 1183 val post_tm = set_pc th ``xLISP (LISP_MOD x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * xPC p * ~xS`` 1184 val result = prove_spec th imp def pre_tm post_tm 1185 in save_thm("X86_LISP_MOD",result) end; 1186 1187 1188(* test eq *) 1189 1190val ARM_LISP_EQ = let 1191 val _ = print "a" 1192 val i = 1 1193 val j = 2 1194 val (arm_spec,_,sts,_) = arm_tools 1195 val inst = "E13"^(int_to_string (i+2))^"000"^(int_to_string (j+2)) 1196 val ((th,_,_),_) = arm_spec inst 1197 val th = RW [WORD_EQ_XOR_ZERO] th 1198 val th = HIDE_POST_RULE ``aS1 psrN`` th 1199 val th = HIDE_POST_RULE ``aS1 psrC`` th 1200 val th = HIDE_POST_RULE ``aS1 psrV`` th 1201 val th = HIDE_PRE_STATUS_RULE sts th 1202 val def = aLISP_def 1203 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 1204 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = y:SExp) * ~(aS1 psrC) * ~(aS1 psrV)`` 1205 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1206 val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm 1207 val imp = lisp_inv_eq 1208 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1209 val result = prove_spec th imp def pre_tm post_tm 1210 in save_thm("ARM_LISP_EQ" ^ (int_to_string i) ^ (int_to_string j),result) end; 1211 1212val X86_LISP_EQ = let 1213 val _ = print "x" 1214 val i = 1 1215 val j = 2 1216 val s = "cmp " ^ (x86_reg i) ^ ", " ^ (x86_reg j) 1217 val s = x86_encode s 1218 val (spec,_,sts,_) = x86_tools 1219 val ((th,_,_),_) = spec s 1220 val th = RW [WORD_EQ_SUB_ZERO] th 1221 val th = HIDE_PRE_STATUS_RULE sts th 1222 val th = HIDE_POST_RULE ``xS1 X_PF`` th 1223 val th = HIDE_POST_RULE ``xS1 X_SF`` th 1224 val th = HIDE_POST_RULE ``xS1 X_AF`` th 1225 val th = HIDE_POST_RULE ``xS1 X_OF`` th 1226 val th = HIDE_POST_RULE ``xS1 X_CF`` th 1227 val def = xLISP_def 1228 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 1229 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = y:SExp)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF`` 1230 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1231 val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm 1232 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 1233 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 1234 val imp = lisp_inv_eq 1235 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1236 val result = prove_spec th imp def pre_tm post_tm 1237 in save_thm("X86_LISP_EQ" ^ (int_to_string i) ^ (int_to_string j),result) end; 1238 1239val PPC_LISP_EQ = let 1240 val _ = print "p" 1241 val i = 1 1242 val j = 2 1243 val s = "cmpw " ^ (int_to_string (i+2)) ^ ", " ^ (int_to_string (j+2)) 1244 val s = ppc_encode s 1245 val (spec,_,sts,_) = ppc_tools 1246 val ((th,_,_),_) = spec s 1247 val th = RW [WORD_EQ_SUB_ZERO] th 1248 val th = HIDE_PRE_STATUS_RULE sts th 1249 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th 1250 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th 1251 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th 1252 val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th 1253 val def = pLISP_def 1254 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1255 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = y:SExp)) * ~(pS1 PPC_CARRY) * 1256 ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)`` 1257 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1258 val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm 1259 val imp = lisp_inv_eq 1260 val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp)) 1261 val result = prove_spec th imp def pre_tm post_tm 1262 in save_thm("PPC_LISP_EQ" ^ (int_to_string i) ^ (int_to_string j),result) end; 1263 1264 1265(* test symbol *) 1266 1267fun ARM_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let 1268 val _ = print "a" 1269 val (arm_spec,_,sts,_) = arm_tools 1270 val s = Arbnum.toHexString(Arbnum.fromInt j) 1271 val s = if size(s) < 2 then "0" ^ s else s 1272 val ((th,_,_),_) = arm_spec ("E33"^(int_to_string (i+2))^"00"^s) 1273 val th = RW [WORD_EQ_XOR_ZERO] th 1274 val th = HIDE_POST_RULE ``aS1 psrN`` th 1275 val th = HIDE_POST_RULE ``aS1 psrC`` th 1276 val th = HIDE_POST_RULE ``aS1 psrV`` th 1277 val th = HIDE_PRE_STATUS_RULE sts th 1278 val def = aLISP_def 1279 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 1280 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = Sym str) * ~(aS1 psrC) * ~(aS1 psrV)`` 1281 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1282 val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm 1283 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) 1284 val imp = RW1 [EQ_SYM_EQ] imp 1285 val result = prove_spec th imp def pre_tm post_tm 1286 val result = RW [GSYM rw] result 1287 in save_thm("ARM_LISP_SYMBOL" ^ name ^ "_" ^ (int_to_string j),result) end; 1288 1289fun X86_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let 1290 val _ = print "x" 1291 val s = "cmp " ^ (x86_reg i) ^ ", " ^ int_to_string j 1292 val s = x86_encode s 1293 val (spec,_,sts,_) = x86_tools 1294 val ((th,_,_),_) = spec s 1295 val th = RW [WORD_EQ_SUB_ZERO] th 1296 val th = HIDE_PRE_STATUS_RULE sts th 1297 val th = HIDE_POST_RULE ``xS1 X_PF`` th 1298 val th = HIDE_POST_RULE ``xS1 X_SF`` th 1299 val th = HIDE_POST_RULE ``xS1 X_AF`` th 1300 val th = HIDE_POST_RULE ``xS1 X_OF`` th 1301 val th = HIDE_POST_RULE ``xS1 X_CF`` th 1302 val def = xLISP_def 1303 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 1304 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = Sym str)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF`` 1305 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1306 val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm 1307 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 1308 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 1309 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) 1310 val imp = RW1 [EQ_SYM_EQ] imp 1311 val result = prove_spec th imp def pre_tm post_tm 1312 val result = RW [GSYM rw] result 1313 in save_thm("X86_LISP_SYMBOL" ^ name ^ "_" ^ (int_to_string j),result) end; 1314 1315fun PPC_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let 1316 val _ = print "p" 1317 val s = "cmpwi " ^ (int_to_string (i+2)) ^ ", " ^ int_to_string j 1318 val s = ppc_encode s 1319 val (spec,_,sts,_) = ppc_tools 1320 val ((th,_,_),_) = spec s 1321 val th = RW [WORD_EQ_SUB_ZERO] th 1322 val th = HIDE_PRE_STATUS_RULE sts th 1323 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th 1324 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th 1325 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th 1326 val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th 1327 val def = pLISP_def 1328 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1329 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = Sym str)) * ~(pS1 PPC_CARRY) * 1330 ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)`` 1331 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1332 val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm 1333 val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i))) 1334 val imp = RW1 [EQ_SYM_EQ] imp 1335 val result = prove_spec th imp def pre_tm post_tm 1336 val result = RW [GSYM rw] result 1337 in save_thm("PPC_LISP_SYMBOL" ^ name ^ "_" ^ (int_to_string j),result) end; 1338 1339val list = let 1340 val th = SIMP_CONV std_ss [builtin_symbols_set_def,word_add_n2w] ``builtin_symbols_set 3w`` 1341 val xs = (helperLib.list_dest (pred_setSyntax.dest_insert) o snd o dest_eq o concl) th 1342 val xs = map pairSyntax.dest_pair (tl (rev xs)) 1343 val xs = map (fn (x,y) => (numSyntax.int_of_term ((snd (dest_comb x))), stringSyntax.fromHOLstring y)) xs 1344 in rev xs end 1345 1346val _ = map (ARM_LISP_EQ_SYMBOL (1,"_EXP",TRUTH)) [hd list]; 1347val _ = map (X86_LISP_EQ_SYMBOL (1,"_EXP",TRUTH)) [hd list]; 1348val _ = map (PPC_LISP_EQ_SYMBOL (1,"_EXP",TRUTH)) [hd list]; 1349 1350val _ = map (ARM_LISP_EQ_SYMBOL (2,"",TRUTH)) list; 1351val _ = map (X86_LISP_EQ_SYMBOL (2,"",TRUTH)) list; 1352val _ = map (PPC_LISP_EQ_SYMBOL (2,"",TRUTH)) list; 1353 1354val _ = ARM_LISP_EQ_SYMBOL (4,"_TASK",TASK_EVAL_def) (3,"nil") 1355val _ = ARM_LISP_EQ_SYMBOL (4,"_TASK",TASK_CONT_def) (15,"t") 1356val _ = ARM_LISP_EQ_SYMBOL (4,"_TASK",TASK_FUNC_def) (27,"quote") 1357 1358val _ = X86_LISP_EQ_SYMBOL (4,"_TASK",TASK_EVAL_def) (3,"nil") 1359val _ = X86_LISP_EQ_SYMBOL (4,"_TASK",TASK_CONT_def) (15,"t") 1360val _ = X86_LISP_EQ_SYMBOL (4,"_TASK",TASK_FUNC_def) (27,"quote") 1361 1362val _ = PPC_LISP_EQ_SYMBOL (4,"_TASK",TASK_EVAL_def) (3,"nil") 1363val _ = PPC_LISP_EQ_SYMBOL (4,"_TASK",TASK_CONT_def) (15,"t") 1364val _ = PPC_LISP_EQ_SYMBOL (4,"_TASK",TASK_FUNC_def) (27,"quote") 1365 1366 1367(* test for zero *) 1368 1369val lisp_inv_test_zero = (SIMP_RULE std_ss [] o Q.SPEC `0`) lisp_inv_eq_0 1370 1371fun ARM_LISP_EQ_ZERO i = let 1372 val _ = print "a" 1373 val (arm_spec,_,sts,_) = arm_tools 1374 val ((th,_,_),_) = arm_spec ("E33"^(int_to_string (i+2))^"0002") 1375 val th = RW [WORD_EQ_XOR_ZERO] th 1376 val th = HIDE_POST_RULE ``aS1 psrN`` th 1377 val th = HIDE_POST_RULE ``aS1 psrC`` th 1378 val th = HIDE_POST_RULE ``aS1 psrV`` th 1379 val th = HIDE_PRE_STATUS_RULE sts th 1380 val def = aLISP_def 1381 val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS`` 1382 val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = Val 0) * ~(aS1 psrC) * ~(aS1 psrV)`` 1383 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1384 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) 1385 val imp = RW1 [EQ_SYM_EQ] imp 1386 val result = prove_spec th imp def pre_tm post_tm 1387 in save_thm("ARM_LISP_EQ_ZERO_" ^ (int_to_string i),result) end; 1388 1389fun X86_LISP_EQ_ZERO i = let 1390 val _ = print "x" 1391 val s = "cmp " ^ (x86_reg i) ^ ", 2" 1392 val s = x86_encode s 1393 val (spec,_,sts,_) = x86_tools 1394 val ((th,_,_),_) = spec s 1395 val th = RW [WORD_EQ_SUB_ZERO] th 1396 val th = HIDE_PRE_STATUS_RULE sts th 1397 val th = HIDE_POST_RULE ``xS1 X_PF`` th 1398 val th = HIDE_POST_RULE ``xS1 X_SF`` th 1399 val th = HIDE_POST_RULE ``xS1 X_AF`` th 1400 val th = HIDE_POST_RULE ``xS1 X_OF`` th 1401 val th = HIDE_POST_RULE ``xS1 X_CF`` th 1402 val def = xLISP_def 1403 val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS`` 1404 val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = Val 0)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF`` 1405 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1406 val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th) 1407 val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm 1408 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) 1409 val imp = RW1 [EQ_SYM_EQ] imp 1410 val result = prove_spec th imp def pre_tm post_tm 1411 in save_thm("X86_LISP_EQ_ZERO_" ^ (int_to_string i),result) end; 1412 1413fun PPC_LISP_EQ_ZERO i = let 1414 val _ = print "p" 1415 val s = "cmpwi " ^ (int_to_string (i+2)) ^ ", 2" 1416 val s = ppc_encode s 1417 val (spec,_,sts,_) = ppc_tools 1418 val ((th,_,_),_) = spec s 1419 val th = RW [WORD_EQ_SUB_ZERO] th 1420 val th = HIDE_PRE_STATUS_RULE sts th 1421 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th 1422 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th 1423 val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th 1424 val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th 1425 val def = pLISP_def 1426 val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS`` 1427 val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = Val 0)) * ~(pS1 PPC_CARRY) * 1428 ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)`` 1429 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 1430 val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i))) 1431 val imp = RW1 [EQ_SYM_EQ] imp 1432 val result = prove_spec th imp def pre_tm post_tm 1433 in save_thm("PPC_LISP_EQ_ZERO_" ^ (int_to_string i),result) end; 1434 1435val _ = map ARM_LISP_EQ_ZERO [1,2,3,4,5,6]; 1436val _ = map X86_LISP_EQ_ZERO [1,2,3,4,5,6]; 1437val _ = map PPC_LISP_EQ_ZERO [1,2,3,4,5,6]; 1438 1439 1440val _ = export_theory(); 1441