diff options
-rw-r--r-- | arm/Op.v | 10 | ||||
-rw-r--r-- | backend/CSE3analysis.v | 14 | ||||
-rw-r--r-- | kvx/Op.v | 10 | ||||
-rw-r--r-- | powerpc/Op.v | 10 | ||||
-rw-r--r-- | riscV/Op.v | 10 | ||||
-rw-r--r-- | x86/Op.v | 10 |
6 files changed, 64 insertions, 0 deletions
@@ -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) := @@ -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) -> @@ -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) -> @@ -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) -> |