seems to work better

2 files changed, 37 insertions, 3 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 7316c9a9..5eb92a82 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -282,12 +282,14 @@ Section OPERATIONS.
 
   Definition oper2 (dst : reg) (op: sym_op)(args : list reg)
            (rel : RELATION.t) : RELATION.t :=
-    let rel' := kill_reg dst rel in
     match eq_find {| eq_lhs := dst;
                      eq_op  := op;
                      eq_args:= args |} with
-    | Some id => PSet.add id rel'
-    | None => rel'
+    | Some id =>
+      if PSet.contains rel id
+      then rel
+      else PSet.add id (kill_reg dst rel)
+    | None => kill_reg dst rel
     end.
 
   Definition oper1 (dst : reg) (op: sym_op) (args : list reg)
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 66b199cc..07a58f23 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -699,6 +699,27 @@ 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 +747,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.