totally switch off conditions in cse3

2 files changed, 21 insertions, 16 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 482069d7..3a680cf7 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -54,22 +54,25 @@ Definition subst_args fmap pc xl :=
   forward_move_l_b (PMap.get pc fmap) xl.
 
 Definition find_cond_in_fmap fmap pc cond args :=
-  match PMap.get pc fmap with
-  | Some rel =>
-    if is_condition_present (ctx:=ctx) pc rel cond args
-    then Some true
-    else
-      let ncond := negate_condition cond in
-      if is_condition_present (ctx:=ctx) pc rel ncond args
-         then Some false
-         else let args' := subst_args fmap pc args in
-              if is_condition_present (ctx:=ctx) pc rel cond args'
-              then Some true
-              else if is_condition_present (ctx:=ctx) pc rel ncond args'
-                   then Some false
-                   else None
-  | None => None
-  end.
+  if Compopts.optim_CSE3_conditions tt
+  then
+    match PMap.get pc fmap with
+    | Some rel =>
+      if is_condition_present (ctx:=ctx) pc rel cond args
+      then Some true
+      else
+        let ncond := negate_condition cond in
+        if is_condition_present (ctx:=ctx) pc rel ncond args
+        then Some false
+        else let args' := subst_args fmap pc args in
+             if is_condition_present (ctx:=ctx) pc rel cond args'
+             then Some true
+             else if is_condition_present (ctx:=ctx) pc rel ncond args'
+                  then Some false
+                  else None
+    | None => None
+    end
+  else None.
 
 Definition transf_instr (fmap : PMap.t RB.t)
            (pc: node) (instr: instruction) :=
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 50a32d56..ca43d0bd 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -983,6 +983,8 @@ Proof.
         unfold find_cond_in_fmap in FIND_COND.
         change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND.
         rewrite FIND_REL in FIND_COND.
+        destruct (Compopts.optim_CSE3_conditions tt).
+        2: discriminate.
         destruct (is_condition_present pc rel cond args).
         { rewrite COND_PRESENT_TRUE in H0 by trivial.
           congruence.