diff options
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/Op.v | 24 |
1 files changed, 17 insertions, 7 deletions
@@ -999,7 +999,7 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) -Definition condition_depends_on_memory (c: condition) : bool := +Definition cond_depends_on_memory (c: condition) : bool := match c with | Ccompu _ => negb Archi.ptr64 | Ccompuimm _ _ => negb Archi.ptr64 @@ -1010,14 +1010,14 @@ Definition condition_depends_on_memory (c: condition) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp c => condition_depends_on_memory c - | Osel c ty => condition_depends_on_memory c + | Ocmp c => cond_depends_on_memory c + | Osel c ty => cond_depends_on_memory c | _ => false end. -Lemma condition_depends_on_memory_correct: +Lemma cond_depends_on_memory_correct: forall c args m1 m2, - condition_depends_on_memory c = false -> + cond_depends_on_memory c = false -> eval_condition c args m1 = eval_condition c args m2. Proof. intros until m2. @@ -1031,12 +1031,22 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence; intros C. -- f_equal; f_equal; apply condition_depends_on_memory_correct; auto. +- f_equal; f_equal; apply cond_depends_on_memory_correct; auto. - destruct args; auto. destruct args; auto. - rewrite (condition_depends_on_memory_correct c args m1 m2 C). + rewrite (cond_depends_on_memory_correct c args m1 m2 C). 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) -> |