1 files changed, 52 insertions, 12 deletions
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index eadda093..a23c37d5 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -38,9 +38,10 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST Integers Floats.
+Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
 Require Import OpHelpers.
+Require Archi.
 
 Local Open Scope cminorsel_scope.
 
@@ -457,7 +458,35 @@ Nondetfunction cast16signed (e: expr) :=
       Eop Ocast16signed (e ::: Enil)
   end.
 
-(** Floating-point conversions *)
+(** ** Selection *)
+
+Definition select_supported (ty: typ) : bool :=
+  match ty with
+  | Tint => true
+  | Tlong => Archi.ptr64
+  | _ => false
+  end.
+
+(** [Asmgen.mk_sel] cannot always handle the conditions that are
+    implemented as a "and" of two processor flags.  However it can
+    handle the negation of those conditions, which are implemented
+    as an "or".  So, for the risky conditions we just take their
+    negation and swap the two arguments of the [select]. *)
+
+Definition select_swap (cond: condition) :=
+  match cond with
+  | Ccompf Cne | Ccompfs Cne | Cnotcompf Ceq | Cnotcompfs Ceq => true
+  | _ => false
+  end.
+
+Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
+  if select_supported ty then
+    if select_swap cond
+    then Some (Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args))
+    else Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
+  else None.
+
+(** ** Floating-point conversions *)
 
 Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
 Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
@@ -471,21 +500,27 @@ Nondetfunction floatofint (e: expr) :=
   end.
 
 Definition intuoffloat (e: expr) :=
-  Elet e
-    (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
-      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
-        (intoffloat (Eletvar 1))
-        (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.
+  if Archi.splitlong then
+    Elet e
+      (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
+        (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
+          (intoffloat (Eletvar 1))
+          (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat
+  else
+    Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil).
 
 Nondetfunction floatofintu (e: expr) :=
   match e with
   | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
-    let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
-    Elet e
-      (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
-        (floatofint (Eletvar O))
-        (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
+    if Archi.splitlong then
+      let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
+      Elet e
+        (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
+          (floatofint (Eletvar O))
+          (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
+    else
+      Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil)
   end.
 
 Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil).
@@ -548,3 +583,8 @@ Definition divf_base (e1: expr) (e2: expr) :=
 
 Definition divfs_base (e1: expr) (e2: expr) :=
   Eop Odivfs (e1 ::: e2 ::: Enil).
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.