1structure derive_specsLib :> derive_specsLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open wordsTheory pred_setTheory arithmeticTheory pairSyntax; 6open set_sepTheory progTheory addressTheory; 7open helperLib backgroundLib file_readerLib stack_introLib stack_analysisLib 8open writerLib; 9open GraphLangTheory 10 11fun spec_rule x = 12 case !arch_name of 13 ARM => arm_spec x 14 | M0 => m0_spec x 15 | RISCV => riscv_spec x; 16 17(* code abbrevs *) 18 19val code_abbreviations = ref ([]:thm list); 20fun add_code_abbrev thms = (code_abbreviations := thms @ !code_abbreviations); 21 22(* formatting *) 23 24fun DISCH_ALL_AS_SINGLE_IMP th = let 25 val th = RW [AND_IMP_INTRO] (DISCH_ALL th) 26 in if is_imp (concl th) then th else DISCH ``T`` th end 27 28(* thm traces *) 29 30fun next_possible_pcs f (th,i,SOME j,p) = 31 if can (find_term (fn tm => aconv tm ``GUARD``)) (concl th) 32 then all_distinct [j,p+i] else [j] 33 | next_possible_pcs f (th,i,NONE,p) = 34 ((th |> concl |> cdr |> find_terms (can (match_term ``p+(n2w n):word32``)) 35 |> filter (fn tm => wordsSyntax.is_word_add tm) 36 |> filter (fn tm => wordsSyntax.is_n2w (cdr tm)) 37 |> filter (fn tm => aconv (cdr (car tm)) (mk_var("p",``:word32``))) 38 |> map (numSyntax.int_of_term o cdr o cdr) 39 |> map f 40 |> sort (fn x => fn y => x <= y)) 41 handle HOL_ERR _ => fail()) 42 43datatype 'a thm_trace = 44 TRACE_CUT of int (* cut because a different branch describes the rest *) 45 | TRACE_END of 'a (* normal end *) 46 | TRACE_STEP of int * 'a * thm * ('a thm_trace) 47 | TRACE_SPLIT of ('a thm_trace) list; 48 49fun print_cfg t = let 50 fun cfg2str prefix (TRACE_CUT p) = "repeat from " ^ (int_to_string p) ^ "\n" ^ prefix 51 | cfg2str prefix (TRACE_END _) = "return\n" ^ prefix 52 | cfg2str prefix (TRACE_STEP (p,_,th,t)) = int_to_string p ^ " " ^ cfg2str prefix t 53 | cfg2str prefix (TRACE_SPLIT qs) = let 54 val s = "\n" ^ prefix ^ ". " ^ concat (map (cfg2str (prefix ^ ". ")) qs) 55 in String.substring(s,0,size(s)-2) end 56 in print ("\n\nCFG:\n " ^ cfg2str " " t ^ "\n\n") end; 57 58(* 59 60There's a bug in the trace generation to do with guards that are not 61just one variable. The following code shows how this happens: 62 63 val code = ["e92d47f0", "e3520003", "959ac000", "97de9002", 64 "979cc109", "8590c00c", "e8bd87f0"] 65 66print_cfg (construct_thm_trace thms) 67 68*) 69 70fun bool_normal_form tm = let 71 val vars = free_vars tm 72 val vsort = sort (fn v1 => fn v2 => fst (dest_var v1) <= fst (dest_var v2)) 73 val vs = vsort vars 74 fun aux t [] = t 75 | aux t (v::vs) = 76 mk_cond(v,aux (subst [v|->T] t) vs,aux (subst [v|->F] t) vs) 77 in SIMP_CONV std_ss [] (aux tm vs) |> concl |> dest_comb |> snd end 78 79fun construct_thm_trace thms = let 80 fun list_lookup i [] = fail() 81 | list_lookup i ((j,x,NONE)::xs) = if i = j then [x] else list_lookup i xs 82 | list_lookup i ((j,x,SOME y)::xs) = if i = j then [x,y] else list_lookup i xs 83 fun extract_pre (th,i,j) = let 84 val th = RW [] th 85 val guard = cdr (find_term (can (match_term ``GUARD n b``)) (concl th)) 86 in (th,bool_normal_form guard) end handle HOL_ERR _ => (th,T) 87 fun resets_status_bits th = let 88 val (_,p,_,q) = dest_spec (concl th) 89 val pv = free_vars p |> filter (fn tm => type_of tm = ``:bool``) 90 val qv = free_vars q |> filter (fn tm => type_of tm = ``:bool``) 91 in not (null (term_diff pv qv)) end 92 fun guard_conj guard (th,pre) = 93 (th,if resets_status_bits th then pre else bool_normal_form (mk_conj(pre,guard))) 94 fun next_directions th = 95 ((th |> concl |> cdr |> find_terms (can (match_term ``p+(n2w n):word32``)) 96 |> filter (fn tm => wordsSyntax.is_word_add tm) 97 |> filter (fn tm => wordsSyntax.is_n2w (cdr tm)) 98 |> filter (fn tm => aconv (cdr (car tm)) (mk_var("p",``:word32``))) 99 |> map (numSyntax.int_of_term o cdr o cdr) 100 |> sort (fn x => fn y => x <= y))) 101 fun mk_TRACE_SPLIT [] = TRACE_END T 102 | mk_TRACE_SPLIT [x] = x 103 | mk_TRACE_SPLIT xs = TRACE_SPLIT xs 104 val aux_calls = ref (tl [(0,T)]) 105 fun int_term_mem (p,tm) [] = false 106 | int_term_mem (p,tm) ((x,y)::xs) = 107 (p = x andalso aconv tm y) orelse int_term_mem (p,tm) xs 108 (* warning: the handling of guards is not perfect, but maybe good enough *) 109 fun aux (p:int) (seen:int list) (guard:term) = 110 if int_term_mem (p,guard) (!aux_calls) then TRACE_CUT p else 111 (aux_calls := (p,guard)::(!aux_calls); 112 if mem p seen then TRACE_CUT p else let 113 (* finds theorems describing program point p *) 114 val xs = list_lookup p thms 115 (* extract boolean precondition *) 116 val xs = map extract_pre xs 117 (* combine with current guard if theorem does not reset status bits *) 118 val xs = map (guard_conj guard) xs 119 (* remove dead paths *) 120 val xs = filter (fn (_,pre) => not (aconv pre F)) xs 121 (* reads the next pcs *) 122 val ys = map (fn (th,gg) => (th,gg,next_directions th)) xs 123 in mk_TRACE_SPLIT (map (fn (th,gs,nexts) => 124 TRACE_STEP (p, gs, th, mk_TRACE_SPLIT (map 125 (fn n => aux (n:int) (p::seen) (gs:term)) nexts))) ys) end) 126 fun is_nop th = (null (hyp th)) andalso 127 can (find_term (fn tm => aconv tm ``GUARD``)) (concl th) 128 fun filter_nops (TRACE_CUT p) = TRACE_CUT p 129 | filter_nops (TRACE_END d) = TRACE_END d 130 | filter_nops (TRACE_SPLIT ts) = TRACE_SPLIT (map filter_nops ts) 131 | filter_nops (TRACE_STEP (p,x,th,t)) = 132 if is_nop th then filter_nops t else TRACE_STEP (p,x,th,filter_nops t) 133 val result = aux 0 [] T 134 in result end 135 136 137(* derive SPEC theorems *) 138 139fun pair_apply f ((th1,x1:int,x2:int option),NONE) = ((f th1,x1,x2),NONE) 140 | pair_apply f ((th1,x1,x2),SOME (th2,y1:int,y2:int option)) = 141 ((f th1,x1,x2),SOME (f th2,y1,y2)) 142 143fun jump_apply f NONE = NONE | jump_apply f (SOME x) = SOME (f x); 144 145fun pair_jump_apply (f:int->int) ((th1,x1:int,x2:int option),NONE) = ((th1,x1,jump_apply f x2),NONE) 146 | pair_jump_apply f ((th1:thm,x1,x2),SOME (th2:thm,y1:int,y2:int option)) = 147 ((th1,x1,jump_apply f x2),SOME (th2,y1,jump_apply f y2)); 148 149val switch_input = ref (0:int ,[]:string list); 150 151val CARRY_OUT_LEMMA = 152 ``CARRY_OUT (x : 'a word) y T`` 153 |> ONCE_REWRITE_CONV [GSYM WORD_NOT_NOT] 154 |> RW [ADD_WITH_CARRY_SUB] 155 |> RW [WORD_NOT_NOT] 156 157val OVERFLOW_LEMMA = 158 ``OVERFLOW (x : 'a word) y T`` 159 |> ONCE_REWRITE_CONV [GSYM WORD_NOT_NOT] 160 |> RW [ADD_WITH_CARRY_SUB] 161 |> RW [WORD_NOT_NOT] 162 163val WORD_NOT_EQ_LESS_EQ = blastLib.BBLAST_PROVE 164 ``v <> w /\ v <=+ w <=> v <+ w:word32`` 165 |> (fn th => CONJ th (RW1 [CONJ_COMM] th)) 166 |> (fn th => CONJ th (RW1 [NEQ_SYM] th)) 167 |> RW [GSYM CONJ_ASSOC] |> GEN_ALL 168 169local 170 val cond_pat = cond_def |> SPEC_ALL |> concl |> dest_eq |> fst 171in 172 fun STAR_cond_CONV c tm = let 173 val (x,y) = dest_star tm 174 val _ = match_term cond_pat y 175 in RAND_CONV (RAND_CONV c) tm end 176end 177 178local 179 val d32 = CONJ (EVAL ``dimindex (:32)``) (EVAL ``dimword (:32)``) 180 val d64 = CONJ (EVAL ``dimindex (:64)``) (EVAL ``dimword (:64)``) 181 val word32_mem_pat = ``word32 (READ8 w1 m) (READ8 w2 m) (READ8 w3 m) (READ8 w4 m)`` 182 val word64_mem_pat = ``word64 (READ8 w1 m) (READ8 w2 m) (READ8 w3 m) (READ8 w4 m) 183 (READ8 w5 m) (READ8 w6 m) (READ8 w7 m) (READ8 w8 m)`` 184 val Align_pat1 = ``arm$Align (w:'a word,n)`` 185 val Align_pat2 = ``m0$Align (w:'a word,n)`` 186 (* ``b /\ ~(w ' 0) /\ b2 /\ (b3 ==> ALIGNED w) /\ ~(w ' 1)`` *) 187 val clean_ALIGNED_CONV = 188 SIMP_CONV (bool_ss++boolSimps.CONJ_ss) [BITS_01_IMP_ALIGNED] THENC 189 SIMP_CONV (bool_ss++boolSimps.CONJ_ss) [ALIGNED_IMP_BITS_01] 190 val n2w_64 = 191 n2w_11 |> INST_TYPE [alpha|->``:64``] |> REWRITE_RULE [EVAL ``dimword (:64)``] 192 val word_arith_lemma_CONV = 193 SIMP_CONV std_ss [word_arith_lemma1] THENC 194 SIMP_CONV std_ss [word_arith_lemma3,word_arith_lemma4,WORD_EQ_SUB_ZERO,n2w_64] 195 val flag_conv = 196 SIMP_CONV std_ss 197 [OVERFLOW_EQ,WORD_MSB_1COMP,WORD_NOT_NOT, 198 GSYM carry_out_def,WORD_0_POS,WORD_SUB_RZERO, 199 GSYM (EVAL ``~(0w:word32)``),d32, 200 GSYM (EVAL ``~(0w:word64)``),d64] THENC 201 ONCE_REWRITE_CONV [word_1comp_n2w,word32_msb_n2w] THENC 202 SIMP_CONV std_ss [d32,d64] 203 val finalise_pre_cond = 204 PRE_CONV (SIMP_CONV (pure_ss++sep_cond_ss) [] THENC 205 TRY_CONV (STAR_cond_CONV wordsLib.WORD_SUB_CONV)) 206 val final_conv = clean_ALIGNED_CONV THENC word_arith_lemma_CONV 207 THENC flag_conv THENC finalise_pre_cond 208 fun is_Align tm = can (match_term Align_pat1) tm orelse 209 can (match_term Align_pat2) tm 210 fun remove_Align th = 211 if not (can (find_term is_Align) (concl th)) then th else let 212 val tms = find_terms is_Align (concl th) 213 val rws = map (fn tm => SPEC (tm |> rand |> pairSyntax.dest_pair |> fst) 214 REMOVE_Align |> UNDISCH) tms 215 in PURE_REWRITE_RULE rws th |> DISCH_ALL 216 |> PURE_REWRITE_RULE [GSYM SPEC_MOVE_COND] 217 |> SIMP_RULE (pure_ss++sep_cond_ss) [] end 218 fun READ8_INTRO_CONV tm = 219 (if tm |> rator |> is_var then REWR_CONV (GSYM READ8_def) tm 220 else NO_CONV tm) 221 handle HOL_ERR _ => NO_CONV tm 222 val lemma31 = blastLib.BBLAST_PROVE 223 ``(((((31 >< 1) (w:word32)):31 word) @@ (0w:1 word)) : word32) = 224 w && 0xFFFFFFFEw`` 225 val fix_sub_word64 = prove( 226 ``(n2w n + w = if n < dimword (:'a) DIV 2 then n2w n + (w:'a word) 227 else w - n2w (dimword (:'a) - n MOD dimword (:'a))) /\ 228 (w + n2w n = if n < dimword (:'a) DIV 2 then w + n2w n 229 else w - n2w (dimword (:'a) - n MOD dimword (:'a)))``, 230 simp [Once WORD_ADD_COMM] \\ rw [] 231 \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [GSYM WORD_NEG_NEG])) 232 \\ rewrite_tac [WORD_EQ_NEG,word_2comp_n2w]) 233 |> INST_TYPE [alpha|->``:64``] 234 |> SIMP_RULE std_ss [EVAL ``dimword (:64)``] 235 val riscv_mask_byte = 236 blastLib.BBLAST_PROVE ``w2w (w && 2w ��� 7 ��� 1w) = (w2w (w:word64)) : word8`` 237in 238 fun clean_spec_thm th = let 239 val th = th |> REWRITE_RULE [GSYM word32_def, GSYM word64_def, 240 decomp_simp1,GSYM READ32_def,GSYM READ64_def, 241 GSYM WRITE32_def,GSYM WRITE64_def,WRITE64_intro,riscv_mask_byte, 242 word_extract_thm,GSYM word_add_with_carry_def] 243 |> CONV_RULE (DEPTH_CONV READ8_INTRO_CONV) 244 |> REWRITE_RULE [GSYM WRITE8_def] 245 |> SIMP_RULE std_ss [AC CONJ_COMM CONJ_ASSOC,word_bit_def,d32,d64, 246 SHIFT_ZERO(*,WORD_MUL_LSL,word_mul_n2w*), 247 GSYM ADD_ASSOC,lemma31,count_leading_zero_bits_thm] 248 val tms32 = find_terms (can (match_term word32_mem_pat)) (concl th) 249 val tms64 = find_terms (can (match_term word64_mem_pat)) (concl th) 250 fun READ32_RW tm = let 251 val (y,x) = tm |> rand |> dest_comb 252 val goal = mk_eq(tm,``READ32 ^(rand y) ^x``) 253 val c = 254 SIMP_CONV std_ss [READ32_def,word_arith_lemma1,READ8_def] THENC 255 SIMP_CONV std_ss [word_arith_lemma2,word_arith_lemma3,word_arith_lemma4] 256 in MATCH_MP EQ_T (c goal) end handle HOL_ERR _ => TRUTH; 257 fun READ64_RW tm = let 258 val (y,x) = tm |> rand |> dest_comb 259 val goal = mk_eq(tm,``READ64 ^(rand y) ^x``) 260 val c = 261 SIMP_CONV std_ss [READ64_def,word_arith_lemma1,READ8_def] THENC 262 SIMP_CONV std_ss [word_arith_lemma2,word_arith_lemma3,word_arith_lemma4] 263 in MATCH_MP EQ_T (c goal) end handle HOL_ERR _ => TRUTH; 264 val th = th |> PURE_REWRITE_RULE ([ALIGNED_Align] @ map READ32_RW tms32 265 @ map READ64_RW tms64) 266 val th = remove_Align th 267 val th = CONV_RULE final_conv th 268 val th = SIMP_RULE std_ss [word_cancel_extra] th 269 |> CONV_RULE word_arith_lemma_CONV 270 val th = th |> ONCE_REWRITE_RULE [fix_sub_word64] 271 |> SIMP_RULE std_ss [m0_preprocessing] 272 in th end 273end 274 275fun remove_arm_CONFIGURE th = 276 if can (find_term (fn tm => aconv tm ``arm_CONFIG``)) (concl th) then let 277 val var = ``var:bool`` 278 val pat = ``arm_CONFIG (VFPv3,ARMv7_A,F,^var,mode)`` 279 val m = match_term pat 280 val n = subst (fst (m (find_term (can m) (concl th)))) var 281 val th = DISCH (mk_neg n) th |> SIMP_RULE bool_ss [] 282 |> SIMP_RULE (bool_ss++sep_cond_ss) [GSYM SPEC_MOVE_COND, 283 GSYM arm_decompTheory.arm_OK_def] 284 val _ = if can m (concl th) 285 then failwith "unable to remove arm_CONFIGURE" else () 286 in th end 287 else th 288 289(* 290val (pos,switch_code) = !switch_input 291*) 292 293fun get_spec_for_switch (pos,switch_code) = let 294 val _ = (switch_input := (pos,switch_code)) 295 fun remove_colon_prefix s = last (String.tokens (fn x => x = #":") s) 296 val raw_code = map remove_colon_prefix switch_code 297 val ((th1,_,_),_) = spec_rule (el 1 raw_code) 298 val ((th2,_,_),th2a) = spec_rule (el 2 raw_code) 299 val ((th3,_,_),_) = spec_rule (el 3 raw_code) 300 val (th2a,_,_) = the th2a 301 val (_,_,sts,_) = get_tools() 302 val (reg,case_count) = let 303 val thB = SPEC_COMPOSE_RULE [th1,th2a,th3] 304 val thB = thB |> SIMP_RULE (std_ss++sep_cond_ss) [precond_def, 305 SPEC_MOVE_COND,CARRY_OUT_LEMMA,WORD_EQ_SUB_ZERO] 306 |> CONV_RULE (BINOP1_CONV (SIMP_CONV (srw_ss()) [])) 307 |> RW [WORD_NOT_EQ_LESS_EQ] 308 |> Q.INST [`pc`|->`n2w ^(numLib.term_of_int pos)`] 309 |> SIMP_RULE (srw_ss()) [word_add_n2w,OVERFLOW_LEMMA] 310 |> CONV_RULE (SIMP_CONV (pure_ss++star_ss) [] THENC 311 REWRITE_CONV [STAR_ASSOC]) 312 val reg = thB |> concl |> find_term (can (match_term ``arm_REG x y``)) 313 in (reg,thB |> concl |> dest_imp |> fst |> rator |> rand |> rand 314 |> numLib.int_of_term |> (curry (op +) 1)) end 315 fun genlist f 0 k = [] 316 | genlist f n k = f k :: genlist f (n-1) (k+1) 317 val targets = zip (genlist I case_count 0) (take case_count (drop 3 raw_code)) 318 val thA = th2 319 val thA = RW [WORD_CMP_NORMALISE,precond_def] thA 320 val thA = thA |> DISCH ``arm$Aligned (w0:word32,2)`` 321 |> SIMP_RULE std_ss [Aligned_Align] 322 val thA = remove_arm_CONFIGURE thA 323 val thA = thA |> Q.INST [`pc`|->`n2w ^(numLib.term_of_int (pos+4))`] 324 val thA = thA |> Q.INST [`w0`|->`n2w target`] 325 val thA = thA |> INST [reg |> rand|->``n2w n:word32``] 326 fun eval_case (c,p) = let 327 val n = p |> Arbnum.fromHexString |> Arbnum.toInt |> numLib.term_of_int 328 val cnv = PRE_CONV (MOVE_OUT_CONV (rator reg)) THENC 329 POST_CONV (MOVE_OUT_CONV (rator reg)) 330 val th = thA |> INST [``target:num``|->n,``n:num``|->numSyntax.term_of_int c] 331 val th = th |> SIMP_RULE (srw_ss()) [armTheory.Aligned_def,armTheory.Align_def, 332 CARRY_OUT_LEMMA,OVERFLOW_LEMMA] 333 |> CONV_RULE (PRE_CONV ((RAND_CONV o RAND_CONV) 334 (REWRITE_CONV [armTheory.Aligned_def,armTheory.Align_def] 335 THENC EVAL))) |> RW [SEP_CLAUSES] 336 |> CONV_RULE cnv |> RW1 [SWITCH_LEMMA] |> SPEC (rand reg) 337 |> CONV_RULE (SIMP_CONV (pure_ss++star_ss) [] THENC 338 REWRITE_CONV [STAR_ASSOC]) 339 in th end 340 val xs = map eval_case targets 341 fun combine (x,th) = MATCH_MP SWITCH_COMBINE (CONJ x th) 342 val th = foldr combine (last xs) (butlast xs) 343 val assum = th |> concl |> dest_imp |> fst 344 val (w,n) = dest_eq(repeat (snd o dest_imp) assum) 345 val new_assum = ``^w <+ ^n + 1w`` 346 val lemma = blastLib.BBLAST_PROVE (mk_imp(new_assum,assum)) 347 val th = 348 MP th (UNDISCH lemma) 349 |> DISCH_ALL 350 |> CONV_RULE ((RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss [word_add_n2w])) 351 |> RW [GSYM SPEC_MOVE_COND] 352 val (_,_,c,_) = dest_spec (concl th) 353 val code_list = find_terms pairSyntax.is_pair c |> term_all_distinct 354 val code_set = code_list |> pred_setSyntax.mk_set 355 val th = MATCH_MP SPEC_SUBSET_CODE th |> SPEC code_set 356 |> CONV_RULE (BINOP1_CONV (REWRITE_CONV [UNION_SUBSET, 357 INSERT_SUBSET,EMPTY_SUBSET,IN_INSERT])) 358 val th = MP th TRUTH 359 val th2a = th2a |> Q.INST [`pc`|->`n2w ^(numLib.term_of_int (pos+4))`] 360 val (_,_,c,_) = dest_spec (concl th) 361 val th2a = MP (MATCH_MP SPEC_SUBSET_CODE th2a |> SPEC c 362 |> CONV_RULE (BINOP1_CONV (EVAL))) TRUTH 363 in (th1,th,th2a,th3, (length code_list)) end 364 365fun inst_pc_var tools thms = let 366 fun triple_apply f (y,(th1,x1:int,x2:int option),NONE) = (y,(f y th1,x1,x2),NONE) 367 | triple_apply f (y,(th1,x1,x2),SOME (th2,y1:int,y2:int option)) = 368 (y,(f y th1,x1,x2),SOME (f y th2,y1,y2)) 369 val i = [mk_var("eip",``:word32``) |-> mk_var("p",``:word32``), 370 mk_var("rip",``:word64``) |-> mk_var("p",``:word64``)] 371 val (_,_,_,pc) = tools 372 val ty = (hd o snd o dest_type o type_of) pc 373 fun f y th = let 374 val aa = (hd o tl o snd o dest_type) ty 375 val th = INST i th 376 val (_,p,_,_) = dest_spec (concl th) 377 val pattern = inst [``:'a``|->aa] ``(p:'a word) + n2w n`` 378 val new_p = subst [mk_var("n",``:num``)|-> numSyntax.mk_numeral (Arbnum.fromInt y)] pattern 379 val th = INST [mk_var("p",type_of new_p)|->new_p] th 380 val (_,_,_,q) = dest_spec (concl th) 381 val tm = find_term (fn tm => aconv (car tm) pc handle HOL_ERR e => false) q handle HOL_ERR _ => ``T`` 382 val cc = SIMP_CONV std_ss [word_arith_lemma1,word_arith_lemma3,word_arith_lemma4] 383 val th = CONV_RULE ((RATOR_CONV o RAND_CONV) cc) th 384 val thi = QCONV cc tm 385 in PURE_ONCE_REWRITE_RULE [thi,WORD_ADD_0] th end; 386 in map (triple_apply f) thms end 387 388fun pull_let_wider_CONV tm = let 389 val x = find_term (can (pairSyntax.dest_anylet)) tm 390 val (y,d) = pairSyntax.dest_anylet x 391 val tm2 = pairSyntax.mk_anylet(y,subst [x|->d] tm) 392 val goal = mk_eq(tm,tm2) 393 val lemma = auto_prove "pull_let_wider_CONV" (goal, 394 SIMP_TAC std_ss [LET_DEF] 395 THEN CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) 396 THEN REWRITE_TAC []) 397 in lemma end handle HOL_ERR _ => NO_CONV tm; 398 399local 400 val pc_var1_32 = mk_var("pc",``:word32``) 401 val pc_var2_32 = mk_var("p",``:word32``) 402 val pc_var1_64 = mk_var("pc",``:word64``) 403 val pc_var2_64 = mk_var("p",``:word64``) 404 fun get_pc_pat () = let 405 val (_,_,_,pc) = get_tools () 406 in ``^pc w`` end 407in 408 fun inst_pc pos th = let 409 val new_pc_32 = ``n2w ^(numSyntax.term_of_int pos):word32`` 410 val new_pc_64 = ``n2w ^(numSyntax.term_of_int pos):word64`` 411 val th = INST [pc_var1_32 |-> new_pc_32, pc_var2_32 |-> new_pc_32, 412 pc_var1_64 |-> new_pc_64, pc_var2_64 |-> new_pc_64] th 413 val pc_pat = get_pc_pat () 414 val tms = find_terms (can (match_term pc_pat)) (rand (concl th)) 415 val rws = map (QCONV (RAND_CONV EVAL)) tms 416 val th = ONCE_REWRITE_RULE rws th 417 in th end 418end 419 420fun mk_call_tag fname is_tail_call = let 421 val b = if is_tail_call then T else F 422 val fname_tm = stringSyntax.fromMLstring fname 423 in mk_comb(mk_comb(``CALL_TAG``,fname_tm),b) end 424 425fun dest_call_tag tm = let 426 val (xy,z) = dest_comb tm 427 val (x,y) = dest_comb xy 428 val _ = (aconv x ``CALL_TAG``) orelse fail() 429 in (stringSyntax.fromHOLstring y, 430 if aconv z T then true else 431 if aconv z F then false else fail()) end 432 433exception NoInstructionSpec 434 435fun wrap_get_spec f asm = f asm 436 handle HOL_ERR e => if #origin_structure e = "arm_progLib" 437 then raise NoInstructionSpec 438 else failwith ("Unable to derive spec for " ^ asm ^ ": " ^ format_ERR e) 439 440fun derive_individual_specs code = let 441 val tools = get_tools() 442 fun mk_new_var prefix v = let 443 val (n,ty) = dest_var v 444 in mk_var (prefix ^ "@" ^ n, ty) end 445 val (f,_,hide_th,pc) = tools 446 fun get_model_status_list th = 447 (map dest_sep_hide o list_dest dest_star o snd o dest_eq o concl) th handle HOL_ERR e => [] 448 val delete_spaces = (implode o filter (fn x => not(x = #" ")) o explode) 449 fun list_find name [] = fail () 450 | list_find name ((x,y)::xs) = if name = x then y else list_find name xs 451 val prefix_len = size "switch:" 452 fun remove_switch_prefix s = 453 if String.isPrefix "switch:" s 454 then remove_switch_prefix (String.substring(s,prefix_len,size s - prefix_len)) else s 455 val bad_insts = ["rfeia","mrc","mcr","mcrr","strex","cpsid","svc"] 456 fun bad_instruction asm_name = 457 length (filter (fn s => String.isPrefix s asm_name) bad_insts) <> 0 458 val white_chars = explode " \t\n" 459 fun get_asm_name asm = asm |> String.tokens (fn c => mem c white_chars) |> hd 460 461(* 462 val ((th,_,_),_) = res 463 val th = (inst_pc pos o RW [precond_def]) th 464*) 465 466 fun get_local_const pos = let 467 val (_,c,_) = first (fn (p,_,_) => p = pos) code 468 val _ = String.isPrefix "const:" c orelse failwith "const load from non-const" 469 val hex = String.tokens (fn c => c = #":") c |> el 2 470 val tm = Arbnum.fromHexString hex |> numSyntax.mk_numeral 471 in ``n2w (^tm):word32`` end 472 fun has_free_vars tm = length (free_vars tm) <> 0 473 fun inst_pc_rel_const th = let 474 val (_,_,c,_) = dest_spec (concl th) 475 in if not (has_free_vars c) then th else let 476 fun do_inst tm = let 477 val (pos_tm,v) = pairSyntax.dest_pair tm 478 in v |-> get_local_const (pos_tm |> rand 479 |> numSyntax.int_of_term) end 480 val i = find_terms (fn tm => pairSyntax.is_pair tm andalso 481 is_var (rand tm)) c 482 |> map (do_inst o rand o concl o QCONV EVAL) 483 val th = INST i th |> CONV_RULE (RATOR_CONV (RAND_CONV EVAL)) 484 in th end end 485 486 fun remove_tab s = 487 s |> explode |> map (fn c => if c = #"\t" then #" " else c) |> implode 488 fun placeholder_spec asm len = let 489 val t = String.tokens (fn x => x = #":") asm |> last |> remove_tab 490 in (SPECL [stringSyntax.fromMLstring t, numSyntax.term_of_int len] 491 (case !arch_name of 492 ARM => SKIP_SPEC_ARM 493 | M0 => SKIP_SPEC_M0 494 | RISCV => SKIP_SPEC_RISCV), len, SOME len) end 495 496(* 497 val ((pos,instruction,asm)::code) = code 498 val ((pos,instruction,asm)::code) = drop 1 code 499 val ((pos,instruction,asm)::code) = drop 17 code 500*) 501 fun get_specs [] = [] 502 | get_specs ((pos,instruction,asm)::code) = let 503 val instruction = delete_spaces instruction 504 in 505 if String.isPrefix "call:" instruction then let 506 val ts = String.tokens (fn x => x = #":") instruction 507 val fname = ts |> el 2 508 val instruction = ts |> el 3 509 fun add_call_tag th = 510 th |> DISCH (mk_call_tag fname false) |> UNDISCH 511 val g = add_call_tag o 512 clean_spec_thm o 513 remove_arm_CONFIGURE o 514 inst_pc_rel_const o 515 inst_pc pos o RW [precond_def] 516 val res = wrap_get_spec f instruction 517 val (x,y) = pair_apply g res 518 in (pos,x,y) :: get_specs code end 519 else if String.isPrefix "const:" instruction then 520 get_specs code 521 else if not (code = []) andalso 522 String.isPrefix "switch:" ((fn (_,x,_) => x) (hd code)) then let 523 val switch_code = instruction :: map (fn (_,x,_) => x) code 524 val _ = write_line "Switch found." 525 val (th1,th2,th2a,th3,l) = get_spec_for_switch (pos,switch_code) 526 val code = drop (l-1) code 527 val th2 = th2 |> RW [SPEC_MOVE_COND] 528 |> SIMP_RULE std_ss [] |> UNDISCH_ALL 529 fun g pos = clean_spec_thm o 530 remove_arm_CONFIGURE o 531 inst_pc_rel_const o 532 inst_pc pos o RW [precond_def] 533 in (pos,(g pos th1,4,SOME 4),NONE) :: 534 (pos+4,(g (pos+4) th2,4,NONE),SOME (g (pos+4) th2a,4,SOME 4)) :: 535 (pos+8,(g (pos+8) th3,4*l-8,SOME 4),NONE) :: 536 get_specs code end 537 else if String.isPrefix "dmb" asm then raise NoInstructionSpec 538 else let 539 val g = clean_spec_thm o 540 remove_arm_CONFIGURE o 541 inst_pc_rel_const o 542 inst_pc pos o RW [precond_def] 543 val res = wrap_get_spec f instruction 544 handle HOL_ERR _ => raise NoInstructionSpec 545 val (x,y) = pair_apply g res 546 in (pos,x,y) :: get_specs code end 547 end handle NoInstructionSpec => let 548 val asm = String.translate (fn c => 549 if c = #"\r" then "" else 550 if c = #"\t" then " " else implode [c]) asm 551 val _ = write_line ("Skipping " ^ instruction ^ " " ^ asm) 552 val len = if size instruction (* in hex *) < 8 then 2 else 4 (* bytes *) 553 val (thi,x1,x2) = (placeholder_spec asm len) 554 in (pos,(inst_pc pos thi,x1,x2),NONE) :: get_specs code end 555 556(* 557 val (pos,instruction,asm) = hd code 558 val n = 8 559 val instruction = hd (drop 22 code) 560 val iss = drop 13 code 561 val ((th,_,_),_) = f instruction 562 val th = renamer th 563 val prefix = "foo@" 564*) 565 val res = get_specs code 566 val has_bad_insts = exists bad_instruction 567 (map (fn (_,_,asm) => get_asm_name asm) code) 568 fun calc_addresses i [] = [] 569 | calc_addresses i ((n:int,(th1:thm,l1,j1),y)::xs) = let 570 val (x,y) = pair_jump_apply (fn j => i+j) ((th1,l1,j1),y) 571 in (i,x,y) :: calc_addresses (i+l1) xs end 572 val res = calc_addresses 0 res 573 val res = inst_pc_var tools res 574 (* deal with silly blx instructions that call a constant pointer *) 575 val pc_rel_var = mk_var("pc_rel",``:word32``) 576 fun basic_find_pc_rel_load v = 577 first (fn (n,(th,i,k),y) => let 578 val vs = free_vars (concl th) 579 in term_mem pc_rel_var vs andalso term_mem (mk_new_var "new" v) vs end) res 580 fun find_pc_rel_load nn v = let 581 fun exit_pc_is_var th = let 582 val v = cdr (find_term (can (match_term ``arm_PC w``)) (cdr (concl th))) 583 in is_var v end; 584 val res2 = map (fn (nn,(th,i,x),y) => 585 if (x = NONE) andalso exit_pc_is_var th 586 then hd (inst_pc_var tools [(nn,(fake_spec,i,SOME 4),y)]) 587 else (nn,(th,i,x),y)) (butlast res) @ [last res] 588 fun is_assign th = let 589 val vs = free_vars (concl th) 590 in term_mem pc_rel_var vs andalso term_mem (mk_new_var "new" v) vs end 591 fun assign curr (TRACE_CUT p) = [] 592 | assign curr (TRACE_END _) = [] 593 | assign curr (TRACE_SPLIT qs) = append_lists (map (assign curr) qs) 594 | assign curr (TRACE_STEP (p,_,th,t)) = 595 if p = nn then [curr] else 596 assign (if is_assign th then p else curr) t 597 val xs = (diff (assign ~1 (construct_thm_trace res2)) [~1]) 598 val _ = length xs > 0 orelse failwith("can't find assignment") 599 val i = hd xs 600 fun thms_lookup n [] = fail() 601 | thms_lookup n ((nn,x,y)::xs) = if n = nn then (nn,x,y) else thms_lookup n xs 602 in thms_lookup i res end handle HOL_ERR _ => basic_find_pc_rel_load v 603 fun delete_long_jump (nn,(th,i,SOME k),y) = (nn,(th,i,SOME k),y) 604 | delete_long_jump (nn,(th,i,NONE),y) = let 605 val v = cdr (find_term (can (match_term ``arm_PC w``)) (cdr (concl th))) 606 val (n,(r,_,_),_) = find_pc_rel_load nn v 607 val (_,_,c,_) = dest_spec (concl r) 608 val k = el 2 (list_dest pred_setSyntax.dest_insert c) 609 |> dest_pair |> fst |> cdr |> cdr |> numSyntax.int_of_term 610 val xs = String.tokens (fn c => c = #":") ((fn (_,x,_) => x) (el (k div 4 + 1) code)) 611 val a = el 2 xs |> Arbnum.fromHexString |> numSyntax.mk_numeral 612 |> (fn n => wordsSyntax.mk_n2w(n,``:32``)) 613 val name = el 3 xs 614 val rw = GSYM (ASSUME (mk_eq(a,v))) 615 val th = CONV_RULE (POST_CONV (MOVE_OUT_CONV ``arm_PC``)) th 616 val th = CONV_RULE ((RATOR_CONV o RAND_CONV) (REWRITE_CONV [rw])) th 617 val th = CONV_RULE ((POST_CONV o RAND_CONV) (REWRITE_CONV [rw])) th 618 val th = DISCH_ALL_AS_SINGLE_IMP th 619 val th = CONV_RULE ((RATOR_CONV o RAND_CONV) (REWRITE_CONV [rw] THENC EVAL)) th 620 val th = UNDISCH_ALL th 621 val (th1,_,_) = (print "Not found in memory.\n\n"; fail()) 622 val th = RW [hide_th] th 623 val th = CONV_RULE (POST_CONV (MOVE_OUT_CONV ``aR 14w``)) th 624 val th = CONV_RULE (PRE_CONV (MOVE_OUT_CONV ``arm_PC``)) th 625 val th = SPEC_COMPOSE_RULE [th,th1] 626 val th = DISCH_ALL th |> REWRITE_RULE [GSYM SPEC_MOVE_COND] 627 val th = RW [sidecond_def,hide_th,STAR_ASSOC] th 628 val th = CONV_RULE (POST_CONV pull_let_wider_CONV) th 629 in (nn,(th,i,SOME (nn+i)),y) end handle HOL_ERR _ => (nn,(th,i,NONE),y) 630 val res = map delete_long_jump res 631 in (has_bad_insts, res) end; 632 633fun inst_pc_rel_const tools thms code = let 634 fun triple_apply f (y,(th1,x1:int,x2:int option),NONE) = (y,(f y th1,x1,x2),NONE) 635 | triple_apply f (y,(th1,x1,x2),SOME (th2,y1:int,y2:int option)) = 636 (y,(f y th1,x1,x2),SOME (f y th2,y1,y2)) 637 fun find_instr [] p = hd [] 638 | find_instr (x::xs) p = if p < 4 then x else find_instr xs (p-4) 639 val pc_rel = mk_var("pc_rel",``:word32``) 640 val has_pc_rel = can (find_term (fn x => aconv x pc_rel)) 641 fun foo y th = 642 if not (has_pc_rel (concl th)) then th else let 643 val (_,_,c,_) = dest_spec (concl th) 644 val ys = find_terms (can (match_term ``(x1:word32,x2:word32)``)) c 645 val const = ys |> filter has_pc_rel |> hd |> dest_pair |> fst 646 |> cdr |> cdr |> numSyntax.int_of_term |> find_instr code 647 val const = if String.isPrefix "const:" const 648 then el 2 (String.tokens (fn c => c = #":") const) else const 649 val n = numSyntax.mk_numeral (Arbnum.fromHexString const) 650 val th = INST [pc_rel|->wordsSyntax.mk_n2w(n,``:32``)] th 651 in th end 652 in map (triple_apply foo) thms end 653 654fun UNABBREV_CODE_RULE th = let 655 val rw = (!code_abbreviations) 656 val c = REWRITE_CONV rw THENC 657 SIMP_CONV std_ss [word_arith_lemma1] THENC 658 REWRITE_CONV [INSERT_UNION_EQ,UNION_EMPTY] 659 val th = CONV_RULE ((RATOR_CONV o RAND_CONV) c) th 660 in th end; 661 662fun tidy_up_name name = let 663 val name = if String.isPrefix "_" name then "fun" ^ name else name 664 in String.translate (fn c => if c = #"-" then "_" else implode [c]) name end 665 666fun abbreviate_code name thms = let 667 fun extract_code (_,(th,_,_),_) = let val (_,_,c,_) = dest_spec (concl th) in c end 668 val cs = map extract_code thms 669 val ty = (hd o snd o dest_type o type_of o hd) cs 670 val tm = foldr pred_setSyntax.mk_union (pred_setSyntax.mk_empty ty) cs 671 val cth = QCONV (PURE_REWRITE_CONV [INSERT_UNION_EQ,UNION_EMPTY]) tm 672 val c = (cdr o concl) cth 673 val (_,(th,_,_),_) = hd thms 674 val (m,_,_,_) = dest_spec (concl th) 675 val model_name = (to_lower o implode o take_until (fn x => x = #"_") o explode o fst o dest_const) m 676 val x = list_mk_pair (free_vars c) 677 val def_name = name ^ "_" ^ model_name 678 val def_name = tidy_up_name def_name 679 val v = if aconv x ``():unit`` then mk_var(def_name,type_of c) 680 else mk_var(def_name,type_of(mk_pabs(x,c))) 681 val code_def = new_definition(def_name ^ "_def", 682 if aconv x ``():unit`` then mk_eq(v,c) 683 else mk_eq(mk_comb(v,x),c)) 684 val _ = add_code_abbrev [code_def] 685 fun triple_apply f (y,(th1,x1:int,x2:int option),NONE) = (y,(f th1,x1,x2),NONE) 686 | triple_apply f (y,(th1,x1,x2),SOME (th2,y1:int,y2:int option)) = 687 (y,(f th1,x1,x2),SOME (f th2,y1,y2)) 688 val code_thm = CONV_RULE (RAND_CONV (fn _ => GSYM cth)) (SPEC_ALL code_def) 689 fun foo th = let 690 val thi = MATCH_MP ABBBREV_CODE_LEMMA (DISCH_ALL_AS_SINGLE_IMP th) 691 val thi = SPEC ((fst o dest_eq o concl o SPEC_ALL) code_def) thi 692 val goal = (fst o dest_imp o concl) thi 693 val lemma = auto_prove "abbreviate_code" (goal, 694 REPEAT (REWRITE_TAC [code_thm,SUBSET_DEF,IN_UNION] THEN REPEAT STRIP_TAC 695 THEN ASM_REWRITE_TAC [] THEN (fn _ => fail())) 696 THEN REWRITE_TAC [EMPTY_SUBSET] 697 THEN REWRITE_TAC [SUBSET_DEF,IN_INSERT,IN_UNION,NOT_IN_EMPTY,code_def] 698 THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss []) 699 val thi = UNDISCH_ALL (PURE_REWRITE_RULE [GSYM AND_IMP_INTRO] (MP thi lemma)) 700 in thi end 701 val thms = map (triple_apply foo) thms 702 val _ = (aconv x ``():unit``) orelse failwith "code contains variables" 703 in (code_def,thms) end 704 705fun apply_thms f (i:int,(th,l:int,j:int option),NONE) = (i,(f th,l,j),NONE) 706 | apply_thms f (i,(th,l,j),SOME (th1,l1,j1)) = (i,(f th,l,j),SOME (f th1,l1,j1)) 707 708fun try_map g f [] = [] 709 | try_map g f (x::xs) = let 710 val y = f x 711 in y :: try_map g f xs end 712 handle HOL_ERR _ => 713 (g x; try_map g f xs) 714 715val stack_intro_fails = ref ([] : (int * string) list); 716 717fun print_stack_intro_fail (pos,sec_name) = let 718 val b = !writer_prints 719 val _ = (writer_prints := true) 720 val _ = write_line ("Stack intro failed in " ^ sec_name ^ " for pos " ^ 721 (int_to_hex pos) ^ ".") 722 val _ = (writer_prints := b) 723 in () end 724 725fun add_stack_intro_fail pos sec_name = 726 (print_stack_intro_fail (pos,sec_name); 727 stack_intro_fails := (pos, sec_name) :: (!stack_intro_fails)); 728 729fun clear_stack_intro_fails () = (stack_intro_fails := []); 730 731fun print_stack_intro_report () = 732 (if length (!stack_intro_fails) = 0 then 733 (write_line "No stack intro failures."; []) 734 else (has_failures := true; 735 map print_stack_intro_fail (!stack_intro_fails))) 736 737fun derive_specs_for sec_name = let 738 val code = section_body sec_name 739 val _ = write_subsection "Deriving specifications" 740 val cl = int_to_string (length code) 741 val str = "Section `"^sec_name^"` consists of "^cl^" instructions." 742 val _ = write_line str 743 val thms = snd (derive_individual_specs code) 744 val stack_accesses = 745 if length thms = 0 then [] else 746 find_stack_accesses sec_name thms 747 handle HOL_ERR _ => (add_stack_intro_fail 0 sec_name; []) 748 val _ = (writer_prints := false) 749 val thms = try_map (fn (n,_,_) => add_stack_intro_fail n sec_name) 750 (apply_thms (STACK_INTRO_RULE stack_accesses)) thms 751 val _ = (writer_prints := true) 752 val (code_abbrev_def, thms) = 753 if length thms = 0 then (TRUTH, thms) else 754 abbreviate_code sec_name thms 755 in thms end; 756 757(* 758 759 val base_name = "loop-riscv/example" 760 val base_name = "kernel-riscv/kernel-riscv" 761 val _ = read_files base_name [] 762 val _ = open_current "test" 763 val sec_name = "lookupSlot" 764 val sec_name = "memzero" 765 val sec_name = "memcpy" 766 val sec_name = "isIRQPending" 767 val sec_name = "createNewObjects" 768 val sec_name = "get_num_avail_p_regs" 769 val sec_name = "ensureEmptySlot" 770 771 val _ = file_readerLib.show_code sec_name 772 773 val base_name = "loop/example" 774 val _ = read_files base_name [] 775 val _ = open_current "test" 776 val sec_name = "g" 777 778val l3_arm_tools = arm_decompLib.l3_arm_tools 779val (arm_spec,_,_,_) = l3_arm_tools 780val instruction = "e200300f" 781val th = arm_spec instruction 782 783 val (f,_,_,_) = l3_arm_tools 784 785 ``increment`` 786 787 788 [(0, "e200300f", "and\tr3, r0, #15"), 789 (4, "e0830180", "add\tr0, r3, r0, lsl #3"), 790 (8, "e12fff1e", "bx\tlr")]: 791 792*) 793 794end 795