diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-07 09:06:29 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-07 09:08:40 +0200 |
| commit | 36ae0cba3a8cdec08b0f1f426b3ab27f8819afbe (patch) | |
| tree | 6660cbf48eefbb30f37138f5cebaccfca5be41e4 /x86/SelectOp.vp | |
| parent | f92ca339e9d1851fa4d469cdc867bfe1719c42a1 (diff) | |
| download | compcert-36ae0cba3a8cdec08b0f1f426b3ab27f8819afbe.tar.gz compcert-36ae0cba3a8cdec08b0f1f426b3ab27f8819afbe.zip | |
x86 branchless implementation of float -> unsigned int32 conversionfloatofintu
Adapted from Rémi Hutin's pull request #295.
On average it is slightly slower than the old, branch-full implementation,
hence flag -ffavor-branchless selects between the two implementations.
Diffstat (limited to 'x86/SelectOp.vp')
| -rw-r--r-- | x86/SelectOp.vp | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index df9c5394..701e8e0d 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -500,11 +500,17 @@ Nondetfunction floatofint (e: expr) := Parameter favor_branchless: unit -> bool. Definition intuoffloat (e: expr) := + let e1 := intoffloat (Eletvar 1%nat) in + let e2 := addimm Float.ox8000_0000 + (intoffloat (subf (Eletvar 1%nat) (Eletvar 0%nat))) in 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 favor_branchless tt then + Eop (Osel (Ccompf Clt) Tint) + (e1 ::: e2 ::: Eletvar 1 ::: Eletvar 0 ::: Enil) + else + Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + e1 e2))%nat. Nondetfunction floatofintu (e: expr) := match e with |