From 0a13bf127bb385df424bd9e392742d4fc5bef86a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 13:15:53 +0100
Subject: begin implementing -fcse3-conditions

---
 backend/CSE3analysis.v      | 11 +++++++----
 backend/CSE3analysisproof.v | 12 ++++++++----
 2 files changed, 15 insertions(+), 8 deletions(-)

(limited to 'backend')

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.
   
   (*
-- 
cgit