From 3830a91a4711c4570394e02e93e4e08db88eac6f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
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 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 86 insertions(+)

(limited to 'backend')

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) :=
-- 
cgit