begin implementing -fcse3-conditions

6 files changed, 24 insertions, 8 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 383147bb..75e00f67 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -477,10 +477,13 @@ Section OPERATIONS.
     end.
 
   Definition apply_cond cond args (rel : RELATION.t) : RB.t :=
-    match apply_cond1 cond args rel with
-    | Some rel => Some (apply_cond0 cond args rel)
-    | None => RB.bot
-    end.
+    if Compopts.optim_CSE3_conditions tt
+    then 
+      match apply_cond1 cond args rel with
+      | Some rel => Some (apply_cond0 cond args rel)
+      | None => RB.bot
+      end
+    else Some rel.
       
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 29d171eb..d53cf604 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1350,10 +1350,14 @@ Section SOUNDNESS.
   Proof.
     unfold apply_cond.
     intros.
-    pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
-    destruct apply_cond1 eqn:COND1.
-    { apply apply_cond0_sound; auto. }
-    exact SOUND1.
+    destruct (Compopts.optim_CSE3_conditions tt).
+    {
+      pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
+      destruct apply_cond1 eqn:COND1.
+      { apply apply_cond0_sound; auto. }
+      exact SOUND1.
+    }
+    exact REL.
   Qed.
   
   (*
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 991720bf..55d1bb1c 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -35,6 +35,8 @@ let option_fcse3_across_merges = ref true
 let option_fcse3_glb = ref true
 let option_fcse3_trivial_ops = ref false
 let option_fcse3_refine = ref true
+let option_fcse3_conditions = ref true
+                        
 let option_fredundancy = ref true
 
 (** Options relative to superblock scheduling *)
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 0c90ee52..65264124 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -57,6 +57,9 @@ Parameter optim_CSE3_glb: unit -> bool.
 (** Flag -fcse3-trivial-ops. For DMonniaux's common subexpression elimination, simplify trivial operations as well. *)
 Parameter optim_CSE3_trivial_ops: unit -> bool.
 
+(** Flag -fcse3-conditions. For DMonniaux's common subexpression elimination: remove redundant conditional branches. *)
+Parameter optim_CSE3_conditions: unit -> bool.
+
 (** Flag -fmove-loop-invariants. *)
 Parameter optim_move_loop_invariants: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 089cd423..38028806 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -204,6 +204,7 @@ Processing options:
   -fcse3-glb            Refine CSE3 information using greatest lower bounds [on]
   -fcse3-trivial-ops    Replace trivial operations as well using CSE3 [off]
   -fcse3-refine         Refine CSE3 invariants by descending iteration [on]
+  -fcse3-conditions     Remove redundant conditions using CSE3 [on]
   -fmove-loop-invariants Perform loop-invariant code motion [off]
   -fredundancy   Perform redundancy elimination [on]
   -mtune=         Type of CPU (for scheduling on some architectures)
@@ -418,6 +419,7 @@ let cmdline_actions =
   @ f_opt "cse3-glb" option_fcse3_glb
   @ f_opt "cse3-trivial-ops" option_fcse3_trivial_ops
   @ f_opt "cse3-refine" option_fcse3_refine
+  @ f_opt "cse3-conditions" option_fcse3_conditions
   @ f_opt "move-loop-invariants" option_fmove_loop_invariants
   @ f_opt "redundancy" option_fredundancy
   @ [ Exact "-mtune", String (fun s -> option_mtune := s) ]
diff --git a/extraction/extraction.v b/extraction/extraction.v
index f5af7998..2d081d17 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -129,6 +129,8 @@ Extract Constant Compopts.optim_CSE3_glb =>
   "fun _ -> !Clflags.option_fcse3_glb".
 Extract Constant Compopts.optim_CSE3_trivial_ops =>
   "fun _ -> !Clflags.option_fcse3_trivial_ops".
+Extract Constant Compopts.optim_CSE3_conditions =>
+  "fun _ -> !Clflags.option_fcse3_conditions".
 Extract Constant Compopts.optim_move_loop_invariants =>
   "fun _ -> !Clflags.option_fmove_loop_invariants".