Characterizing Op dependency on memory

2 files changed, 51 insertions, 0 deletions

diff --git a/common/Memory.v b/common/Memory.v
index cd8a2001..65f36966 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1322,6 +1322,18 @@ Proof.
   eapply load_store_same.
   eassumption.
 Qed.
+
+Theorem storev_preserv_valid (b : block) (ofs: Z): valid_pointer m1 b ofs = valid_pointer m2 b ofs.
+Proof.
+  unfold storev in STORE.
+  cut (valid_pointer m1 b ofs = true <-> valid_pointer m2 b ofs = true).
+  { destruct (valid_pointer _ _ _), (valid_pointer _ _ _); intuition congruence. }
+  destruct addr; try congruence.
+  rewrite! valid_pointer_valid_access. split.
+  - intros; eapply store_valid_access_1; eauto.
+  - intros; eapply store_valid_access_2; eauto.
+Qed.
+
 End STOREV.
 
 Lemma load_store_overlap:
diff --git a/kvx/Op.v b/kvx/Op.v
index 544bb081..b78b7b97 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -1238,6 +1238,45 @@ Proof.
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma Val_cmpu_bool_valid_pointer_eq m1 m2 c v1 v2:
+   (forall (b : block) (z : Z), Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+   Val.cmpu_bool( Mem.valid_pointer m1) c v1 v2 = Val.cmpu_bool (Mem.valid_pointer m2) c v1 v2.
+Proof.
+  intros MEM; unfold Val.cmpu_bool; destruct v1; try congruence;
+  destruct v2; try congruence;
+  rewrite !MEM; auto.
+Qed.
+
+Lemma Val_cmplu_bool_valid_pointer_eq m1 m2 c v1 v2:
+   (forall (b : block) (z : Z), Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+   Val.cmplu_bool( Mem.valid_pointer m1) c v1 v2 = Val.cmplu_bool (Mem.valid_pointer m2) c v1 v2.
+Proof.
+  intros MEM; unfold Val.cmplu_bool; destruct v1; try congruence;
+  destruct v2; try congruence;
+  rewrite !MEM; auto.
+Qed.
+
+Lemma op_valid_pointer_eq:
+  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
+Proof.
+  intros until m2. destruct op; simpl; try congruence.
+  - intros MEM; destruct cond; simpl; try congruence;
+    repeat (destruct args; simpl; try congruence);
+    erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto.
+  - intros MEM; destruct c0; simpl; try congruence;
+    repeat (destruct args; simpl; try congruence);
+    erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto.
+  - intros MEM; destruct c0; simpl; try congruence;
+    repeat (destruct args; simpl; try congruence);
+    erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto.
+  - intros MEM; destruct c0; simpl; try congruence;
+    repeat (destruct args; simpl; try congruence);
+    erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
+
 (** Global variables mentioned in an operation or addressing mode *)
 
 Definition globals_addressing (addr: addressing) : list ident :=