From a49044a62393a1a831e22c34cae656f4c7294059 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 25 Nov 2020 13:39:00 +0100 Subject: kill_store_sound --- backend/CSE3analysisproof.v | 49 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 50a2c469..5c89c4e7 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -657,6 +657,55 @@ Section SOUNDNESS. Hint Resolve kill_mem_sound : cse3. + (* TODO: shouldn't this already be proved somewhere else? *) + Lemma store_preserves_validity: + forall m m' wchunk a v + (STORE : Mem.storev wchunk m a v = Some m') + (b : block) (z : Z), + Mem.valid_pointer m' b z = Mem.valid_pointer m b z. + Proof. + unfold Mem.storev. + intros. + destruct a; try discriminate. + Local Transparent Mem.store. + unfold Mem.store in STORE. + destruct Mem.valid_access_dec in STORE. + 2: discriminate. + inv STORE. + reflexivity. + Qed. + + Hint Resolve store_preserves_validity : cse3. + + Theorem kill_store_sound : + forall rel rs m m' wchunk a v, + (sem_rel rel rs m) -> + (Mem.storev wchunk m a v = Some m') -> + (sem_rel (kill_store (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_store. + intros until v. + intros REL STORE i eq. + specialize REL with (i := i) (eq0 := eq). + intros SUBTRACT CATALOG. + rewrite PSet.gsubtract in SUBTRACT. + rewrite andb_true_iff in SUBTRACT. + intuition. + destruct (eq_op eq) as [op | chunk addr] eqn:OP. + - rewrite op_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. + - specialize ctx_kill_store_has_depends_on_store with (eq0 := eq) (j := i). + destruct eq as [lhs op args]; simpl in *. + rewrite OP in ctx_kill_store_has_depends_on_store. + rewrite negb_true_iff in H0. + rewrite OP in CATALOG. + intuition. + congruence. + Qed. + + Hint Resolve kill_store_sound : cse3. + Theorem eq_find_sound: forall no eq id, eq_find (ctx := ctx) no eq = Some id -> -- cgit