From f59c540aa7cf85c89ee0cb07c20374c8ad76a46c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 27 Oct 2020 15:21:11 +0100
Subject: new CSE3

---
 backend/CSE3analysisproof.v | 53 +++++++++++++++++++++++++++++++++++++--------
 1 file changed, 44 insertions(+), 9 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 66b199cc..ea4d37ca 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -699,6 +699,28 @@ Section SOUNDNESS.
       + congruence.
   Qed.
 
+
+  Lemma arglist_idem_write:
+    forall { A : Type} args (rs : Regmap.t A) dst,
+      (rs # dst <- (rs # dst)) ## args = rs ## args.
+  Proof.
+    induction args; trivial.
+    intros. cbn.
+    f_equal; trivial.
+    apply Regmap.gsident.
+  Qed.
+  
+  Lemma sem_rhs_idem_write:
+    forall sop args rs dst m v,
+      sem_rhs sop args rs m v ->
+      sem_rhs sop args (rs # dst <- (rs # dst)) m v.
+  Proof.
+    intros.
+    unfold sem_rhs in *.
+    rewrite arglist_idem_write.
+    assumption.
+  Qed.
+  
   Theorem oper2_sound:
     forall no dst sop args rel rs m v,
       sem_rel rel rs m ->
@@ -726,6 +748,17 @@ Section SOUNDNESS.
       rewrite Regmap.gss.
       apply sem_rhs_depends_on_args_only; auto.
     }
+    intros INi.
+    destruct (PSet.contains rel e) eqn:CONTAINSe.
+    { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe.
+      pose proof (REL i eq CONTAINS INi) as RELi.
+      unfold sem_eq in *.
+      cbn in RELe.
+      replace v with (rs # dst) by (eapply sem_rhs_det; eassumption).
+      rewrite Regmap.gsident.
+      apply sem_rhs_idem_write.
+      assumption.
+    }
     rewrite PSet.gaddo in CONTAINS by congruence.
     apply (kill_reg_sound rel rs m dst v REL i eq); auto.
   Qed.
@@ -821,11 +854,7 @@ Section SOUNDNESS.
       subst.
       rewrite <- (forward_move_sound rel rs m r) by auto.
       apply move_sound; auto.
-    - destruct (is_trivial_sym_op sop).
-      {
-        apply kill_reg_sound; auto.
-      }
-      destruct rhs_find as [src |] eqn:RHS_FIND.
+    - destruct rhs_find as [src |] eqn:RHS_FIND.
       + 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.
@@ -833,12 +862,18 @@ Section SOUNDNESS.
              2: eassumption.
              rewrite <- (sem_rhs_det SOUND RHS).
              apply move_sound; auto.
+          ** apply sem_rel_glb; split.
+             *** apply oper1_sound; auto.
+                 apply forward_move_rhs_sound; auto.
+             *** apply oper1_sound; auto.
+        * apply sem_rel_glb; split.
           ** 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.
+          ** apply oper1_sound; auto.
+      + apply sem_rel_glb; split.
+        * apply oper1_sound; auto.
+          apply forward_move_rhs_sound; auto.
+        * apply oper1_sound; auto.
   Qed.
 
   Hint Resolve oper_sound : cse3.
-- 
cgit