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