From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- common/Values.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) (limited to 'common') 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. -- cgit