From 6171f6a0880acbf0d007a7715cc37984ac25d851 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 6 May 2020 22:33:02 +0200
Subject: -fcse3-glb

---
 backend/CSE3analysis.v      | 24 +++++++++++++++++-------
 backend/CSE3analysisproof.v | 18 +++++++++++-------
 2 files changed, 28 insertions(+), 14 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index bd507dec..ade79c28 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -78,7 +78,10 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
   Definition lub x y :=
     if Compopts.optim_CSE3_across_merges tt
     then PSet.inter x y
-    else PSet.empty.
+    else
+      if PSet.eq x y
+      then x
+      else PSet.empty.
   
   Definition glb := PSet.union.
   
@@ -94,8 +97,10 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
       intuition.
     - apply PSet.is_subset_spec.
       intro.
-      rewrite PSet.gempty.
-      discriminate.
+      destruct (PSet.eq x y).
+      + auto.
+      + rewrite PSet.gempty.
+        discriminate.
   Qed.
   
   Lemma ge_lub_right: forall x y, ge (lub x y) y.
@@ -110,8 +115,10 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
       intuition.
     - apply PSet.is_subset_spec.
       intro.
-      rewrite PSet.gempty.
-      discriminate.
+      destruct (PSet.eq x y).
+      + subst. auto.
+      + rewrite PSet.gempty.
+        discriminate.
   Qed.
 
   Definition top := PSet.empty.
@@ -310,8 +317,11 @@ Section OPERATIONS.
     else
       let args' := forward_move_l rel args in
       match rhs_find op args' rel with
-      | Some r => (* FIXME RELATION.glb ( *) move r dst rel (* )
-                                                               (oper1 dst op args' rel) *)
+      | Some r =>
+        if Compopts.optim_CSE3_glb tt
+        then RELATION.glb (move r dst rel)
+                          (oper1 dst op args' rel)
+        else oper1 dst op args' rel
       | None => oper1 dst op args' rel
       end.
   
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 0c2aeb8e..f4e3672d 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -799,13 +799,17 @@ Section SOUNDNESS.
       rewrite <- (forward_move_sound rel rs m r) by auto.
       apply move_sound; auto.
     - destruct rhs_find as [src |] eqn:RHS_FIND.
-      + (* FIXME apply sem_rel_glb; split. *)
-        * pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
-          eapply forward_move_rhs_sound in RHS.
-          2: eassumption.
-          rewrite <- (sem_rhs_det SOUND RHS).
-          apply move_sound; auto.
-        (* FIXME * apply oper1_sound; auto. *)
+      + destruct (Compopts.optim_CSE3_glb tt).
+        * apply sem_rel_glb; split.
+          ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
+             eapply forward_move_rhs_sound in RHS.
+             2: eassumption.
+             rewrite <- (sem_rhs_det SOUND RHS).
+             apply move_sound; auto.
+          ** apply oper1_sound; auto.
+             apply forward_move_rhs_sound; auto.
+        * ** apply oper1_sound; auto.
+             apply forward_move_rhs_sound; auto.
       + apply oper1_sound; auto.
         apply forward_move_rhs_sound; auto.
   Qed.
-- 
cgit