diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:09:19 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:11:48 +0200 |
commit | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (patch) | |
tree | 597b2ccc5867bc2bbb083c4e13f792671b2042c1 /x86/SelectOpproof.v | |
parent | 36e64ee96ded0c94c83da6fb12202c276e66ba45 (diff) | |
parent | b7e0d70de2ace6f0a22f9f65cc244d875ee48496 (diff) | |
download | compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.tar.gz compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.zip |
Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion
Diffstat (limited to 'x86/SelectOpproof.v')
-rw-r--r-- | x86/SelectOpproof.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 1eeb5906..5e0f84e3 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -773,6 +773,32 @@ Proof. TrivialExists. Qed. +Theorem eval_select: + forall le ty cond al vl a1 v1 a2 v2 a b, + select ty cond al a1 a2 = Some a -> + eval_exprlist ge sp e m le al vl -> + eval_expr ge sp e m le a1 v1 -> + eval_expr ge sp e m le a2 v2 -> + eval_condition cond vl m = Some b -> + exists v, + eval_expr ge sp e m le a v + /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v. +Proof. + unfold select; intros. + destruct (select_supported ty); try discriminate. + destruct (select_swap cond); inv H. +- exists (Val.select (Some (negb b)) v2 v1 ty); split. + apply eval_Eop with (v2 :: v1 :: vl). + constructor; auto. constructor; auto. + simpl. rewrite eval_negate_condition, H3; auto. + destruct b; auto. +- exists (Val.select (Some b) v1 v2 ty); split. + apply eval_Eop with (v1 :: v2 :: vl). + constructor; auto. constructor; auto. + simpl. rewrite H3; auto. + auto. +Qed. + Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. Proof. red; intros. unfold singleoffloat. TrivialExists. |