1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_final"; 2 3open lisp_evalTheory lisp_parseTheory lisp_printTheory lisp_proofTheory; 4open lisp_invTheory; 5open pairSyntax helperLib; 6open listTheory pred_setTheory; 7open progTheory addressTheory set_sepTheory; 8open finite_mapTheory; 9 10val aLISP_def = lisp_opsTheory.aLISP_def; 11val pLISP_def = lisp_opsTheory.pLISP_def; 12val xLISP_def = lisp_opsTheory.xLISP_def; 13 14(* aid in hiding the code, temporarily *) 15 16fun take_until p [] = [] 17 | take_until p (x::xs) = if p x then [] else x:: take_until p xs 18 19val code_abbreviations = ref ([]:thm list); 20fun add_code_abbrev thms = (code_abbreviations := thms @ !code_abbreviations); 21 22fun ABBREV_CODE_RULE name th = let 23 val (m,_,c,_) = (dest_spec o concl o SPEC_ALL) th 24 val model_name = (to_lower o implode o take_until (fn x => x = #"_") o explode o fst o dest_const) m 25 val x = list_mk_pair (free_vars c) 26 val def_name = name ^ "_" ^ model_name 27 val v = mk_var(def_name,type_of(mk_pabs(x,c))) 28 val code_def = new_definition(def_name ^ "_def",mk_eq(mk_comb(v,x),c)) 29 val th = CONV_RULE ((RATOR_CONV o RAND_CONV) 30 (ONCE_REWRITE_CONV [GSYM code_def])) (UNDISCH_ALL th) 31 val _ = add_code_abbrev [code_def] 32 in th end; 33 34(* SPEC tools *) 35 36fun SPEC_STRENGTHEN_RULE th pre = let 37 val th = SPEC pre (MATCH_MP progTheory.SPEC_STRENGTHEN th) 38 val goal = (fst o dest_imp o concl) th 39 in (th,goal) end; 40 41fun SPEC_WEAKEN_RULE th post = let 42 val th = SPEC post (MATCH_MP progTheory.SPEC_WEAKEN th) 43 val goal = (fst o dest_imp o concl) th 44 in (th,goal) end; 45 46fun SPEC_FRAME_RULE th frame = 47 SPEC frame (MATCH_MP progTheory.SPEC_FRAME th) 48 49fun SPEC_BOOL_FRAME_RULE th frame = let 50 val th = MATCH_MP progTheory.SPEC_FRAME th 51 val th = Q.SPEC `cond boolean_variable_name` th 52 val th = INST [mk_var("boolean_variable_name",``:bool``) |-> frame] th 53 in th end 54 55fun subst_SPEC_PC th tm = let 56 val p = find_term (can (match_term ``aPC p``)) (cdr (concl th)) handle e => 57 find_term (can (match_term ``pPC p``)) (cdr (concl th)) handle e => 58 find_term (can (match_term ``xPC p``)) (cdr (concl th)) 59 val p = cdr p 60 val tm = subst [mk_var("p",``:word32``) |-> p] tm 61 in tm end; 62 63fun spec_pre th = let 64 val (_,p,_,_) = dest_spec (concl th) in (list_dest dest_star p, type_of p) end; 65fun spec_post th = let 66 val (_,_,_,q) = dest_spec (concl th) in (list_dest dest_star q, type_of q) end; 67 68fun spec_post_and_pre th1 th2 = let 69 val (_,_,_,q) = dest_spec (concl th1) 70 val (_,p,_,_) = dest_spec (concl th2) 71 in (list_dest dest_star q, list_dest dest_star p, type_of q) end; 72 73fun DISCH_ALL_AS_SINGLE_IMP th = let 74 val th = RW [AND_IMP_INTRO] (DISCH_ALL th) 75 in if is_imp (concl th) then th else DISCH ``T`` th end 76 77fun remove_primes th = let 78 fun last s = substring(s,size s-1,1) 79 fun delete_last_prime s = if last s = "'" then substring(s,0,size(s)-1) else fail() 80 fun foo [] ys i = i 81 | foo (x::xs) ys i = let 82 val name = (fst o dest_var) x 83 val new_name = repeat delete_last_prime name 84 in if name = new_name then foo xs (x::ys) i else let 85 val new_var = mk_var(new_name,type_of x) 86 in foo xs (new_var::ys) ((x |-> new_var) :: i) end end 87 val i = foo (free_varsl (concl th :: hyp th)) [] [] 88 in INST i th end 89 90fun find_composition1 th1 th2 = let 91 val (q,p,ty) = spec_post_and_pre th1 th2 92 fun get_match_term tm = get_sep_domain tm 93 fun mm x y = get_match_term x ~~ get_match_term y 94 fun fetch_match x [] zs = fail() 95 | fetch_match x (y::ys) zs = 96 if mm x y then (y, rev zs @ ys) else fetch_match x ys (y::zs) 97 fun partition [] ys (xs1,xs2,ys1) = (rev xs1, rev xs2, rev ys1, ys) 98 | partition (x::xs) ys (xs1,xs2,ys1) = 99 let val (y,zs) = fetch_match x ys [] in 100 partition xs zs (x::xs1, xs2, y::ys1) 101 end handle e => 102 partition xs ys (xs1, x::xs2, ys1) 103 val (xs1,xs2,ys1,ys2) = partition q p ([],[],[]) 104 val tm1 = mk_star (list_mk_star xs1 ty, list_mk_star xs2 ty) 105 val tm2 = mk_star (list_mk_star ys1 ty, list_mk_star ys2 ty) 106 val th1 = CONV_RULE (POST_CONV (MOVE_STAR_CONV tm1)) th1 107 val th2 = CONV_RULE (PRE_CONV (MOVE_STAR_CONV tm2)) th2 108 val th = MATCH_MP SPEC_FRAME_COMPOSE (DISCH_ALL_AS_SINGLE_IMP th2) 109 val th = MATCH_MP th (DISCH_ALL_AS_SINGLE_IMP th1) 110 val th = UNDISCH_ALL (PURE_REWRITE_RULE [GSYM AND_IMP_INTRO,AND_CLAUSES] th) 111 val th = SIMP_RULE std_ss [INSERT_UNION_EQ,UNION_EMPTY,word_arith_lemma1, 112 word_arith_lemma2,word_arith_lemma3,word_arith_lemma4,SEP_CLAUSES] th 113 in remove_primes th end; 114 115fun find_composition2 th1 th2 = let 116 val (q,p,ty) = spec_post_and_pre th1 th2 117 val post_not_hidden = map get_sep_domain (filter (not o can dest_sep_hide) q) 118 val pre_not_hidden = map get_sep_domain (filter (not o can dest_sep_hide) p) 119 fun f (d:term,(zs,to_be_hidden)) = 120 if not (can dest_sep_hide d) then (zs,to_be_hidden) else 121 (zs,filter (fn x => get_sep_domain d ~~ x) zs @ to_be_hidden) 122 val hide_from_post = snd (foldr f (post_not_hidden,[]) p) 123 val hide_from_pre = snd (foldr f (pre_not_hidden,[]) q) 124 val th1 = foldr (uncurry HIDE_POST_RULE) th1 hide_from_post 125 val th2 = foldr (uncurry HIDE_PRE_RULE) th2 hide_from_pre 126 in find_composition1 th1 th2 end; 127 128val SPEC_COMPOSE_RULE = find_composition2; 129 130fun LISP_SPEC_COMPOSE_RULE [] = fail() 131 | LISP_SPEC_COMPOSE_RULE [th] = th 132 | LISP_SPEC_COMPOSE_RULE (th1::th2::thms) = 133 LISP_SPEC_COMPOSE_RULE ((SPEC_COMPOSE_RULE th1 th2)::thms) 134 135(* SEP_EXISTS tools *) 136 137(* val tm = ``(SEP_EXISTS f z. cond (z = f + 5)) s`` *) 138 139open set_sepTheory 140open wordsTheory 141 142fun SEP_EXISTS_CONV tm = let 143 val m = ``$SEP_EXISTS (P :'a -> ('b -> bool) -> bool) (x :'b -> bool)`` 144 val i = match_term m tm 145 val (i,m) = match_term ((cdr o car o concl) SEP_EXISTS) ((car o car) tm) 146 val v = (fst o dest_abs o cdr o car) tm 147 val ty = (type_of o fst o dest_abs o cdr o car) tm 148 fun BETTER_ALPHA_CONV s tm = let 149 val (v,x) = dest_abs(tm) 150 in ALPHA_CONV (mk_var(s,type_of v)) tm end 151 val thi = CONV_RULE ( 152 (RAND_CONV) (BETTER_ALPHA_CONV "_") THENC 153 (RAND_CONV o ABS_CONV o ABS_CONV o RAND_CONV) 154 (ALPHA_CONV v)) (INST_TYPE m SEP_EXISTS) 155 in (((RATOR_CONV o RATOR_CONV) (fn tm => thi)) 156 THENC (RATOR_CONV BETA_CONV) THENC BETA_CONV 157 THENC (QUANT_CONV o RATOR_CONV) BETA_CONV) tm end 158 159fun EX_TAC [] = ALL_TAC 160 | EX_TAC (x::xs) = Q.EXISTS_TAC x THEN EX_TAC xs 161 162(* print *) 163 164val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9"] 165 166val one_string_IMP_string_mem = prove( 167 ``!s a c df f. one_string a s c (fun2set (f,df)) ==> string_mem s (a,f,df)``, 168 Induct 169 THEN FULL_SIMP_TAC std_ss [one_string_def,MAP,one_list_def,cond_def, 170 string_mem_def,one_STAR,IN_fun2set,GSYM AND_IMP_INTRO,fun2set_DELETE] 171 THEN ONCE_REWRITE_TAC [EQ_SYM_EQ] 172 THEN FULL_SIMP_TAC std_ss [fun2set_DELETE] 173 THEN REPEAT STRIP_TAC 174 THEN RES_TAC 175 THEN POP_ASSUM MP_TAC 176 THEN REPEAT (POP_ASSUM (K ALL_TAC)) 177 THEN Q.SPEC_TAC (`a+1w`,`b`) 178 THEN Induct_on `s` 179 THEN ASM_SIMP_TAC std_ss [string_mem_def,IN_DELETE]); 180 181val aLISP1_def = Define ` 182 aLISP1 (x,l) = SEP_EXISTS x2 x3 x4 x5 x6. aLISP (x,x2,x3,x4,x5,x6,l)`; 183val pLISP1_def = Define ` 184 pLISP1 (x,l) = SEP_EXISTS x2 x3 x4 x5 x6. pLISP (x,x2,x3,x4,x5,x6,l)`; 185val xLISP1_def = Define ` 186 xLISP1 (x,l) = SEP_EXISTS x2 x3 x4 x5 x6. xLISP (x,x2,x3,x4,x5,x6,l)`; 187 188val aSTRING_SPACE_def = Define ` 189 aSTRING_SPACE a n = SEP_EXISTS df f c. aBYTE_MEMORY df f * 190 cond (one_space a (n + 1) c (fun2set (f,df)))`; 191val pSTRING_SPACE_def = Define ` 192 pSTRING_SPACE a n = SEP_EXISTS df f c. pBYTE_MEMORY df f * 193 cond (one_space a (n + 1) c (fun2set (f,df)))`; 194val xSTRING_SPACE_def = Define ` 195 xSTRING_SPACE a n = SEP_EXISTS df f c. xBYTE_MEMORY df f * 196 cond (one_space a (n + 1) c (fun2set (f,df)))`; 197 198val one_space_EXPAND = prove( 199 ``!n a b s. one_space a n b s <=> 200 one_space a n (a + n2w n) s /\ (b = a + n2w n)``, 201 Induct 202 THEN SIMP_TAC std_ss [one_space_def,WORD_ADD_0,cond_def,SEP_EXISTS] 203 THEN SIMP_TAC std_ss [one_STAR] 204 THEN ONCE_ASM_REWRITE_TAC [] 205 THEN SIMP_TAC std_ss [DECIDE ``SUC n = 1 + n``,GSYM word_add_n2w,WORD_ADD_ASSOC] 206 THEN METIS_TAC []); 207 208val arm_sexp2string_th = let 209 val th = arm_sexp2string_thm 210 val imp = arm_print_sexp_lemma 211 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp 212 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp) 213 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp 214 val imp = RW [] imp 215 val tm = (fst o dest_imp o concl) imp 216 val th = SPEC_BOOL_FRAME_RULE th tm 217 val th = Q.INST [`r3`|->`w1`] th 218 val post = ``SEP_EXISTS r3 dg g dm m dh h. aR 3w r3 * aSTRING r3 (sexp2string t1) 219 * aBYTE_MEMORY dg g * aMEMORY dh h * aMEMORY dm m * ~aR 0w * 220 ~aR 1w * ~aR 2w * ~aR 4w * ~aR 5w * ~aR 6w * ~aR 7w 221 * ~aR 8w * ~aR 9w * aPC p * ~aS`` 222 val post = subst_SPEC_PC th post 223 val (th,goal) = SPEC_WEAKEN_RULE th post 224 val tac = 225 SIMP_TAC std_ss [aSTRING_def] 226 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 227 THEN STRIP_TAC 228 THEN IMP_RES_TAC (Q.INST [`w1`|->`r3`] imp) 229 THEN FULL_SIMP_TAC (std_ss++sep_cond_ss) [arm_sexp2string_def,LET_DEF] 230 THEN SIMP_TAC std_ss [SEP_IMP_def] 231 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 232 THEN REPEAT STRIP_TAC 233 THEN EX_TAC [`r1`,`dg`,`g`,`dm`,`m`,`dh`,`hi`,`df`,`fi`] 234 THEN IMP_RES_TAC one_string_IMP_string_mem 235 THEN ASM_SIMP_TAC std_ss [cond_STAR] 236 THEN FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM] 237 val th = MP th (prove(goal,tac)) 238 val th = foldr (uncurry EXISTS_PRE) th [`df`,`f`,`dg`,`g`,`dm`,`m`,`dh`,`h`,`sym`] 239 val th = foldr (uncurry EXISTS_PRE) th [`t2`,`t3`,`t4`,`t5`,`t6`] 240 val th = foldr (uncurry EXISTS_PRE) th [`w1`,`w2`,`w3`,`w4`,`w5`,`w6`,`r9`] 241 val pre = ``aLISP1 (t1,l) * aR 1w r1 * aSTRING_SPACE r1 (LENGTH (sexp2string t1)) * 242 ~aR 0w * aPC p * ~aS`` 243 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 244 val tac = 245 SIMP_TAC std_ss [aSTRING_SPACE_def] 246 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 247 THEN SIMP_TAC std_ss [aLISP1_def,aLISP_def] 248 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 249 THEN SIMP_TAC std_ss [SEP_IMP_def] 250 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 251 THEN SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,Once one_space_EXPAND] 252 THEN NTAC 2 STRIP_TAC 253 THEN EX_TAC [`r3`,`r4`,`r5`,`r6`,`r7`,`r8`,`a`] 254 THEN EX_TAC [`x2`,`x3`,`x4`,`x5`,`x6`] 255 THEN EX_TAC [`df`,`f`,`dg`,`g`,`dm`,`m`,`df'`,`f'`,`s'`] 256 THEN IMP_RES_TAC imp 257 THEN ASM_SIMP_TAC std_ss [arm_sexp2string_pre_def,LET_DEF] 258 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `aR 4w` SEP_HIDE_def,SEP_CLAUSES] 259 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `aR 5w` SEP_HIDE_def,SEP_CLAUSES] 260 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `aR 6w` SEP_HIDE_def,SEP_CLAUSES] 261 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `aR 7w` SEP_HIDE_def,SEP_CLAUSES] 262 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `aR 8w` SEP_HIDE_def,SEP_CLAUSES] 263 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 264 THEN EX_TAC [`r4`,`r5`,`r6`,`r7`,`r8`] 265 THEN FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM] 266 val th = MP th (prove(goal,tac)) 267 in th end; 268 269val ppc_sexp2string_th = let 270 val th = ppc_sexp2string_thm 271 val imp = arm_print_sexp_lemma 272 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp 273 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp) 274 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp 275 val imp = RW [] imp 276 val tm = (fst o dest_imp o concl) imp 277 val th = SPEC_BOOL_FRAME_RULE th tm 278 val th = Q.INST [`r3`|->`w1`] th 279 val post = ``SEP_EXISTS r3 dg g dm m dh h. pR 3w r3 * pSTRING r3 (sexp2string t1) 280 * pBYTE_MEMORY dg g * pMEMORY dh h * pMEMORY dm m * ~pR 0w * 281 ~pR 1w * ~pR 2w * ~pR 4w * ~pR 5w * ~pR 6w * ~pR 7w 282 * ~pR 8w * ~pR 9w * pPC p * ~pS`` 283 val post = subst_SPEC_PC th post 284 val (th,goal) = SPEC_WEAKEN_RULE th post 285 val tac = 286 SIMP_TAC std_ss [pSTRING_def] 287 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 288 THEN STRIP_TAC 289 THEN IMP_RES_TAC (Q.INST [`w1`|->`r3`] imp) 290 THEN FULL_SIMP_TAC (std_ss++sep_cond_ss) [ppc_sexp2string_def,LET_DEF,WORD_OR_CLAUSES] 291 THEN SIMP_TAC std_ss [SEP_IMP_def] 292 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 293 THEN REPEAT STRIP_TAC 294 THEN EX_TAC [`r1`,`dg`,`g`,`dm`,`m`,`dh`,`hi`,`df`,`fi`] 295 THEN IMP_RES_TAC one_string_IMP_string_mem 296 THEN ASM_SIMP_TAC std_ss [cond_STAR] 297 THEN FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM] 298 val th = MP th (prove(goal,tac)) 299 val th = foldr (uncurry EXISTS_PRE) th [`df`,`f`,`dg`,`g`,`dm`,`m`,`dh`,`h`,`sym`] 300 val th = foldr (uncurry EXISTS_PRE) th [`t2`,`t3`,`t4`,`t5`,`t6`] 301 val th = foldr (uncurry EXISTS_PRE) th [`w1`,`w2`,`w3`,`w4`,`w5`,`w6`,`r9`] 302 val pre = ``pLISP1 (t1,l) * pR 1w r1 * pSTRING_SPACE r1 (LENGTH (sexp2string t1)) * 303 pPC p * ~pS`` 304 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 305 val tac = 306 SIMP_TAC std_ss [pSTRING_SPACE_def] 307 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 308 THEN SIMP_TAC std_ss [pLISP1_def,pLISP_def] 309 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 310 THEN SIMP_TAC std_ss [SEP_IMP_def] 311 THEN CONV_TAC ((REDEPTH_CONV SEP_EXISTS_CONV)) 312 THEN SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,Once one_space_EXPAND] 313 THEN NTAC 2 STRIP_TAC 314 THEN EX_TAC [`r3`,`r4`,`r5`,`r6`,`r7`,`r8`,`a`] 315 THEN EX_TAC [`x2`,`x3`,`x4`,`x5`,`x6`] 316 THEN EX_TAC [`df`,`f`,`dg`,`g`,`dm`,`m`,`df'`,`f'`,`s'`] 317 THEN IMP_RES_TAC imp 318 THEN ASM_SIMP_TAC std_ss [ppc_sexp2string_pre_def,LET_DEF,WORD_OR_CLAUSES] 319 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `pR 4w` SEP_HIDE_def,SEP_CLAUSES] 320 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `pR 5w` SEP_HIDE_def,SEP_CLAUSES] 321 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `pR 6w` SEP_HIDE_def,SEP_CLAUSES] 322 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `pR 7w` SEP_HIDE_def,SEP_CLAUSES] 323 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `pR 8w` SEP_HIDE_def,SEP_CLAUSES] 324 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 325 THEN EX_TAC [`r4`,`r5`,`r6`,`r7`,`r8`] 326 THEN FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM] 327 val th = MP th (prove(goal,tac)) 328 in th end; 329 330val xSTACK_def = Define ` 331 (xSTACK a [] = cond (ALIGNED a)) /\ 332 (xSTACK a (w::ws) = xM a w * xSTACK (a + 4w) ws)`; 333 334val xSTACK_PUSH_EDI = let 335 val (th,t_def) = decompilerLib.decompile 336 prog_x86Lib.x86_tools "test" [QUOTE (x86_encodeLib.x86_encode "push edi")] 337 val th = SIMP_RULE std_ss [t_def,LET_DEF] th 338 val th = Q.INST [`df`|->`{esp - 4w}`,`f`|->`\x.w`] th 339 val th = SPEC_BOOL_FRAME_RULE th ``ALIGNED esp`` 340 val post = ``xSTACK (esp-4w) [edi] * xR EDI edi * xR ESP (esp - 0x4w) * xPC (p + 0x1w)`` 341 val (th,goal) = SPEC_WEAKEN_RULE th post 342 val tac = 343 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,xSTACK_def,prog_x86Theory.xM_THM, 344 ALIGNED,SEP_CLAUSES] THEN SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL] 345 val th = MP th (prove(goal,tac)) 346 val pre = ``xSTACK (esp-4w) [w] * xR EDI edi * xR ESP esp * xPC p`` 347 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 348 val tac = 349 SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_MOVE_COND,xSTACK_def,prog_x86Theory.xM_THM, 350 ALIGNED,SEP_CLAUSES,SEP_IMP_REFL,IN_INSERT,NOT_IN_EMPTY] 351 THEN SIMP_TAC (std_ss++star_ss) [ALIGNED_INTRO,ALIGNED,SEP_CLAUSES,SEP_IMP_REFL] 352 val th = MP th (prove(goal,tac)) 353 in th end; 354 355val xSTACK_MOVE_EDI = let 356 val (th,t_def) = decompilerLib.decompile 357 prog_x86Lib.x86_tools "test" [QUOTE (x86_encodeLib.x86_encode "mov edi, [esp]")] 358 val th = SIMP_RULE std_ss [t_def,LET_DEF] th 359 val th = Q.INST [`df`|->`{esp}`,`f`|->`\x.w`] th 360 val th = SPEC_BOOL_FRAME_RULE th ``ALIGNED esp`` 361 val post = ``xSTACK esp [w] * xR EDI w * xR ESP esp * xPC (p + 0x3w)`` 362 val (th,goal) = SPEC_WEAKEN_RULE th post 363 val tac = 364 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,xSTACK_def,prog_x86Theory.xM_THM, 365 ALIGNED,SEP_CLAUSES] THEN SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL] 366 val th = MP th (prove(goal,tac)) 367 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p`` 368 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 369 val tac = 370 SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_MOVE_COND,xSTACK_def,prog_x86Theory.xM_THM, 371 ALIGNED,SEP_CLAUSES,SEP_IMP_REFL,IN_INSERT,NOT_IN_EMPTY] 372 THEN SIMP_TAC (std_ss++star_ss) [ALIGNED_INTRO,ALIGNED,SEP_CLAUSES,SEP_IMP_REFL] 373 val th = MP th (prove(goal,tac)) 374 in th end; 375 376val xSTACK_POP_EDI = let 377 val (th,t_def) = decompilerLib.decompile 378 prog_x86Lib.x86_tools "test" [QUOTE (x86_encodeLib.x86_encode "pop edi")] 379 val th = SIMP_RULE std_ss [t_def,LET_DEF] th 380 val th = Q.INST [`df`|->`{esp}`,`f`|->`\x.w`] th 381 val th = SPEC_BOOL_FRAME_RULE th ``ALIGNED esp`` 382 val post = ``xSTACK esp [w] * xR EDI w * xR ESP (esp+4w) * xPC (p + 0x1w)`` 383 val (th,goal) = SPEC_WEAKEN_RULE th post 384 val tac = 385 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,xSTACK_def,prog_x86Theory.xM_THM, 386 ALIGNED,SEP_CLAUSES] THEN SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL] 387 val th = MP th (prove(goal,tac)) 388 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p`` 389 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 390 val tac = 391 SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_MOVE_COND,xSTACK_def,prog_x86Theory.xM_THM, 392 ALIGNED,SEP_CLAUSES,SEP_IMP_REFL,IN_INSERT,NOT_IN_EMPTY] 393 THEN SIMP_TAC (std_ss++star_ss) [ALIGNED_INTRO,ALIGNED,SEP_CLAUSES,SEP_IMP_REFL] 394 val th = MP th (prove(goal,tac)) 395 in th end; 396 397val x86_sexp2string_th = let 398 val th = SPEC_COMPOSE_RULE xSTACK_MOVE_EDI x86_sexp2string_thm 399 val post = ``(let (eax,ecx,edi,esi,ebp,dh,h,df,f,dm,m,dg,g) = 400 arm_print_sexp (eax,w,ebp,dh,h,df,f,dm,m,dg,g) 401 in 402 xBYTE_MEMORY df f * xBYTE_MEMORY dg g * xMEMORY dh h * 403 xMEMORY dm m * xR EAX eax * xR EBP ebp * ~xR EBX * xR ECX ecx * 404 ~xR EDX * xR ESI esi * ~xS) * 405 (~xR EDI * xSTACK esp [w] * xR ESP esp * xPC p)`` 406 val post = subst_SPEC_PC th post 407 val (th,goal) = SPEC_WEAKEN_RULE th post 408 val tac = 409 SIMP_TAC std_ss [LET_DEF] 410 THEN CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV) 411 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR EDI` SEP_HIDE_def,SEP_CLAUSES] 412 THEN SIMP_TAC std_ss [SEP_IMP_def] 413 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 414 THEN REPEAT STRIP_TAC 415 THEN Q.EXISTS_TAC `(FST 416 (SND (SND (arm_print_sexp (eax,w,ebp,dh,h,df,f,dm,m,dg,g)))))` 417 THEN FULL_SIMP_TAC std_ss [AC STAR_COMM STAR_ASSOC] 418 val th = MP th (prove(goal,tac)) 419 val th = SPEC_COMPOSE_RULE th xSTACK_POP_EDI 420 val th = RW [] (DISCH_ALL th) 421 val imp = arm_print_sexp_lemma 422 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp 423 val imp = SIMP_RULE std_ss [] (RW1 [one_space_EXPAND] imp) 424 val imp = Q.INST [`c`|->`r1 + n2w (STRLEN (sexp2string t1) + 1)`] imp 425 val imp = RW [] imp 426 val tm = (fst o dest_imp o concl) imp 427 val th = SPEC_BOOL_FRAME_RULE th tm 428 val th = Q.INST [`eax`|->`w1`,`ebp`|->`r9`,`r1`|->`w`] th 429 val post = ``SEP_EXISTS edi dg g dm m dh h. xR EDI edi * xSTRING edi (sexp2string t1) 430 * xBYTE_MEMORY dg g * xMEMORY dh h * xMEMORY dm m * 431 ~xR EAX * ~xR EBP * ~xR EBX * ~xR ECX * ~xR EDX * ~xR ESI 432 * xPC p * ~xS * xSTACK esp [w] * xR ESP (esp + 0x4w)`` 433 val post = subst_SPEC_PC th post 434 val (th,goal) = SPEC_WEAKEN_RULE th post 435 val tac = 436 SIMP_TAC std_ss [xSTRING_def] 437 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 438 THEN STRIP_TAC 439 THEN IMP_RES_TAC imp 440 THEN FULL_SIMP_TAC (std_ss++sep_cond_ss) [LET_DEF,WORD_OR_CLAUSES] 441 THEN SIMP_TAC std_ss [SEP_IMP_def] 442 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 443 THEN REPEAT STRIP_TAC 444 THEN EX_TAC [`w`,`dg`,`g`,`dm`,`m`,`dh`,`hi`,`df`,`fi`] 445 THEN IMP_RES_TAC one_string_IMP_string_mem 446 THEN ASM_SIMP_TAC std_ss [cond_STAR] 447 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR ECX` SEP_HIDE_def,SEP_CLAUSES] 448 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 449 THEN EX_TAC [`r4i`] 450 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR EAX` SEP_HIDE_def,SEP_CLAUSES] 451 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 452 THEN EX_TAC [`w`] 453 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR EBP` SEP_HIDE_def,SEP_CLAUSES] 454 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 455 THEN EX_TAC [`r9`] 456 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR ESI` SEP_HIDE_def,SEP_CLAUSES] 457 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 458 THEN EX_TAC [`r8i`] 459 THEN FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM] 460 val th = MP th (prove(goal,tac)) 461 val th = foldr (uncurry EXISTS_PRE) th [`df`,`f`,`dg`,`g`,`dm`,`m`,`dh`,`h`,`sym`] 462 val th = foldr (uncurry EXISTS_PRE) th [`t2`,`t3`,`t4`,`t5`,`t6`] 463 val th = foldr (uncurry EXISTS_PRE) th [`w1`,`w2`,`w3`,`w4`,`w5`,`w6`,`r9`] 464 val pre = ``xLISP1 (t1,l) * xSTRING_SPACE w (LENGTH (sexp2string t1)) * 465 xPC p * ~xS * xSTACK esp [w] * xR ESP esp`` 466 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 467 val tac = 468 SIMP_TAC std_ss [xSTRING_SPACE_def] 469 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 470 THEN SIMP_TAC std_ss [xLISP1_def,xLISP_def] 471 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_MOVE_COND] 472 THEN SIMP_TAC std_ss [SEP_IMP_def] 473 THEN CONV_TAC ((REDEPTH_CONV SEP_EXISTS_CONV)) 474 THEN SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,Once one_space_EXPAND] 475 THEN NTAC 2 STRIP_TAC 476 THEN EX_TAC [`r3`,`r4`,`r5`,`r6`,`r7`,`r8`,`a`] 477 THEN EX_TAC [`x2`,`x3`,`x4`,`x5`,`x6`] 478 THEN EX_TAC [`df`,`f`,`dg`,`g`,`dm`,`m`,`df'`,`f'`,`s'`] 479 THEN IMP_RES_TAC imp 480 THEN ASM_SIMP_TAC std_ss [LET_DEF,WORD_OR_CLAUSES] 481 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR ESI` SEP_HIDE_def,SEP_CLAUSES] 482 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 483 THEN EX_TAC [`r8`] 484 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR EDI` SEP_HIDE_def,SEP_CLAUSES] 485 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 486 THEN EX_TAC [`r7`] 487 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR EBX` SEP_HIDE_def,SEP_CLAUSES] 488 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 489 THEN EX_TAC [`r6`] 490 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR EDX` SEP_HIDE_def,SEP_CLAUSES] 491 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 492 THEN EX_TAC [`r5`] 493 THEN SIMP_TAC (std_ss++sep_cond_ss) [Q.ISPEC `xR ECX` SEP_HIDE_def,SEP_CLAUSES] 494 THEN CONV_TAC (REPEATC (DEPTH_CONV SEP_EXISTS_CONV)) 495 THEN EX_TAC [`r4`] 496 THEN FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM] 497 val th = MP th (prove(goal,tac)) 498 in th end; 499 500val R_ev_thm = let 501 val rw = RW [] (MATCH_MP SET_TO_LIST_THM FINITE_EMPTY) 502 val thi = Q.SPECL [`s`,`FEMPTY`,`t`,`l`] LISP_EVAL_CORRECT 503 val thi = CONJ thi (Q.SPECL [`s`,`FEMPTY`,`t`,`l`] LISP_EVAL_LIMIT_CORRECT) 504 val thi = SIMP_RULE std_ss [rw,fmap2list_def,FDOM_FEMPTY,MAP,alist2sexp_def,list2sexp_def,LISP_EVAL_def] thi 505 in thi end; 506 507fun auto_prove th post = let 508 val th = Q.INST [`x`|->`Sym "nil"`] th 509 val th = Q.INST [`y`|->`Sym "nil"`] th 510 val th = Q.INST [`z`|->`Sym "nil"`] th 511 val th = Q.INST [`stack`|->`Sym "nil"`] th 512 val th = Q.INST [`alist`|->`Sym "nil"`] th 513 val post = subst_SPEC_PC th post 514 val th = SPEC_BOOL_FRAME_RULE th ``R_ev (s,FEMPTY) s2 /\ (exp = term2sexp s)`` 515 val (th,goal) = SPEC_WEAKEN_RULE th post 516 val tac = 517 SIMP_TAC std_ss [LISP_EVAL_def,aLISP1_def,pLISP1_def,xLISP1_def] 518 THEN `?exp2 x2 y2 z2 stack2 alist2 l2. 519 lisp_eval (exp,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) = 520 (exp2,x2,y2,z2,stack2,alist2,l2)` by METIS_TAC [pairTheory.PAIR] 521 THEN ASM_SIMP_TAC std_ss [LET_DEF,SEP_IMP_def,cond_STAR] 522 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_EXISTS_THM] 523 THEN REPEAT STRIP_TAC 524 THEN EX_TAC [`x2`,`y2`,`z2`,`stack2`,`alist2`] 525 THEN FULL_SIMP_TAC (std_ss++star_ss) [] 526 THEN MP_TAC (Q.INST [`t`|->`s2`] R_ev_thm) 527 THEN ASM_SIMP_TAC std_ss [] 528 THEN REPEAT STRIP_TAC 529 THEN FULL_SIMP_TAC std_ss [] 530 val th = MP th (prove(goal,tac)) 531 in th end; 532 533val arm_th = auto_prove SPEC_lisp_eval_arm_thm 534 ``aLISP1 (sexpression2sexp s2,l) * aPC p * ~aS`` 535 536val ppc_th = auto_prove SPEC_lisp_eval_ppc_thm 537 ``pLISP1 (sexpression2sexp s2,l) * pPC p * ~pS`` 538 539val x86_th = auto_prove SPEC_lisp_eval_x86_thm 540 ``xLISP1 (sexpression2sexp s2,l) * xPC p * ~xS`` 541 542val _ = codegen_x86Lib.set_x86_regs 543 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi")] 544 545val (th1,th2,th3) = compilerLib.compile_all `` 546 add32 (r5:word32) = let r5 = r5 + 32w in r5``; 547 548val setup_code = 549 map (fn (s,th) => (s,SIMP_RULE std_ss [th2,th3,LET_DEF,SEP_CLAUSES] th)) th1 550 551fun find_thm t [] = fail() 552 | find_thm t ((s,th)::xs) = if t = s then th else find_thm t xs 553 554val arm_eval_th = LISP_SPEC_COMPOSE_RULE 555 [find_thm "arm" setup_code, 556 arm_string2sexp_arm_thm, 557 arm_th, 558 arm_sexp2string_th] 559 560val ppc_eval_th = LISP_SPEC_COMPOSE_RULE 561 [find_thm "ppc" setup_code, 562 arm_string2sexp_ppc_thm, 563 ppc_th, 564 ppc_sexp2string_th] 565 566val x86_eval_th = LISP_SPEC_COMPOSE_RULE 567 [find_thm "x86" setup_code, 568 xSTACK_PUSH_EDI, 569 arm_string2sexp_x86_thm, 570 x86_th, 571 Q.INST [`w`|->`edi`,`esp`|->`esp-4w`] x86_sexp2string_th] 572 573 574val _ = save_thm("arm_eval_th",arm_eval_th); 575val _ = save_thm("ppc_eval_th",ppc_eval_th); 576val _ = save_thm("x86_eval_th",x86_eval_th); 577 578open export_codeLib; 579 580val _ = write_code_to_file "arm_eval.s" arm_eval_th 581val _ = write_code_to_file "ppc_eval.s" ppc_eval_th 582val _ = write_code_to_file "x86_eval.s" x86_eval_th 583 584val _ = export_theory(); 585