1(* 2structure arm_translateLib :> arm_translateLib = 3struct 4 5 loadPath := 6 (concat Globals.HOLDIR "/examples/dev/sw") :: 7 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 8 (concat Globals.HOLDIR "/examples/elliptic/sep") :: 9 (concat Globals.HOLDIR "/examples/elliptic/swsep") :: 10 !loadPath; 11 12 use (concat Globals.HOLDIR "/examples/dev/sw/compiler"); 13 quietdec := true; 14 15 map load ["arm_progTheory", "arm_instTheory", "pred_setSyntax", "swsepTheory", "set_sepLib"]; 16 17 quietdec := false; 18*) 19 20 21open HolKernel boolLib bossLib Parse; 22open Portable Assem wordsTheory ANF pairTheory pairLib listTheory arithmeticTheory whileTheory wordsLib PairedLambda mechReasoning IRSyntax; 23open swsepTheory arm_progTheory progTheory pred_setTheory set_sepLib set_sepTheory arm_instTheory listTheory 24 wordsTheory pairTheory wordsLib markerTheory 25 26fun extract_ir (_, _, _, _, _, spec, _, wf, _, _, _) = 27 let 28 val ir = rand (concl wf); 29 val (st_var, _) = dest_forall (concl spec); 30 val new_var = prim_variant [st_var] st_var; 31 32 val replace = ``^new_var = run_ir ^ir ^st_var``; 33 val replace_thm = ASSUME replace 34 val thm = GEN_ALL (DISCH replace (REWRITE_RULE [GSYM replace_thm] (SPEC_ALL spec))) 35 in 36 (thm, wf, ir) 37 end; 38 39fun translate_ir ir = 40 let 41 val t1 = ``CTL_STRUCTURE2INSTRUCTION_LIST ^ir`` 42 val t2 = ``CONTAINS_MEMORY_DOPER ^ir`` 43 val t3 = ``IS_WELL_FORMED_CTL_STRUCTURE ^ir`` 44 val thm1 = EVAL t1 45 val thm2 = EVAL t2 46 val thm3 = EVAL t3 47 in 48 (rhs (concl thm1), thm1, thm2, thm3) 49 end; 50 51 52fun spec_ir comp = 53 let 54 val (spec, wf, ir) = extract_ir comp; 55 val (vars, body) = strip_forall (concl spec); 56 57 fun replace var_old var_new = 58 subst [``mread ^var_old (RR R0)`` |-> ``^var_new (MREG2REG R0)``, 59 ``mread ^var_old (RR R1)`` |-> ``^var_new (MREG2REG R1)``, 60 ``mread ^var_old (RR R2)`` |-> ``^var_new (MREG2REG R2)``, 61 ``mread ^var_old (RR R3)`` |-> ``^var_new (MREG2REG R3)``, 62 ``mread ^var_old (RR R4)`` |-> ``^var_new (MREG2REG R4)``, 63 ``mread ^var_old (RR R5)`` |-> ``^var_new (MREG2REG R5)``, 64 ``mread ^var_old (RR R6)`` |-> ``^var_new (MREG2REG R6)``, 65 ``mread ^var_old (RR R7)`` |-> ``^var_new (MREG2REG R7)``, 66 ``mread ^var_old (RR R8)`` |-> ``^var_new (MREG2REG R8)``, 67 ``mread ^var_old (RR R9)`` |-> ``^var_new (MREG2REG R9)``, 68 ``mread ^var_old (RR R10)`` |-> ``^var_new (MREG2REG R10)``, 69 ``mread ^var_old (RR R11)`` |-> ``^var_new (MREG2REG R11)``, 70 ``mread ^var_old (RR R12)`` |-> ``^var_new (MREG2REG R12)``, 71 ``mread ^var_old (RR R13)`` |-> ``^var_new (MREG2REG R13)``, 72 ``mread ^var_old (RR R14)`` |-> ``^var_new (MREG2REG R14)``]; 73 74 val new_var1 = prim_variant (free_vars body) (mk_var ("r", ``:word4 -> word32``)) 75 val new_var2 = prim_variant (new_var1::free_vars body) (mk_var ("r", ``:word4 -> word32``)) 76 77 val spec_term = rand (body); 78 val spec_term = replace (el 1 vars) new_var2 spec_term; 79 val spec_term = replace (el 2 vars) new_var1 spec_term; 80 val spec_term = mk_abs (new_var2, spec_term); 81 val spec_term = mk_abs (new_var1, spec_term); 82 83 84 85 val (_, ir_thm, mem_thm, wf_thm2) = translate_ir ir; 86 val thm = SIMP_RULE std_ss [dimindex_24] TRANSLATION_SPEC_thm; 87 val thm = SPECL [ir, spec_term] thm 88 val thm = SIMP_RULE list_ss [wf, ir_thm, mem_thm, wf_thm2, state2reg_fun2mread, 89 arm_mem_state2reg_fun2REG_READ, spec, ILTheory.from_reg_index_def] thm 90 in 91 thm 92 end; 93 94 95 96 fun FILTER_CONV conv t = 97 let 98 val thm = ONCE_REWRITE_CONV [FILTER] t; 99 val thm = BETA_RULE thm 100 val r = rhs (concl thm) 101 val e = if (is_cond r) then 102 let 103 val thm2 = ((RATOR_CONV (RATOR_CONV conv)) THENC REWRITE_CONV []) r; 104 val thm = CONV_RULE (RHS_CONV (REWRITE_CONV [thm2])) thm 105 in 106 CONV_RULE (RHS_CONV (DEPTH_CONV (FILTER_CONV conv))) thm 107 end 108 else 109 thm 110 in 111 e 112 end; 113 114fun post_process_sep thm = 115 let 116 val thm = (SIMP_RULE std_ss [GSYM SEP_HIDE_THM, STAR_ASSOC]) thm 117 val thm = (CONV_RULE (DEPTH_CONV ETA_CONV)) thm 118 119 val (_, body) = strip_forall (concl thm); 120 val (arm_prog, args) = strip_comb body; 121 val pre = hd args; 122 val opr = rator (rator pre); 123 val used_values = free_vars (el 4 args); 124 val pre_parts = liteLib.binops opr pre 125 126 fun remove_unused t = 127 if mem (rand t) used_values then t else 128 liteLib.mk_icomb (``$~:('a -> 'b -> bool) -> 'b -> bool``, rator t) 129 130 val new_preparts = map remove_unused pre_parts 131 132 val new_pre = mk_icomb (arm_prog, foldr (fn (t1, t2) => liteLib.list_mk_icomb opr [t1, t2]) (``emp:('a ARMel -> bool) -> bool``) new_preparts) 133 val new_pre = rhs (concl (SIMP_CONV std_ss [emp_STAR, STAR_ASSOC] new_pre)) 134 val new_pre_thm = SIMP_CONV (std_ss++SEP_EXISTS_ss) [SEP_HIDE_THM] new_pre; 135 136 val new_term = liteLib.list_mk_icomb new_pre (tl args) 137 val new_term = gen_all new_term; 138 139 val thm = prove (new_term, 140 SIMP_TAC std_ss [GSYM SEP_HIDE_THM, new_pre_thm] THEN 141 ONCE_REWRITE_TAC[prove(``ARM_PROG (p:'a ARMset set) = ARM_PROG (emp * p)``, REWRITE_TAC[emp_STAR])] THEN 142 SIMP_TAC std_ss [GSYM ARM_PROG_HIDE_PRE] THEN 143 SIMP_TAC std_ss [emp_STAR, thm]); 144 in 145 thm 146 end; 147 148 149fun spec_sep (comp:(string * hol_type * (IRSyntax.exp * 'a * IRSyntax.exp) * thm list * thm * thm * thm * thm * thm * string * string list)) = 150 let 151 val (spec, wf, ir) = extract_ir comp; 152 val input_regs = listSyntax.mk_list (map IRSyntax.convert_reg (IRSyntax.pair2list (#1 (#3 comp))), Type `:MREG`); 153 154 val unchanged_thm = CONJUNCT1 (REWRITE_RULE [ILTheory.UNCHANGED_STACK_def] (#9 comp)) 155 156 val uregs_all = rand (rator (concl unchanged_thm)); 157 val uregs_term = ``FILTER (\r. ~MEM r ^input_regs) ^uregs_all`` 158 val uregs_thm = (FILTER_CONV (SIMP_CONV std_ss [MEM, ILTheory.MREG_distinct])) 159 uregs_term 160 val uregs = rhs (concl uregs_thm) 161 162 val uregs_input = rhs (concl ((FILTER_CONV (SIMP_CONV std_ss [MEM, ILTheory.MREG_distinct])) 163 ``FILTER (\r. MEM r ^uregs_all) ^input_regs``)) 164 val r_unchanged_thm = REWRITE_RULE [uregs_thm] 165 (prove (``UNCHANGED ^uregs_term ^ir``, 166 MP_TAC unchanged_thm THEN 167 REWRITE_TAC [ILTheory.UNCHANGED_def, MEM_FILTER] THEN 168 PROVE_TAC[])); 169 170 val (vars, body) = strip_forall (concl spec); 171 val body_rel = rand body 172 val body_rel = 173 (rhs (concl (SIMP_CONV std_ss [PAIR_FST_SND_EQ] body_rel))) 174 handle _ => body_rel 175 176 val vals = ``vals:word4->word32``; 177 fun replace var_old = 178 subst [``mread ^var_old (RR R0)`` |-> ``^vals (MREG2REG R0)``, 179 ``mread ^var_old (RR R1)`` |-> ``^vals (MREG2REG R1)``, 180 ``mread ^var_old (RR R2)`` |-> ``^vals (MREG2REG R2)``, 181 ``mread ^var_old (RR R3)`` |-> ``^vals (MREG2REG R3)``, 182 ``mread ^var_old (RR R4)`` |-> ``^vals (MREG2REG R4)``, 183 ``mread ^var_old (RR R5)`` |-> ``^vals (MREG2REG R5)``, 184 ``mread ^var_old (RR R6)`` |-> ``^vals (MREG2REG R6)``, 185 ``mread ^var_old (RR R7)`` |-> ``^vals (MREG2REG R7)``, 186 ``mread ^var_old (RR R8)`` |-> ``^vals (MREG2REG R8)``, 187 ``mread ^var_old (RR R9)`` |-> ``^vals (MREG2REG R9)``, 188 ``mread ^var_old (RR R10)`` |-> ``^vals (MREG2REG R10)``, 189 ``mread ^var_old (RR R11)`` |-> ``^vals (MREG2REG R11)``, 190 ``mread ^var_old (RR R12)`` |-> ``^vals (MREG2REG R12)``, 191 ``mread ^var_old (RR R13)`` |-> ``^vals (MREG2REG R13)``, 192 ``mread ^var_old (RR R14)`` |-> ``^vals (MREG2REG R14)``]; 193 194 val body_rel = replace (el 2 vars) body_rel 195 val body_list = strip_conj body_rel; 196 val x = mk_var ("x", Type `:word4`); 197 fun extract_oregs_f [] = (uregs_input, mk_comb(vals,x)) | 198 extract_oregs_f (t::l) = 199 let 200 val (oregs, f) = extract_oregs_f l; 201 val (ls', rs') = dest_eq t; 202 val oreg = rand (rand ls'); 203 204 val oregs = listSyntax.mk_cons(oreg, oregs); 205 val f = mk_cond (mk_eq (x, ``MREG2REG ^oreg``), rs', f) 206 in 207 (oregs, f) 208 end; 209 val (oregs, f) = extract_oregs_f body_list 210 211 val f = rhs (concl (REWRITE_CONV [MREG2REG_def, ILTheory.index_of_reg_def] f)); 212 val f = mk_abs (vals, (mk_abs (x, f))) 213 214 val oregs_words_thm = REWRITE_CONV [MAP, MREG2REG_def, ILTheory.index_of_reg_def] (``MAP MREG2REG ^oregs``); 215 val oregs_words = rhs (concl oregs_words_thm); 216 val uregs_words_thm = REWRITE_CONV [MAP, MREG2REG_def, ILTheory.index_of_reg_def] (``MAP MREG2REG ^uregs``); 217 val uregs_words = rhs (concl uregs_words_thm); 218 219 val oregs_uregs_distinct = (SIMP_CONV list_ss [DISJ_IMP_THM, ILTheory.MREG_distinct] ``(!x. MEM x ^oregs ==> ~MEM x ^uregs)``) 220 221 222 val regs_list = ``[(0w:word4,rv0:word32); (1w,rv1); (2w,rv2); (3w,rv3); (4w,rv4); (5w,rv5); 223 (6w,rv6); (7w,rv7); (8w,rv8); (9w,rv9); (10w,rv10); (11w,rv11); 224 (12w,rv12); (13w,rv13); (14w,rv14)]``; 225 226 val f_thm = GEN_ALL (SIMP_CONV std_ss [LIST_TO_FUN_def, preARMTheory.word4_distinct] ``^f (LIST_TO_FUN 0w ^regs_list)``) 227 228 229 val input_regs_list_thm = GEN_ALL ( 230 FILTER_CONV (REWRITE_CONV [MEM, preARMTheory.word4_distinct]) 231 ``FILTER (\x. ~MEM (FST x) ^uregs_words) ^regs_list``) 232 val input_regs_list = rhs (concl (SPEC_ALL input_regs_list_thm)) 233 234 val fe_var = mk_var ("fe", Type `:word4 -> word32`); 235 val output_regs_list_term = ``(FILTER (\x. MEM (FST x) ^oregs_words) 236 (MAP (\(r,v). (r, ^fe_var r)) ^regs_list))`` 237 val output_regs_thm1 = 238 ((SIMP_CONV std_ss [MAP]) THENC (FILTER_CONV (REWRITE_CONV [MEM, preARMTheory.word4_distinct]))) output_regs_list_term 239 val output_regs_thm2 = 240 SPEC ``^f (LIST_TO_FUN 0w ^regs_list)`` ( 241 GEN fe_var output_regs_thm1 242 ) 243 val output_regs_thm = SIMP_RULE std_ss [f_thm, preARMTheory.word4_distinct] output_regs_thm2 244 245 246 val unknown_changed_regs_list_thm = GEN_ALL ( 247 ((SIMP_CONV std_ss [MAP]) THENC (FILTER_CONV (REWRITE_CONV [MEM, preARMTheory.word4_distinct]))) 248 ``FILTER (\x. ~MEM x ^oregs_words) (MAP FST ^input_regs_list)``) 249 250 val f_depend_term = ``!f1 f2. 251 (!q. MEM q ^input_regs_list ==> (f1 (FST q) = f2 (FST q))) ==> 252 !r. MEM r ^oregs_words ==> (^f f1 r = ^f f2 r)`` 253 val f_depend_thm = GEN_ALL (SIMP_RULE std_ss [] ( 254 SIMP_CONV list_ss [DISJ_IMP_THM, FORALL_AND_THM, preARMTheory.word4_distinct] f_depend_term)) 255 256 val f_spec_term = ``!st r. 257 MEM r ^oregs_words ==> 258 (state2reg_fun (run_ir ^ir st) r = ^f (state2reg_fun st) r)`` 259 260 val f_spec_thm = prove (f_spec_term, (*set_goal ([], f_spec_term)*) 261 SIMP_TAC list_ss [DISJ_IMP_THM, state2reg_fun2mread2, preARMTheory.word4_distinct] THEN 262 WORDS_TAC THEN 263 MP_TAC unchanged_thm THEN 264 SIMP_TAC std_ss [ILTheory.from_reg_index_def, ILTheory.UNCHANGED_def, 265 GSYM rulesTheory.mread_def] THEN 266 REWRITE_TAC[MEM] THEN 267 METIS_TAC[spec, FST, SND, PAIR_EQ]) 268 269 270 271 val (_, ir_thm, mem_thm, wf_thm2) = translate_ir ir; 272 val thm = TRANSLATION_SPEC_SEP_thm; 273 val thm2 = SPECL [ir, uregs, oregs, f] thm 274 val thm3 = REWRITE_RULE [wf, ir_thm, mem_thm, wf_thm2, spec, r_unchanged_thm, 275 uregs_words_thm, oregs_words_thm, oregs_uregs_distinct] thm2 276 val thm4 = SIMP_RULE std_ss [input_regs_list_thm, f_thm, output_regs_thm, 277 unknown_changed_regs_list_thm, f_spec_thm] thm3 278 val thm5 = REWRITE_RULE [f_depend_thm, Once (prove (``!X. (MAP enc X) = (unint (MAP enc X))``, SIMP_TAC std_ss [unint_def]))] thm4 279 val thm6 = SIMP_RULE list_ss [LENGTH, dimindex_24, reg_spec_def, FOLDR, 280 spec_list_def, emp_STAR, xM_list_def, rest_list_def, xR_list_def, 281 GSYM (SIMP_RULE std_ss [STAR_SYM] SEP_EXISTS_ABSORB_STAR), 282 Cong (REFL ``unint X``) 283 ] thm5 284 val thm7 = REWRITE_RULE [unint_def] thm6 285 val thm8 = post_process_sep thm7 286 in 287 thm8 288 end 289