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 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'backend/NeedDomain.v') 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. *) -- cgit