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