1structure prog_ppcLib :> prog_ppcLib =
2struct
3
4open HolKernel boolLib bossLib;
5open wordsLib stringLib addressTheory pred_setTheory combinTheory;
6open set_sepTheory ppc_Theory prog_ppcTheory helperLib ppc_Lib;
7open ppc_coretypesTheory ppc_seq_monadTheory;
8
9infix \\
10val op \\ = op THEN;
11
12
13val ppc_status = pS_HIDE
14val ppc_pc = ``pPC``;
15
16fun process v tm =
17  if type_of tm = ``:ppc_reg`` then
18     if tm = ``PPC_PC``  then (``pPC`` ,``p:word32``) else
19     if tm = ``PPC_LR``  then (``pLR`` ,``lr:word32``) else
20     if tm = ``PPC_CTR`` then (``pCTR``,``ctr:word32``) else
21       let val tm = snd (dest_comb tm)
22           val f = int_to_string o numSyntax.int_of_term o snd o dest_comb in
23         (mk_comb(``pR``,tm),mk_var("r" ^ f tm,``:word32``)) end
24   else if type_of tm = ``:ppc_bit`` then
25     if tm = ``PPC_CARRY``  then (``pS1 PPC_CARRY`` ,``c:bool option``) else
26       let val f = int_to_string o numSyntax.int_of_term o snd o dest_comb o snd o dest_comb in
27         (mk_comb(``pS1``,tm),mk_var("s" ^ f tm,``:bool option``)) end
28   else if type_of tm = ``:word32`` then
29     (mk_comb(``pM1``,tm),v)
30   else fail();
31
32fun pre_process_thm th = let
33  val rs = find_terml (can (match_term ``PREAD_R x s``)) (concl th)
34  val fs = find_terml (can (match_term ``PREAD_S x s``)) (concl th)
35  val regs = map (fn tm => mk_eq(tm,(snd o process T o cdr o car) tm)) rs
36  fun f t = optionSyntax.mk_some o (fn x => mk_var(x,t)) o fst o dest_var
37  val flags = map (fn tm => mk_eq(tm,(f ``:bool`` o snd o process T o cdr o car) tm)) fs
38  val th = foldr (uncurry DISCH) th (regs @ flags)
39  val th = SIMP_RULE bool_ss [optionTheory.option_CLAUSES] th
40  val ms = find_terml (can (match_term ``~(PREAD_M x s = NONE)``)) (concl th)
41  val ms = map (fst o dest_eq o dest_neg) ms
42  val mems = map (fn tm => mk_eq(tm,f ``:word8`` (genvar(``:bool``)))) ms
43  val th = foldr (uncurry DISCH) th mems
44  val th = RW [AND_IMP_INTRO,GSYM CONJ_ASSOC,wordsTheory.WORD_XOR_CLAUSES,
45             wordsTheory.WORD_AND_CLAUSES] (SIMP_RULE std_ss [] th)
46  in th end;
47
48fun ppc_pre_post g = let
49  val regs = collect_term_of_type ``:ppc_reg`` g;
50  val bits = collect_term_of_type ``:ppc_bit`` g;
51  val mems = find_terml (can (match_term ``(PREAD_M x s = SOME y)``)) g
52  val mems = filter (is_var o cdr o cdr) mems
53  val mems = map (fn tm => ((cdr o car o fst o dest_eq) tm, cdr tm)) mems
54  val assignments = find_terml (can (match_term ``PWRITE_S a x``)) g
55                  @ find_terml (can (match_term ``PWRITE_R a x``)) g
56                  @ find_terml (can (match_term ``PWRITE_M a x``)) g
57  val assignments = map (fn tm => (cdr (car tm), cdr tm)) assignments
58  fun assigned_aux x y [] = y
59    | assigned_aux x y ((q,z)::zs) = if x = q then z else assigned_aux x y zs
60  fun get_assigned_value x y = assigned_aux x y assignments
61  fun mk_pre_post_assertion (x,v) = let
62    val (y,z) = process v x
63    val q = get_assigned_value x z
64    in (mk_comb(y,z),mk_comb(y,q)) end
65  val pre_post = map mk_pre_post_assertion (map (fn tm => (tm,T)) (regs @ bits) @ mems)
66  val pre = list_mk_star (map fst pre_post) ``:ppc_set -> bool``
67  val post = list_mk_star (map snd pre_post) ``:ppc_set -> bool``
68  fun is_precond tm =
69   (not (can (match_term ``PREAD_R r s = v``) tm) andalso
70    not (can (match_term ``PREAD_M r s = v``) tm) andalso
71    not (can (match_term ``PREAD_S r s = v``) tm)) handle e => true
72  val all_conds = (list_dest dest_conj o fst o dest_imp) g
73  val pre_conds = (filter is_precond) all_conds
74  val pre_conds = (filter (fn tm => not (tm = ``p && 3w = 0w:word32``))) pre_conds
75  val ss = foldr (fn (x,y) => (fst (dest_eq x) |-> snd (dest_eq x)) :: y handle e => y) []
76             (filter is_precond pre_conds)
77  val ss = ss @ map ((fn tm => mk_var((fst o dest_var o cdr) tm,``:bool option``) |-> tm) o cdr)
78    (filter (can (match_term ``PREAD_S x s = SOME y``)) all_conds)
79  val pre = subst ss pre
80  val post = subst ss post
81  val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds))
82  in (pre,post) end;
83
84fun introduce_pMEMORY th = let
85  val (_,p,c,q) = dest_spec(concl th)
86  val tm3 = find_term (can (match_term ``pM1 (x + 3w) y``)) p
87  val tm = (fst o dest_comb o snd o dest_comb o fst o dest_comb) tm3
88  val vs = FVL [tm] empty_varset
89  val tm0 = mk_comb(mk_comb(``pM1``,snd (dest_comb tm)),``yyy : word8 option``)
90  val tm0 = find_term (can (match_terml [] vs tm0)) p
91  val tm1 = mk_comb(mk_comb(``pM1``,mk_comb(tm,``1w:word32``)),``yyy : word8 option``)
92  val tm1 = find_term (can (match_terml [] vs tm1)) p
93  val tm2 = mk_comb(mk_comb(``pM1``,mk_comb(tm,``2w:word32``)),``yyy : word8 option``)
94  val tm2 = find_term (can (match_terml [] vs tm2)) p
95  val c =
96     LIST_MOVE_OUT_CONV true (List.map (fst o dest_comb) [tm3, tm2, tm1, tm0])
97  val th = CONV_RULE (POST_CONV c THENC PRE_CONV c) th
98  val f = snd o dest_comb o snd o dest_comb
99  fun g th tm tm' = if is_var tm then INST [ tm |-> tm' ] th else th
100  val th = g th (f tm0) ``((7 >< 0) ((w >> 24):word32)):word8``
101  val th = g th (f tm1) ``((7 >< 0) ((w >> 16):word32)):word8``
102  val th = g th (f tm2) ``((7 >< 0) ((w >> 8):word32)):word8``
103  val th = g th (f tm3) ``((7 >< 0) (w:word32)):word8``
104  val h = REWRITE_RULE [GSYM STAR_ASSOC]
105  val th = MATCH_MP (h pMEMORY_INTRO) (h th)
106  val th = SIMP_RULE bool_ss [GSYM ALIGNED_def,SEP_CLAUSES] th
107  val th = REWRITE_RULE [GSYM progTheory.SPEC_MOVE_COND,ALIGNED_def,
108             STAR_ASSOC,bit_listTheory.bytes2word_thm] th
109  fun replace_access_in_pre th = let
110    val (_,p,c,q) = dest_spec(concl th)
111    val tm = find_term (can (match_term ``(a:'a =+ w:'b) f``)) p
112    val (tm,y) = dest_comb tm
113    val (tm,x) = dest_comb tm
114    val a = snd (dest_comb tm)
115    val th = REWRITE_RULE [APPLY_UPDATE_ID] (INST [x |-> mk_comb(y,a)] th)
116    in th end handle e => th
117  val th = replace_access_in_pre th
118  in th end handle e => th;
119
120fun introduce_pBYTE_MEMORY th = let
121  val (_,p,c,q) = dest_spec(concl th)
122  val tm0 = find_term (can (match_term ``pM1 x y``)) p
123  val c = LIST_MOVE_OUT_CONV true [car tm0]
124  val th = CONV_RULE (POST_CONV c THENC PRE_CONV c) th
125  val f = cdr o cdr
126  val h = REWRITE_RULE [GSYM STAR_ASSOC,bit_listTheory.bytes2word_thm]
127  val th = MATCH_MP (h pBYTE_MEMORY_INTRO) (h th)
128  val th = RW [wordsTheory.WORD_ADD_0,GSYM progTheory.SPEC_MOVE_COND] th
129  fun replace_access_in_pre th = let
130    val (_,p,c,q) = dest_spec(concl th)
131    val tm = find_term (can (match_term ``(a:'a =+ w:'b) f``)) p
132    val (tm,y) = dest_comb tm
133    val (tm,x) = dest_comb tm
134    val a = snd (dest_comb tm)
135    val th = REWRITE_RULE [APPLY_UPDATE_ID] (INST [x |-> mk_comb(y,a)] th)
136    in th end handle e => th
137  val th = replace_access_in_pre th
138  val th = RW [STAR_ASSOC] th
139  in th end handle e => th;
140
141fun calculate_length_and_jump th =
142  let val (_,_,_,q) = dest_spec(concl th) in
143    let val v = find_term (fn t => t = ``pPC (p + 4w)``) q in (th,4,SOME 4) end
144  handle e =>
145    let val v = find_term (can (match_term ``pPC (p + n2w n)``)) q
146    in (th,4,SOME (0 + (numSyntax.int_of_term o cdr o cdr o cdr) v)) end
147  handle e =>
148    let val v = find_term (can (match_term ``pPC (p - n2w n)``)) q
149    in (th,4,SOME (0 - (numSyntax.int_of_term o cdr o cdr o cdr) v)) end
150  handle e =>
151    (th,4,NONE) end
152
153fun post_process_thm th = let
154  val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss)
155             [wordsTheory.word_mul_n2w,wordsTheory.WORD_ADD_0,wordsTheory.WORD_OR_IDEM] th
156  val th = CONV_RULE FIX_WORD32_ARITH_CONV th
157  val th = introduce_pMEMORY th
158  val th = introduce_pBYTE_MEMORY th
159  val th = RW [bit_listTheory.bytes2word_thm,extract_byte] th
160  in calculate_length_and_jump th end;
161
162fun ppc_prove_one_spec th c = let
163  val g = concl th
164  val th = Q.INST [`s`|->`(pr,ps,pm)`] th
165  val s = find_term (can (match_term ``PPC_NEXT x = SOME y``)) (concl th)
166  val s = (snd o dest_comb o snd o dest_comb) s
167  val (pre,post) = ppc_pre_post g
168  val tm = ``SPEC PPC_MODEL pre {(p,c)} post``
169  val tm = subst [mk_var("pre",type_of pre) |-> pre,
170                  mk_var("post",type_of post) |-> post,
171                  mk_var("c",type_of c) |-> c] tm
172  val FLIP_TAC = CONV_TAC (ONCE_REWRITE_CONV [EQ_SYM_EQ])
173  val th = RW [PREAD_R_def,PREAD_S_def,PREAD_M_def,PWRITE_R_def,PWRITE_S_def,PWRITE_M_def] th
174  val result = prove(tm,
175    MATCH_MP_TAC IMP_PPC_SPEC \\ REPEAT STRIP_TAC \\ EXISTS_TAC s
176    \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC,
177         STAR_ppc2set, CODE_POOL_ppc2set, pR_def, pPC_def, IN_DELETE,
178         APPLY_UPDATE_THM, ppc_reg_distinct, ppc_reg_11, ALIGNED_INTRO,
179         wordsTheory.n2w_11, ppc_bit_11, ppc_bit_distinct, Q.SPECL [`s`,`x
180         INSERT aaa`] SET_EQ_SUBSET, INSERT_SUBSET, EMPTY_SUBSET,
181         PREAD_R_def,PREAD_S_def,PREAD_M_def,PWRITE_R_def,PWRITE_S_def,PWRITE_M_def]
182    \\ NTAC 3 (FLIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO])
183    \\ FLIP_TAC \\ REWRITE_TAC [AND_IMP_INTRO, GSYM CONJ_ASSOC]
184    \\ SIMP_TAC std_ss [] \\ FLIP_TAC \\ STRIP_TAC \\ STRIP_TAC
185    THEN1 (FLIP_TAC \\ MATCH_MP_TAC (RW [ALIGNED_INTRO] th) \\ FULL_SIMP_TAC std_ss
186           [ALIGNED_def,wordsTheory.WORD_ADD_0,markerTheory.Abbrev_def] \\ EVAL_TAC)
187    \\ ASM_REWRITE_TAC [ALIGNED_INTRO]
188    \\ ASM_SIMP_TAC std_ss [UPDATE_ppc2set'',ALIGNED_CLAUSES]
189    \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4]
190    \\ ASM_SIMP_TAC std_ss [wordsTheory.WORD_ADD_0])
191  in RW [STAR_ASSOC,markerTheory.Abbrev_def] result end;
192
193fun ppc_prove_specs s = let
194  val (s,rename,_) = parse_renamer s
195  val th = ppc_step s
196  val th = pre_process_thm th
197  val c = mk_comb(``n2w:num->word32``,(numSyntax.mk_numeral o Arbnum.fromHexString) s)
198  fun replace_conv th tm = if (fst o dest_eq o concl) th = tm then th else ALL_CONV tm
199  val result =
200     if (is_cond o snd o dest_imp o concl) th then let
201       val (x,y,z) = dest_cond (find_term is_cond (concl th))
202       fun prove_branch cth th = let
203         val tm1 = (fst o dest_imp o concl o ISPECL [x,y,z]) cth
204         val th1 = CONV_RULE (DEPTH_CONV (replace_conv (UNDISCH (ISPECL [x,y,z] cth)))) th
205         val th1 = (RW [AND_IMP_INTRO,GSYM CONJ_ASSOC] o DISCH_ALL) th1
206         val th1 = ppc_prove_one_spec th1 c
207         val th1 = SIMP_RULE std_ss [SEP_CLAUSES] (DISCH tm1 th1)
208         val th1 = RW [CONTAINER_def] th1
209         val th1 = RW [RW [GSYM precond_def] (GSYM progTheory.SPEC_MOVE_COND)] th1
210         in post_process_thm th1 end
211       in (prove_branch CONTAINER_IF_T th, SOME (prove_branch CONTAINER_IF_F th)) end
212     else (post_process_thm (ppc_prove_one_spec th c),NONE)
213  val result =
214    case result of ((th1,i1,j1),NONE) => ((rename th1,i1,j1),NONE)
215    | ((th1,i1,j1),SOME (th2,i2,j2)) => ((rename th1,i1,j1),SOME (rename th2,i2,j2))
216  in result end
217
218fun ppc_jump (tm1:term) (tm2:term) (jump_length:int) (forward:bool) = ("",0)
219
220val ppc_spec = cache ppc_prove_specs;
221val ppc_tools = (ppc_spec, ppc_jump, ppc_status, ppc_pc)
222val ppc_tools_no_status = (ppc_spec, ppc_jump, TRUTH, ppc_pc);
223
224
225(*
226
227  val th = ppc_spec "7C119000";  (* cmpw 17,18    *)
228  val th = ppc_spec "7C812839";  (* and. 1,4,5    *)
229  val th = ppc_spec "7C5A2278";  (* xor 26, 2, 4  *)
230  val th = ppc_spec "7C5A1378";  (* mr 26, 2      *)
231  val th = ppc_spec "7C5A212E";  (* stwx 2, 26, 4 *)
232  val th = ppc_spec "80450004";  (* lwz 2, 4(5)   *)
233  val th = ppc_spec "7C221A14";  (* add 1,2,3     *)
234  val th = ppc_spec "4BFFFFFC";  (* b L1          *)
235  val th = ppc_spec "4181FFF4";  (* bc 12,1,L1    *)
236  val th = ppc_spec "4082FFF0";  (* bc 4,2,L1     *)
237  val th = ppc_spec "4083FFEC";  (* bc 4,3,L1     *)
238  val th = ppc_spec "88830005";  (* lbz 4,5,3     *)
239  val th = ppc_spec "98830005";  (* stb 4,5,3     *)
240  val th = ppc_spec "7C858396";  (* divwu 4,5,16  *)
241
242  (* pMEMORY is not properly introduced for half-words,
243     also fails if more than one memory location is accessed. *)
244
245  val th = ppc_spec "7E7A222E";  (* lhzx 19, 26, 4 *)
246  val th = ppc_spec "7E7A22AE";  (* lhax 19, 26, 4 *)
247
248  val s = ppc_encodeLib.ppc_encode "stb 4,5,3"
249
250*)
251
252
253end
254