1structure straightlineLib :> straightlineLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open listTheory wordsTheory pred_setTheory arithmeticTheory wordsLib pairTheory; 6open set_sepTheory progTheory helperLib addressTheory straightlineTheory; 7open core_decompilerLib tripleTheory derive_specsLib; 8 9open backgroundLib file_readerLib stack_introLib stack_analysisLib writerLib; 10 11val add_DO_NOTHING = let 12 val c = REWR_CONV (GSYM DO_NOTHING_def) 13 in CONV_RULE (POST_CONV c THENC PRE_CONV c) end 14 15local 16 val produce_TRIPLE_fail = ref TRUTH; 17 val index = ref (0:int); 18 fun next_index () = (index := (!index) + 1; (!index)) 19in 20 fun produce_TRIPLE th = let 21 val all_parts = arm_assert_def 22 |> SPEC_ALL |> concl |> dest_eq |> snd 23 |> list_dest dest_star 24 (* move bool conditions into assums *) 25 val th = CONV_RULE (PRE_CONV (MOVE_OUT_CONV ``arm_PC``)) th 26 val th = MATCH_MP SPEC_VAR_PC th |> SPEC_ALL |> UNDISCH_ALL 27 val th = th |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 28 |> UNDISCH_ALL 29 (* make pre have all parts *) 30 val (_,pre,_,_) = dest_spec (concl th) 31 val ps = list_dest dest_star pre 32 val ps' = map rator ps 33 val missing_parts = filter (fn p => not (mem (rator p) ps')) all_parts 34 val frame = list_mk_star missing_parts (type_of pre) 35 val th = SPEC_FRAME_RULE th frame 36 val th = th |> CONV_RULE (PRE_CONV (STAR_REWRITE_CONV (GSYM arm_assert_def))) 37 val th = th |> CONV_RULE (POST_CONV (STAR_REWRITE_CONV (GSYM arm_assert_def))) 38 val th = th |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] 39 val th = if is_imp (concl th) then th else DISCH T th 40 val th = MATCH_MP TRIPLE_INTRO (DISCH_ALL th) 41 val th = th |> REWRITE_RULE [] 42 val tuple = th |> concl |> rator |> rator |> rand 43 val post = th |> concl |> rand 44 val postfix = "@" ^ (int_to_string (next_index ())) 45 val vs = free_vars tuple 46 |> map (fn v => v |-> mk_var(fst (dest_var v) ^ postfix,type_of v)) 47 val new_tuple = subst vs tuple 48 fun mk_new_post (post,tuple,new_tuple) = 49 if not (pairSyntax.is_pair tuple) then 50 if post = tuple then REFL post else ASSUME (mk_eq(post,new_tuple)) 51 else let 52 val (lhs1,rhs1) = dest_pair post 53 val (lhs2,rhs2) = dest_pair tuple 54 val (lhs3,rhs3) = dest_pair new_tuple 55 val th1 = mk_new_post (lhs1,lhs2,lhs3) 56 val th2 = mk_new_post (rhs1,rhs2,rhs3) 57 val lemma = CONJ (DISCH_ALL th1) (DISCH_ALL th2) 58 val th = UNDISCH_ALL (MATCH_MP COMBINE1 lemma) handle HOL_ERR _ => 59 UNDISCH_ALL (MATCH_MP COMBINE2 lemma) handle HOL_ERR _ => 60 UNDISCH_ALL (MATCH_MP COMBINE3 lemma) handle HOL_ERR _ => 61 UNDISCH_ALL (MATCH_MP COMBINE4 lemma) 62 in th end 63 val lemma = mk_new_post (post,tuple,new_tuple) 64 val th = th |> CONV_RULE (RAND_CONV (K lemma)) 65 in add_DO_NOTHING th end 66 handle HOL_ERR e => (produce_TRIPLE_fail := th; raise (HOL_ERR e)); 67 fun last_fail () = !produce_TRIPLE_fail 68end 69 70fun triple_compose_list [] = add_DO_NOTHING TRIPLE_NOP 71 | triple_compose_list (th1::thms) = 72 let val th2 = triple_compose_list thms 73 in compose th1 th2 end 74 75fun remove_var_annotations th = let 76 fun fix_var_name v = let 77 val (s,ty) = dest_var v 78 val t = String.tokens (fn c => c = #"@") s 79 in if length t > 1 then mk_var (hd t,ty) else fail() end 80 fun fix_names tm = 81 if is_comb tm then 82 (RATOR_CONV fix_names THENC RAND_CONV fix_names) tm 83 else let 84 val (n,body) = dest_abs tm 85 in (ALPHA_CONV (fix_var_name n) THENC ABS_CONV fix_names) tm end 86 handle HOL_ERR _ => ALL_CONV tm 87 in CONV_RULE fix_names th end 88 89local 90 val format = SKIP_TAG_def |> SPEC_ALL |> concl |> dest_eq |> fst |> rator 91in 92 val is_SKIP_TAG = can (match_term format) 93end 94 95fun split_at P [] [] = [] 96 | split_at P [] aux = [rev aux] 97 | split_at P (x::xs) [] = 98 if P x then split_at P xs [] else split_at P xs [x] 99 | split_at P (x::xs) aux = 100 if P x then rev aux :: split_at P xs [] else split_at P xs (x::aux) 101 102fun compose_all_for sec_name = let 103 val xs = derive_specs_for sec_name 104 val ys = map (fn (_,(th,_,_),_) => th) xs 105 val yss = split_at (can (find_term is_SKIP_TAG) o concl) ys [] 106 val thms = map (fn ys => let 107 val zs = map produce_TRIPLE ys 108 val th = triple_compose_list zs 109 val th = remove_var_annotations th 110 |> REWRITE_RULE (!code_abbreviations) 111 |> REWRITE_RULE [DO_NOTHING_def] 112 in th end) yss 113 in thms end 114 115fun triples_for base_name = let 116 val _ = read_files base_name [] 117 in map (fn n => (n,compose_all_for n)) (section_names ()) end 118 119end 120