SSA chain makes it possible to rerun CSE3 after

6 files changed, 59 insertions, 10 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index ab95b3ed..f1f7ba52 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -29,6 +29,7 @@ let option_fcse = ref true
 let option_fcse2 = ref false
 
 let option_fcse3 = ref true
+let option_fcse3_2 = ref true
 let option_fcse3_alias_analysis = ref true
 let option_fcse3_across_calls = ref false
 let option_fcse3_across_merges = ref true
@@ -105,6 +106,7 @@ let option_div_i64 = ref "stsud"
 let option_fcoalesce_mem = ref true
 let option_fforward_moves = ref false
 let option_fmove_loop_invariants = ref false
+let option_fmove_loop_invariants_2 = ref false
 let option_fnontrap_loads = ref true
 let option_all_loads_nontrap = ref false
 let option_inline_auto_threshold = ref 0
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index 00d0815e..01999a37 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -157,6 +157,7 @@ EXPAND_RTL_TRANSF_PROGRAM
   @@@ time "RTLdpar" RTLdpar.transl_program
    @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 100)
+EXPAND_POST_SSA_TRANSF_PROGRAM
 EXPAND_POST_RTL_TRANSF_PROGRAM
   @@@ time "Total Mach->Asm generation" Asmgen.transf_program.
 
@@ -292,6 +293,7 @@ EXPAND_RTL_MKPASS
   ::: mkpass RTLparcleanup.match_prog
   ::: mkpass RTLdparproof.match_prog
   ::: mkpass Renumberproof.match_prog
+EXPAND_POST_SSA_MKPASS
 EXPAND_POST_RTL_MKPASS
   ::: mkpass Asmgenproof.match_prog
   ::: pass_nil _.
@@ -388,7 +390,9 @@ EXPAND_RTL_PROOF
   destruct (RTLparcleanup.transl_program p147) as [p148|e] eqn: P148; cbn in T; try discriminate.
   destruct (RTLdpar.transl_program p148) as [p149|e] eqn:P149; cbn in T; try discriminate.
 
-  set (post_rtl0 := Renumber.transf_program p149) in *.
+  set (post_ssa0 := Renumber.transf_program p149) in *.
+EXPAND_POST_SSA_PROOF
+  set (post_rtl0 := post_ssa_last) in *.
 EXPAND_POST_RTL_PROOF
 
   unfold match_prog_SSA; simpl.
@@ -412,8 +416,9 @@ EXPAND_RTL_PROOF2
   exists p148; split. apply RTLparcleanup.transf_program_match; auto.
   exists p149; split. apply RTLdparproof.transf_program_match; auto.
 
-  exists post_rtl0; split. apply Renumberproof.transf_program_match; auto.
+  exists post_ssa0; split. apply Renumberproof.transf_program_match; auto.
 
+EXPAND_POST_SSA_PROOF2
 EXPAND_POST_RTL_PROOF2
   exists tp; split. apply Asmgenproof.transf_program_match; auto.
   reflexivity.
@@ -581,6 +586,9 @@ EXPAND_RTL_FORWARD_SIMULATIONS
 
    eapply compose_forward_simulations.
     eapply Renumberproof.transf_program_correct; eassumption.
+
+EXPAND_POST_SSA_FORWARD_SIMULATIONS
+
   eapply compose_forward_simulations.
     eapply Allocationproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 0c90ee52..c8ca68c6 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -42,6 +42,9 @@ Parameter optim_CSE2: unit -> bool.
 (** Flag -fcse3.  For DMonniaux's common subexpression elimination. *)
 Parameter optim_CSE3: unit -> bool.
 
+(** Flag -fcse3_2.  For DMonniaux's common subexpression elimination. *)
+Parameter optim_CSE3_2: unit -> bool.
+
 (** Flag -fcse3-alias-analysis.  For DMonniaux's common subexpression elimination. Perform a simple alias analysis. *)
 Parameter optim_CSE3_alias_analysis: unit -> bool.
 
@@ -60,6 +63,9 @@ Parameter optim_CSE3_trivial_ops: unit -> bool.
 (** Flag -fmove-loop-invariants. *)
 Parameter optim_move_loop_invariants: unit -> bool.
 
+(** Flag -fmove-loop-invariants_2. *)
+Parameter optim_move_loop_invariants_2: unit -> bool.
+
 (** Flag -fredundancy.  For dead code elimination. *)
 Parameter optim_redundancy: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 9abce51a..adcbb8be 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -452,12 +452,14 @@ let cmdline_actions =
   @ f_opt "cse" option_fcse
   @ f_opt "cse2" option_fcse2
   @ f_opt "cse3" option_fcse3
+  @ f_opt "cse3_2" option_fcse3_2
   @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis
   @ f_opt "cse3-across-calls" option_fcse3_across_calls
   @ f_opt "cse3-across-merges" option_fcse3_across_merges
   @ f_opt "cse3-glb" option_fcse3_glb
   @ f_opt "cse3-trivial-ops" option_fcse3_trivial_ops
   @ f_opt "move-loop-invariants" option_fmove_loop_invariants
+  @ f_opt "move-loop-invariants_2" option_fmove_loop_invariants_2
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
   @ [ Exact "-ftailduplicate", Integer (fun n -> option_ftailduplicate := n) ]
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 34a09330..f2172a27 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -119,6 +119,8 @@ Extract Constant Compopts.optim_CSE2 =>
   "fun _ -> !Clflags.option_fcse2".
 Extract Constant Compopts.optim_CSE3 =>
   "fun _ -> !Clflags.option_fcse3".
+Extract Constant Compopts.optim_CSE3_2 =>
+  "fun _ -> !Clflags.option_fcse3_2".
 Extract Constant Compopts.optim_CSE3_alias_analysis =>
   "fun _ -> !Clflags.option_fcse3_alias_analysis".
 Extract Constant Compopts.optim_CSE3_across_calls =>
@@ -131,6 +133,8 @@ Extract Constant Compopts.optim_CSE3_trivial_ops =>
   "fun _ -> !Clflags.option_fcse3_trivial_ops".
 Extract Constant Compopts.optim_move_loop_invariants =>
   "fun _ -> !Clflags.option_fmove_loop_invariants".
+Extract Constant Compopts.optim_move_loop_invariants_2 =>
+  "fun _ -> !Clflags.option_fmove_loop_invariants_2".
 
 Extract Constant Compopts.optim_redundancy =>
   "fun _ -> !Clflags.option_fredundancy".
diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml
index 1c1b96b1..31539d57 100644
--- a/tools/compiler_expand.ml
+++ b/tools/compiler_expand.ml
@@ -32,17 +32,26 @@ PARTIAL, Always, NoRequire, (Some "Performing tail duplication"), "Tailduplicate
 TOTAL, Always, NoRequire, (Some "Renumbering pre constprop"), "Renumber";
 TOTAL, (Option "optim_constprop"), Require, (Some "Constant propagation"), "Constprop";
 TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber";
+PARTIAL, (Option "optim_move_loop_invariants"), Require, (Some "LICM"), "LICM";
+TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering post LICM"), "Renumber";
 TOTAL, (Option "optim_CSE2"), Require, (Some "CSE2"), "CSE2";
 PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3";
 TOTAL, (Option "optim_CSE3"), Require, (Some "Kill useless moves after CSE3"), "KillUselessMoves";
 TOTAL, (Option "optim_forward_moves"), Require, (Some "Forwarding moves"), "ForwardMoves";
+TOTAL, (Option "all_loads_nontrap"), Require, None, "Allnontrap";
+PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob";
 PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode";
 PARTIAL, (Option "optim_move_loop_invariants"), Require, (Some "LICM"), "LICM";
-TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for LICM"), "Renumber";
-PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "CSE3 for LICM"), "CSE3";
-PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Redundancy elimination for LICM"), "Deadcode";
-TOTAL, (Option "all_loads_nontrap"), Require, None, "Allnontrap";
-PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob"
+|];;
+
+let post_ssa_passes =
+[|
+TOTAL, Always, NoRequire, (Some "Renumbering pre CSE_2"), "Renumber";
+PARTIAL, (Option "optim_move_loop_invariants_2"), Require, (Some "LICM_2"), "LICM";
+TOTAL, (Option "optim_move_loop_invariants_2"), NoRequire, (Some "Renumbering post LICM"), "Renumber";
+PARTIAL, (Option "optim_CSE3_2"), Require, (Some "CSE3_2"), "CSE3";
+TOTAL, (Option "optim_CSE3_2"), Require, (Some "Kill useless moves after CSE3_2"), "KillUselessMoves";
+PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode";
 |];;
 
 let post_rtl_passes =
@@ -59,7 +68,10 @@ let rtl_passes' =
   Array.mapi
        (fun i (a,b,r,c,d) -> (a,b,r,c,d, Print (Printf.sprintf "RTL %d" (i+1))))
        rtl_passes;;
-let all_passes = Array.concat [ rtl_passes'; post_rtl_passes ];;
+let post_ssa_passes' =
+  Array.mapi
+       (fun i (a,b,r,c,d) -> (a,b,r,c,d, Print (Printf.sprintf "RTL %d" (i+200))))
+       post_ssa_passes;;
 
 let totality = function TOTAL -> "total" | PARTIAL -> "partial";;
 
@@ -104,6 +116,7 @@ let print_transf passes oc =
     ) passes;;
 
 let print_rtl_transf = print_transf rtl_passes';;
+let print_post_ssa_transf = print_transf post_ssa_passes';;
 let print_post_rtl_transf = print_transf post_rtl_passes;;
 
 let print_mkpass passes oc =
@@ -117,6 +130,7 @@ let print_mkpass passes oc =
     passes;;
 
 let print_rtl_mkpass = print_mkpass rtl_passes';;
+let print_post_ssa_mkpass = print_mkpass post_ssa_passes';;
 let print_post_rtl_mkpass = print_mkpass post_rtl_passes;;
 
 let print_if kind oc = function
@@ -137,6 +151,7 @@ let print_proof prefix passes oc =
   Printf.fprintf oc "set (%s_last := %s%d) in *.\n" prefix prefix (Array.length passes);;
 
 let print_rtl_proof = print_proof "rtl" rtl_passes';;
+let print_post_ssa_proof = print_proof "post_ssa" post_ssa_passes';;
 let print_post_rtl_proof = print_proof "post_rtl" post_rtl_passes;;
 
 let print_proof2 prefix passes oc =
@@ -153,6 +168,7 @@ let print_proof2 prefix passes oc =
     passes;;
 
 let print_rtl_proof2 = print_proof2 "rtl" rtl_passes';;
+let print_post_ssa_proof2 = print_proof2 "post_ssa" post_ssa_passes';;
 let print_post_rtl_proof2 = print_proof2 "post_rtl" post_rtl_passes;;
 
 let print_forward_simulations passes oc =
@@ -166,6 +182,7 @@ let print_forward_simulations passes oc =
     passes;;
 
 let print_rtl_forward_simulations = print_forward_simulations rtl_passes;;
+let print_post_ssa_forward_simulations = print_forward_simulations post_ssa_passes;;
 
 if (Array.length Sys.argv)<>3
 then exit 1;;
@@ -180,6 +197,8 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in
         match input_line ic with
         | "EXPAND_RTL_TRANSF_PROGRAM" ->
            print_rtl_transf oc
+        | "EXPAND_POST_SSA_TRANSF_PROGRAM" ->
+           print_post_ssa_transf oc
         | "EXPAND_POST_RTL_TRANSF_PROGRAM" ->
            print_post_rtl_transf oc
         | "EXPAND_RTL_REQUIRE" ->
@@ -192,24 +211,32 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in
            print_post_rtl_require_proof oc
         | "EXPAND_RTL_MKPASS" ->
            print_rtl_mkpass oc
+        | "EXPAND_POST_SSA_MKPASS" ->
+           print_post_ssa_mkpass oc
         | "EXPAND_POST_RTL_MKPASS" ->
            print_post_rtl_mkpass oc
         | "EXPAND_RTL_PROOF" ->
            print_rtl_proof oc
+        | "EXPAND_POST_SSA_PROOF" ->
+           print_post_ssa_proof oc
         | "EXPAND_POST_RTL_PROOF" ->
            print_post_rtl_proof oc
         | "EXPAND_RTL_PROOF2" ->
            print_rtl_proof2 oc
+        | "EXPAND_POST_SSA_PROOF2" ->
+           print_post_ssa_proof2 oc
         | "EXPAND_POST_RTL_PROOF2" ->
            print_post_rtl_proof2 oc
         | "EXPAND_ASM_SEMANTICS" ->
            Printf.fprintf oc "    (Asm.semantics p%d)\n"
-             ((Array.length all_passes) + 7)
+             ((Array.length rtl_passes) + (Array.length post_rtl_passes) + 7)
         | "EXPAND_ASM_SEMANTICS_SSA" ->
            Printf.fprintf oc "    (Asm.semantics p%d)\n"
-             ((Array.length all_passes) + 7 + nr_ssa_passes)
+             ((Array.length rtl_passes) + (Array.length post_ssa_passes) + (Array.length post_rtl_passes) + 7 + nr_ssa_passes)
         | "EXPAND_RTL_FORWARD_SIMULATIONS" ->
            print_rtl_forward_simulations oc
+        | "EXPAND_POST_SSA_FORWARD_SIMULATIONS" ->
+           print_post_ssa_forward_simulations oc
         | line -> (output_string oc line;
                    output_char oc '\n')
       done