Support for in64 -> float conversions w/ correct rounding.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 114 insertions, 2 deletions

diff --git a/runtime/ia32/i64_stod.S b/runtime/ia32/i64_stod.S
index 50ac06d..d020e2f 100644
--- a/runtime/ia32/i64_stod.S
+++ b/runtime/ia32/i64_stod.S
@@ -36,10 +36,14 @@
 	
 #include "sysdeps.h"
 
-// Conversion signed long -> float
+// Conversion signed long -> double-precision float
 
 FUNCTION(__i64_stod)
         fildll 4(%esp)
         ret
+    // The result is in extended precision (80 bits) and therefore
+    // exact (64 bits of mantissa).  It will be rounded to double
+    // precision by the caller, when transferring the result
+    // to an XMM register or a 64-bit stack slot.
 ENDFUNCTION(__i64_stod)
 
diff --git a/runtime/ia32/i64_stof.S b/runtime/ia32/i64_stof.S
new file mode 100644
index 0000000..25b1d4f
--- /dev/null
+++ b/runtime/ia32/i64_stof.S
@@ -0,0 +1,49 @@
+// *****************************************************************
+//
+//               The Compcert verified compiler
+//
+//           Xavier Leroy, INRIA Paris-Rocquencourt
+//
+// Copyright (c) 2013 Institut National de Recherche en Informatique et
+//  en Automatique.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//     * Redistributions of source code must retain the above copyright
+//       notice, this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//     * Neither the name of the <organization> nor the
+//       names of its contributors may be used to endorse or promote products
+//       derived from this software without specific prior written permission.
+// 
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+//
+// *********************************************************************
+
+// Helper functions for 64-bit integer arithmetic.  IA32 version.
+	
+#include "sysdeps.h"
+
+// Conversion signed long -> single-precision float
+
+FUNCTION(__i64_stof)
+        fildll 4(%esp)
+  // The TOS is in extended precision and therefore exact.
+  // Force rounding to single precision
+        fstps  4(%esp)
+        flds   4(%esp)
+        ret
+ENDFUNCTION(__i64_stof)
+
diff --git a/runtime/ia32/i64_utod.S b/runtime/ia32/i64_utod.S
index 7754ef2..428a3b9 100644
--- a/runtime/ia32/i64_utod.S
+++ b/runtime/ia32/i64_utod.S
@@ -36,7 +36,7 @@
 	
 #include "sysdeps.h"
 
-// Conversion unsigned long -> float
+// Conversion unsigned long -> double-precision float
 
 FUNCTION(__i64_utod)
         fildll 4(%esp)                  // convert as if signed
@@ -44,6 +44,10 @@ FUNCTION(__i64_utod)
         jns 1f
         fadds LC1                       // adjust by 2^64
 1:      ret
+    // The result is in extended precision (80 bits) and therefore
+    // exact (64 bits of mantissa).  It will be rounded to double
+    // precision by the caller, when transferring the result
+    // to an XMM register or a 64-bit stack slot.
 
         .p2align 2
 LC1:    .long 0x5f800000                // 2^64 in single precision
diff --git a/runtime/ia32/i64_utof.S b/runtime/ia32/i64_utof.S
new file mode 100644
index 0000000..0b58f48
--- /dev/null
+++ b/runtime/ia32/i64_utof.S
@@ -0,0 +1,55 @@
+// *****************************************************************
+//
+//               The Compcert verified compiler
+//
+//           Xavier Leroy, INRIA Paris-Rocquencourt
+//
+// Copyright (c) 2013 Institut National de Recherche en Informatique et
+//  en Automatique.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//     * Redistributions of source code must retain the above copyright
+//       notice, this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//     * Neither the name of the <organization> nor the
+//       names of its contributors may be used to endorse or promote products
+//       derived from this software without specific prior written permission.
+// 
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+//
+// *********************************************************************
+
+// Helper functions for 64-bit integer arithmetic.  IA32 version.
+	
+#include "sysdeps.h"
+
+// Conversion unsigned long -> single-precision float
+
+FUNCTION(__i64_utof)
+        fildll 4(%esp)                  // convert as if signed
+        cmpl $0, 8(%esp)                // is argument >= 2^63?
+        jns 1f
+        fadds LC1                       // adjust by 2^64
+  // The TOS is in extended precision and therefore exact.
+  // Force rounding to single precision
+1:      fstps  4(%esp)
+        flds   4(%esp)
+        ret
+
+        .p2align 2
+LC1:    .long 0x5f800000                // 2^64 in single precision
+
+ENDFUNCTION(__i64_utof)