Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2

4 files changed, 28 insertions, 11 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 9aa4a2bf..ba0246df 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -26,6 +26,7 @@ let option_ffloatconstprop = ref 2
 let option_ftailcalls = ref true
 let option_fconstprop = ref true
 let option_fcse = ref true
+let option_fcse2 = ref true
 let option_fredundancy = ref true
 let option_fpostpass = ref true
 let option_fpostpass_sched = ref "list"
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 24964237..24c3518b 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -42,6 +42,7 @@ Require Duplicate.
 Require Constprop.
 Require CSE.
 Require ForwardMoves.
+Require CSE2.
 Require Deadcode.
 Require Unusedglob.
 Require Allnontrap.
@@ -66,6 +67,7 @@ Require Duplicateproof.
 Require Constpropproof.
 Require CSEproof.
 Require ForwardMovesproof.
+Require CSE2proof.
 Require Deadcodeproof.
 Require Unusedglobproof.
 Require Allnontrapproof.
@@ -140,14 +142,16 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 6)
   @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 7)
-   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
+   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
    @@ print (print_RTL 8)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
    @@ print (print_RTL 9)
-   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 10)
-  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
    @@ print (print_RTL 11)
+  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ print (print_RTL 12)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -254,6 +258,7 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog)
   ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog)
   ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
   ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
@@ -300,8 +305,9 @@ Proof.
   set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
   set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
   destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
-  set (p13bis := total_if optim_forward_moves ForwardMoves.transf_program p13) in *.
-  destruct (partial_if optim_redundancy Deadcode.transf_program p13bis) as [p14|e] eqn:P14; simpl in T; try discriminate.
+  set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *.
+  set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *.
+  destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) 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 (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate.
@@ -324,7 +330,8 @@ Proof.
   exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match.
   exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match.
   exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
-  exists p13bis; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match.
+  exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match.
+  exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match.
   exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
   exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match.
   exists p15; split. apply Unusedglobproof.transf_program_match; auto.
@@ -385,7 +392,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p24)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -412,7 +419,9 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct.
   eapply compose_forward_simulations.
-    eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption.
+  eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct.
+  eapply compose_forward_simulations.
+  eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index fdd2b1d6..4d6a096c 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -36,6 +36,9 @@ Parameter optim_constprop: unit -> bool.
 (** Flag -fcse.  For common subexpression elimination. *)
 Parameter optim_CSE: unit -> bool.
 
+(** Flag -fcse2.  For DMonniaux's common subexpression elimination. *)
+Parameter optim_CSE2: unit -> bool.
+
 (** Flag -fredundancy.  For dead code elimination. *)
 Parameter optim_redundancy: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 992cf8c4..3c97e17f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -195,6 +195,7 @@ Processing options:
   -ffloat-const-prop <n>  Control constant propagation of floats
                    (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
   -fcse          Perform common subexpression elimination [on]
+  -fcse2         Perform inter-loop common subexpression elimination [on]
   -fredundancy   Perform redundancy elimination [on]
   -fpostpass     Perform postpass scheduling (only for K1 architecture) [on]
   -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
@@ -258,8 +259,10 @@ let dump_mnemonics destfile =
   exit 0
 
 let optimization_options = [
-  option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse;
-  option_fpostpass; option_fredundancy; option_finline_functions_called_once;
+    option_ftailcalls; option_fifconversion; option_fconstprop;
+    option_fcse; option_fcse2;
+    option_fpostpass;
+    option_fredundancy; option_finline; option_finline_functions_called_once;
 ]
 
 let set_all opts () = List.iter (fun r -> r := true) opts
@@ -382,6 +385,7 @@ let cmdline_actions =
   @ f_opt "if-conversion" option_fifconversion
   @ f_opt "const-prop" option_fconstprop
   @ f_opt "cse" option_fcse
+  @ f_opt "cse2" option_fcse2
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
   @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched