x86 branchless implementation of unsigned int32 -> float conversion

Based on a suggestion by Rémi Hutin.
The new implementation produces smaller code (3 FP instructions and 2
integer "and") and has no conditional branch.
On average, it is a little slower than the old implementation.
Hence both implementations are supported:
- with -ffavor-branchless, use the new implementation
- by default, use the old, branching implementation

1 files changed, 12 insertions, 5 deletions

diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index cf0f37ec..df9c5394 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -497,6 +497,8 @@ Nondetfunction floatofint (e: expr) :=
   | _ => Eop Ofloatofint (e ::: Enil)
   end.
 
+Parameter favor_branchless: unit -> bool.
+
 Definition intuoffloat (e: expr) :=
   Elet e
     (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
@@ -508,11 +510,16 @@ 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 favor_branchless tt then
+      Elet e (subf 
+        (Eop Ofloatofint (andimm Float.ox7FFF_FFFF (Eletvar O) ::: Enil))
+        (Eop Ofloatofint (andimm Float.ox8000_0000 (Eletvar O) ::: Enil)))
+    else
+      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))
   end.
 
 Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil).