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 | |
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')
-rw-r--r-- | backend/NeedDomain.v | 28 | ||||
-rw-r--r-- | backend/ValueDomain.v | 58 |
2 files changed, 86 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) := |