1 files changed, 38 insertions, 12 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5f87d9b9..c3eda068 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -13,17 +13,10 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import Maps.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
 Require Import SelectOp.
 
 Local Open Scope cminorsel_scope.
@@ -812,7 +805,7 @@ Qed.
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
   red; intros. unfold cast8unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm; auto. compute; auto.
+  rewrite Val.zero_ext_and. apply eval_andimm; auto. omega.
 Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
@@ -825,7 +818,7 @@ Qed.
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
 Proof.
   red; intros. unfold cast16unsigned.
-  rewrite Val.zero_ext_and. apply eval_andimm; auto. compute; auto.
+  rewrite Val.zero_ext_and. apply eval_andimm; auto. omega.
 Qed.
 
 Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
@@ -1000,6 +993,27 @@ Proof.
   exists (Val.singleoffloat v); split. EvalOp. inv D; auto.
 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 (match ty with Tint => true | Tfloat => true | Tsingle => true | Tlong => Archi.ppc64 | _ => false end); inv H.
+  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_addressing:
   forall le chunk a v b ofs,
   eval_expr ge sp e m le a v ->
@@ -1044,4 +1058,16 @@ Proof.
 - constructor; auto.
 Qed.
 
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.