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