Implement a `Osel` operation for x86

The operation compiles down to conditional moves.

1 files changed, 26 insertions, 0 deletions

diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index fdbadaa8..b412ccf7 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -769,6 +769,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.