seems to work better

1 files changed, 32 insertions, 0 deletions

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.