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