machine-code/decompiler/decompilerLib.sml

44 fun add_code_abbrev thms = (code_abbreviations := thms @ !code_abbreviations);
311 fun introduce_guards thms = let
337   val thms = map intro thms
338   in thms end
382 fun inst_pc_var tools thms = let
409   in map (triple_apply f) thms end
424 fun abbreviate_code name thms = let
427   val cs = map extract_code thms
432   val (_,(th,_,_),_) = hd thms
459   val thms = map (triple_apply foo) thms
460   in thms end
464      val thms = derive_individual_specs tools code
465      val thms = inst_pc_var tools thms
466      val thms = abbreviate_code name thms
468      thms
476 fun extract_graph thms = let
479   val jumps = append_lists (map extract_jumps thms)
582       val thms = stage_1 name tools code
583       val jumps = extract_graph thms
586       (thms, loops)
639 fun format_for_multi_entry entry thms = let
689   val thms = map (apply process) thms
690   in (case_list,thms) end handle HOL_ERR _ => ([],thms);
744 fun tree_composition (th,i:int,thms,entry,exit,conds,firstTime) =
747     val (_,thi1,thi2) = number_GUARD (find_first i thms)
753                tree_composition (th2,the i2,thms,entry,exit,conds,false)
758                        (th1,the i1,thms,entry,exit,cond'::conds,false)
760                        (th2,the i2,thms,entry,exit,negate cond'::conds,false)
765        val result = tree_composition (th,the i,thms,entry,exit,conds,false)
779 fun generate_spectree thms (entry,exit) = let
781   val (_,(th,_,_),_) = hd thms
786   val thms = map (apply_to_th (RW [hide_th])) thms
787   val (case_list,thms) = format_for_multi_entry entry thms
788   val (_,(th,_,_),_) = hd thms
796              val t = tree_composition (th,i,thms,entry,exit,conds,firstTime)
1815 fun decompile_part name thms (entry,exit)
1817   val t = generate_spectree thms (entry,exit)
1830   val (thms,loops) = stage_12 name tools (q code)
1831   fun decompile_all thms (defs,pres) [] prev =
1833     | decompile_all thms (defs,pres) ((entry,exit)::loops) prev = let
1842          decompile_part part_name thms (entry,exit) function_in_out
1843       val thms = prepare_for_reuse entry (result,0,SOME (hd exit)) 0 @ thms
1844       in decompile_all thms (def::defs,pre::pres) loops result end
1845   val (def,pre,result) = decompile_all thms ([],[]) loops TRUTH
1867   val (thms,loops) = stage_12 name tools (q code)
1870   val (def,pre,result) = decompile_part name thms (entry,exit) function_in_out