kill_store_sound

1 files changed, 49 insertions, 0 deletions

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 ->