diff options
-rw-r--r-- | Makefile | 5 | ||||
-rw-r--r-- | backend/Unusedglob.v | 2 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 4 | ||||
-rw-r--r-- | driver/Compiler.vexpand (renamed from driver/Compiler.v) | 37 | ||||
-rw-r--r-- | tools/compiler_expand.ml | 62 |
5 files changed, 71 insertions, 39 deletions
@@ -201,6 +201,8 @@ tools/ndfun: tools/ndfun.ml ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml tools/modorder: tools/modorder.ml ocamlopt -o tools/modorder str.cmxa tools/modorder.ml +tools/compiler_expand: tools/compiler_expand.ml + ocamlopt -o $@ $+ latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -216,6 +218,9 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod a-w $*.v +driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand + tools/compiler_expand driver/Compiler.vexpand $@ + compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ echo "prepro=$(CPREPRO)"; \ diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 93ca7af4..3b8e19ad 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -126,7 +126,7 @@ Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef u Definition global_defined (p: program) (pm: prog_map) (id: ident) : bool := match pm!id with Some _ => true | None => ident_eq id (prog_main p) end. -Definition transform_program (p: program) : res program := +Definition transf_program (p: program) : res program := let pm := prog_defmap p in match used_globals p pm with | None => Error (msg "Unusedglob: analysis failed") diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index fa120b6d..160c0b18 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -428,9 +428,9 @@ Qed. End TRANSFORMATION. Theorem transf_program_match: - forall p tp, transform_program p = OK tp -> match_prog p tp. + forall p tp, transf_program p = OK tp -> match_prog p tp. Proof. - unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *. + unfold transf_program; intros p tp TR. set (pm := prog_defmap p) in *. destruct (used_globals p pm) as [u|] eqn:U; try discriminate. destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR. exists u; split. diff --git a/driver/Compiler.v b/driver/Compiler.vexpand index 69041ab0..4c7c963a 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.vexpand @@ -138,42 +138,7 @@ Definition partial_if {A: Type} Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) - @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program) - @@ print (print_RTL 1) - @@@ time "Inlining" Inlining.transf_program - @@ print (print_RTL 2) - @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) - @@ print (print_RTL 3) - @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) - @@ print (print_RTL 4) - @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) - @@ print (print_RTL 5) - @@ time "Renumbering" Renumber.transf_program - @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) - @@ print (print_RTL 7) - @@ time "Renumbering pre constprop" Renumber.transf_program - @@ print (print_RTL 8) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) - @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) - @@ print (print_RTL 10) - @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) - @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) - @@ print (print_RTL 12) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) - @@ print (print_RTL 13) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) - @@ print (print_RTL 14) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program - @@ print (print_RTL 15) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) - @@ print (print_RTL 16) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@ print (print_RTL 17) - @@@ time "Unused globals" Unusedglob.transform_program - @@ print (print_RTL 18) +EXPAND_TRANSF_PROGRAM @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml new file mode 100644 index 00000000..63808c1f --- /dev/null +++ b/tools/compiler_expand.ml @@ -0,0 +1,62 @@ +type is_partial = TOTAL | PARTIAL;; +type when_triggered = Always | Option of string;; + +let passes = +[| +TOTAL, (Option "optim_tailcalls"), (Some "Tail calls"), "Tailcall"; +PARTIAL, Always, (Some "Inlining"), "Inlining"; +TOTAL, (Option "profile_arcs"), (Some "Profiling insertion"), "Profiling"; +TOTAL, (Option "branch_probabilities"), (Some "Profiling use"), "ProfilingExploit"; +TOTAL, (Option "optim_move_loop_invariants"), (Some "Inserting initial nop"), "FirstNop"; +TOTAL, Always, (Some "Renumbering"), "Renumber"; +PARTIAL, (Option "optim_duplicate"), (Some "Tail-duplicating"), "Duplicate"; +TOTAL, Always, (Some "Renumbering pre constprop"), "Renumber"; +TOTAL, (Option "optim_constprop"), (Some "Constant propagation"), "Constprop"; +PARTIAL, (Option "optim_move_loop_invariants"), (Some "LICM"), "LICM"; +TOTAL, (Option "optim_move_loop_invariants"), (Some "Renumbering pre CSE"), "Renumber"; +PARTIAL, (Option "optim_CSE"), (Some "CSE"), "CSE"; +TOTAL, (Option "optim_CSE2"), (Some "CSE2"), "CSE2"; +PARTIAL, (Option "optim_CSE3"), (Some "CSE3"), "CSE3"; +TOTAL, (Option "optim_forward_moves"), (Some "Forwarding moves"), "ForwardMoves"; +PARTIAL, (Option "optim_redundancy"), (Some "Redundancy elimination"), "Deadcode"; +TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; +PARTIAL, Always, (Some "Unused globals"), "Unusedglob" +|];; + +let totality = function TOTAL -> "total" | PARTIAL -> "partial";; + +let print_transf oc = + Array.iteri + (fun i (partial, trigger, time_label, pass_name) -> + output_string oc (match partial with + | TOTAL -> " @@ " + | PARTIAL -> " @@@ "); + (match trigger with + | Always -> () + | Option s -> + Printf.fprintf oc "%s_if Compopts.%s " (totality partial) s); + output_char oc '('; + (match time_label with + | None -> () + | Some s -> + 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;; + +if (Array.length Sys.argv)<>3 +then exit 1;; + +let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in + let ic = open_in filename_in and oc = open_out filename_out 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') + done + with End_of_file -> + (close_in ic; close_out oc);; |