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