begin scripting the Compiler.v file

5 files changed, 71 insertions, 39 deletions

diff --git a/Makefile b/Makefile
index a69f7e2e..2f9ab029 100644
--- a/Makefile
+++ b/Makefile
@@ -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);;