1structure prog_armLib :> prog_armLib = 2struct 3 4open HolKernel boolLib bossLib; 5open wordsLib stringLib addressTheory pred_setTheory combinTheory; 6open set_sepTheory prog_armTheory helperLib wordsTheory progTheory finite_mapTheory; 7 8open armLib; 9 10infix \\ 11val op \\ = op THEN; 12 13val use_stack = ref false; 14fun arm_use_stack b = (use_stack := b); 15 16val arm_enc = armLib.arm_encode_from_string; 17 18local val arm_memory_pred = ref "auto" 19in 20 fun get_arm_memory_pred () = !arm_memory_pred; 21 fun set_arm_memory_pred s = 22 if mem s ["auto","aM1","aM","aBYTE_MEMORY","aMEM"] 23 then (arm_memory_pred := s) else fail(); 24end; 25 26val arm_status = aS_HIDE; 27val arm_pc = ``aPC``; 28 29fun process tm = let 30 fun replace_plus c = if c = #"+" then #"_" else c; 31 fun name_of_tm tm = 32 "m_" ^ (implode o filter is_normal_char o map replace_plus o explode o term_to_string) tm; 33 in if type_of tm = ``:word4`` then let 34 val f = int_to_string o numSyntax.int_of_term o snd o dest_comb 35 in (mk_comb(``aR``,tm),mk_var("r" ^ f tm,``:word32``)) end 36 else if tm = ``psrN:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrn",``:bool``)) 37 else if tm = ``psrZ:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrz",``:bool``)) 38 else if tm = ``psrC:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrc",``:bool``)) 39 else if tm = ``psrV:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrv",``:bool``)) 40 else if tm = ``psrQ:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrq",``:bool``)) 41 else if type_of tm = ``:word32`` then 42 (mk_comb(``aM1:word32 -> word8 -> arm_set -> bool``,tm),mk_var(name_of_tm tm,``:word8``)) 43 else fail() end; 44 45val state = ``s:arm_state`` 46val r15 = mk_var("r15",``:word32``) 47 48fun rewrite_names tm = let 49 fun aux v = let val m = match_term tm (car (car v)) in (snd o process o cdr o car) v end 50 in replace_terml aux end; 51 52fun arm_pre_post s g = let 53 val cpsr_var = mk_var("cpsr",``:word32``) 54 val g = subst [``ARM_READ_MASKED_CPSR s``|->cpsr_var] g 55 val regs = collect_term_of_type ``:word4`` g 56 val regs = filter wordsSyntax.is_n2w regs 57 val bits = collect_term_of_type ``:arm_bit`` g 58 val h = rewrite_names ``ARM_READ_STATUS`` (rewrite_names ``ARM_READ_REG`` g) 59 val mems1 = find_terml (can (match_term ``ARM_READ_MEM a ^state``)) h 60 val mems2 = find_terms (can (match_term ``ARM_WRITE_MEM a x ^state``)) h 61 val mems = map (cdr o car) mems1 @ map (cdr o car o car) mems2 62 val mems = filter (fn x => not (mem x [``r15 + 3w:word32``, 63 ``r15 + 2w:word32``,``r15 + 1w:word32``,r15])) mems 64 val h2 = rewrite_names ``ARM_READ_MEM`` h 65 val reg_assign = find_terml_all (can (match_term ``ARM_WRITE_REG r x ^state``)) h2 66 val mem_assign = find_terml_all (can (match_term ``ARM_WRITE_MEM a x ^state``)) h2 67 val sts_assign = find_terml_all (can (match_term ``ARM_WRITE_STATUS f x ^state``)) h2 68 val assignments = map (fn x => (cdr (car (car x)),cdr (car x))) reg_assign 69 val assignments = map (fn x => (cdr (car (car x)),cdr (car x))) mem_assign @ assignments 70 val assignments = map (fn x => (cdr (car (car x)),cdr (car x))) sts_assign @ assignments 71 fun all_distinct [] = [] 72 | all_distinct (x::xs) = x :: filter (fn y => not (x = y)) (all_distinct xs) 73 val mems = rev (all_distinct mems) 74 val code = subst [mk_var("c",``:num``) |-> 75 numSyntax.mk_numeral(Arbnum.fromHexString s)] 76 ``(r15:word32,(n2w (c:num)):word32)`` 77 fun is_pc_relative tm = mem (mk_var("r15",``:word32``)) (free_vars tm) 78 val mems_pc_rel = filter is_pc_relative mems 79 val has_read_from_mem = (mems_pc_rel = mems) andalso (length mems = 4) 80 val (mems,assignments,code) = 81 if not has_read_from_mem then 82 (mems,assignments,subst [mk_var("x",``:word32#word32``)|->code] ``{x:word32#word32}``) 83 else let 84 val xx = find_term wordsSyntax.is_word_concat h2 85 val v = mk_var("pc_rel",``:word32``) 86 val addr = (cdr o fst o process o hd) mems 87 val assignments = map (fn (x,y) => (x,subst [xx |-> v]y)) assignments 88 val code = subst [mk_var("x",``:word32#word32``)|->code, 89 mk_var("y",``:word32#word32``)|->pairSyntax.mk_pair(addr,v)] 90 ``{(x:word32#word32);y}`` 91 in ([],assignments,code) end 92 fun get_assigned_value_aux x y [] = y 93 | get_assigned_value_aux x y ((q,z)::zs) = 94 if x = q then z else get_assigned_value_aux x y zs 95 fun get_assigned_value x y = get_assigned_value_aux x y assignments 96 fun mk_pre_post_assertion x = let 97 val (y,z) = process x 98 val q = get_assigned_value x z 99 in (mk_comb(y,z),mk_comb(y,q)) end 100 val pre_post = map mk_pre_post_assertion (regs @ bits @ mems) 101 val pre = list_mk_star (map fst pre_post) ((type_of o fst o hd) pre_post) 102 val post = list_mk_star (map snd pre_post) ((type_of o fst o hd) pre_post) 103 val (pre,post) = if not (mem cpsr_var (free_vars g)) then (pre,post) else let 104 val res = (fst o dest_eq o concl o SPEC cpsr_var) aCPSR_def 105 in (mk_star(pre,res),mk_star(post,res)) end 106 fun match_any [] tm = fail () 107 | match_any (x::xs) tm = match_term x tm handle HOL_ERR _ => match_any xs tm 108 fun pass tm = let 109 val (s,i) = match_any [``ARM_OK s``, 110 ``ALIGNED r15``, 111 ``ARM_READ_MEM (r15 + 3w) s = n2w n``, 112 ``ARM_READ_MEM (r15 + 2w) s = n2w n``, 113 ``ARM_READ_MEM (r15 + 1w) s = n2w n``, 114 ``ARM_READ_MEM (r15 + 0w) s = n2w n``, 115 ``ARM_READ_MEM r15 s = n2w n``] tm 116 in not (subst s r15 = r15) end handle HOL_ERR _ => true 117 val pre_conds = (filter pass o list_dest dest_conj o fst o dest_imp) h 118 val pre_conds = filter (not o can (find_term (fn x => x = ``ARM_READ_MEM``))) pre_conds 119 val pre_conds = filter (fn x => not (is_neg x andalso is_eq (cdr x) andalso mem r15 (free_vars x))) pre_conds 120 fun all_bool tm = (filter (fn x => not (type_of x = ``:bool``)) (free_vars tm)) = [] 121 val bools = filter all_bool pre_conds 122 val pre_conds = if bools = [] then pre_conds else let 123 val pre_bool = (fst o dest_eq o concl o SPEC (list_mk_conj bools)) markerTheory.Abbrev_def 124 in pre_bool :: filter (not o all_bool) pre_conds end 125 val pc_post = snd (hd (filter (fn x => (fst x = ``15w:word4``)) assignments)) 126 val pc = mk_var("r15",``:word32``) 127 val pre_conds = if mem pc (free_vars pc_post) then pre_conds else mk_comb(``ALIGNED``,pc_post) :: pre_conds 128 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``CONTAINER``,list_mk_conj pre_conds)) 129 val ss = subst [``aR 15w``|->``aPC``,pc|->``p:word32``] 130 in (ss pre,ss code,ss post) end; 131 132fun remove_primes th = let 133 fun last s = substring(s,size s-1,1) 134 fun delete_last_prime s = if last s = "'" then substring(s,0,size(s)-1) else fail() 135 fun foo [] ys i = i 136 | foo (x::xs) ys i = let 137 val name = (fst o dest_var) x 138 val new_name = repeat delete_last_prime name 139 in if name = new_name then foo xs (x::ys) i else let 140 val new_var = mk_var(new_name,type_of x) 141 in foo xs (new_var::ys) ((x |-> new_var) :: i) end end 142 val i = foo (free_varsl (concl th :: hyp th)) [] [] 143 in INST i th end 144 145val SING_SUBSET = prove( 146 ``!x:'a y. {x} SUBSET y = x IN y``, 147 REWRITE_TAC [INSERT_SUBSET,EMPTY_SUBSET]); 148 149fun introduce_aBYTE_MEMORY th = if 150 not (can (find_term (can (match_term ``aM1``))) (concl th)) 151 then th else let 152 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 153 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 154 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 155 val (_,p,_,q) = dest_spec(concl th) 156 val xs = (rev o list_dest dest_star) p 157 val tm = (fst o dest_eq o concl o SPEC_ALL) aM1_def 158 val xs = filter (can (match_term tm)) xs 159 fun foo tm = cdr tm |-> mk_comb(mk_var("f",``:word32->word8``),(cdr o car) tm) 160 val th = INST (map foo xs) th 161 in if xs = [] then th else let 162 val (_,p,_,q) = dest_spec(concl th) 163 val xs = (rev o list_dest dest_star) p 164 val tm = (fst o dest_eq o concl o SPEC_ALL) aM1_def 165 val xs = filter (can (match_term tm)) xs 166 val ys = (map (cdr o car) xs) 167 fun foo [] = mk_var("df",``:word32 set``) 168 | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v) 169 val frame = mk_comb(mk_comb(``aBYTE_MEMORY``,foo ys),mk_var("f",``:word32->word8``)) 170 val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th) 171 val th = RW [GSYM STAR_ASSOC] th 172 val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) aBYTE_MEMORY_INSERT 173 fun compact th = let 174 val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th) 175 val rw = (INST (fst (match_term fff x)) o SPEC_ALL o GSYM) aBYTE_MEMORY_INSERT 176 val th = DISCH ((fst o dest_imp o concl) rw) th 177 val th = SIMP_RULE bool_ss [GSYM aBYTE_MEMORY_INSERT] th 178 in th end 179 val th = repeat compact th 180 val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th 181 val th = RW [APPLY_UPDATE_ID] th 182 (* val te = (cdr o car o find_term (can (match_term (cdr fff))) o concl) th 183 val t1 = repeat (snd o pred_setSyntax.dest_insert) te 184 val t2 = repeat (fst o pred_setSyntax.dest_delete) t1 185 val th = SIMP_RULE bool_ss [] (DISCH (mk_eq(te,t2)) th) 186 val th = RW [AND_IMP_INTRO] th *) 187 val v = hd (filter (is_var) ys @ ys) 188 fun ss [] = ``{}:word32 set`` 189 | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs) 190 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word32 set``)) 191 val u2 = u1 192 val u3 = (fst o dest_imp o concl) th 193 val goal = mk_imp(u2,u3) 194 val imp = prove(goal, 195 ONCE_REWRITE_TAC [ALIGNED_MOD_4] 196 THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO] 197 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 198 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 199 THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET] 200 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 201 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 202 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC 203 THEN ASM_SIMP_TAC std_ss [] 204 THEN CCONTR_TAC 205 THEN FULL_SIMP_TAC std_ss [] 206 THEN FULL_SIMP_TAC std_ss []) 207 val th = DISCH_ALL (MATCH_MP th (UNDISCH imp)) 208 val th = RW [GSYM progTheory.SPEC_MOVE_COND] th 209 val th = remove_primes th 210 val th = REWRITE_RULE [SING_SUBSET] th 211 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 212 in th end end 213 214fun introduce_aM th = let 215 val index = ref 0 216 fun next_var () = (index := (!index)+1; mk_var("w" ^ int_to_string (!index),``:word32``)) 217 val lemma = (el 2 o CONJUNCTS o SPEC_ALL) bit_listTheory.bytes2word_thm 218 val f = SIMP_RULE std_ss [WORD_ADD_0] o 219 SIMP_RULE std_ss [word_arith_lemma3,word_arith_lemma4] o 220 SIMP_RULE std_ss [word_arith_lemma1,word_arith_lemma2] 221 val th = f th 222 fun foo th = let 223 val tm = (fst o dest_eq o concl o SPEC (next_var()) o GEN_ALL) lemma 224 val tm2 = find_term (fn t => car t = car tm handle HOL_ERR _ => false) (concl th) 225 in RW [lemma] (INST (fst (match_term tm2 tm)) th) end 226 fun hoo th = let 227 val (_,p,_,_) = dest_spec(concl th) 228 fun is_aM1 tm = (``aM1`` = repeat car tm) 229 val xs = (filter is_aM1 o list_dest dest_star) p 230 val _ = if length xs < 4 then fail() else () 231 val th = RW [f (SPEC ((cdr o car o hd) xs) aM_INTRO),bit_listTheory.bytes2word_INTRO] th 232 in repeat foo th end 233 in repeat hoo th end; 234 235fun introduce_aMEMORY th = if 236 not (can (find_term (can (match_term ``aM``))) (concl th)) 237 then th else let 238 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 239 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 240 val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th 241 val (_,p,_,q) = dest_spec(concl th) 242 val xs = (rev o list_dest dest_star) p 243 val tm = (fst o dest_eq o concl o SPEC_ALL) aM_def 244 val xs = filter (can (match_term tm)) xs 245 fun foo tm = cdr tm |-> mk_comb(mk_var("f",``:word32->word32``),(cdr o car) tm) 246 val th = INST (map foo xs) th 247 in if xs = [] then th else let 248 val (_,p,_,q) = dest_spec(concl th) 249 val xs = (rev o list_dest dest_star) p 250 val tm = (fst o dest_eq o concl o SPEC_ALL) aM_def 251 val xs = filter (can (match_term tm)) xs 252 val ys = (map (cdr o car) xs) 253 fun foo [] = mk_var("df",``:word32 set``) 254 | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v) 255 val frame = mk_comb(mk_comb(``aMEMORY``,foo ys),mk_var("f",``:word32->word32``)) 256 val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th) 257 val th = RW [GSYM STAR_ASSOC] th 258 val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL) aMEMORY_INSERT 259 fun compact th = let 260 val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th) 261 val rw = (INST (fst (match_term fff x)) o SPEC_ALL) aMEMORY_INSERT 262 val th = DISCH ((fst o dest_imp o concl) rw) th 263 val th = SIMP_RULE bool_ss [aMEMORY_INSERT] th 264 in th end 265 val th = repeat compact th 266 val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th 267 val th = RW [APPLY_UPDATE_ID] th 268 val te = (cdr o car o find_term (can (match_term (cdr fff))) o concl) th 269 val t1 = repeat (snd o pred_setSyntax.dest_insert) te 270 val t2 = repeat (fst o pred_setSyntax.dest_delete) t1 271 val th = SIMP_RULE bool_ss [] (DISCH (mk_eq(te,t2)) th) 272 val th = RW [AND_IMP_INTRO] th 273 val v = hd (filter (is_var) ys @ ys) 274 fun ss [] = ``{}:word32 set`` 275 | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs) 276 val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word32 set``)) 277 val u2 = mk_conj(mk_comb(``ALIGNED``,v),u1) 278 val u3 = (fst o dest_imp o concl) th 279 val goal = mk_imp(u2,u3) 280 val imp = prove(goal, 281 ONCE_REWRITE_TAC [ALIGNED_MOD_4] 282 THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO] 283 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 284 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 285 THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET] 286 THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def] 287 THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w] 288 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC 289 THEN ASM_SIMP_TAC std_ss [] 290 THEN CCONTR_TAC 291 THEN FULL_SIMP_TAC std_ss [] 292 THEN FULL_SIMP_TAC std_ss []) 293 val th = DISCH_ALL (MATCH_MP th (UNDISCH imp)) 294 val th = RW [GSYM progTheory.SPEC_MOVE_COND] th 295 val th = remove_primes th 296 val th = REWRITE_RULE [SING_SUBSET] th 297 val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th 298 in th end end 299 300(* 301val th1 = th 302val th = th1 303*) 304 305val introduce_aMEM_lemma = 306 Q.GEN `x` (CONJ (Q.SPEC `x` WRITE32_THM) (Q.SPEC `x` (GSYM READ32_def))); 307val introduce_aMEM_pattern = aBYTE_MEMORY_def |> SPEC_ALL |> concl |> dest_eq |> fst; 308val introduce_aMEM_pattern2 = ``(w:word8 @@ v:word24):word32`` 309fun introduce_aMEM_aux th = let 310 val th = Q.INST [`df`|->`FDOM (m:word32 |-> word8)`,`f`|->`\x. m ' x`] th 311 val xs = map cdr (find_terms (can (match_term ``ALIGNED w``)) (concl th)) 312 val xs = map (fn x => (cdr o cdr o cdr o cdr) x handle HOL_ERR _ => ``0w:word32``) 313 (find_terms (can (match_term introduce_aMEM_pattern2)) (concl th)) @ xs 314 fun foo tm = (cdr o car o car o cdr o cdr o cdr) tm :: 315 foo ((cdr o cdr o cdr o cdr) tm) handle HOL_ERR _ => [] 316 val xs = foo (find_term (can (match_term ``(a:word32 =+ w:word8) f``)) (concl th)) @ xs 317 handle HOL_ERR _ => xs 318 val lemma = LIST_CONJ 319 (map (fn x => SIMP_RULE std_ss [word_arith_lemma1,word_arith_lemma3,word_arith_lemma4] (SPEC x introduce_aMEM_lemma)) xs) 320 handle HOL_ERR _ => TRUTH 321 val th = SIMP_RULE std_ss [GSYM aMEM_def,lemma] th 322 val th = SIMP_RULE std_ss [aMEM_WRITE_BYTE] th 323 val (_,_,_,q) = dest_spec (concl th) 324 in if not (can (find_term (can (match_term introduce_aMEM_pattern))) q) then 325 th else let 326 val tm = find_term (can (match_term introduce_aMEM_pattern)) q 327 val tm2 = tm |> cdr |> dest_abs |> snd |> car |> cdr 328 val goal = mk_eq(tm,cdr(car(concl (SPEC tm2 aMEM_def)))) 329 val assum = th |> SIMP_RULE std_ss [SPEC_MOVE_COND] |> concl |> dest_imp |> fst 330 val lemma = prove(mk_imp(assum,goal), 331 REPEAT STRIP_TAC THEN REWRITE_TAC [aMEM_def] 332 THEN AP_THM_TAC THEN AP_TERM_TAC 333 THEN FULL_SIMP_TAC std_ss [INSERT_SUBSET,WRITE32_def,FDOM_FUPDATE,EXTENSION] 334 THEN FULL_SIMP_TAC std_ss [word_arith_lemma1,word_arith_lemma3,word_arith_lemma4] 335 THEN FULL_SIMP_TAC std_ss [IN_INSERT] 336 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC 337 THEN FULL_SIMP_TAC std_ss [WORD_ADD_0] 338 THEN CCONTR_TAC THEN FULL_SIMP_TAC std_ss []) 339 val th = SIMP_RULE std_ss [SPEC_MOVE_COND] th 340 val lemma = UNDISCH lemma 341 val tt = lemma |> concl |> dest_eq |> fst 342 val th = CONV_RULE (DEPTH_CONV (fn tm => if tm = tt then lemma else NO_CONV tm)) (UNDISCH th) 343 val th = SIMP_RULE std_ss [GSYM SPEC_MOVE_COND] (DISCH_ALL th) 344 in th end end; 345 346fun collect_READ32_WRITE32 th = let 347 val xs = map cdr (find_terms (can (match_term ``ALIGNED w``)) (concl th)) 348 val xs = map (fn x => (cdr o cdr o cdr o cdr) x handle HOL_ERR _ => ``0w:word32``) 349 (find_terms (can (match_term introduce_aMEM_pattern2)) (concl th)) @ xs 350 fun foo tm = (cdr o car o car o cdr o cdr o cdr) tm :: 351 foo ((cdr o cdr o cdr o cdr) tm) handle HOL_ERR _ => [] 352 val xs = foo (find_term (can (match_term ``(a:word32 =+ w:word8) f``)) (concl th)) @ xs 353 handle HOL_ERR _ => xs 354 val lemma = LIST_CONJ 355 (map (fn x => SIMP_RULE std_ss [word_arith_lemma1,word_arith_lemma3,word_arith_lemma4] (SPEC x introduce_aMEM_lemma)) xs) 356 handle HOL_ERR _ => TRUTH 357 val th = RW [lemma] th 358 in th end 359 360fun introduce_aMEM th = let 361 val th = introduce_aBYTE_MEMORY th 362 val th = collect_READ32_WRITE32 th 363 val th = Q.INST [`df`|->`dm`,`f`|->`m`] th 364 val th = RW1 [GSYM WRITE8_def] th 365 val m = mk_var("m",``:word32->word8``) 366 fun READ8_CONV tm = 367 if rator tm = m then REWR_CONV (GSYM READ8_def) tm else NO_CONV tm 368 val th = CONV_RULE (DEPTH_CONV READ8_CONV) th 369 (* val th = introduce_aMEM_aux th 370 val _ = not (can (find_term (fn tm => tm = ``aBYTE_MEMORY``)) (concl th)) orelse fail() *) 371 in th end 372 373fun introduce_aSTACK th = 374 if not (!use_stack) then th else th (* let 375 val (_,p,c,q) = dest_spec(concl th) 376 val sp = mk_var("r13",``:word32``) 377 fun access_sp tm = (tm = sp) orelse 378 (can (match_term ``(v:word32) - n2w n``) tm andalso (sp = (cdr o car) tm)) 379 val tm1 = find_terms (fn tm => 380 can (match_term ``aM x y``) tm andalso (access_sp o cdr o car) tm) p 381 val tm2 = find_terms (fn tm => 382 can (match_term ``aM x y``) tm andalso (access_sp o cdr o car) tm) q 383 val tm = cdr (find_term (can (match_term ``aR 13w w``)) q) 384 fun genlist 0 f = [] 385 | genlist n f = f n :: genlist (n-1) f 386 val (stack_pre,stack_post) = 387 if wordsSyntax.is_word_sub tm then (* this is a push *) let 388 val n = numSyntax.int_of_term (cdr (cdr tm)) div 4 389 val pre = subst [``n:num``|->numSyntax.term_of_int n] ``aSTACK bp (l+n,ss)`` 390 val post = ``aSTACK bp (l,ss ++ xs)`` 391 else if wordsSyntax.is_word_add tm then (* this is a pop *) let 392 val n = numSyntax.int_of_term (cdr (cdr tm)) div 4 393 else fail() 394 val tm2 = find_term (can (match_term (mk_comb(car tm1,genvar(``:word32``))))) q 395 val c1 = MOVE_OUT_CONV ``aR 11w`` THENC MOVE_OUT_CONV (car tm1) 396 val c2 = MOVE_OUT_CONV ``aR 11w`` THENC MOVE_OUT_CONV (car tm2) 397 val th = CONV_RULE (POST_CONV c2 THENC PRE_CONV c1) th 398 val th = DISCH ``ALIGNED r11`` th 399 val th = SIMP_RULE bool_ss [ALIGNED,SEP_CLAUSES] th 400 val th = MATCH_MP aSTACK_INTRO th handle HOL_ERR e => 401 MATCH_MP (RW [WORD_SUB_RZERO] (Q.INST [`n`|->`0`] aSTACK_INTRO)) th 402 fun mk_stack_var i = mk_var("s" ^ int_to_string i,``:word32``) 403 val index = (Arbnum.toInt o numSyntax.dest_numeral o cdr o cdr o cdr o car) tm1 404 handle HOL_ERR _ => 0 405 val index = index div 4 406 fun mk_slist i = if i = 0 then ``[]:word32 list`` else 407 listSyntax.mk_cons(mk_stack_var (index - i), mk_slist (i-1)) 408 val th = SPECL [mk_slist index,mk_var("ss",``:word32 list``)] th 409 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [listTheory.LENGTH]) THENC 410 REWRITE_CONV [listTheory.APPEND]) th 411 val th = INST [cdr tm1 |-> mk_stack_var index] th 412 in th end handle HOL_ERR _ => th *); 413 414fun calculate_length_and_jump th = 415 let val (_,_,_,q) = dest_spec(concl th) in 416 let val v = find_term (fn t => t = ``aPC (p + 4w)``) q in (th,4,SOME 4) end 417 handle e => 418 let val v = find_term (can (match_term ``aPC (p + n2w n)``)) q 419 in (th,4,SOME (0 + (numSyntax.int_of_term o cdr o cdr o cdr) v)) end 420 handle e => 421 let val v = find_term (can (match_term ``aPC (p - n2w n)``)) q 422 in (th,4,SOME (0 - (numSyntax.int_of_term o cdr o cdr o cdr) v)) end 423 handle e => (th,4,NONE) end 424 425val sp_var = mk_var("r13",``:word32``); 426val has_stack_access_pattern = aM1_def |> SPEC_ALL |> concl |> dest_eq |> fst 427fun has_stack_access th = let 428 val xs = find_terms (can (match_term has_stack_access_pattern)) (concl th) 429 in exists (mem sp_var o free_vars) xs end; 430 431fun post_process_thm th = let 432 val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [wordsTheory.word_mul_n2w] th 433 val th = CONV_RULE FIX_WORD32_ARITH_CONV th 434 val th = if mem (get_arm_memory_pred()) ["auto","aM"] then introduce_aM th else th 435 val th = introduce_aSTACK th 436 val th = if mem (get_arm_memory_pred()) ["auto","aBYTE_MEMORY"] 437 then introduce_aBYTE_MEMORY th else th 438 val th = if not (get_arm_memory_pred() = "aMEM") then th else 439 if has_stack_access th then (introduce_aM th) 440 else introduce_aMEM th 441 val th = if get_arm_memory_pred() = "auto" then introduce_aMEMORY th else th 442 val th = RW [WORD_EQ_XOR_ZERO,wordsTheory.WORD_EQ_SUB_ZERO,ALIGNED_def, 443 WORD_TIMES2,WORD_SUB_INTRO] th 444 in calculate_length_and_jump th end; 445 446val pc_rel = mk_var("pc_rel",``:word32``) 447fun FIX_PC_REL_CONV tm = 448 if is_eq tm andalso mem pc_rel (free_vars (cdr tm)) then SYM_CONV tm else ALL_CONV tm 449fun RESTORE_FIX_PC_REL_CONV tm = 450 if is_eq tm andalso mem pc_rel (free_vars (car tm)) then SYM_CONV tm else ALL_CONV tm 451 452fun arm_prove_one_spec s th = let 453 val g = concl th 454 val next = cdr (find_term (can (match_term ``ARM_NEXT x s = s'``)) g) 455 val (pre,code,post) = arm_pre_post s g 456 val tm = ``SPEC ARM_MODEL pre code post`` 457 val tm = subst [mk_var("pre",type_of pre) |-> pre, 458 mk_var("post",type_of post) |-> post, 459 mk_var("code",type_of code) |-> code] tm 460 val FLIP_TAC = CONV_TAC (ONCE_REWRITE_CONV [EQ_SYM_EQ]) 461(* 462 set_goal([],tm) 463*) 464 val result = prove(tm, 465 MATCH_MP_TAC IMP_ARM_SPEC \\ REPEAT STRIP_TAC \\ EXISTS_TAC (cdr next) 466 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 467 STAR_arm2set, CODE_POOL_arm2set, aPC_def, IN_DELETE, 468 APPLY_UPDATE_THM, GSYM ALIGNED_def, wordsTheory.n2w_11,WORD_ADD_0, 469 arm_stepTheory.arm_bit_distinct, Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, 470 INSERT_SUBSET, EMPTY_SUBSET, ARM_READ_WRITE, GSYM ADDR30_def] 471 \\ NTAC 3 (FLIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]) 472 \\ FLIP_TAC \\ REWRITE_TAC [AND_IMP_INTRO, GSYM CONJ_ASSOC] 473 \\ SIMP_TAC std_ss [] \\ FLIP_TAC \\ STRIP_TAC \\ STRIP_TAC 474 THEN1 (SIMP_TAC std_ss [ALIGNED_def] \\ FLIP_TAC 475 \\ REPEAT (Q.PAT_X_ASSUM `xxx = ARM_READ_MEM x s` MP_TAC) 476 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 477 \\ REPEAT (Q.PAT_X_ASSUM `ARM_READ_REG x s = xxx` (fn th => ONCE_REWRITE_TAC [GSYM th] THEN MP_TAC th)) 478 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC th 479 \\ FULL_SIMP_TAC std_ss [ALIGNED_def,ARM_READ_UNDEF_def, 480 markerTheory.Abbrev_def,CONTAINER_def,aligned4_thm,WORD_ADD_0] 481 \\ REPEAT (POP_ASSUM MP_TAC) \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 482 \\ SIMP_TAC std_ss [BYTES_TO_WORD_LEMMA] \\ REPEAT STRIP_TAC \\ EVAL_TAC) 483 \\ ASM_SIMP_TAC std_ss [UPDATE_arm2set'',ALIGNED_CLAUSES, 484 ARM_WRITE_STS_INTRO,ARM_READ_WRITE] 485 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 486 \\ ASM_SIMP_TAC std_ss [wordsTheory.WORD_ADD_0,ARM_READ_WRITE] 487 \\ FULL_SIMP_TAC bool_ss [markerTheory.Abbrev_def,CONTAINER_def] 488 \\ REPEAT (POP_ASSUM (MP_TAC o GSYM)) \\ ASM_SIMP_TAC std_ss [] 489 \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,BYTES_TO_WORD_LEMMA]) 490 in RW [STAR_ASSOC,CONTAINER_def] result end; 491 492val cond_STAR_cond = prove( 493 ``!x y. cond (x /\ y) = cond x * (cond y):'a set -> bool``, 494 SIMP_TAC (std_ss) [SEP_CLAUSES]); 495 496val precond_INTRO = prove( 497 ``!x. cond (Abbrev x) = precond x:'a set -> bool``, 498 SIMP_TAC (std_ss) [SEP_CLAUSES,precond_def,markerTheory.Abbrev_def]); 499 500val minus_one = EVAL ``-1w:word32`` 501val minus_one_mult = 502 REWRITE_CONV [GSYM minus_one,GSYM WORD_NEG_MUL,GSYM word_sub_def] 503 ``x + (0xFFFFFFFFw:word32) * y`` 504val minus_one_mult = CONJ (RW1 [WORD_ADD_COMM] minus_one_mult) minus_one_mult 505val minus_one_mult = CONJ (RW1 [WORD_MULT_COMM] minus_one_mult) minus_one_mult 506 507val ARM_WRITE_STATUS_T_IGNORE_UPDATE = prove( 508 ``(~ARM_READ_STATUS psrT s ==> (ARM_WRITE_STATUS psrT F s = s)) /\ 509 (ARM_WRITE_STATUS psrT b (ARM_WRITE_REG r w s) = 510 ARM_WRITE_REG r w (ARM_WRITE_STATUS psrT b s))``, 511 EVAL_TAC \\ SRW_TAC [] [FUN_EQ_THM,APPLY_UPDATE_THM, 512 arm_seq_monadTheory.arm_state_component_equality, 513 arm_coretypesTheory.ARMpsr_component_equality] \\ SRW_TAC [] [] 514 \\ ASM_SIMP_TAC std_ss []); 515 516val aligned_bx_lemma = prove( 517 ``!w:word32. aligned (w,4) ==> aligned_bx w /\ ~(w ' 0)``, 518 SIMP_TAC std_ss [aligned4_thm,ALIGNED_BITS,arm_stepTheory.aligned_bx_thm]); 519 520fun remove_aligned_bx th = let 521 val tm = cdr (find_term (can (match_term ``aligned_bx (w:word32)``)) (concl th)) 522 val imp = SPEC tm aligned_bx_lemma 523 val th = SIMP_RULE std_ss [imp] (DISCH ((fst o dest_imp o concl) imp) th) 524 val th = RW [AND_IMP_INTRO] th 525 val th = SIMP_RULE std_ss [ARM_WRITE_STATUS_T_IGNORE_UPDATE] th 526 in th end handle HOL_ERR _ => th; 527 528fun arm_prove_specs m_pred s = let 529 val (s,rename,_) = parse_renamer s 530 val _ = set_arm_memory_pred m_pred 531 val thms = [arm_step "v6" s] 532 val thms = (thms @ [arm_step "v6,fail" s]) handle HOL_ERR _ => thms 533 val thms = map (RW [minus_one,minus_one_mult]) thms 534 val th = hd thms 535 val ARM_READ_MASKED_CPSR = ARM_READ_MASKED_CPSR_def |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat car 536 fun derive_spec th = let 537 val th = SPEC state th 538 val th = RW [ADD_WITH_CARRY_SUB,pairTheory.FST,pairTheory.SND,ADD_WITH_CARRY_SUB_n2w] th 539 val th = SIMP_RULE std_ss [] th 540 val th = remove_aligned_bx th 541 val tm = (fst o dest_eq o concl o SPEC state) ARM_OK_def 542 val th = (RW [AND_IMP_INTRO] o RW [GSYM ARM_OK_def] o SIMP_RULE bool_ss [ARM_OK_def] o DISCH tm) th 543 val th = SIMP_RULE std_ss [aligned4_thm,aligned2_thm,ARM_READ_MASKED_CPSR_INTRO] th 544 val th = if not (can (find_term (fn x => x = ARM_READ_MASKED_CPSR)) (concl th)) then th else let 545 val th = SIMP_RULE std_ss [FCP_UPDATE_WORD_AND] th 546 val gg = SIMP_RULE (std_ss++SIZES_ss) [bitTheory.BIT_def,bitTheory.BITS_THM] o 547 RW1 [fcpTheory.FCP_APPLY_UPDATE_THM,word_index_n2w] 548 fun f th = let 549 val t2 = find_term (can (match_term ``(n :+ F) ((n2w k):word32)``)) (concl th) 550 in RW [EVAL t2] th end 551 in repeat f ((gg o gg o gg o gg o gg)th) end 552 val th = SIMP_RULE std_ss [word_arith_lemma1] th 553 val th = arm_prove_one_spec s th 554 in post_process_thm th end 555 val result = map derive_spec thms 556 in if length result < 2 then let 557 val (th1,i1,j1) = hd result 558 val th1 = REWRITE_RULE [markerTheory.Abbrev_def,SEP_CLAUSES] th1 559 in ((rename th1,i1,j1), NONE) end 560 else let 561 val (th1,i1,j1) = hd result 562 val (th2,i2,j2) = hd (tl result) 563 val th2 = PURE_REWRITE_RULE [GSYM precond_def,markerTheory.Abbrev_def] th2 564 val th1 = RW [cond_STAR_cond] th1 565 val th1 = RW [precond_INTRO] th1 566 val th1 = SIMP_RULE (std_ss++sep_cond_ss) [] th1 567 in ((rename th1,i1,j1), SOME (rename th2,i2,j2)) end end 568 569fun arm_jump tm1 tm2 jump_length forward = let 570 fun arm_mk_jump cond jump_length = let 571 val s = "b" ^ cond ^ (if forward then " +#" else " -#") ^ (int_to_string jump_length) 572 fun prefix_zero s = if length (explode s) < 8 then prefix_zero ("0"^s) else s 573 in prefix_zero (arm_enc s) end; 574 val (x,y) = if tm2 = ``aS1 psrN`` then ("mi","pl") else 575 if tm2 = ``aS1 psrZ`` then ("eq","ne") else 576 if tm2 = ``aS1 psrC`` then ("cs","cc") else 577 if tm2 = ``aS1 psrV`` then ("vs","vc") else ("","") 578 val z = if is_neg tm1 then y else x 579 val jump_length = if forward then jump_length + 4 else 0 - jump_length 580 in (arm_mk_jump z jump_length,4) end 581 582val arm_spec = cache (arm_prove_specs "auto"); 583val arm_spec_m = cache (arm_prove_specs "aM"); 584val arm_spec_m1 = cache (arm_prove_specs "aM1"); 585val arm_spec_mem = cache (arm_prove_specs "aMEM"); 586val arm_spec_byte_memory = cache (arm_prove_specs "aBYTE_MEMORY"); 587 588val arm_tools = (arm_spec, arm_jump, arm_status, arm_pc); 589val arm_tools_no_status = (arm_spec, arm_jump, TRUTH, arm_pc); 590val arm_tools_mem = (arm_spec_mem, arm_jump, arm_status, arm_pc); 591val arm_tools_byte = (arm_spec_byte_memory, arm_jump, arm_status, arm_pc); 592 593 594(* 595 596 val m_pred = "auto" 597 fun enc s = let val _ = print ("\n\n"^s^"\n\n") in arm_enc s end 598 599 val thms = arm_spec (enc "TST r5, #3"); 600 val thms = arm_spec (enc "ADD r1, #10"); 601 val thms = arm_spec (enc "CMP r1, #10"); 602 val thms = arm_spec (enc "TST r2, #6"); 603 val thms = arm_spec (enc "SUBCS r1, r1, #10"); 604 val thms = arm_spec (enc "MOV r0, #0"); 605 val thms = arm_spec (enc "CMP r1, #0"); 606 val thms = arm_spec (enc "ADDNE r0, r0, #1"); 607 val thms = arm_spec (enc "LDRNE r1, [r1]"); 608 val thms = arm_spec (enc "BNE -#12"); 609 val thms = arm_spec (enc "MOVGT r2, #5"); 610 val thms = arm_spec (enc "LDRBNE r2, [r3]"); 611 val thms = arm_spec (enc "BNE +#420"); 612 val thms = arm_spec (enc "LDRLS r2, [r11, #-40]"); 613 val thms = arm_spec (enc "SUBLS r2, r2, #1"); 614 val thms = arm_spec (enc "SUBLS r11, r11, #4"); 615 val thms = arm_spec (enc "MOVGT r12, r0"); 616 val thms = arm_spec (enc "ADD r0, pc, #16"); 617 val thms = arm_spec (enc "SUB r0, pc, #60"); 618 val thms = arm_spec (enc "SUBLS r2, r2, #1"); 619 val thms = arm_spec (enc "SUBLS r11, r11, #4"); 620 val thms = arm_spec (enc "LDRGT r0, [r11, #-44]"); 621 val thms = arm_spec (enc "MOVGT r1, r3"); 622 val thms = arm_spec (enc "MOVGT r12, r5"); 623 val thms = arm_spec (enc "MOVGT r1, r6"); 624 val thms = arm_spec (enc "MOVGT r0, r6"); 625 val thms = arm_spec (enc "ADD r5, pc, #4096"); 626 val thms = arm_spec (enc "ADD r6, pc, #4096"); 627 val thms = arm_spec (enc "STRB r2, [r3]"); 628 val thms = arm_spec (enc "STMIA r4, {r5-r10}"); 629 val thms = arm_spec (enc "LDMIA r4, {r5-r10}"); 630 val thms = arm_spec (enc "STRB r2, [r1], #1"); 631 val thms = arm_spec (enc "STRB r3, [r1], #1"); 632 val thms = arm_spec (enc "STMIB r8!, {r14}"); 633 val thms = arm_spec (enc "STMIB r8!, {r0, r14}"); 634 val thms = arm_spec (enc "LDR pc, [r8]"); 635 val thms = arm_spec (enc "LDRLS pc, [r8], #-4"); 636 val thms = arm_spec (enc "LDMIA sp!, {r0-r2, r15}"); 637 val thms = arm_spec (enc "LDR r0, [pc, #308]"); 638 val thms = arm_spec (enc "LDR r0, [pc, #4056]"); 639 val thms = arm_spec (enc "LDR r8, [pc, #3988]"); 640 val thms = arm_spec (enc "LDR r2, [pc, #3984]"); 641 val thms = arm_spec (enc "LDR r12, [pc, #3880]"); 642 val thms = arm_spec (enc "LDR r12, [pc, #3856]"); 643 val thms = arm_spec (enc "LDR r1, [pc, #1020]"); 644 val thms = arm_spec (enc "LDR r1, [pc, #-20]"); 645 val thms = arm_spec (enc "STMDB sp!, {r0-r2, r15}"); 646 val thms = arm_spec (enc "LDRB r2, [r3]"); 647 val thms = arm_spec (enc "STRB r2, [r3]"); 648 val thms = arm_spec (enc "SWPB r2, r4, [r3]"); 649 val thms = arm_spec (enc "LDR r2, [r3,#12]"); 650 val thms = arm_spec (enc "STR r2, [r3,#12]"); 651 val thms = arm_spec (enc "SWP r2, r4, [r3]"); 652 val thms = arm_spec (enc "LDMIB r4, {r5-r7}"); 653 val thms = arm_spec (enc "STMIA r4, {r5-r6}"); 654 val thms = arm_spec (enc "LDRH r2, [r3]"); 655 val thms = arm_spec (enc "STRH r2, [r3]"); 656 val thms = arm_spec (enc "MSR CPSR, r1"); 657 val thms = arm_spec (enc "MSR CPSR, #219"); 658 val thms = arm_spec (enc "MRS r1, CPSR"); 659 val thms = arm_spec (enc "LDR r0, [r11, #-8]"); 660 val thms = arm_spec (enc "LDR r0, [r11]"); 661 val thms = arm_spec (enc "STR r0, [r11, #-8]"); 662 val thms = arm_spec (enc "BX lr"); 663 664 val m_pred = "aMEM"; 665 val thms = arm_spec_mem (enc "SWP r0, r1, [r11]"); 666 val thms = arm_spec_mem (enc "LDR r0, [r11]"); 667 val thms = arm_spec_mem (enc "LDRB r0, [r11]"); 668 val thms = arm_spec_mem (enc "STRB r0, [r11]"); 669 val thms = arm_spec_mem (enc "STR r0, [r11]"); 670 val thms = arm_spec_mem (enc "STR r0, [r11,#8]"); 671 val thms = arm_spec_mem (enc "LDR r0, [r11,#8]"); 672 val thms = arm_spec_mem (enc "STR r0, [r11,#-8]"); 673 val thms = arm_spec_mem (enc "LDR r0, [r11,#-8]"); 674 val thms = arm_spec_mem (enc "LDMDB r0, {r2-r4}"); 675 val thms = arm_spec_mem (enc "STMDB r0, {r2-r4}"); 676 val thms = arm_spec_mem (enc "LDR r0, [sp,#8]"); 677 val thms = arm_spec_mem (enc "PUSH {r0-r2}"); 678 val thms = arm_spec_mem (enc "POP {r0-r2}"); 679 val thms = arm_spec_mem (enc "POP {r0-r2,pc}"); 680 val thms = arm_spec_mem (enc "POP {r4,pc}"); 681 val thms = arm_spec_mem (enc "BLNE -#40"); 682 val thms = arm_spec_mem (enc "LDRLS pc,[pc,r3,lsl #2]"); 683 val thms = arm_spec_mem "15832014" 684 685 val thms = arm_spec_m (enc "POP {r4,pc}"); 686 val thms = arm_spec_m (enc "STM r0, {r2-r3}"); 687 688*) 689 690end 691