PowerPC: add SelectOp.select function

This function and its proof should have been part of commit 43e7b67.
They are already there for the other ports.

2 files changed, 31 insertions, 0 deletions

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index d2ca408a..41bc0efc 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -516,6 +516,17 @@ Definition singleofintu (e: expr) :=
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
+(** ** Selection *)
+
+Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
+  if match ty with
+     | Tint => true
+     | Tlong => Archi.ppc64
+     | _ => false
+     end
+  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
+  else None.
+
 (** ** Recognition of addressing modes for load and store operations *)
 
 Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5f87d9b9..5bf25722 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -1000,6 +1000,26 @@ 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 | 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 ->