diff options
Diffstat (limited to 'kvx/Op.v')
| -rw-r--r-- | kvx/Op.v | 49 |
1 files changed, 36 insertions, 13 deletions
@@ -1205,12 +1205,25 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) +Definition cond_depends_on_memory (c: condition) : bool := + match c with + | Ccompu _ | Ccompuimm _ _ => negb Archi.ptr64 + | Ccomplu _ | Ccompluimm _ _ => Archi.ptr64 + | _ => false + end. + +Lemma cond_depends_on_memory_correct: + forall c args m1 m2, + cond_depends_on_memory c = false -> + eval_condition c args m1 = eval_condition c args m2. +Proof. + intros; destruct c; cbn; discriminate || reflexivity. +Qed. + Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp (Ccompu _) => negb Archi.ptr64 - | Ocmp (Ccompuimm _ _) => negb Archi.ptr64 - | Ocmp (Ccomplu _) => Archi.ptr64 - | Ocmp (Ccompluimm _ _) => Archi.ptr64 + | Ocmp (Ccompu _ | Ccompuimm _ _) => negb Archi.ptr64 + | Ocmp (Ccomplu _ | Ccompluimm _ _) => Archi.ptr64 | Osel (Ccompu0 _) _ | Oselimm (Ccompu0 _) _ | Osellimm (Ccompu0 _) _ => negb Archi.ptr64 | Osel (Ccomplu0 _) _ | Oselimm (Ccomplu0 _) _ | Osellimm (Ccomplu0 _) _ => Archi.ptr64 @@ -1238,23 +1251,33 @@ 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) -> 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); + intros until m2. destruct op; cbn; try congruence. + - intros MEM; destruct cond; cbn; try congruence; + repeat (destruct args; cbn; try congruence); erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - - intros MEM; destruct c0; simpl; try congruence; - repeat (destruct args; simpl; try congruence); + - intros MEM; destruct c0; cbn; try congruence; + repeat (destruct args; cbn; try congruence); erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - - intros MEM; destruct c0; simpl; try congruence; - repeat (destruct args; simpl; try congruence); + - intros MEM; destruct c0; cbn; try congruence; + repeat (destruct args; cbn; try congruence); erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - - intros MEM; destruct c0; simpl; try congruence; - repeat (destruct args; simpl; try congruence); + - intros MEM; destruct c0; cbn; try congruence; + repeat (destruct args; cbn; try congruence); erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. |