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
36(*
37val funcs_def = TRUTH
38*)
39
40fun func_export sec_name th funcs_def = let
41  val f = th |> concl |> rand
42  val name = sec_name
43  val rhs = ``func_body_trans ^f``
44  val lhs = mk_var(name,type_of rhs)
45  val name = tidy_up_name name
46  val trans_def = new_definition(name,mk_eq(lhs,rhs))
47  val _ = write_subsection "Evaluating graph"
48  val c = REWRITE_CONV [func_body_trans_def,func_trans_def,funcs_def]
49          THENC REWRITE_CONV [wordsTheory.word_extract_mask,export_init_rw]
50          THENC EVAL THENC PURE_REWRITE_CONV [GSYM word_sub_def]
51          THENC (DEPTH_CONV remove_bif_field_insert_conv)
52          THENC prepare_for_export_conv
53  val lemma = trans_def |> CONV_RULE (RAND_CONV c)
54  val xs = lemma |> concl |> rand |> rator |> rand |> rand
55                 |> listSyntax.dest_list |> fst
56  val node_count = length xs |> int_to_string
57  val msg = "The graph for `" ^ sec_name ^ "` has " ^ node_count ^ " nodes."
58  val _ = write_line msg
59  val _ = (writer_prints := false)
60  val _ = map write_term xs
61  val _ = (writer_prints := true)
62  val ml_name = export_func lemma
63  in (trans_def," o " ^ ml_name) end
64  handle HOL_ERR _ => let
65    val _ = print ("Export FAILED for " ^ sec_name ^ ".\n")
66    val _ = add_export_fail sec_name
67    in (TRUTH,"") end;
68
69fun print_title (s:string) = ()
70
71fun get_loction_as_word sec_name = let
72  val str = section_location sec_name
73  val str = if size str <= 8 then str else String.substring(str,8,size str - 8)
74  val tm = str |> Arbnumcore.fromHexString |> numSyntax.mk_numeral
75  in wordsSyntax.mk_n2w(tm,tysize ()) end
76
77val sec_name = "f"
78
79fun func_decompile print_title sec_name = let
80  val _ = (writer_prints := true)
81  val _ = open_current sec_name
82  val _ = print_title sec_name
83  val thms = derive_insts_for sec_name
84(*  val thms = clean_conds thms *)
85  val code = thms |> hd |> concl |> rator |> rator |> rand
86             handle Empty => (case !arch_name of
87                                ARM => ``ARM {}``
88                              | M0 => ``M0 {}``
89                              | RISCV => ``RISCV {}``)
90  val lemma = prove(``LIST_IMPL_INST ^code locs []``,
91                    SIMP_TAC std_ss [LIST_IMPL_INST_def])
92  fun combine [] = lemma
93    | combine (th::thms) =
94        MATCH_MP IMP_LIST_IMPL_INST (CONJ th (combine thms))
95  val th = combine thms
96  val entry = th |> concl |> rand |> rator |> rand
97                 |> rator |> rator |> rand
98              handle HOL_ERR _ => get_loction_as_word sec_name
99  val th = MATCH_MP IMP_func_ok th |> Q.INST [`entry`|->`^entry`]
100  val goal = th |> concl |> dest_imp |> fst
101  val lemma = auto_prove "inst_locs_distinct"
102    (goal,REWRITE_TAC [MAP,inst_loc_def] \\ EVAL_TAC)
103  val th = MP th lemma
104  val entry = th |> concl |> rand |> rand |> listSyntax.dest_cons |> fst
105                 |> rator |> rator |> rand
106              handle HOL_ERR _ => get_loction_as_word sec_name
107  val name = stringSyntax.fromMLstring sec_name
108  val th = th |> Q.INST [`name`|->`^name`,`entry`|->`^entry`]
109  val funcs_def_rhs = th |> concl |> rand |> rand
110  val funcs_name = sec_name ^ "_funcs"
111  val funcs_name = tidy_up_name funcs_name
112  val funcs_def_lhs = mk_var(funcs_name,type_of funcs_def_rhs)
113  val funcs_def = new_definition(funcs_name,``^funcs_def_lhs = ^funcs_def_rhs``)
114  val th = CONV_RULE (RAND_CONV (RAND_CONV (REWR_CONV (GSYM funcs_def)))) th
115  in (th,func_export sec_name th funcs_def) end
116
117fun list_mk_union [] = ``{}:'a set``
118  | list_mk_union [x] = x
119  | list_mk_union (x::xs) = pred_setSyntax.mk_union(list_mk_union xs,x)
120
121fun arch_to_string () =
122  case !arch_name of
123    RISCV => "riscv"
124  | ARM => "arm"
125  | M0 => "m0";
126
127(*
128  val sec_name = "bi_finalise"
129*)
130
131fun prove_funcs_ok names = let
132  val _ = clear_stack_intro_fails ()
133  val _ = clear_graph_spec_fails ()
134  val _ = clear_export_fails ()
135  fun print_title sec_name = let
136    fun find_index [] = ~2000
137      | find_index (x::xs) = if x = sec_name then 1 else find_index xs + 1
138    val i = find_index names
139    val str = "Section " ^ sec_name ^ " (" ^
140                int_to_string i ^ " of " ^ int_to_string (length names) ^ ")"
141    in write_section str end
142  (* decompile all sections *)
143  val fs_and_trans_defs = map (func_decompile print_title) names
144  val fs = map fst fs_and_trans_defs
145  (* abbreviate all codes *)
146(*
147  val bad_fs = fs |> filter (can (find_term pred_setSyntax.is_empty) o
148                             rand o rator o rator o concl)
149  val fs = fs |> filter (not o can (find_term pred_setSyntax.is_empty) o
150                         rand o rator o rator o concl)
151*)
152  val all_code = fs |> map (rand o rator o rator o concl)
153  val code_name = all_code |> hd |> rator
154  val all_code = mk_comb(code_name, (all_code |> map rand |> list_mk_union))
155  val all_code_name = "all_" ^ arch_to_string () ^ "_code"
156  val all_code_var = mk_var(all_code_name,type_of all_code)
157  val all_code_def = new_definition(all_code_name,mk_eq(all_code_var,all_code))
158  val all_code_const = all_code_def |> concl |> dest_eq |> fst
159  val pair_case_of = TypeBase.case_def_of ``:'a # 'b``;
160  fun expend_code th = let
161    val th = MATCH_MP func_ok_EXPEND_CODE th |> SPEC all_code_const
162    val goal = th |> concl |> dest_imp |> fst
163    val lemma = auto_prove "expand_code" (goal,
164      REWRITE_TAC [all_code_def,SUBSET_DEF,IN_UNION,pair_case_of,
165                   ARM_def,M0_def,RISCV_def]
166      \\ CONV_TAC (DEPTH_CONV BETA_CONV)
167      \\ REWRITE_TAC [all_code_def,SUBSET_DEF,IN_UNION,pair_case_of]
168      \\ CONV_TAC (DEPTH_CONV BETA_CONV)
169      \\ REWRITE_TAC [all_code_def,SUBSET_DEF,IN_UNION,pair_case_of]
170      \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [])
171    in MP th lemma end
172  val fs = map expend_code fs
173  (* complete fs *)
174  val _ = write_subsection "\nCompleting graph"
175  val fs = let
176    val all = fs |> map (rand o concl)
177    val w_var = mk_var("w",wsize ())
178    val pat = ``locs (name:string) = SOME ^w_var``
179    fun f tm = subst (fst (match_term pat tm)) ``Func name ^w_var []``
180    val extra = graph_specsLib.try_map (fn x => x) f (flatten (map hyp fs))
181    val all_rator = map rator all
182    val extra = filter (fn ex => not (term_mem (rator ex) all_rator)) extra
183    val r = fs |> hd |> concl |> rator
184    val extra_fs = map (fn tm => prove(mk_comb(r,tm),
185                     SIMP_TAC (srw_ss()) [func_ok_def])) extra
186    (*
187    val th = hd extra_fs
188    val th = mk_thm([],``func_ok all_riscv_code locs (Func "__ctzdi2" 2147580890w [])``)
189    *)
190    fun export_empty th = let
191      val sec_name = th |> concl |> rand |> rator |> rator |> rand
192                        |> stringLib.fromHOLstring
193      in func_export sec_name th TRUTH end
194    val _ = map export_empty extra_fs
195    in fs @ extra_fs end
196  (* package up into funcs_ok *)
197  val code = fs |> hd |> concl |> rator |> rator |> rand
198  val lemma = prove(``EVERY (func_ok ^code locs) []``,
199                    SIMP_TAC std_ss [EVERY_DEF])
200  fun combine [] = lemma
201    | combine (th::thms) =
202        MATCH_MP IMP_EVERY_func_ok (CONJ th (combine thms))
203  val th = combine fs
204  val funcs = th |> concl |> rand
205  val th = th |> Q.INST [`locs`|->`fs_locs ^funcs`]
206              |> CONV_RULE (REWR_CONV (GSYM funcs_ok_def))
207              |> DISCH_ALL |> DISCH T
208              |> PURE_REWRITE_RULE [fs_locs_def,AND_IMP_INTRO]
209  val goal = th |> concl |> dest_imp |> fst
210  val _ = write_line ""
211  val _ = write_section "Proving correctness of call offsets"
212  fun prove_fs_locs goal =
213    if aconv goal T then (TRUTH,true) else
214    if is_conj goal then let
215      val (x,y) = dest_conj goal
216      val (th1,s1) = prove_fs_locs x
217      val (th2,s2) = prove_fs_locs y
218      in (CONJ th1 th2, s1 andalso s2) end
219    else (MATCH_MP EQ_T (EVAL goal), true)
220      handle HOL_ERR _ => let
221        val (lhs,rhs) = dest_eq goal
222        val name = lhs |> rand |> stringSyntax.fromHOLstring
223        val v = optionSyntax.dest_some rhs |> rand
224                   |> numSyntax.int_of_term |> int_to_hex
225        val _ = write_line ("Failed to prove that " ^ name ^ " is at " ^ v ^ ".")
226        in (mk_thm([],goal),false) end
227      handle HOL_ERR _ => failwith "internal error"
228  val (lemma,fs_locs_success) = prove_fs_locs goal
229  val th = MP th lemma
230  fun print_fs_locs_success () =
231    write_line (if fs_locs_success
232                then "No call offset failures."
233                else (has_failures := true;
234                      "Failed to prove correctness of some call offsets."))
235  val _ = if fs_locs_success then write_line "Offsets proved correct." else ()
236  (* export top-level graph definition *)
237  val funcs = th |> concl |> rand
238  val trans_defs = map (fst o snd) fs_and_trans_defs
239  val name = "complete_graph"
240  val _ = open_current name
241  val rhs = ``list_func_trans ^funcs``
242  val lhs = mk_var(name,type_of rhs)
243  val graph = new_definition(name,mk_eq(lhs,rhs))
244  val c = REWRITE_CONV [list_func_trans_thm] THENC EVAL
245          THENC REWRITE_CONV (map GSYM trans_defs)
246          THENC prepare_for_export_conv
247  val lemma = graph |> CONV_RULE (RAND_CONV c)
248  val _ = write_section "Summary"
249  val _ = print_stack_intro_report ()
250  val _ = print_graph_spec_report ()
251  val _ = print_export_report ()
252  val _ = print_fs_locs_success ()
253  val _ = close_current ()
254  in th end
255
256(*
257
258  val base_name = "kernel-riscv/kernel-riscv"
259  val base_name = "loop-riscv/example"
260  val base_name = "seL4-kernel/arm/kernel"
261  val _ = read_files base_name []
262  val _ = open_current "test"
263  val sec_name = "lookupSlot"
264  val sec_name = "memzero"
265  val sec_name = "memcpy"
266  val sec_name = "isIRQPending"
267  val sec_name = "get_num_avail_p_regs"
268  val sec_name = "ndks_boot"
269  val sec_name = "num_avail_p_regs"
270  val sec_name = "resolveAddressBits"
271
272  val names = ["performInvocation_Reply","performInvocation_Endpoint"]
273  val names = section_names()
274
275  val base_name = "loop-riscv/example"
276  val _ = read_files base_name []
277  val _ = open_current "test"
278  val sec_name = "memcpy"
279  val sec_name = "memzero"
280  val names = section_names()
281
282  val base_name = "kernel-gcc-O1/kernel"
283  val base_name = "loop/example"
284  val base_name = "loop-m0/example"
285  val () = read_files base_name []
286  val _ = (skip_proofs := true)
287  val _ = (skip_proofs := false)
288  val names = section_names()
289
290  val sec_name = "g"
291
292  local val randgen = Random.newgen()
293  in fun get_rand_name () =
294       el (Random.range(1,length names) randgen) names end
295
296  val _ = func_decompile print_title (get_rand_name ());
297  val _ = func_decompile print_title sec_name;
298
299  val _ = max_print_depth := 5;
300
301  val th = prove_funcs_ok names
302
303*)
304
305end
306