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.

3 files changed, 212 insertions, 0 deletions

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.