1 files changed, 91 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v
index 6401ba52..5d32e54e 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -89,6 +89,27 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | _, _ => False
   end.
 
+Definition has_type_b (v: val) (t: typ) :=
+  match v, t with
+  | Vundef, _ => true
+  | Vint _, Tint => true
+  | Vlong _, Tlong => true
+  | Vfloat _, Tfloat => true
+  | Vsingle _, Tsingle => true
+  | Vptr _ _, Tint => negb Archi.ptr64
+  | Vptr _ _, Tlong => Archi.ptr64
+  | (Vint _ | Vsingle _), Tany32 => true
+  | Vptr _ _, Tany32 => negb Archi.ptr64
+  | _, Tany64 => true
+  | _, _ => false
+  end.
+
+Lemma has_type_b_correct: forall v t,
+    has_type_b v t = true <-> has_type v t.
+Proof.
+  destruct v; destruct t; cbn; destruct Archi.ptr64; cbn; split; intros; auto; discriminate.
+Qed.
+
 Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop :=
   match vl, tl with
   | nil, nil => True
@@ -2613,6 +2634,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.
@@ -2706,3 +2776,24 @@ Proof.
   unfold compose_meminj; rewrite H1; rewrite H3; eauto.
   rewrite Ptrofs.add_assoc. decEq. unfold Ptrofs.add. apply Ptrofs.eqm_samerepr. auto with ints.
 Qed.
+
+
+(** Particular cases of extensionality lemma *)
+
+Lemma cmpu_bool_valid_pointer_eq vptr1 vptr2 c v1 v2:
+   (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) ->
+   Val.cmpu_bool vptr1 c v1 v2 = Val.cmpu_bool vptr2 c v1 v2.
+Proof.
+  intros EQ; unfold Val.cmpu_bool; destruct v1; try congruence;
+  destruct v2; try congruence;
+  rewrite !EQ; auto.
+Qed.
+
+Lemma cmplu_bool_valid_pointer_eq  vptr1 vptr2 c v1 v2:
+   (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) ->
+   Val.cmplu_bool vptr1 c v1 v2 = Val.cmplu_bool vptr2 c v1 v2.
+Proof.
+  intros EQ; unfold Val.cmplu_bool; destruct v1; try congruence;
+  destruct v2; try congruence;
+  rewrite !EQ; auto.
+Qed.