cond_valid_pointer_eq

6 files changed, 64 insertions, 0 deletions

diff --git a/arm/Op.v b/arm/Op.v
index 6f22cece..c7588d33 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -751,6 +751,16 @@ Proof.
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+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) ->
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 8b7f1190..84f4a426 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -160,6 +160,20 @@ Proof.
   decide equality.
 Defined.
 
+Record condition_fact :=
+  mkcondition_fact
+    { cond_op : condition ;
+      cond_args : list reg }.
+
+Definition eq_dec_condition_fact :
+  forall cf cf' : condition_fact, {cf = cf'} + {cf <> cf'}.
+Proof.
+  generalize peq.
+  generalize eq_condition.
+  generalize eq_dec_args.
+  decide equality.
+Defined.
+
 Definition eq_id := node.
 
 Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
diff --git a/kvx/Op.v b/kvx/Op.v
index 794bc87b..f9501485 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -1238,6 +1238,16 @@ Proof.
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+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) ->
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 4f14bfac..0610bc9c 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -797,6 +797,16 @@ Proof.
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+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) ->
diff --git a/riscV/Op.v b/riscV/Op.v
index 762c3a02..9e98d517 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -872,6 +872,16 @@ Proof.
   unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+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) ->
diff --git a/x86/Op.v b/x86/Op.v
index 776f9495..e7c910c2 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1037,6 +1037,16 @@ Proof.
   auto.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+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) ->