1structure prog_x64Lib :> prog_x64Lib = 2struct 3 4open HolKernel boolLib bossLib; 5open wordsLib stringLib addressTheory pred_setTheory combinTheory; 6open set_sepTheory x64_Theory x64_Lib helperLib; 7open x64_seq_monadTheory x64_coretypesTheory x64_astTheory x64_icacheTheory; 8open prog_x64Theory wordsTheory x64_encodeLib; 9 10structure Parse = struct 11 open Parse 12 val (Type,Term) = 13 prog_x64Theory.prog_x64_grammars 14 |> apsnd ParseExtras.grammar_loose_equality 15 |> parse_from_grammars 16end 17open Parse 18 19 20infix \\ 21val op \\ = op THEN; 22 23val x64_status = zS_HIDE; 24val x64_pc = ``zPC``; 25val x64_exec_flag = ref true; 26val x64_code_write_perm = ref false; 27val x64_use_stack = ref false; 28fun set_x64_exec_flag b = (x64_exec_flag := b); 29fun set_x64_code_write_perm_flag b = (x64_code_write_perm := b); 30fun set_x64_use_stack b = (x64_use_stack := b); 31val Zreg_distinct = x64_decoderTheory.Zreg_distinct; 32 33datatype mpred_type = zMEM_AUTO | zMEM_BYTE_MEMORY | zMEM_MEMORY64; 34 35fun name_for_resource counter tm = let 36 val to_lower_drop_two = implode o tl o tl o explode o to_lower 37 in if type_of tm = ``:Zreg`` then let 38 val name = fst (dest_const tm) 39 val reg_name = snd (hd (filter (fn (x,y) => x = name) 40 [("RAX","r0"), ("RCX","r1"), ("RDX","r2"), ("RBX","r3"), 41 ("RSP","r4"), ("RBP","r5"), ("RSI","r6"), ("RDI","r7"), 42 ("zR8","r8"), ("zR9","r9"), ("zR10","r10"), ("zR11","r11"), 43 ("zR12","r12"), ("zR13","r13"), ("zR14","r14"), 44 ("zR15","r15")])) 45 in reg_name end 46 else if type_of tm = ``:Zeflags`` 47 then "z_" ^ (to_lower_drop_two o fst o dest_const) tm else 48 (counter := 1 + !counter; ("x" ^ int_to_string (!counter))) end; 49 50val word2bytes_lemma = CONJ (EVAL ``word2bytes 2 (w:'a word)``) 51 (EVAL ``word2bytes 4 (w:'a word)``) 52 53val w2n_MOD = prove( 54 ``!imm32. w2n (imm32:word32) MOD 4294967296 = w2n imm32``, 55 Cases THEN FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]); 56 57fun pre_process_thm th = let 58 val th = RW [ZREAD_MEM2_WORD64_THM,ZWRITE_MEM2_WORD64_THM,wordsTheory.WORD_ADD_0, 59 ZREAD_MEM2_WORD16_def,ZWRITE_MEM2_WORD16_def,bit_listTheory.bytes2word_def, 60 wordsTheory.ZERO_SHIFT,wordsTheory.WORD_OR_CLAUSES,word2bytes_lemma,EL_thm] th 61 val x = ref 0 62 fun all_distinct [] = [] 63 | all_distinct (x::xs) = x :: all_distinct (filter (fn y => x !~ y) xs) 64 val rs = find_terml (fn tm => type_of tm = ``:Zreg``) (concl th) 65 val fs = find_terml (fn tm => type_of tm = ``:Zeflags``) (concl th) 66 val ws = find_terml (can (match_term ``ZREAD_MEM2_WORD32 a``)) (concl th) 67 val ws = ws @ find_terml (can (match_term ``ZWRITE_MEM2_WORD32 a``)) (concl th) 68 val ws = all_distinct (map cdr ws) 69 val bs = find_terml (can (match_term ``ZREAD_MEM2 a``)) (concl th) 70 val bs = bs @ find_terml (can (match_term ``ZWRITE_MEM2 a``)) (concl th) 71 val bs = all_distinct (map cdr bs) 72 fun make_eq_tm pattern lhs name = let 73 val var = mk_var(name_for_resource x name, type_of pattern) 74 in mk_eq(subst [lhs |-> name] pattern,var) end 75 val rs2 = map (make_eq_tm ``ZREAD_REG r s`` ``r:Zreg``) rs 76 val fs2 = map (make_eq_tm ``ZREAD_EFLAG f s`` ``f:Zeflags``) fs 77 val ws2 = map (make_eq_tm ``ZREAD_MEM2_WORD32 a s`` ``a:word64``) ws 78 val bs2 = map (make_eq_tm ``ZREAD_MEM2 a s`` ``a:word64``) bs 79 val result = rs2 @ fs2 @ ws2 @ bs2 @ [``ZREAD_RIP s = rip``] 80 val th = foldr (uncurry DISCH) th result 81 val th = RW [AND_IMP_INTRO,GSYM CONJ_ASSOC,wordsTheory.WORD_XOR_CLAUSES, 82 wordsTheory.WORD_AND_CLAUSES,w2n_MOD] (SIMP_RULE std_ss [] th) 83 in th end; 84 85fun x64_pre_post g s = let 86 fun get_arg tm = (cdr o car) tm 87 val h = g 88 val xs = find_terml (can (match_term ``(ZREAD_REG x s = y)``)) h 89 @ find_terml (can (match_term ``(ZREAD_EFLAG x s = y)``)) h 90 @ find_terml (can (match_term ``(ZREAD_MEM2_WORD32 x s = y)``)) h 91 @ find_terml (can (match_term ``(ZREAD_MEM2 x s = y)``)) h 92 val xs = map (fn tm => ((get_arg o cdr o car) tm, cdr tm)) xs 93 val ys = find_terml (can (match_term ``ZWRITE_MEM2 a x``)) h 94 @ find_terml (can (match_term ``ZWRITE_MEM2_WORD32 a x``)) h 95 @ find_terml (can (match_term ``ZWRITE_EFLAG a x``)) h 96 @ find_terml (can (match_term ``ZWRITE_REG a x``)) h 97 val ys = map (fn tm => (get_arg tm, cdr tm)) ys 98 val new_rip = (cdr o hd) (find_terml (can (match_term ``ZWRITE_RIP e``)) h) 99 fun assigned_aux x y [] = y 100 | assigned_aux x y ((q,z)::zs) = if aconv x q then z else assigned_aux x y zs 101 fun get_assigned_value x y = assigned_aux x y ys 102 fun mk_pre_post_assertion (name,var) = let 103 val (pattern,name_tm,var_tm) = 104 if type_of name = ``:Zreg`` then 105 (``zR1 a w``,``a:Zreg``,``w:word64``) 106 else if type_of name = ``:Zeflags`` then 107 (``zS1 a w``,``a:Zeflags``,``w:bool option``) 108 else if type_of var = ``:word8`` then 109 (``~(zM1 a (SOME (w,zDATA_PERM ex)))``,``a:word64``,``w:word8``) 110 else if type_of var = ``:word32`` then 111 (``zM a w``,``a:word64``,``w:word32``) 112 else fail() 113 in (subst [name_tm|->name,var_tm|->var] pattern, 114 subst [name_tm|->name,var_tm|->get_assigned_value name var] pattern) end 115 val pre_post = map mk_pre_post_assertion xs 116 val pre = list_mk_star (map fst pre_post) ``:x64_set -> bool`` 117 val post = list_mk_star (map snd pre_post) ``:x64_set -> bool`` 118 fun is_precond tm = 119 (not (can (match_term ``ZREAD_REG r s = v``) tm) andalso 120 not (can (match_term ``ZREAD_MEM2 r s = v``) tm) andalso 121 not (can (match_term ``ZREAD_MEM2_WORD32 r s = v``) tm) andalso 122 not (can (match_term ``CAN_ZWRITE_MEM r s``) tm) andalso 123 not (can (match_term ``CAN_ZREAD_MEM r s``) tm) andalso 124 not (can (match_term ``ZREAD_INSTR r s = v``) tm) andalso 125 not (can (match_term ``ZREAD_EFLAG r s = v``) tm) andalso 126 not (can (match_term ``ZREAD_RIP s = v``) tm)) handle e => true 127 val all_conds = (list_dest dest_conj o fst o dest_imp) h 128 val pre_conds = (filter is_precond) all_conds 129 val ss = foldr (fn (x,y) => (fst (dest_eq x) |-> snd (dest_eq x)) :: y handle e => y) [] 130 (filter is_precond pre_conds) 131 val ss = ss @ map ((fn tm => mk_var((fst o dest_var o cdr) tm,``:bool option``) |-> tm) o cdr) 132 (filter (can (match_term ``ZREAD_EFLAG x s = SOME y``)) all_conds) 133 val pre = subst ss pre 134 val post = subst ss post 135 val pre = mk_star (``zPC rip``,pre) 136 val post = mk_star (mk_comb(``zPC``,new_rip),post) 137 val pre = if null pre_conds then pre 138 else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) 139 in (pre,post) end; 140 141val SING_SUBSET = prove( 142 ``!x:'a y. {x} SUBSET y = x IN y``, 143 REWRITE_TAC [INSERT_SUBSET,EMPTY_SUBSET]); 144 145fun introduce_zBYTE_MEMORY_ANY th = if 146 not (can (find_term (can (match_term ``zM1``))) (concl th)) 147 then th else let 148 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 149 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 150 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 151 val (_,p,_,q) = dest_spec(concl th) 152 val xs = (rev o list_dest dest_star) p 153 val tm = ``~(zM1 a x)`` 154 val xs = filter (can (match_term tm)) xs 155 fun foo tm = (fst o pairSyntax.dest_pair o cdr o cdr o cdr) tm |-> 156 mk_comb(mk_var("g",``:word64->word8``),(cdr o car o cdr) tm) 157 val th = INST (map foo xs) th 158 in if null xs then th else let 159 val (_,p,_,q) = dest_spec(concl th) 160 val xs = (rev o list_dest dest_star) p 161 val tm = ``~(zM1 a x)`` 162 val xs = filter (can (match_term tm)) xs 163 val ys = (map (cdr o car o cdr) xs) 164 fun foo [] = mk_var("dg",``:word64 set``) 165 | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v) 166 val frame = mk_comb(mk_comb(``zBYTE_MEMORY_ANY ex``,foo ys),mk_var("g",``:word64->word8``)) 167 val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th) 168 val th = RW [GSYM STAR_ASSOC] th 169 val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) zBYTE_MEMORY_ANY_INSERT 170 fun compact th = let 171 val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th) 172 val rw = (INST (fst (match_term fff x)) o SPEC_ALL o GSYM) zBYTE_MEMORY_ANY_INSERT 173 val th = DISCH ((fst o dest_imp o concl) rw) th 174 val th = SIMP_RULE bool_ss [GSYM zBYTE_MEMORY_ANY_INSERT] th 175 in th end 176 val th = repeat compact th 177 val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th 178 val th = RW [APPLY_UPDATE_ID] th 179 val v = hd (filter (is_var) ys @ ys) 180 fun ss [] = ``{}:word64 set`` 181 | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs) 182 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("dg",``:word64 set``)) 183 val u2 = u1 184 val u3 = (fst o dest_imp o concl) th 185 val goal = mk_imp(u2,u3) 186 val imp = prove(goal, 187 ONCE_REWRITE_TAC [ALIGNED_MOD_4] 188 THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO] 189 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 190 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 191 THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET] 192 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 193 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 194 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC 195 THEN ASM_SIMP_TAC std_ss [] 196 THEN CCONTR_TAC 197 THEN FULL_SIMP_TAC std_ss [] 198 THEN FULL_SIMP_TAC std_ss []) 199 val th = DISCH_ALL (MATCH_MP th (UNDISCH imp)) 200 val th = RW [GSYM progTheory.SPEC_MOVE_COND] th 201 val th = remove_primes th 202 val th = REWRITE_RULE [SING_SUBSET] th 203 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 204 in th end end 205 206fun introduce_zMEMORY th = if 207 not (can (find_term (can (match_term ``zM``))) (concl th)) 208 then th else let 209 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 210 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 211 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 212 val (_,p,_,q) = dest_spec(concl th) 213 val xs = (rev o list_dest dest_star) p 214 val tm = ``zM a x`` 215 val xs = filter (can (match_term tm)) xs 216 fun foo tm = cdr tm |-> 217 mk_comb(mk_var("f",``:word64->word32``),(cdr o car) tm) 218 val th = INST (map foo xs) th 219 in if null xs then th else let 220 val (_,p,_,q) = dest_spec(concl th) 221 val xs = (rev o list_dest dest_star) p 222 val tm = ``zM a x`` 223 val xs = filter (can (match_term tm)) xs 224 val ys = (map (cdr o car) xs) 225 fun foo [] = mk_var("df",``:word64 set``) 226 | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v) 227 val frame = mk_comb(mk_comb(``zMEMORY``,foo ys),mk_var("f",``:word64->word32``)) 228 val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th) 229 val th = RW [GSYM STAR_ASSOC] th 230 val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) zMEMORY_INSERT 231 fun compact th = let 232 val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th) 233 val rw = (INST (fst (match_term fff x)) o SPEC_ALL o DISCH_ALL o GSYM o UNDISCH) zMEMORY_INSERT 234 val th = DISCH ((fst o dest_imp o concl) rw) th 235 val th = SIMP_RULE bool_ss [GSYM zMEMORY_INSERT] th 236 in th end 237 val th = repeat compact th 238 val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th 239 val th = RW [APPLY_UPDATE_ID] th 240 val v = hd (filter (is_var) ys @ ys) 241 fun ss [] = ``{}:word64 set`` 242 | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs) 243 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word64 set``)) 244 val u3 = (fst o dest_imp o concl) th 245 val u2 = list_mk_conj (u1::filter is_eq (list_dest dest_conj u3)) 246 val goal = mk_imp(u2,u3) 247 val imp = prove(goal, 248 ONCE_REWRITE_TAC [ALIGNED_MOD_4] 249 THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO] 250 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 251 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 252 THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET] 253 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 254 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 255 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC 256 THEN ASM_SIMP_TAC std_ss [] 257 THEN CCONTR_TAC 258 THEN FULL_SIMP_TAC std_ss [] 259 THEN FULL_SIMP_TAC std_ss []) 260 val th = DISCH_ALL (MATCH_MP th (UNDISCH imp)) 261 val th = RW [GSYM progTheory.SPEC_MOVE_COND] th 262 val th = remove_primes th 263 val th = REWRITE_RULE [SING_SUBSET] th 264 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 265 in th end end 266 267fun introduce_zM64 th = if 268 not (can (find_term (can (match_term ``zM``))) (concl th)) 269 then th else let 270 val pattern = ``zM (a + 4w) x1 * zM a x2`` 271 val tag = (RW [GSYM STAR_ASSOC] th) |> concl |> car 272 |> find_term (can (match_term pattern)) 273 val x1 = (cdr o cdr o car) tag 274 val x2 = (cdr o cdr) tag 275 val a = (cdr o car o cdr) tag 276 val res = SPECL [a,mk_var("xx",``:word64``)] (RW1[STAR_COMM]zM64_def) 277 val y1 = (cdr o cdr o car) ((snd o dest_eq o concl) res) 278 val y2 = (cdr o cdr) ((snd o dest_eq o concl) res) 279 val th = RW [GSYM res,GSYM STAR_ASSOC] (INST [x1|->y1,x2|->y2] th) 280 val th = RW [STAR_ASSOC,LOAD64] th 281 in th end handle HOL_ERR _ => th; 282 283val is_spec_1 = true 284val is_spec_1 = false 285 286val SPEC_1_pat = temporalTheory.SPEC_1_def |> SPEC_ALL |> concl |> dest_eq |> fst 287fun dest_spec_1 tm = 288 if can (match_term SPEC_1_pat) tm then let 289 val (x1234,x5) = dest_comb tm 290 val (x123,x4) = dest_comb x1234 291 val (x12,x3) = dest_comb x123 292 val (x1,x2) = dest_comb x12 293 val (x0,x1) = dest_comb x1 294 in (x1,x2,x3,x4) end 295 else failwith("not a SPEC_1") 296 297fun introduce_zMEMORY64_spec_or_spec_1 th is_spec_1 = 298 let val th = introduce_zM64 th in 299 if not (can (find_term (can (match_term ``zM64``))) (concl th)) 300 then th else let 301 val pre_conv = if is_spec_1 then RATOR_CONV o PRE_CONV else PRE_CONV 302 val th = CONV_RULE (pre_conv STAR_REVERSE_CONV) th 303 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 304 val th = CONV_RULE (pre_conv STAR_REVERSE_CONV) th 305 val (_,p,_,q) = dest_spec(concl th) handle HOL_ERR _ => dest_spec_1(concl th) 306 val xs = (rev o list_dest dest_star) p 307 val tm = ``zM64 a x`` 308 val xs = filter (can (match_term tm)) xs 309 fun foo tm = cdr tm |-> 310 mk_comb(mk_var("f",``:word64->word64``),(cdr o car) tm) 311 val th = INST (map foo xs) th 312 in if null xs then th else let 313 val (_,p,_,q) = dest_spec(concl th) handle HOL_ERR _ => dest_spec_1(concl th) 314 val xs = (rev o list_dest dest_star) p 315 val tm = ``zM64 a x`` 316 val xs = filter (can (match_term tm)) xs 317 val ys = (map (cdr o car) xs) 318 fun foo [] = mk_var("df",``:word64 set``) 319 | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v) 320 val frame = mk_comb(mk_comb(``zMEMORY64``,foo ys),mk_var("f",``:word64->word64``)) 321 val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th) 322 handle HOL_ERR _ => 323 SPEC frame (MATCH_MP temporalTheory.SPEC_1_FRAME th) 324 val th = RW [GSYM STAR_ASSOC,SEP_CLAUSES] th 325 val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) zMEMORY64_INSERT 326 fun compact th = let 327 val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th) 328 val rw = (INST (fst (match_term fff x)) o SPEC_ALL o DISCH_ALL o GSYM o UNDISCH) zMEMORY64_INSERT 329 val th = DISCH ((fst o dest_imp o concl) rw) th 330 val th = SIMP_RULE bool_ss [GSYM zMEMORY64_INSERT] th 331 in th end 332 val th = repeat compact th 333 val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th 334 val th = RW [APPLY_UPDATE_ID] th 335 val v = hd (filter (is_var) ys @ ys) 336 fun ss [] = ``{}:word64 set`` 337 | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs) 338 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word64 set``)) 339 val u3 = (fst o dest_imp o concl) th 340 val u2 = list_mk_conj (u1::filter is_eq (list_dest dest_conj u3)) 341 val goal = mk_imp(u2,u3) 342 val imp = prove(goal, 343 ONCE_REWRITE_TAC [ALIGNED_MOD_4] 344 THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO] 345 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 346 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 347 THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET] 348 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 349 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 350 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC 351 THEN ASM_SIMP_TAC std_ss [] 352 THEN CCONTR_TAC 353 THEN FULL_SIMP_TAC std_ss [] 354 THEN FULL_SIMP_TAC std_ss []) 355 val th = DISCH_ALL (MATCH_MP th (UNDISCH imp)) 356 val th = RW [GSYM progTheory.SPEC_MOVE_COND, 357 GSYM temporalTheory.SPEC_MOVE_1_COND] th 358 val th = remove_primes th 359 val th = REWRITE_RULE [SING_SUBSET] th 360 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 361 in th end end end 362 363fun introduce_zMEMORY64 th = introduce_zMEMORY64_spec_or_spec_1 th false; 364fun introduce_zMEMORY64_1 th = introduce_zMEMORY64_spec_or_spec_1 th true; 365 366(* 367fun introduce_zSTACK th = 368 if not (can (find_term (fn x => x = ``RSP``)) (concl th)) then th else let 369 val pattern = ``zM (a + 4w) x1 * zM a x2`` 370 val tag = (RW [GSYM STAR_ASSOC] th) |> concl |> car 371 |> find_term (can (match_term pattern)) 372 val x1 = (cdr o cdr o car) tag 373 val x2 = (cdr o cdr) tag 374 val a = (cdr o car o cdr) tag 375 val _ = mem (mk_var("r4",``:word64``)) (free_vars a) orelse fail() 376 val res = SPECL [a,mk_var("xx",``:word64``)] (RW1[STAR_COMM]zM64_def) 377 val y1 = (cdr o cdr o car) ((snd o dest_eq o concl) res) 378 val y2 = (cdr o cdr) ((snd o dest_eq o concl) res) 379 val th = RW [GSYM res,GSYM STAR_ASSOC] (INST [x1|->y1,x2|->y2] th) 380 val th = RW [STAR_ASSOC,LOAD64] th 381 in th end handle HOL_ERR _ => th; 382*) 383 384fun calculate_length_and_jump th = let 385 val (_,_,c,q) = dest_spec (concl th) 386 val l = c |> car |> cdr |> cdr |> listSyntax.dest_list |> fst |> length 387 in 388 let val v = find_term (can (match_term ``zPC (p + n2w n)``)) q 389 in (th,l,SOME (0 + (numSyntax.int_of_term o cdr o cdr o cdr) v)) end 390 handle e => 391 let val v = find_term (can (match_term ``zPC (p - n2w n)``)) q 392 in (th,l,SOME (0 - (numSyntax.int_of_term o cdr o cdr o cdr) v)) end 393 handle e => 394 (th,l,NONE) end 395 396fun post_process_thm mpred no_status th = let 397 val th = if mpred = zMEM_MEMORY64 then introduce_zMEMORY64 th else th 398 (* val th = if mpred = zMEM_AUTO then introduce_zSTACK th else th *) 399 val th = RW [GSYM zR_def] th 400 val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [wordsTheory.word_mul_n2w,SEP_CLAUSES] th 401 val th = CONV_RULE FIX_WORD32_ARITH_CONV th 402 val th = if mpred = zMEM_AUTO then introduce_zMEMORY th else th 403 val th = introduce_zBYTE_MEMORY_ANY th 404 val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [GSYM wordsTheory.WORD_ADD_ASSOC, 405 word_arith_lemma1,word_arith_lemma2,word_arith_lemma3,word_arith_lemma4] th 406 val th = CONV_RULE FIX_WORD32_ARITH_CONV th 407 val th = RW [wordsTheory.WORD_ADD_ASSOC,wordsTheory.WORD_ADD_0] th 408 fun f th = let 409 val x = find_term (can (match_term ``(THE x):'a``)) (concl th) 410 val y = optionSyntax.mk_some(mk_var(fst (dest_var (cdr x)),type_of x)) 411 val th = INST [cdr x |-> y] th 412 val th = SIMP_RULE bool_ss [SEP_CLAUSES,optionLib.option_rws] th 413 in th end 414 val th = if no_status then th else repeat f th 415 val th = RW [ALIGNED_def] th 416 val th = SIMP_RULE std_ss [wordsTheory.WORD_EQ_SUB_ZERO,w2w_eq_n2w,w2w_CLAUSES] th 417 val th = th |> SIMP_RULE (std_ss++wordsLib.SIZES_ss) [WORD_w2w_OVER_BITWISE, 418 WORD_w2w_n2w_OVER_BITWISE,w2w_OVER_ARITH,w2w_OVER_ARITH_n2w] 419 |> SIMP_RULE (std_ss++wordsLib.SIZES_ss) [w2w_w2w,w2w_id,w2n_n2w, 420 WORD_ALL_BITS,WORD_BITS_BITS_ZERO,WORD_BITS_NOT_BITS_ZERO] 421 in calculate_length_and_jump th end; 422 423fun calc_code th = let 424 val tms = find_terml (can (match_term ``ZREAD_INSTR a s = SOME x``)) (concl th) 425 val tms = map dest_eq tms 426 fun addr tm = (Arbnum.toInt o numSyntax.dest_numeral o cdr o cdr o cdr o car) tm 427 handle e => 0 428 val tms = map (fn (x,y) => (addr x, cdr y)) tms 429 val code = map snd (sort (fn (x,_) => fn (y,_) => x <= y) tms) 430 in listSyntax.mk_list (code, ``:word8``) end; 431 432fun x64_prove_one_spec_or_spec_1 th c is_spec_1 = let 433 val g = concl th 434 val s = find_term (can (match_term ``X64_NEXT x = SOME y``)) g 435 val s = (snd o dest_comb o snd o dest_comb) s 436 val (pre,post) = x64_pre_post g s 437 val tm = if is_spec_1 438 then ``SPEC_1 X64_MODEL pre {(rip,c)} post SEP_F`` 439 else ``SPEC X64_MODEL pre {(rip,c)} post`` 440 val tm = subst [mk_var("pre",type_of pre) |-> pre, 441 mk_var("post",type_of post) |-> post, 442 mk_var("c",type_of c) |-> c] tm 443 val FLIP_TAC = CONV_TAC (ONCE_REWRITE_CONV [EQ_SYM_EQ]) 444 val th1 = Q.INST [`s`|->`X64_ICACHE_UPDATE x (r,e,t,m,i)`] th 445 val th1 = RW [ZREAD_CLAUSES,ZWRITE_MEM2_WORD32_def] th1 446 val th1 = RW [ZWRITE_EFLAG_def,X64_ICACHE_UPDATE_def,ZWRITE_MEM2_def, 447 ZWRITE_REG_def, 448 APPLY_UPDATE_THM,WORD_EQ_ADD_CANCEL,x64_address_lemma,ZWRITE_RIP_def] th1 449 val th = prove(tm, 450(* 451 set_goal([],tm) 452*) 453 MATCH_MP_TAC (if is_spec_1 then IMP_X64_SPEC_1 else IMP_X64_SPEC) 454 \\ REPEAT STRIP_TAC 455 \\ EXISTS_TAC ((cdr o cdr o concl o UNDISCH) th1) 456 \\ STRIP_TAC \\ REWRITE_TAC [X64_ICACHE_UPDATE_def] 457 THENL [MATCH_MP_TAC th1,ALL_TAC] 458 \\ REPEAT (POP_ASSUM MP_TAC) 459 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 460 STAR_x64_2set, IN_DELETE, APPLY_UPDATE_THM, Zreg_distinct, 461 GSYM ALIGNED_def, wordsTheory.n2w_11, Zeflags_distinct, 462 Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET, 463 EMPTY_SUBSET, SEP_CLAUSES,X64_ICACHE_UPDATE_def,ZCLEAR_ICACHE_def, 464 X64_ICACHE_REVERT_def,zM_def,WORD_EQ_ADD_CANCEL,x64_address_lemma] 465 \\ ONCE_REWRITE_TAC [CODE_POOL_x64_2set] 466 \\ REWRITE_TAC [listTheory.LENGTH,address_list_def] 467 \\ SIMP_TAC std_ss [arithmeticTheory.ADD1,X64_ICACHE_EXTRACT_def] 468 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 469 STAR_x64_2set, IN_DELETE, APPLY_UPDATE_THM, Zreg_distinct, 470 GSYM ALIGNED_def, wordsTheory.n2w_11, Zeflags_distinct, 471 Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET, 472 EMPTY_SUBSET,x64_pool_def,X64_ACCURATE_CLAUSES] 473 \\ SIMP_TAC std_ss [ZREAD_REG_def,ZREAD_EFLAG_def,ZREAD_RIP_def] 474 \\ NTAC 3 (FLIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]) 475 \\ SIMP_TAC std_ss [CAN_ZREAD_MEM,CAN_ZWRITE_MEM,IN_INSERT,word_arith_lemma1] 476 \\ SIMP_TAC std_ss [ZREAD_MEM2_WORD32_def,ZREAD_MEM2_WORD64_def, 477 ZREAD_MEM2_def,wordsTheory.WORD_ADD_0] 478 \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_zDATA_PERM] 479 \\ SIMP_TAC std_ss [CAN_ZREAD_MEM,CAN_ZWRITE_MEM,IN_INSERT,word_arith_lemma1] 480 \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_zDATA_PERM] 481 THEN1 (SIMP_TAC std_ss [GSYM arithmeticTheory.ADD_ASSOC] 482 \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_zDATA_PERM] 483 \\ SIMP_TAC std_ss [arithmeticTheory.ADD_ASSOC] 484 \\ SIMP_TAC std_ss [markerTheory.Abbrev_def] 485 \\ REPEAT STRIP_TAC \\ FLIP_TAC \\ MATCH_MP_TAC (GEN_ALL ZREAD_INSTR_IMP) 486 \\ Q.EXISTS_TAC `T` \\ ASM_SIMP_TAC std_ss [] 487 \\ FULL_SIMP_TAC std_ss [wordsTheory.word_add_n2w,GSYM wordsTheory.WORD_ADD_ASSOC]) 488 \\ SIMP_TAC std_ss [word2bytes_thm,EL_thm,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET] 489 \\ FULL_SIMP_TAC std_ss [UPDATE_x64_2set'',word_arith_lemma1, 490 ALIGNED_CLAUSES,icache_revert_ID,X64_ACCURATE_UPDATE] 491 \\ SIMP_TAC std_ss [AND_IMP_INTRO] 492 \\ STRIP_TAC \\ IMP_RES_TAC X64_ACCURATE_IMP 493 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] 494 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,GSYM word_add_n2w] 495 \\ SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET]) 496 val th = INST [``w:bool``|-> (if !x64_code_write_perm then T else F)] th 497 in RW [STAR_ASSOC,SEP_CLAUSES,markerTheory.Abbrev_def] th end; 498 499fun x64_prove_one_spec th c = 500 x64_prove_one_spec_or_spec_1 th c false; 501 502fun x64_prove_one_spec_1 th c = 503 x64_prove_one_spec_or_spec_1 th c true; 504 505fun x64_prove_specs mpred no_status s = let 506 val th = x64_step s 507 val th = if mpred = zMEM_BYTE_MEMORY then 508 RW [ZWRITE_MEM2_WORD32_def,ZREAD_MEM2_WORD32_def] th else th 509 val c = calc_code th 510 val th = pre_process_thm th 511 val th = RW [w2n_MOD] th 512(* val th = x64_prove_one_spec th c *) 513 in if (is_cond o cdr o cdr o snd o dest_imp o concl) th then let 514 val (x,y,z) = dest_cond (find_term is_cond (concl th)) 515 fun replace_conv th tm = 516 if (fst o dest_eq o concl) th ~~ tm then th else ALL_CONV tm 517 fun prove_branch cth th = let 518 val tm1 = (fst o dest_imp o concl o ISPECL [x,y,z]) cth 519 val th1 = CONV_RULE (DEPTH_CONV (replace_conv (UNDISCH (ISPECL [x,y,z] cth)))) th 520 val th1 = (RW [AND_IMP_INTRO,GSYM CONJ_ASSOC] o DISCH_ALL) th1 521 val th1 = x64_prove_one_spec th1 c 522 val th1 = SIMP_RULE std_ss [SEP_CLAUSES] (DISCH tm1 th1) 523 val th1 = RW [CONTAINER_def] th1 524 val th1 = RW [RW [GSYM precond_def] (GSYM progTheory.SPEC_MOVE_COND)] th1 525 in post_process_thm mpred no_status th1 end 526 in (prove_branch CONTAINER_IF_T th, SOME (prove_branch CONTAINER_IF_F th)) end 527 else (post_process_thm mpred no_status (x64_prove_one_spec th c),NONE) end 528 529fun x64_jump (tm1:term) (tm2:term) (jump_length:int) (forward:bool) = ("",0) 530 531fun x64_spec_aux mpred = cache (x64_prove_specs mpred false); 532 533val x64_spec_aux_auto = cache (x64_prove_specs zMEM_AUTO false); 534val x64_spec_aux_byte = cache (x64_prove_specs zMEM_BYTE_MEMORY false); 535val x64_spec_aux_memory64 = cache (x64_prove_specs zMEM_MEMORY64 false); 536val x64_spec_aux_memory64_no_status = cache (x64_prove_specs zMEM_MEMORY64 true); 537 538fun apply_to_thm f ((th1,i1,j1),NONE) = ((f th1,i1,j1),NONE) 539 | apply_to_thm f ((th1,i1,j1),SOME (th2,i2,j2)) = ((f th1,i1,j1),SOME (f th2,i2,j2)) 540 541fun x64_spec s = let 542 val (s,rename,_) = parse_renamer s 543 val ((th,i,j),other) = x64_spec_aux_auto s 544 val b = if !x64_exec_flag then T else F 545 val th = INST [``ex:bool``|->b] th 546 val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th 547 in apply_to_thm rename ((th,i,j),other) end 548 549fun x64_spec_byte_memory s = let 550 val (s,rename,_) = parse_renamer s 551 val ((th,i,j),other) = x64_spec_aux_byte s 552 val b = if !x64_exec_flag then T else F 553 val th = INST [``ex:bool``|->b] th 554 val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th 555 in apply_to_thm rename ((th,i,j),other) end 556 557fun x64_spec_memory64 s = let 558 val (s,rename,_) = parse_renamer s 559 val ((th,i,j),other) = x64_spec_aux_memory64 s 560 val b = if !x64_exec_flag then T else F 561 val th = INST [``ex:bool``|->b] th 562 val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th 563 in apply_to_thm rename ((th,i,j),other) end 564 565fun x64_spec_memory64_no_status s = let 566 val (s,rename,_) = parse_renamer s 567 val ((th,i,j),other) = x64_spec_aux_memory64_no_status s 568 val b = if !x64_exec_flag then T else F 569 val th = INST [``ex:bool``|->b] th 570 val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th 571 in apply_to_thm rename ((th,i,j),other) end 572 573val x64_tools = (x64_spec, x64_jump, x64_status, x64_pc); 574val x64_tools_no_status = (x64_spec, x64_jump, TRUTH, x64_pc); 575val x64_tools_64 = (x64_spec_memory64, x64_jump, x64_status, x64_pc); 576val x64_tools_64_no_status = (x64_spec_memory64_no_status, x64_jump, TRUTH, x64_pc); 577 578 579(* 580 581 val mpred = zMEM_AUTO 582 val th = x64_spec (x64_encode "add r0,5"); 583 val th = x64_spec (x64_encode "inc r11"); 584 val th = x64_spec (x64_encode "je 40"); 585 val th = x64_spec (x64_encode "loop -40"); 586 val th = x64_spec "E9"; (* jmp imm32 *) 587 val th = x64_spec (x64_encode "add eax,5"); 588 val th = x64_spec (x64_encode "cmove rax, rcx"); 589 val th = x64_spec (x64_encode "mov al, [rax+rbx+4]"); 590 val th = x64_spec (x64_encode "mov [rax+rbx+4], al"); 591 val th = x64_spec (x64_encode "mov ax, [rax]"); 592 val th = x64_spec (x64_encode "mov [rax], ax"); 593 val th = x64_spec (x64_encode "add [rax], ax"); 594 val th = x64_spec (x64_encode "add [rax], eax"); 595 val th = x64_spec (x64_encode "add [rax], rax"); 596 val th = x64_spec (x64_encode "call r2"); 597 val th = x64_spec (x64_encode "ret"); 598 val th = x64_spec (x64_encode "add rsp,80"); 599 val th = x64_spec (x64_encode "push rax"); 600 val th = x64_spec (x64_encode "pop rax"); 601 val th = x64_spec (x64_encode "mov BYTE [r11+1],124"); 602 603 val ((th,_,_),_) = x64_spec (x64_encode "mov [rax],r1b") 604 val th = th |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n, 605 GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def] 606 |> Q.GEN `g` |> Q.GEN `dg` 607 |> Q.INST [`r0`|->`a+n2w (LENGTH (xs:word8 list))`] 608 |> MATCH_MP zCODE_HEAP_SNOC 609 610 val ((th,_,_),_) = x64_spec "C600" 611 val th = th |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n, 612 GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def] 613 |> Q.GEN `g` |> Q.GEN `dg` 614 |> Q.INST [`r0`|->`a+n2w (LENGTH (xs:word8 list))`,`imm8`|->`n2w k`] 615 |> MATCH_MP zCODE_HEAP_SNOC 616 617 val th = x64_spec_memory64 (x64_encode "add [rax], rax"); 618 val th = x64_spec_memory64 (x64_encode "mov [rax+40], rbx"); 619 val th = x64_spec_memory64 (x64_encode "mov rbx,[rax+40]"); 620 621 val s = "mov r8d, [r7+4*r3+6000]" 622 val s = x64_encode s 623 val (spec,_,sts,_) = x64_tools 624 val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8)) 625 626 val s = "mov [r7+4*r3+6000], r8d" 627 val s = x64_encode s 628 val (spec,_,sts,_) = x64_tools 629 val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8)) 630 631 val th = x64_spec_memory64_no_status (x64_encode "adc r8,r9") 632 val th = x64_spec_memory64_no_status (x64_encode "je 400") 633 634*) 635 636end 637