1structure prog_x86Lib :> prog_x86Lib = 2struct 3 4open HolKernel boolLib bossLib; 5open wordsLib stringLib addressTheory pred_setTheory combinTheory; 6open set_sepTheory x86_Theory x86_Lib helperLib; 7open x86_seq_monadTheory x86_coretypesTheory x86_astTheory x86_icacheTheory; 8open prog_x86Theory; 9 10infix \\ 11val op \\ = op THEN; 12 13 14 15val x86_status = xS_HIDE; 16val x86_pc = ``xPC``; 17val x86_exec_flag = ref false; 18val x86_code_write_perm = ref false; 19val x86_use_stack = ref false; 20fun set_x86_exec_flag b = (x86_exec_flag := b); 21fun set_x86_code_write_perm_flag b = (x86_code_write_perm := b); 22fun set_x86_use_stack b = (x86_use_stack := b); 23 24fun name_for_resource counter tm = let 25 val to_lower_drop_two = implode o tl o tl o explode o to_lower 26 in if type_of tm = ``:Xreg`` then (to_lower o fst o dest_const) tm else 27 if type_of tm = ``:Xeflags`` then (to_lower_drop_two o fst o dest_const) tm else 28 (counter := 1 + !counter; ("x" ^ int_to_string (!counter))) end; 29 30fun pre_process_thm th = let 31 val x = ref 0 32 fun all_distinct [] = [] 33 | all_distinct (x::xs) = x :: all_distinct (filter (fn y => not (x = y)) xs) 34 val rs = find_terml (fn tm => type_of tm = ``:Xreg``) (concl th) 35 val fs = find_terml (fn tm => type_of tm = ``:Xeflags``) (concl th) 36 val ws = find_terml (can (match_term ``XREAD_MEM2_WORD a``)) (concl th) 37 val ws = ws @ find_terml (can (match_term ``XWRITE_MEM2_WORD a``)) (concl th) 38 val ws = all_distinct (map cdr ws) 39 val bs = find_terml (can (match_term ``XREAD_MEM2 a``)) (concl th) 40 val bs = bs @ find_terml (can (match_term ``XWRITE_MEM2 a``)) (concl th) 41 val bs = all_distinct (map cdr bs) 42 fun make_eq_tm pattern lhs name = let 43 val var = mk_var(name_for_resource x name, type_of pattern) 44 in mk_eq(subst [lhs |-> name] pattern,var) end 45 val rs2 = map (make_eq_tm ``XREAD_REG r s`` ``r:Xreg``) rs 46 val fs2 = map (make_eq_tm ``XREAD_EFLAG f s`` ``f:Xeflags``) fs 47 val ws2 = map (make_eq_tm ``XREAD_MEM2_WORD a s`` ``a:word32``) ws 48 val bs2 = map (make_eq_tm ``XREAD_MEM2 a s`` ``a:word32``) bs 49 val result = rs2 @ fs2 @ ws2 @ bs2 @ [``XREAD_EIP s = eip``] 50 val th = foldr (uncurry DISCH) th result 51 val th = RW [AND_IMP_INTRO,GSYM CONJ_ASSOC,wordsTheory.WORD_XOR_CLAUSES, 52 wordsTheory.WORD_AND_CLAUSES,wordsTheory.WORD_ADD_0] (SIMP_RULE std_ss [] th) 53 in th end; 54 55fun x86_pre_post g s = let 56 val h = g 57 val xs = find_terml (can (match_term ``(XREAD_REG x s = y)``)) h 58 @ find_terml (can (match_term ``(XREAD_MEM2_WORD x s = y)``)) h 59 @ find_terml (can (match_term ``(XREAD_MEM2 x s = y)``)) h 60 @ find_terml (can (match_term ``(XREAD_EFLAG x s = y)``)) h 61 val xs = map (fn tm => ((cdr o car o cdr o car) tm, cdr tm)) xs 62 val ys = find_terml (can (match_term ``XWRITE_EFLAG a x``)) h 63 @ find_terml (can (match_term ``XWRITE_MEM2 a x``)) h 64 @ find_terml (can (match_term ``XWRITE_MEM2_WORD a x``)) h 65 @ find_terml (can (match_term ``XWRITE_REG a x``)) h 66 val ys = map (fn tm => ((cdr o car) tm, cdr tm)) ys 67 val new_eip = (cdr o hd) (find_terml (can (match_term ``XWRITE_EIP e``)) h) 68 fun assigned_aux x y [] = y 69 | assigned_aux x y ((q,z)::zs) = if aconv x q then z else assigned_aux x y zs 70 fun get_assigned_value x y = assigned_aux x y ys 71 fun mk_pre_post_assertion (name,var) = let 72 val (pattern,name_tm,var_tm) = 73 if type_of name = ``:Xreg`` then 74 (``xR a w``,``a:Xreg``,``w:word32``) 75 else if type_of name = ``:Xeflags`` then 76 (``xS1 a w``,``a:Xeflags``,``w:bool option``) 77 else if type_of var = ``:word8`` then 78 (``~(xM1 a (SOME (w,xDATA_PERM ex)))``,``a:word32``,``w:word8``) 79 else if type_of var = ``:word32`` then 80 (``xM a w``,``a:word32``,``w:word32``) else fail() 81 in (subst [name_tm|->name,var_tm|->var] pattern, 82 subst [name_tm|->name,var_tm|->get_assigned_value name var] pattern) end 83 val pre_post = map mk_pre_post_assertion xs 84 val pre = list_mk_star (map fst pre_post) ``:x86_set -> bool`` 85 val post = list_mk_star (map snd pre_post) ``:x86_set -> bool`` 86 fun is_precond tm = 87 (not (can (match_term ``XREAD_REG r s = v``) tm) andalso 88 not (can (match_term ``XREAD_MEM2 r s = v``) tm) andalso 89 not (can (match_term ``XREAD_MEM2_WORD r s = v``) tm) andalso 90 not (can (match_term ``CAN_XWRITE_MEM r s``) tm) andalso 91 not (can (match_term ``CAN_XREAD_MEM r s``) tm) andalso 92 not (can (match_term ``XREAD_INSTR r s = v``) tm) andalso 93 not (can (match_term ``XREAD_EFLAG r s = v``) tm) andalso 94 not (can (match_term ``XREAD_EIP s = v``) tm)) handle e => true 95 val all_conds = (list_dest dest_conj o fst o dest_imp) h 96 val pre_conds = (filter is_precond) all_conds 97 val ss = foldr (fn (x,y) => (fst (dest_eq x) |-> snd (dest_eq x)) :: y handle e => y) [] 98 (filter is_precond pre_conds) 99 val ss = ss @ map ((fn tm => mk_var((fst o dest_var o cdr) tm,``:bool option``) |-> tm) o cdr) 100 (filter (can (match_term ``XREAD_EFLAG x s = SOME y``)) all_conds) 101 val pre = subst ss pre 102 val post = subst ss post 103 val pre = mk_star (pre,``xPC eip``) 104 val post = mk_star (post,mk_comb(``xPC``,new_eip)) 105 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) 106 in (pre,post) end; 107 108fun introduce_xMEMORY th = let 109 val (_,p,c,q) = dest_spec(concl th) 110 val tm = find_term (can (match_term ``xM x y``)) p 111 val c = LIST_MOVE_OUT_CONV true [car tm] 112 val th = CONV_RULE (POST_CONV c THENC PRE_CONV c) th 113 val th = MATCH_MP xMEMORY_INTRO (RW [GSYM STAR_ASSOC] th) 114 val th = RW [GSYM progTheory.SPEC_MOVE_COND,STAR_ASSOC] th 115 fun replace_access_in_pre th = let 116 val (_,p,c,q) = dest_spec(concl th) 117 val tm = find_term (can (match_term ``(a:'a =+ w:'b) f``)) p 118 val (tm,y) = dest_comb tm 119 val (tm,x) = dest_comb tm 120 val a = snd (dest_comb tm) 121 val th = REWRITE_RULE [APPLY_UPDATE_ID] (INST [x |-> mk_comb(y,a)] th) 122 in th end handle e => th 123 val th = replace_access_in_pre th 124 in th end handle e => th; 125 126fun introduce_xBYTE_MEMORY_ANY th = let 127 val (_,p,c,q) = dest_spec(concl th) 128 val tm1 = find_term (can (match_term ``xM1 x y``)) p 129 val tm2 = find_term (can (match_term ``xM1 x y``)) q 130 val c1 = LIST_MOVE_OUT_CONV true [tm1] 131 val c2 = LIST_MOVE_OUT_CONV true [tm2] 132 val th = CONV_RULE (POST_CONV c2 THENC PRE_CONV c1) th 133 val th = MATCH_MP xBYTE_MEMORY_ANY_INTRO (RW [GSYM STAR_ASSOC] th) 134 val th = RW [GSYM progTheory.SPEC_MOVE_COND,STAR_ASSOC] th 135 fun replace_access_in_pre th = let 136 val (_,p,c,q) = dest_spec(concl th) 137 val tm = find_term (can (match_term ``(a:'a =+ w:'b) f``)) p 138 val (tm,y) = dest_comb tm 139 val (tm,x) = dest_comb tm 140 val a = snd (dest_comb tm) 141 val th = REWRITE_RULE [APPLY_UPDATE_ID] (INST [x |-> mk_comb(y,a)] th) 142 in th end handle e => th 143 val th = replace_access_in_pre th 144 in th end handle e => th; 145 146fun introduce_xSTACK th = 147 if not (!x86_use_stack) then th else let 148 val (_,p,c,q) = dest_spec(concl th) 149 val ebp = mk_var("ebp",``:word32``) 150 fun access_ebp tm = (tm = ebp) orelse 151 (can (match_term ``(v:word32) - n2w n``) tm andalso (ebp = (cdr o car) tm)) 152 val tm1 = find_term (fn tm => 153 can (match_term ``xM x y``) tm andalso (access_ebp o cdr o car) tm) p 154 val tm2 = find_term (can (match_term (mk_comb(car tm1,genvar(``:word32``))))) q 155 val c1 = MOVE_OUT_CONV ``xR EBP`` THENC MOVE_OUT_CONV (car tm1) 156 val c2 = MOVE_OUT_CONV ``xR EBP`` THENC MOVE_OUT_CONV (car tm2) 157 val th = CONV_RULE (POST_CONV c2 THENC PRE_CONV c1) th 158 val th = DISCH ``ALIGNED ebp`` th 159 val th = MATCH_MP xSTACK_INTRO_EBX th 160 fun mk_stack_var i = mk_var("s" ^ int_to_string i,``:word32``) 161 val index = (Arbnum.toInt o numSyntax.dest_numeral o cdr o cdr o cdr o car) tm1 162 val index = index div 4 163 fun mk_slist i = if i = 0 then ``[]:word32 list`` else 164 listSyntax.mk_cons(mk_stack_var (index - i), mk_slist (i-1)) 165 val th = SPECL [mk_slist index,mk_var("ss",``:word32 list``)] th 166 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [listTheory.LENGTH]) THENC 167 REWRITE_CONV [listTheory.APPEND]) th 168 val th = INST [cdr tm1 |-> mk_stack_var index] th 169 in th end handle e => th; 170 171fun calculate_length_and_jump th = let 172 val (_,_,c,q) = dest_spec (concl th) 173 val l = (length o fst o listSyntax.dest_list o cdr o car o cdr o cdr o car) c 174 in 175 let val v = find_term (can (match_term ``xPC (p + n2w n)``)) q 176 in (th,l,SOME (0 + (numSyntax.int_of_term o cdr o cdr o cdr) v)) end 177 handle e => 178 let val v = find_term (can (match_term ``xPC (p - n2w n)``)) q 179 in (th,l,SOME (0 - (numSyntax.int_of_term o cdr o cdr o cdr) v)) end 180 handle e => 181 (th,l,NONE) end 182 183fun post_process_thm th = let 184 val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [wordsTheory.word_mul_n2w,SEP_CLAUSES] th 185 val th = CONV_RULE FIX_WORD32_ARITH_CONV th 186 val th = introduce_xSTACK th 187 val th = introduce_xMEMORY th 188 val th = introduce_xBYTE_MEMORY_ANY th 189 val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [GSYM wordsTheory.WORD_ADD_ASSOC, 190 word_arith_lemma1,word_arith_lemma2,word_arith_lemma3,word_arith_lemma4] th 191 val th = CONV_RULE FIX_WORD32_ARITH_CONV th 192 val th = RW [wordsTheory.WORD_ADD_ASSOC,wordsTheory.WORD_ADD_0] th 193 fun f th = let 194 val x = find_term (can (match_term ``(THE x):'a``)) (concl th) 195 val y = optionSyntax.mk_some(mk_var(fst (dest_var (cdr x)),type_of x)) 196 val th = INST [cdr x |-> y] th 197 val th = SIMP_RULE bool_ss [SEP_CLAUSES,optionLib.option_rws] th 198 in th end 199 val th = repeat f th 200 val th = RW [ALIGNED_def] th 201 val th = SIMP_RULE std_ss [wordsTheory.WORD_EQ_SUB_ZERO,w2w_eq_n2w,w2w_CLAUSES] th 202 in calculate_length_and_jump th end; 203 204fun calc_code th = let 205 val tms = find_terml (can (match_term ``XREAD_INSTR a s = SOME x``)) (concl th) 206 val tms = map dest_eq tms 207 fun addr tm = (Arbnum.toInt o numSyntax.dest_numeral o cdr o cdr o cdr o car) tm 208 handle e => 0 209 val tms = map (fn (x,y) => (addr x, cdr y)) tms 210 val code = map snd (sort (fn (x,_) => fn (y,_) => x <= y) tms) 211 in listSyntax.mk_list (code, ``:word8``) end; 212 213fun x86_prove_one_spec th c = let 214 val g = concl th 215 val s = find_term (can (match_term ``X86_NEXT x = SOME y``)) g 216 val s = (snd o dest_comb o snd o dest_comb) s 217 val (pre,post) = x86_pre_post g s 218 val tm = ``SPEC X86_MODEL pre {(eip,(c,w))} post`` 219 val tm = subst [mk_var("pre",type_of pre) |-> pre, 220 mk_var("post",type_of post) |-> post, 221 mk_var("c",type_of c) |-> c] tm 222 val FLIP_TAC = CONV_TAC (ONCE_REWRITE_CONV [EQ_SYM_EQ]) 223 val th1 = Q.INST [`s`|->`X86_ICACHE_UPDATE x (r,e,t,m,i)`] th 224 val th1 = RW [XREAD_CLAUSES,XWRITE_MEM2_WORD_def] th1 225 val th1 = RW [XWRITE_EFLAG_def,X86_ICACHE_UPDATE_def,XWRITE_MEM2_def,XWRITE_REG_def, 226 APPLY_UPDATE_THM,WORD_EQ_ADD_CANCEL,x86_address_lemma,XWRITE_EIP_def] th1 227 val th = prove(tm, 228(* 229 set_goal([],tm) 230*) 231 MATCH_MP_TAC IMP_X86_SPEC \\ REPEAT STRIP_TAC 232 \\ EXISTS_TAC ((cdr o cdr o concl o UNDISCH) th1) 233 \\ STRIP_TAC \\ REWRITE_TAC [X86_ICACHE_UPDATE_def] 234 THENL [MATCH_MP_TAC th1,ALL_TAC] 235 \\ REPEAT (POP_ASSUM MP_TAC) 236 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 237 STAR_x86_2set, IN_DELETE, APPLY_UPDATE_THM, Xreg_distinct, 238 GSYM ALIGNED_def, wordsTheory.n2w_11, Xeflags_distinct, 239 Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET, 240 EMPTY_SUBSET, SEP_CLAUSES,X86_ICACHE_UPDATE_def,XCLEAR_ICACHE_def, 241 X86_ICACHE_REVERT_def,xM_def,WORD_EQ_ADD_CANCEL,x86_address_lemma] 242 \\ ONCE_REWRITE_TAC [CODE_POOL_x86_2set] 243 \\ REWRITE_TAC [listTheory.LENGTH,address_list_def] 244 \\ SIMP_TAC std_ss [arithmeticTheory.ADD1,X86_ICACHE_EXTRACT_def] 245 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 246 STAR_x86_2set, IN_DELETE, APPLY_UPDATE_THM, Xreg_distinct, 247 GSYM ALIGNED_def, wordsTheory.n2w_11, Xeflags_distinct, 248 Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET, 249 EMPTY_SUBSET,x86_pool_def,X86_ACCURATE_CLAUSES] 250 \\ SIMP_TAC std_ss [XREAD_REG_def,XREAD_EFLAG_def,XREAD_EIP_def] 251 \\ NTAC 3 (FLIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]) 252 \\ SIMP_TAC std_ss [CAN_XREAD_MEM,CAN_XWRITE_MEM,IN_INSERT] 253 \\ SIMP_TAC std_ss [XREAD_MEM2_WORD_def,XREAD_MEM2_def,wordsTheory.WORD_ADD_0] 254 \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_xDATA_PERM] 255 THEN1 (SIMP_TAC std_ss [markerTheory.Abbrev_def] 256 \\ REPEAT STRIP_TAC \\ FLIP_TAC \\ MATCH_MP_TAC XREAD_INSTR_IMP 257 \\ Q.EXISTS_TAC `w` \\ ASM_SIMP_TAC std_ss [] 258 \\ FULL_SIMP_TAC std_ss [wordsTheory.word_add_n2w,GSYM wordsTheory.WORD_ADD_ASSOC]) 259 \\ SIMP_TAC std_ss [word2bytes_thm,EL_thm,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET] 260 \\ FULL_SIMP_TAC std_ss [UPDATE_x86_2set'',word_arith_lemma1, 261 ALIGNED_CLAUSES,icache_revert_ID,X86_ACCURATE_UPDATE] 262 \\ SIMP_TAC std_ss [AND_IMP_INTRO] 263 \\ STRIP_TAC \\ IMP_RES_TAC X86_ACCURATE_IMP 264 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def]) 265 val th = INST [``w:bool``|-> (if !x86_code_write_perm then T else F)] th 266 in RW [STAR_ASSOC,SEP_CLAUSES,markerTheory.Abbrev_def] th end; 267 268fun x86_prove_specs s = let 269 val th = x86_step s 270 val c = calc_code th 271 val th = pre_process_thm th 272 fun replace_conv th tm = if (fst o dest_eq o concl) th = tm then th else ALL_CONV tm 273 in if (is_cond o cdr o cdr o snd o dest_imp o concl) th then let 274 val (x,y,z) = dest_cond (find_term is_cond (concl th)) 275 fun prove_branch cth th = let 276 val tm1 = (fst o dest_imp o concl o ISPECL [x,y,z]) cth 277 val th1 = CONV_RULE (DEPTH_CONV (replace_conv (UNDISCH (ISPECL [x,y,z] cth)))) th 278 val th1 = (RW [AND_IMP_INTRO,GSYM CONJ_ASSOC] o DISCH_ALL) th1 279 val th1 = x86_prove_one_spec th1 c 280 val th1 = SIMP_RULE std_ss [SEP_CLAUSES] (DISCH tm1 th1) 281 val th1 = RW [CONTAINER_def] th1 282 val th1 = RW [RW [GSYM precond_def] (GSYM progTheory.SPEC_MOVE_COND)] th1 283 in post_process_thm th1 end 284 in (prove_branch CONTAINER_IF_T th, SOME (prove_branch CONTAINER_IF_F th)) end 285 else (post_process_thm (x86_prove_one_spec th c),NONE) end 286 287fun x86_jump (tm1:term) (tm2:term) (jump_length:int) (forward:bool) = ("",0) 288 289val x86_spec_aux = cache x86_prove_specs; 290fun x86_spec s = let 291 val (s,rename,exec_flag) = parse_renamer s 292 val ((th,i,j),other) = x86_spec_aux s 293 val b = if exec_flag then T else F 294 val th = INST [``ex:bool``|->b] th 295 val th = RW [GSYM xBYTE_MEMORY_def,GSYM xBYTE_MEMORY_X_def] th 296 val other = case other of NONE => NONE | SOME (th,i,j) => SOME (rename th,i,j) 297 in ((rename th,i,j),other) end 298 299val x86_tools = (x86_spec, x86_jump, x86_status, x86_pc) 300val x86_tools_no_status = (x86_spec, x86_jump, TRUTH, x86_pc); 301 302(* 303 304open x86_encodeLib; 305 306 val th = x86_spec "40"; (* inc eax *) 307 val th = x86_spec "F7C203000000"; (* test edx,3 *) 308 val th = x86_spec "89EE"; (* mov esi,ebp *) 309 val th = x86_spec "81E603000000"; (* and esi,3 *) 310 val th = x86_spec "4E"; (* dec esi *) 311 val th = x86_spec "89EA"; (* mov edx,ebp *) 312 val th = x86_spec "4A"; (* dec edx *) 313 val th = x86_spec "89CD"; (* mov ebp,ecx *) 314 val th = x86_spec "45"; (* inc ebp *) 315 val th = x86_spec "EBF7"; (* jmp L1 *) 316 val th = x86_spec "8B36"; (* mov esi, [esi] *) 317 val th = x86_spec "8B2A"; (* mov ebp,[edx] *) 318 val th = x86_spec "8B7204"; (* mov esi,[edx+4] *) 319 val th = x86_spec "8929"; (* mov [ecx],ebp *) 320 val th = x86_spec "897104"; (* mov [ecx+4],esi *) 321 val th = x86_spec "892A"; (* mov [edx],ebp *) 322 val th = x86_spec "813337020000"; (* xor dword [ebx],567 *) 323 val th = x86_spec "310B"; (* xor [ebx], ecx *) 324 val th = x86_spec "F720"; (* mul dword [eax] *) 325 val th = x86_spec "F7F6"; (* div esi *) 326 val th = x86_spec "883E"; (* mov_byte [esi],edi *) 327 val th = x86_spec "0FB63E"; (* mov_byte edi,[esi] *) 328 val th = x86_spec "E2FD"; (* loop L *) 329 val th = x86_spec "751D"; (* jne L1 *) 330 val th = x86_spec "740D"; (* je L2 *) 331 val th = x86_spec "0F44C1"; (* cmove eax, ecx *) 332 val th = x86_spec (x86_encode "mov_byte [esi],-10") 333 334 val th = x86_spec "31C0"; 335 val th = x86_spec "85F6"; 336 val th = x86_spec "8B36"; 337 val th = x86_spec "85F6"; 338 val th = x86_spec "7405"; 339 340 val th = x86_spec (x86_encode "jmp edx") 341 val th = x86_spec (x86_encode "add [ebp-20],eax") 342 343 val th = x86_spec 344val s = (x86_encode "mov [edi+400],3477") 345 346 val th = x86_spec "813337020000"; (* mov dword [ebx],567 *) 347 348 val th = x86_spec "E9"; (* jmp imm32 *) 349 350*) 351 352end 353