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