diff options
| -rw-r--r-- | backend/CSE3analysisproof.v | 37 |
1 files changed, 34 insertions, 3 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 10ae4cd0..7c276625 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 -> @@ -706,8 +728,6 @@ Section SOUNDNESS. sem_rhs sop args rs m v -> sem_rel (oper2 (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. Proof. - Admitted. - (* unfold oper2. intros until v. intros REL NOTIN RHS. @@ -728,9 +748,20 @@ 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. *) + Qed. Hint Resolve oper2_sound : cse3. |