1structure func_decompileLib :> func_decompileLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5open listTheory wordsTheory pred_setTheory
6open GraphLangTheory
7open backgroundLib file_readerLib derive_specsLib graph_specsLib exportLib;
8open writerLib cond_cleanLib;
9
10val _ = max_print_depth := ~1;
11val _ = set_trace "Unicode" 0;
12
13local
14  val export_fails = ref ([]:string list)
15in
16  fun add_export_fail sec_name = (export_fails := sec_name :: (!export_fails))
17  fun get_export_fails () = rev (!export_fails)
18  fun clear_export_fails () = (export_fails := [])
19end;
20
21local
22  val th = bit_field_insert |> SPEC_ALL |> REWRITE_RULE [LET_THM]
23  val pat = th |> UNDISCH |> concl |> dest_eq |> fst
24in
25  fun remove_bif_field_insert_conv tm = let
26    val (i,t) = match_term pat tm
27    val lemma = INST i (INST_TYPE t th)
28                |> CONV_RULE ((RATOR_CONV o RAND_CONV) EVAL)
29    val lemma = MP lemma TRUTH
30                |> CONV_RULE ((RAND_CONV o RAND_CONV) EVAL THENC
31                              RAND_CONV BETA_CONV)
32    in lemma end
33    handle HOL_ERR _ => NO_CONV tm
34end
35
36fun func_export sec_name th funcs_def = let
37  val f = th |> concl |> rand
38  val name = sec_name
39  val rhs = ``func_body_trans ^f``
40  val lhs = mk_var(name,type_of rhs)
41  val trans_def = new_definition(name,mk_eq(lhs,rhs))
42  val _ = write_subsection "Evaluating graph"
43  val c = REWRITE_CONV [func_body_trans_def,func_trans_def,funcs_def]
44          THENC REWRITE_CONV [wordsTheory.word_extract_mask,export_init_rw]
45          THENC (DEPTH_CONV remove_bif_field_insert_conv)
46          THENC EVAL THENC PURE_REWRITE_CONV [GSYM word_sub_def]
47          THENC prepare_for_export_conv
48  val lemma = trans_def |> CONV_RULE (RAND_CONV c)
49  val xs = lemma |> concl |> rand |> rator |> rand |> rand
50                 |> listSyntax.dest_list |> fst
51  val node_count = length xs |> int_to_string
52  val msg = "The graph for `" ^ sec_name ^ "` has " ^ node_count ^ " nodes."
53  val _ = write_line msg
54  val _ = (writer_prints := false)
55  val _ = map write_term xs
56  val _ = (writer_prints := true)
57  val ml_name = export_func lemma
58  in (trans_def," o " ^ ml_name) end
59  handle HOL_ERR _ => let
60    val _ = print ("Export FAILED for " ^ sec_name ^ ".\n")
61    val _ = add_export_fail sec_name
62    in (TRUTH,"") end;
63
64fun print_title (s:string) = ()
65
66fun get_loction_as_word sec_name = let
67  val tm = section_location sec_name
68           |> Arbnumcore.fromHexString |> numSyntax.mk_numeral
69  in ``n2w (^tm):word32`` end
70
71fun func_decompile print_title sec_name = let
72  val _ = (writer_prints := true)
73  val _ = open_current sec_name
74  val _ = print_title sec_name
75  val thms = derive_insts_for sec_name
76(*  val thms = clean_conds thms *)
77  val code = thms |> hd |> concl |> rator |> rator |> rand
78             handle Empty => (if !arch_name = ARM
79                              then ``(ARM {}):code``
80                              else ``(M0 {}):code``)
81  val lemma = prove(``LIST_IMPL_INST ^code locs []``,
82                    SIMP_TAC std_ss [LIST_IMPL_INST_def])
83  fun combine [] = lemma
84    | combine (th::thms) =
85        MATCH_MP IMP_LIST_IMPL_INST (CONJ th (combine thms))
86  val th = combine thms
87  val entry = th |> concl |> rand |> rator |> rand
88                 |> rator |> rator |> rand
89              handle HOL_ERR _ => get_loction_as_word sec_name
90  val th = MATCH_MP IMP_func_ok th |> Q.INST [`entry`|->`^entry`]
91  val goal = th |> concl |> dest_imp |> fst
92  val lemma = auto_prove "inst_locs_distinct"
93    (goal,REWRITE_TAC [MAP,inst_loc_def] \\ EVAL_TAC)
94  val th = MP th lemma
95  val entry = th |> concl |> rand |> rand |> listSyntax.dest_cons |> fst
96                 |> rator |> rator |> rand
97              handle HOL_ERR _ => get_loction_as_word sec_name
98  val name = stringSyntax.fromMLstring sec_name
99  val th = th |> Q.INST [`name`|->`^name`,`entry`|->`^entry`]
100  val funcs_def_rhs = th |> concl |> rand |> rand
101  val funcs_name = sec_name ^ "_funcs"
102  val funcs_def_lhs = mk_var(funcs_name,type_of funcs_def_rhs)
103  val funcs_def = new_definition(funcs_name,``^funcs_def_lhs = ^funcs_def_rhs``)
104  val th = CONV_RULE (RAND_CONV (RAND_CONV (REWR_CONV (GSYM funcs_def)))) th
105  in (th,func_export sec_name th funcs_def) end
106
107fun list_mk_union [] = ``{}:'a set``
108  | list_mk_union [x] = x
109  | list_mk_union (x::xs) = pred_setSyntax.mk_union(list_mk_union xs,x)
110
111(*
112  val sec_name = "bi_finalise"
113*)
114
115fun prove_funcs_ok names = let
116  val _ = clear_stack_intro_fails ()
117  val _ = clear_graph_spec_fails ()
118  val _ = clear_export_fails ()
119  fun print_title sec_name = let
120    fun find_index [] = ~2000
121      | find_index (x::xs) = if x = sec_name then 1 else find_index xs + 1
122    val i = find_index names
123    val str = "Section " ^ sec_name ^ " (" ^
124                int_to_string i ^ " of " ^ int_to_string (length names) ^ ")"
125    in write_section str end
126  (* decompile all sections *)
127  val fs_and_trans_defs = map (func_decompile print_title) names
128  val fs = map fst fs_and_trans_defs
129  (* abbreviate all codes *)
130  val all_code = fs |> map (rand o rator o rator o concl)
131  val code_name = all_code |> hd |> rator
132  val all_code = mk_comb(code_name, (all_code |> map rand |> list_mk_union))
133  val all_code_def = new_definition("all_code",``all_code = ^all_code``);
134  val code_case_of = TypeBase.case_def_of ``:code``;
135  val pair_case_of = TypeBase.case_def_of ``:'a # 'b``;
136  fun expend_code th = let
137    val th = MATCH_MP func_ok_EXPEND_CODE th |> Q.SPEC `all_code`
138    val goal = th |> concl |> dest_imp |> fst
139    val lemma = auto_prove "expand_code" (goal,
140      REWRITE_TAC [all_code_def,SUBSET_DEF,IN_UNION,code_case_of,pair_case_of]
141      \\ CONV_TAC (DEPTH_CONV BETA_CONV)
142      \\ REWRITE_TAC [all_code_def,SUBSET_DEF,IN_UNION,code_case_of,pair_case_of]
143      \\ CONV_TAC (DEPTH_CONV BETA_CONV)
144      \\ REWRITE_TAC [all_code_def,SUBSET_DEF,IN_UNION,code_case_of,pair_case_of]
145      \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [])
146    in MP th lemma end
147  val fs = map expend_code fs
148  (* complete fs *)
149  val fs = let
150    val all = fs |> map (rand o concl)
151    val pat = ``locs (name:string) = SOME (w:word32)``
152    fun f tm = subst (fst (match_term pat tm)) ``Func name w []``
153    val extra = graph_specsLib.try_map (fn x => x) f (flatten (map hyp fs))
154    val all_rator = map rator all
155    val extra = filter (fn ex => not (mem (rator ex) all_rator)) extra
156    val r = fs |> hd |> concl |> rator
157    val extra_fs = map (fn tm => prove(mk_comb(r,tm),
158                     SIMP_TAC (srw_ss()) [func_ok_def])) extra
159    fun export_empty th = let
160      val sec_name = th |> concl |> rand |> rator |> rator |> rand
161                        |> stringLib.fromHOLstring
162      in func_export sec_name th TRUTH end
163    val _ = map export_empty extra_fs
164    in fs @ extra_fs end
165  (* package up into funcs_ok *)
166  val code = fs |> hd |> concl |> rator |> rator |> rand
167  val lemma = prove(``EVERY (func_ok ^code locs) []``,
168                    SIMP_TAC std_ss [EVERY_DEF])
169  fun combine [] = lemma
170    | combine (th::thms) =
171        MATCH_MP IMP_EVERY_func_ok (CONJ th (combine thms))
172  val th = combine fs
173  val funcs = th |> concl |> rand
174  val th = th |> Q.INST [`locs`|->`fs_locs ^funcs`]
175              |> CONV_RULE (REWR_CONV (GSYM funcs_ok_def))
176              |> DISCH_ALL |> DISCH T
177              |> PURE_REWRITE_RULE [fs_locs_def,AND_IMP_INTRO]
178  val goal = th |> concl |> dest_imp |> fst
179  val _ = write_line ""
180  val _ = write_section "Proving correctness of call offsets"
181  fun prove_fs_locs goal =
182    if goal = T then (TRUTH,true) else
183    if is_conj goal then let
184      val (x,y) = dest_conj goal
185      val (th1,s1) = prove_fs_locs x
186      val (th2,s2) = prove_fs_locs y
187      in (CONJ th1 th2, s1 andalso s2) end
188    else (MATCH_MP EQ_T (EVAL goal), true)
189      handle HOL_ERR _ => let
190        val (lhs,rhs) = dest_eq goal
191        val name = lhs |> rand |> stringSyntax.fromHOLstring
192        val v = optionSyntax.dest_some rhs |> rand
193                   |> numSyntax.int_of_term |> int_to_hex
194        val _ = write_line ("Failed to prove that " ^ name ^ " is at " ^ v ^ ".")
195        in (mk_thm([],goal),false) end
196      handle HOL_ERR _ => failwith "internal error"
197  val (lemma,fs_locs_success) = prove_fs_locs goal
198  val th = MP th lemma
199  fun print_fs_locs_success () =
200    write_line (if fs_locs_success
201                then "No call offset failures."
202                else "Failed to prove correctness of some call offsets.")
203  val _ = if fs_locs_success then write_line "Offsets proved correct." else ()
204  (* export top-level graph definition *)
205  val funcs = th |> concl |> rand
206  val trans_defs = map (fst o snd) fs_and_trans_defs
207  val name = "complete_graph"
208  val _ = open_current name
209  val rhs = ``list_func_trans ^funcs``
210  val lhs = mk_var(name,type_of rhs)
211  val graph = new_definition(name,mk_eq(lhs,rhs))
212  val c = REWRITE_CONV [list_func_trans_thm] THENC EVAL
213          THENC REWRITE_CONV (map GSYM trans_defs)
214          THENC prepare_for_export_conv
215  val lemma = graph |> CONV_RULE (RAND_CONV c)
216  val _ = write_section "Summary"
217  val _ = print_stack_intro_report ()
218  val _ = print_graph_spec_report ()
219  val _ = print_export_report ()
220  val _ = print_fs_locs_success ()
221  val _ = close_current ()
222  in th end
223
224(*
225
226  val base_name = "loop-m0/example"
227  val base_name = "kernel-gcc-O1/kernel"
228  val () = read_files base_name ["f"]
229  val _ = (skip_proofs := true)
230  val _ = (skip_proofs := false)
231  val names = section_names()
232
233  local val randgen = Random.newgen()
234  in fun get_rand_name () =
235       el (Random.range(1,length names) randgen) names end
236
237  val _ = func_decompile print_title (get_rand_name ());
238  val _ = func_decompile print_title sec_name;
239
240  val _ = max_print_depth := 5;
241
242  val th = prove_funcs_ok names
243
244*)
245
246end
247