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