Val_cmp* -> Val.mxcmp*

1 files changed, 49 insertions, 0 deletions

diff --git a/common/Values.v b/common/Values.v
index 41138e8e..4146dd59 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -2613,6 +2613,55 @@ Qed.
 
 End VAL_INJ_OPS.
 
+(* Specializations of cmpu_bool, cmpu, cmplu_bool, and cmplu for maximal pointer validity *)
+
+Definition mxcmpu_bool cmp v1 v2: option bool :=
+  cmpu_bool (fun _ _ => true) cmp v1 v2.
+
+Lemma mxcmpu_bool_correct vptr (cmp: comparison) (v1 v2: val) b:
+   cmpu_bool vptr cmp v1 v2 = Some b
+   -> mxcmpu_bool cmp v1 v2 = Some b.
+Proof.
+  intros; eapply cmpu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition mxcmpu cmp v1 v2 := of_optbool (mxcmpu_bool cmp v1 v2).
+
+Lemma mxcmpu_correct vptr (cmp: comparison) (v1 v2: val):
+   lessdef (cmpu vptr cmp v1 v2) (mxcmpu cmp v1 v2).
+Proof.
+  unfold cmpu, mxcmpu.
+  remember (cmpu_bool _ cmp v1 v2) as ob.
+  destruct ob; simpl.
+  - erewrite mxcmpu_bool_correct; eauto.
+    econstructor.
+  - econstructor.
+Qed.
+
+Definition mxcmplu_bool (cmp: comparison) (v1 v2: val)
+ := (cmplu_bool (fun _ _ => true) cmp v1 v2).
+
+Lemma mxcmplu_bool_correct vptr (cmp: comparison) (v1 v2: val) b:
+   (cmplu_bool vptr cmp v1 v2) = Some b
+   -> (mxcmplu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply cmplu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition mxcmplu cmp v1 v2 := of_optbool (mxcmplu_bool cmp v1 v2).
+
+Lemma mxcmplu_correct vptr (cmp: comparison) (v1 v2: val):
+   lessdef (maketotal (cmplu vptr cmp v1 v2))
+               (mxcmplu cmp v1 v2).
+Proof.
+  unfold cmplu, mxcmplu.
+  remember (cmplu_bool _ cmp v1 v2) as ob.
+  destruct ob as [b|]; simpl.
+  - erewrite mxcmplu_bool_correct; eauto.
+    simpl. econstructor.
+  - econstructor.
+Qed.
+
 End Val.
 
 Notation meminj := Val.meminj.