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