diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-12 17:35:18 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-20 18:00:46 +0200 |
| commit | 3830a91a4711c4570394e02e93e4e08db88eac6f (patch) | |
| tree | 4008888998c3c61a8a18adc4ca37e3b8e2e34000 /backend/NeedDomain.v | |
| parent | e9cca9c8166fadb16c64df0fbb0b9ca640c0f594 (diff) | |
| download | compcert-kvx-3830a91a4711c4570394e02e93e4e08db88eac6f.tar.gz compcert-kvx-3830a91a4711c4570394e02e93e4e08db88eac6f.zip | |
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.
Diffstat (limited to 'backend/NeedDomain.v')
| -rw-r--r-- | backend/NeedDomain.v | 28 |
1 files changed, 28 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. *) |