machine-code/decompiler/decompilerLib.sml

547   (* attempt to find common exit point *)
555   val exit = (all_distinct o map last o filter (not o is_loop)) paths
556   val zero = ([0],exit)
557   val zs = if filter (fn (x,y) => mem 0 x andalso subset exit y) zs = []
575     val exit = diff (all_distinct (append_lists (map snd loops))) entry
576     in [(sort (fn x => fn y => (x <= y)) entry,exit)] end
637 (* multi-entry/exit preformatting *)
744 fun tree_composition (th,i:int,thms,entry,exit,conds,firstTime) =
746   if mem i exit then LEAF (th,i) else let
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
796              val t = tree_composition (th,i,thms,entry,exit,conds,firstTime)
1546 fun extract_function name th entry exit function_in_out = let
1578   val exit_tm = gen_pc (hd exit)
1815 fun decompile_part name thms (entry,exit)
1817   val t = generate_spectree thms (entry,exit)
1819   val (th,def,pre) = extract_function name th entry exit function_in_out
1833     | decompile_all thms (defs,pres) ((entry,exit)::loops) prev = let
1835   val (entry,exit)::loops = loops
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
1846   val exit = snd (last loops)
1847   val _ = add_decompiled (name,result,hd exit,SOME (hd exit))
1868   val (entry,exit) = (fn (x,y) => (hd x, hd y)) (last loops)
1869   val (entry,exit) = ([entry],[exit])
1870   val (def,pre,result) = decompile_part name thms (entry,exit) function_in_out
1871   val _ = add_decompiled (name,result,hd exit,SOME (hd exit))