From 1bd4d678fb719a6a52ade232eb2b36a6e621677a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 21 Apr 2020 22:24:31 +0200
Subject: Require autogen

---
 driver/Compiler.vexpand  | 38 ++++----------------------------------
 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);;
-- 
cgit