diff options
| -rw-r--r-- | driver/Compiler.vexpand | 38 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 30 |
2 files changed, 26 insertions, 42 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 4c7c963a..d0ba33d3 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -35,22 +35,7 @@ Require Cshmgen. Require Cminorgen. Require Selection. Require RTLgen. -Require Tailcall. -Require Inlining. -Require Profiling. -Require ProfilingExploit. -Require FirstNop. -Require Renumber. -Require Duplicate. -Require Constprop. -Require LICM. -Require CSE. -Require ForwardMoves. -Require CSE2. -Require CSE3. -Require Deadcode. -Require Unusedglob. -Require Allnontrap. +EXPAND_RTL_REQUIRE Require Allocation. Require Tunneling. Require Linearize. @@ -65,22 +50,7 @@ Require Cshmgenproof. Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. -Require Tailcallproof. -Require Inliningproof. -Require Profilingproof. -Require ProfilingExploitproof. -Require FirstNopproof. -Require Renumberproof. -Require Duplicateproof. -Require Constpropproof. -Require LICMproof. -Require CSEproof. -Require ForwardMovesproof. -Require CSE2proof. -Require CSE3proof. -Require Deadcodeproof. -Require Unusedglobproof. -Require Allnontrapproof. +EXPAND_RTL_REQUIRE_PROOF Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -138,7 +108,7 @@ Definition partial_if {A: Type} Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) -EXPAND_TRANSF_PROGRAM +EXPAND_RTL_TRANSF_PROGRAM @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -308,7 +278,7 @@ Proof. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Unusedglob.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 63808c1f..7ca3c755 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -1,7 +1,7 @@ type is_partial = TOTAL | PARTIAL;; type when_triggered = Always | Option of string;; -let passes = +let rtl_passes = [| TOTAL, (Option "optim_tailcalls"), (Some "Tail calls"), "Tailcall"; PARTIAL, Always, (Some "Inlining"), "Inlining"; @@ -25,7 +25,17 @@ PARTIAL, Always, (Some "Unused globals"), "Unusedglob" let totality = function TOTAL -> "total" | PARTIAL -> "partial";; -let print_transf oc = +let print_rtl_require oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + Printf.fprintf oc "Require %s.\n" pass_name) + rtl_passes;; + +let print_rtl_require_proof oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + Printf.fprintf oc "Require %sproof.\n" pass_name) + rtl_passes;; + +let print_rtl_transf oc = Array.iteri (fun i (partial, trigger, time_label, pass_name) -> output_string oc (match partial with @@ -42,7 +52,7 @@ let print_transf oc = Printf.fprintf oc "time \"%s\" " s); Printf.fprintf oc "%s.transf_program)\n" pass_name; Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i) - ) passes;; + ) rtl_passes;; if (Array.length Sys.argv)<>3 then exit 1;; @@ -52,11 +62,15 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in try while true do - let line = input_line ic in - if line = "EXPAND_TRANSF_PROGRAM" - then print_transf oc - else (output_string oc line; - output_char oc '\n') + match input_line ic with + | "EXPAND_RTL_TRANSF_PROGRAM" -> + print_rtl_transf oc + | "EXPAND_RTL_REQUIRE" -> + print_rtl_require oc + | "EXPAND_RTL_REQUIRE_PROOF" -> + print_rtl_require_proof oc + | line -> (output_string oc line; + output_char oc '\n') done with End_of_file -> (close_in ic; close_out oc);; |