From 3830a91a4711c4570394e02e93e4e08db88eac6f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 12 Apr 2019 17:35:18 +0200 Subject: Support a "select" operation between two values `Val.select ob v1 v2 ty` is a conditional operation that chooses between the values `v1` and `v2` depending on the comparison `ob : option bool`. If `ob` is `None`, `Vundef` is returned. If the selected value does not match type `ty`, `Vundef` is returned. This operation will be used to model a "select" (or "conditional move") operation at the CminorSel/RTL/LTL/Mach level. --- backend/NeedDomain.v | 28 +++++++++++ backend/ValueDomain.v | 58 +++++++++++++++++++++++ common/Values.v | 126 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 212 insertions(+) diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 5d19e8f6..b35c90b2 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -786,6 +786,34 @@ Proof. inv H0. rewrite iagree_and_eq in H. rewrite H. auto. Qed. +(** The needs of a select *) + +Lemma normalize_sound: + forall v w x ty, + vagree v w x -> + vagree (Val.normalize v ty) (Val.normalize w ty) x. +Proof. + intros. destruct x; simpl in *. +- auto. +- unfold Val.normalize. destruct v. + auto. + destruct w; try contradiction. destruct ty; auto. + destruct ty; auto. + destruct ty; auto. + destruct ty; auto. + destruct ty; destruct Archi.ptr64; auto. +- apply Val.normalize_lessdef; auto. +Qed. + +Lemma select_sound: + forall ob v1 v2 w1 w2 ty x, + vagree v1 w1 x -> vagree v2 w2 x -> + vagree (Val.select ob v1 v2 ty) (Val.select ob w1 w2 ty) x. +Proof. + unfold Val.select; intros. destruct ob as [b|]; auto with na. + apply normalize_sound. destruct b; auto. +Qed. + (** The default abstraction: if the result is unused, the arguments are unused; otherwise, the arguments are needed in full. *) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 3ba2a35b..f6afa836 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2824,6 +2824,64 @@ Proof. intros. inv H; simpl in H0; congruence. Qed. +(** Select either returns one of its arguments, or Vundef. *) + +Definition add_undef (x: aval) := + match x with + | Vbot => ntop + | I i => + if Int.lt i Int.zero + then sgn Pbot (ssize i) + else uns Pbot (usize i) + | L _ | F _ | FS _ => ntop + | _ => x + end. + +Lemma add_undef_sound: + forall v x, vmatch v x -> vmatch v (add_undef x). +Proof. + destruct 1; simpl; auto with va. + destruct (Int.lt i Int.zero). + apply vmatch_sgn; apply is_sgn_ssize. + apply vmatch_uns; apply is_uns_usize. +Qed. + +Lemma add_undef_undef: + forall x, vmatch Vundef (add_undef x). +Proof. + destruct x; simpl; auto with va. + destruct (Int.lt n Int.zero); auto with va. +Qed. + +Lemma add_undef_normalize: + forall v x ty, vmatch v x -> vmatch (Val.normalize v ty) (add_undef x). +Proof. + intros. destruct (Val.lessdef_normalize v ty); + auto using add_undef_sound, add_undef_undef. +Qed. + +Definition select (ab: abool) (x y: aval) := + match ab with + | Bnone => ntop + | Just b | Maybe b => add_undef (if b then x else y) + | Btop => add_undef (vlub x y) + end. + +Lemma select_sound: + forall ob v w ab x y ty, + cmatch ob ab -> vmatch v x -> vmatch w y -> + vmatch (Val.select ob v w ty) (select ab x y). +Proof. + unfold Val.select, select; intros. inv H. +- auto with va. +- apply add_undef_normalize; destruct b; auto. +- apply add_undef_undef. +- apply add_undef_normalize; destruct b; auto. +- destruct ob as [b|]. ++ apply add_undef_normalize. destruct b; [apply vmatch_lub_l|apply vmatch_lub_r]; auto. ++ apply add_undef_undef. +Qed. + (** Normalization at load time *) Definition vnormalize (chunk: memory_chunk) (v: aval) := diff --git a/common/Values.v b/common/Values.v index a20dd567..a51a390f 100644 --- a/common/Values.v +++ b/common/Values.v @@ -132,6 +132,23 @@ Proof. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. Qed. +Definition has_type_dec (v: val) (t: typ) : { has_type v t } + { ~ has_type v t }. +Proof. + unfold has_type; destruct v. +- auto. +- destruct t; auto. +- destruct t; auto. +- destruct t; auto. +- destruct t; auto. +- destruct t. + apply bool_dec. + auto. + apply bool_dec. + auto. + apply bool_dec. + auto. +Defined. + (** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. Other values are neither true nor false. *) @@ -898,6 +915,55 @@ Definition offset_ptr (v: val) (delta: ptrofs) : val := | _ => Vundef end. +(** Normalize a value to the given type, turning it into Vundef if it does not + match the type. *) + +Definition normalize (v: val) (ty: typ) : val := + match v, ty with + | Vundef, _ => Vundef + | Vint _, Tint => v + | Vlong _, Tlong => v + | Vfloat _, Tfloat => v + | Vsingle _, Tsingle => v + | Vptr _ _, (Tint | Tany32) => if Archi.ptr64 then Vundef else v + | Vptr _ _, Tlong => if Archi.ptr64 then v else Vundef + | (Vint _ | Vsingle _), Tany32 => v + | _, Tany64 => v + | _, _ => Vundef + end. + +Lemma normalize_type: + forall v ty, has_type (normalize v ty) ty. +Proof. + intros; destruct v; simpl. +- auto. +- destruct ty; exact I. +- destruct ty; exact I. +- destruct ty; exact I. +- destruct ty; exact I. +- unfold has_type; destruct ty, Archi.ptr64; auto. +Qed. + +Lemma normalize_idem: + forall v ty, has_type v ty -> normalize v ty = v. +Proof. + unfold has_type, normalize; intros. destruct v. +- auto. +- destruct ty; intuition auto. +- destruct ty; intuition auto. +- destruct ty; intuition auto. +- destruct ty; intuition auto. +- destruct ty, Archi.ptr64; intuition congruence. +Qed. + +(** Select between two values based on the result of a comparison. *) + +Definition select (cmp: option bool) (v1 v2: val) (ty: typ) := + match cmp with + | Some b => normalize (if b then v1 else v2) ty + | None => Vundef + end. + (** [load_result] reflects the effect of storing a value with a given memory chunk, then reading it back with the same chunk. Depending on the chunk and the type of the value, some normalization occurs. @@ -2044,6 +2110,36 @@ Proof. intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. Qed. +Lemma lessdef_normalize: + forall v ty, lessdef (normalize v ty) v. +Proof. + intros. destruct v; simpl. + - auto. + - destruct ty; auto. + - destruct ty; auto. + - destruct ty; auto. + - destruct ty; auto. + - destruct ty, Archi.ptr64; auto. +Qed. + +Lemma normalize_lessdef: + forall v v' ty, lessdef v v' -> lessdef (normalize v ty) (normalize v' ty). +Proof. + intros. inv H; auto. +Qed. + +Lemma select_lessdef: + forall ob ob' v1 v1' v2 v2' ty, + ob = None \/ ob = ob' -> + lessdef v1 v1' -> lessdef v2 v2' -> + lessdef (select ob v1 v2 ty) (select ob' v1' v2' ty). +Proof. + intros; unfold select. destruct H. +- subst ob; auto. +- subst ob'; destruct ob as [b|]; auto. + apply normalize_lessdef. destruct b; auto. +Qed. + (** * Values and memory injections *) (** A memory injection [f] is a function from addresses to either [None] @@ -2328,6 +2424,36 @@ Proof. intros. unfold Val.hiword; inv H; auto. Qed. +Lemma normalize_inject: + forall v v' ty, inject f v v' -> inject f (normalize v ty) (normalize v' ty). +Proof. + intros. inv H. +- destruct ty; constructor. +- destruct ty; constructor. +- destruct ty; constructor. +- destruct ty; constructor. +- simpl. destruct ty. ++ destruct Archi.ptr64; econstructor; eauto. ++ auto. ++ destruct Archi.ptr64; econstructor; eauto. ++ auto. ++ destruct Archi.ptr64; econstructor; eauto. ++ econstructor; eauto. +- constructor. +Qed. + +Lemma select_inject: + forall ob ob' v1 v1' v2 v2' ty, + ob = None \/ ob = ob' -> + inject f v1 v1' -> inject f v2 v2' -> + inject f (select ob v1 v2 ty) (select ob' v1' v2' ty). +Proof. + intros; unfold select. destruct H. +- subst ob; auto. +- subst ob'; destruct ob as [b|]; auto. + apply normalize_inject. destruct b; auto. +Qed. + End VAL_INJ_OPS. End Val. -- cgit