1structure x86_Lib :> x86_Lib = 2struct 3 4open HolKernel boolLib bossLib; 5open wordsLib stringLib listSyntax simpLib listTheory wordsTheory; 6open opmonTheory bit_listTheory combinTheory ConseqConv; 7 8open x86_Theory x86_seq_monadTheory x86_opsemTheory x86_astTheory; 9open x86_coretypesTheory x86_icacheTheory; 10 11 12(* decoder *) 13 14fun nTimes n f x = if n = 0 then x else nTimes (n-1) f (f x) 15 16fun eval_term_ss tm_name tm = conv_ss 17 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) }; 18 19val bytes_LEMMA = SIMP_RULE std_ss [LENGTH] (Q.SPEC `[v1;v2;v3;v4;v5;v6;v7;v8]` bits2num_LESS) 20 21val n2w_SIGN_EXTEND = prove( 22 ``!n. n < 256 ==> (n2w (SIGN_EXTEND 8 32 n):word32 = sw2sw ((n2w n):word8))``, 23 SIMP_TAC (std_ss++SIZES_ss) [sw2sw_def,w2n_n2w]); 24 25fun raw_x86_decode s = let 26 fun mk_bool_list n = 27 if n = 0 then ``[]:bool list`` else 28 mk_cons(mk_var("vvv"^int_to_string n,``:bool``),mk_bool_list (n-1)) 29 val l = length (explode s) div 2 30 val tm = mk_bool_list (8 * (20 - l)) 31 val tm = subst [``s:string`` |-> fromMLstring s, ``t:bool list``|->tm] ``bytebits s ++ t`` 32 val tm = (snd o dest_eq o concl o EVAL) tm 33 val th = EVAL (mk_comb(``x86_decode``,tm)) 34 val _ = computeLib.add_funs [th] 35 val (th,l) = let 36 val x = find_term (can (match_term ``bits2num xs``)) (concl th) 37 val thi = Q.INST [`w`|->`imm32`] w2bits_word32 38 val i = fst (match_term (snd (dest_comb x)) ((snd o dest_eq o concl o SPEC_ALL) thi)) 39 val th = REWRITE_RULE [GSYM thi] (INST i th) 40 val th = REWRITE_RULE [bits2num_w2bits,n2w_w2n] th 41 in (th,l+4) end handle e => (th,l) 42 val (th,l) = let 43 val x = find_term (can (match_term ``bits2num xs``)) (concl th) 44 val th = REWRITE_RULE [bytes_LEMMA, MATCH_MP n2w_SIGN_EXTEND bytes_LEMMA] th 45 val thi = Q.INST [`w`|->`imm8`] w2bits_word8 46 val i = fst (match_term (snd (dest_comb x)) ((snd o dest_eq o concl o SPEC_ALL) thi)) 47 val th = REWRITE_RULE [GSYM thi] (INST i th) 48 val th = REWRITE_RULE [bits2num_w2bits,n2w_w2n] th 49 in (th,l+1) end handle e => (th,l) 50 val tm = (snd o dest_comb o fst o dest_eq o concl) th 51 in (th,tm,l) end; 52 53fun x86_decode s = let 54 val (th,tm,l) = raw_x86_decode s 55 val th = MATCH_MP X86_NEXT_THM th 56 val th = SIMP_RULE std_ss [LENGTH] th 57 val th = nTimes l (SIMP_RULE std_ss [EVERY_DEF] o ONCE_REWRITE_RULE [XREAD_INSTR_BYTES_def]) th 58 fun assums i n = 59 if i = 0 then [] else 60 subst [``n:num``|->numSyntax.term_of_int n] 61 ``XREAD_INSTR (XREAD_EIP s + n2w n) s = SOME (b2w I (TAKE 8 (DROP (8 * n) t)))`` :: assums (i-1) (n+1) 62 val th = foldr (uncurry DISCH) th (assums l 0) 63 val th = SIMP_RULE std_ss [WORD_ADD_0,GSYM WORD_ADD_ASSOC,word_add_n2w] th 64 val th = INST [``t:bool list``|->tm] th 65 val b2w_ss = eval_term_ss "b2w" ``(TAKE n t):bool list`` 66 val w2bits_ss = eval_term_ss "w2bits" ``w2bits ((b2w I x):word8):bool list`` 67 val th = SIMP_RULE (std_ss++b2w_ss) [FOLDR,MAP] th 68 val th = REWRITE_RULE [w2bits_b2w_word32,APPEND,CONS_11,COLLECT_BYTES_n2w_bits2num] th 69 val th = nTimes l UNDISCH th 70 val th = nTimes 20 (SIMP_RULE std_ss [EVERY_DEF,GSYM WORD_ADD_ASSOC,word_add_n2w] o 71 ONCE_REWRITE_RULE [XREAD_INSTR_BYTES_def]) th 72 val th = SIMP_RULE std_ss [MAP,FOLDR,GSYM WORD_ADD_ASSOC,word_add_n2w,EVERY_DEF] th 73 val th = REWRITE_RULE [GSYM AND_IMP_INTRO,w2bits_EL] th 74 fun inst_one th = let 75 val (x,y) = (dest_eq o fst o dest_imp o concl) th 76 in UNDISCH (INST [y|->x] th) end 77 val th = repeat inst_one th 78 val th = REWRITE_RULE [] (DISCH_ALL th) 79 val th = REWRITE_RULE [GSYM w2bits_word8,COLLECT_BYTES_n2w_bits2num] th 80 val th = REWRITE_RULE [AND_IMP_INTRO,CONJ_ASSOC] th 81 val th = ONCE_REWRITE_RULE [CONJ_COMM] th 82 val th = REWRITE_RULE [GSYM CONJ_ASSOC,GSYM AND_IMP_INTRO] th 83 val any_b2w_ss = eval_term_ss "any_b2w" ``(b2w I xs):'a word`` 84 val th = SIMP_RULE (std_ss++any_b2w_ss) [] th 85 in th end handle e => (print " Decoding failed.\n" ; raise e); 86 87(* one step symbolic simulation *) 88 89val else_none_read_mem_lemma = (UNDISCH o SPEC_ALL) x86_else_none_read_mem_lemma 90val else_none_write_mem_lemma = (UNDISCH o SPEC_ALL) x86_else_none_write_mem_lemma 91val else_none_eflag_lemma = (UNDISCH o SPEC_ALL) x86_else_none_eflag_lemma 92val else_none_assert_lemma = (UNDISCH o SPEC_ALL) option_apply_assertT 93val else_none_conv1 = (fst o dest_eq o concl) else_none_read_mem_lemma 94val else_none_conv2 = (fst o dest_eq o concl) else_none_write_mem_lemma 95val else_none_conv3 = (fst o dest_eq o concl) else_none_eflag_lemma 96val else_none_conv4 = (fst o dest_eq o concl) else_none_assert_lemma 97fun else_none_conv tm = let 98 val ((i,t),th) = (match_term else_none_conv1 tm, else_none_read_mem_lemma) handle HOL_ERR _ => 99 (match_term else_none_conv2 tm, else_none_write_mem_lemma) handle HOL_ERR _ => 100 (match_term else_none_conv3 tm, else_none_eflag_lemma) handle HOL_ERR _ => 101 (match_term else_none_conv4 tm, else_none_assert_lemma) 102 in INST i (INST_TYPE t th) end; 103 104val ss = rewrites [x86_exec_def, XREAD_REG_def, XREAD_EFLAG_def, 105 XREAD_MEM_def, XREAD_EIP_def, XWRITE_REG_def, XWRITE_EFLAG_def, 106 XWRITE_REG_def, XWRITE_MEM_def, XWRITE_EIP_def, bump_eip_def, 107 constT_def, addT_def, lockT_def, failureT_def, seqT_def, parT_def, 108 parT_unit_def, write_reg_def, read_reg_def, write_eflag_def, 109 read_eflag_def, write_eip_def, read_eip_def, write_m32_def, 110 read_m32_def, write_m8_def, read_m8_def, seq_monad_thm, 111 read_src_ea_byte_def, write_ea_byte_def, read_ea_byte_def, 112 write_monop_def, ea_Xr_def, ea_Xi_def, ea_Xrm_base_def, 113 read_reg_byte_def, ea_Xrm_index_def, ea_Xrm_def, ea_Xdest_def, 114 ea_Xsrc_def, read_dest_ea_byte_def, ea_Ximm_rm_def, read_ea_def, 115 read_src_ea_def, read_dest_ea_def, write_ea_def, write_PF_def, 116 write_ZF_def, write_SF_def, write_logical_eflags_def, 117 x86_exec_pop_def, x86_exec_pop_eip_def, write_binop_with_carry_def, 118 write_arith_eflags_except_CF_OF_def, write_arith_eflags_def, 119 add_with_carry_out_def, clear_icache_seq_def, 120 sub_with_borrow_out_def, write_arith_result_def, clear_icache_def, 121 write_arith_result_no_CF_OF_def, write_arith_result_no_write_def, 122 write_logical_result_def, write_logical_result_no_write_def, 123 write_binop_def, write_monop_def, read_cond_def, read_reg_seq_def, 124 read_eip_seq_def, write_eip_seq_def, read_m8_seq_def, 125 write_m8_seq_def, read_m32_seq_def, write_m32_seq_def, 126 APPLY_UPDATE_THM, WORD_EQ_ADD_LCANCEL, x86_address_lemma, 127 write_reg_seq_def, jump_to_ea_def, x86_exec_push_def, 128 x86_exec_push_eip_def, rm_is_memory_access_def, write_eflag_seq_def, 129 if_some_lemma, XREAD_CLAUSES, call_dest_from_ea_def, 130 Xbinop_name_distinct, get_ea_address_def, erase_eflags_def, 131 write_result_erase_eflags_def, word_signed_overflow_add_def, 132 word_signed_overflow_sub_def] 133 134fun x86_step s = let 135 val th = x86_decode s 136 val tm = (fst o dest_eq o fst o dest_imp o concl) th 137 val th1 = SIMP_CONV (std_ss++ss++wordsLib.SIZES_ss) 138 [x86_execute_def,Xrm_distinct,Xrm_11,Xreg_distinct] tm 139 fun cc th = CONV_RULE (ONCE_DEPTH_CONV else_none_conv) th 140 fun f th = (DISCH_ALL o CONV_RULE (RAND_CONV (SIMP_CONV std_ss [pull_if_lemma])) o 141 UNDISCH_ALL o SIMP_RULE (std_ss++ss) [LET_DEF,Xreg_distinct,Xeflags_distinct] o 142 DISCH_ALL o cc) th 143 fun change f x = let val y = f x in if concl y = concl x then x else change f y end 144 val th1 = change f th1 145 val th1 = SIMP_RULE (std_ss++ss) [Xreg_distinct, Xeflags_distinct] th1 146 val th1 = DISCH_ALL (MATCH_MP th (UNDISCH_ALL th1)) 147 val th1 = REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] (DISCH_ALL th1) 148 val th1 = REWRITE_RULE [GSYM XREAD_MEM2_WORD_def,GSYM XWRITE_MEM2_WORD_def] th1 149 val th1 = STRENGTHEN_CONSEQ_CONV_RULE 150 (CONSEQ_REWRITE_CONV ([],[CAN_XREAD_XWRITE_THM],[])) th1 151 handle UNCHANGED => th1 152 val th1 = SIMP_RULE bool_ss [GSYM AND_IMP_INTRO,pred_setTheory.IN_INSERT,pred_setTheory.NOT_IN_EMPTY] th1 153 val th1 = SIMP_RULE bool_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC] th1 154 in th1 end; 155 156 157(* 158 159 open x86_encodeLib; 160 161 (* works *) 162 163 val th = x86_step (x86_encode "dec eax") 164 val th = x86_step "E9" (* example of partial decoder evaluation with imm32 *) 165 val th = x86_step "83F1" (* example of partial decoder evaluation with imm8 *) 166 val th = x86_step (x86_encode "mov [esi],45") 167 val th = x86_step (x86_encode "mov BYTE [eax],-100") 168 val th = x86_step (x86_encode "div esi") 169 val th = x86_step (x86_encode "jmp esi") 170 val th = x86_step (x86_encode "xchg [ebx],eax") 171 val th = x86_step (x86_encode "mov BYTE [esi],edx"); 172 val th = x86_step (x86_encode "movzx edx,BYTE [esi]"); 173 val th = x86_step "0538000000"; (* add eax,56 *) 174 val th = x86_step "8B3E"; (* mov edi,[esi] *) 175 val th = x86_step "810037020000"; (* add dword [eax],567 *) 176 val th = x86_step "010B"; (* add [ebx], ecx *) 177 val th = x86_step "0119"; (* add [ecx], ebx *) 178 val th = x86_step "2538000000"; (* and eax,56 *) 179 val th = x86_step "812037020000"; (* and dword [eax],567 *) 180 val th = x86_step "210B"; (* and [ebx], ecx *) 181 val th = x86_step "2319"; (* and ebx, [ecx] *) 182 val th = x86_step "81FE38000000"; (* cmp esi,56 *) 183 val th = x86_step "813B37020000"; (* cmp dword [ebx],567 *) 184 val th = x86_step "390B"; (* cmp [ebx], ecx *) 185 val th = x86_step "3B19"; (* cmp ebx, [ecx] *) 186 val th = x86_step "893E"; (* mov [esi],edi *) 187 val th = x86_step "8B3E"; (* mov edi,[esi] *) 188 val th = x86_step "BC37020000"; (* mov esp,567 *) 189 val th = x86_step "81CE38000000"; (* or esi,56 *) 190 val th = x86_step "810B37020000"; (* or dword [ebx],567 *) 191 val th = x86_step "090B"; (* or [ebx], ecx *) 192 val th = x86_step "0B19"; (* or ebx, [ecx] *) 193 val th = x86_step "81EE38000000"; (* sub esi,56 *) 194 val th = x86_step "812B37020000"; (* sub dword [ebx],567 *) 195 val th = x86_step "290B"; (* sub [ebx], ecx *) 196 val th = x86_step "2B19"; (* sub ebx, [ecx] *) 197 val th = x86_step "F7C638000000"; (* test esi,56 *) 198 val th = x86_step "F70337020000"; (* test dword [ebx],567 *) 199 val th = x86_step "850B"; (* test [ebx], ecx *) 200 val th = x86_step "81F638000000"; (* xor esi,56 *) 201 val th = x86_step "813337020000"; (* xor dword [ebx],567 *) 202 val th = x86_step "310B"; (* xor [ebx], ecx *) 203 val th = x86_step "3319"; (* xor ebx, [ecx] *) 204 val th = x86_step "FF4E3C"; (* dec dword [esi+60] *) 205 val th = x86_step "4C"; (* dec esp *) 206 val th = x86_step "FF80401F0000"; (* inc dword [eax+8000] *) 207 val th = x86_step "40"; (* inc eax *) 208 val th = x86_step "F750C8"; (* not dword [eax-56] *) 209 val th = x86_step "EBB9"; (* jmp l1 *) 210 val th = x86_step "F7583C"; (* neg dword [eax+60] *) 211 val th = x86_step "74B7"; (* je l1 *) 212 val th = x86_step "75B5"; (* jne l1 *) 213 val th = x86_step "0F44C1"; (* cmove eax, ecx *) 214 val th = x86_step "0F454104"; (* cmovne eax, [ecx+4] *) 215 val th = x86_step "8F0590010000"; (* pop dword [400] *) 216 val th = x86_step "50"; (* push eax *) 217 val th = x86_step "C3"; (* ret *) 218 val th = x86_step "C20500"; (* ret 5 *) 219 val th = x86_step "E8BDFFFFFF"; (* call l1 *) 220 val th = x86_step "FFB42DEA000000"; (* push dword [ebp + ebp + 234] *) 221 val th = x86_step "FFB498C8010000"; (* push dword [eax + 4*ebx + 456] *) 222 val th = x86_step "FF749801"; (* push dword [eax + 4*ebx + 1] *) 223 val th = x86_step "FF74AD02"; (* push dword [ebp + 4*ebp + 2] *) 224 val th = x86_step "FF746D2D"; (* push dword [ebp + 2*ebp + 45] *) 225 val th = x86_step "FFB4B6EE711202"; (* push dword [esi + 4*esi + 34763246] *) 226 val th = x86_step "E2AF"; (* loop l1 *) 227 val th = x86_step "E1AD"; (* loope l1 *) 228 val th = x86_step "E0AB"; (* loopne l1 *) 229 val th = x86_step "59"; (* pop ecx *) 230 val th = x86_step "FFD0"; (* call eax *) 231 val th = x86_step "0FB110"; (* cmpxchg [eax],edx *) 232 val th = x86_step "0FC11E"; (* xadd [esi],ebx *) 233 val th = x86_step "93"; (* xchg eax, ebx *) 234 val th = x86_step "8731"; (* xchg [ecx], esi *) 235 val th = x86_step "F720"; (* mul dword [eax] *) 236 val th = x86_step "F7F6"; (* div esi *) 237 238 (* not sure *) 239 240 val th = x86_step "60"; (* pushad *) 241 val th = x86_step "61"; (* popad *) 242 243*) 244 245val _ = output_words_as_hex(); 246 247fun x86_test_aux inst input output = let 248 val rw = x86_step inst 249 fun format state (i,j) = 250 if i = "EIP" 251 then ("XREAD_EIP "^state^" = 0x"^j^"w") 252 else if length (explode i) = 3 253 then ("XREAD_REG "^i^" "^state^" = 0x"^j^"w") 254 else if length (explode i) = 2 255 then ("XREAD_EFLAG X_"^i^" "^state^" = SOME "^j) 256 else ("XREAD_MEM 0x"^i^"w "^state^" = SOME (0x"^j^"w)") 257 fun p y = Parse.Term [QUOTE y] 258 fun f s = map (p o format s) 259 val th = foldr (fn (x,y) => DISCH x y) rw (f "s" input) 260 val th = SIMP_RULE std_ss [Xrm_distinct,Xrm_11,Xreg_distinct,Xeflags_distinct] th 261 val th = SIMP_RULE std_ss [word_add_n2w,WORD_ADD_0,b2w_def,bits2num_def,GSYM AND_IMP_INTRO] th 262 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_n2w,word_mul_n2w,word_add_n2w,word_sub_def,word_2comp_n2w] th 263 val ss = eval_term_ss "a" ``(bytes2word (xs:word8 list)):word32`` 264 val th = SIMP_RULE (std_ss++ss++SIZES_ss) [n2w_11] th 265 val th = ONCE_REWRITE_RULE [XREAD_EIP_ADD_0] th 266 val th = REWRITE_RULE [AND_IMP_INTRO] th 267 val th = REWRITE_RULE [GSYM CONJ_ASSOC] th 268 val xs = find_terms (can (match_term ``XWRITE_EFLAG x NONE``)) (concl th) 269 val xs = map (implode o tl o tl o explode o fst o dest_const o snd o dest_comb o fst o dest_comb) xs 270 fun distinct [] = [] | distinct (x::xs) = x::distinct (filter (fn y => not (y = x)) xs) 271 val xs = distinct xs 272 val output2 = filter (fn (x,y) => not (mem x xs)) output 273 val output1 = filter (fn (x,y) => mem x xs) output 274 val _ = map (fn (x,y) => print (" Value of "^x^" is left unspecified by model.\n")) output1 275 val tm = list_mk_conj (f "(THE (X86_NEXT s))" output2) 276 val tm2 = (hd o hyp o UNDISCH) th 277 val goal = mk_imp(tm2,tm) 278(* 279 set_goal([],goal) 280*) 281 val result = prove(goal, 282 STRIP_TAC 283 THEN (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO]) th 284 THEN ASM_SIMP_TAC std_ss [XREAD_CLAUSES,optionTheory.THE_DEF,Xreg_distinct,Xeflags_distinct] 285 THEN STRIP_ASSUME_TAC x86_state_EXPAND 286 THEN FULL_SIMP_TAC std_ss [XREAD_REG_def,XREAD_EFLAG_def,XREAD_MEM_def,XREAD_EIP_def, 287 XWRITE_MEM_def,XWRITE_REG_def,XWRITE_EFLAG_def,XWRITE_EIP_def, APPLY_UPDATE_THM,Xreg_distinct] 288 THEN EVAL_TAC) 289 val result = REWRITE_RULE [GSYM AND_IMP_INTRO] result 290 in result end; 291 292fun x86_test inst input output = let 293 fun p s = if length (explode s) < 4 then s else "["^s^"]" 294 val _ = print ("\nTesting:\n instruction = "^inst^"\n") 295 val _ = print ("Input:\n") 296 val _ = map (fn (x,y) => print (" "^(p x)^" = "^y^"\n")) input 297 val _ = print ("Output:\n") 298 val _ = map (fn (x,y) => print (" "^(p x)^" = "^y^"\n")) output 299 val _ = print ("Result:\n") 300 val th = SOME (x86_test_aux inst input output) handle e => NONE 301 in case th of 302 NONE => (print " Test failed.\n"; TRUTH) 303 | SOME th => (print " Test successful.\n\n"; print_thm th; print "\n\n"; th) 304 end; 305 306 307end 308