From fe57280950fc20b2d1650a022033484b152ae51d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 14 Feb 2015 11:08:57 +0100 Subject: C reference implementation of the int64 helper functions. In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range. --- runtime/c/i64.h | 43 +++++++++++++ runtime/c/i64_dtos.c | 74 +++++++++++++++++++++++ runtime/c/i64_dtou.c | 69 +++++++++++++++++++++ runtime/c/i64_sar.c | 56 +++++++++++++++++ runtime/c/i64_sdiv.c | 51 ++++++++++++++++ runtime/c/i64_shl.c | 55 +++++++++++++++++ runtime/c/i64_shr.c | 55 +++++++++++++++++ runtime/c/i64_smod.c | 51 ++++++++++++++++ runtime/c/i64_stod.c | 46 ++++++++++++++ runtime/c/i64_stof.c | 56 +++++++++++++++++ runtime/c/i64_udiv.c | 45 ++++++++++++++ runtime/c/i64_udivmod.c | 158 ++++++++++++++++++++++++++++++++++++++++++++++++ runtime/c/i64_umod.c | 46 ++++++++++++++ runtime/c/i64_utod.c | 45 ++++++++++++++ runtime/c/i64_utof.c | 55 +++++++++++++++++ 15 files changed, 905 insertions(+) create mode 100644 runtime/c/i64.h create mode 100644 runtime/c/i64_dtos.c create mode 100644 runtime/c/i64_dtou.c create mode 100644 runtime/c/i64_sar.c create mode 100644 runtime/c/i64_sdiv.c create mode 100644 runtime/c/i64_shl.c create mode 100644 runtime/c/i64_shr.c create mode 100644 runtime/c/i64_smod.c create mode 100644 runtime/c/i64_stod.c create mode 100644 runtime/c/i64_stof.c create mode 100644 runtime/c/i64_udiv.c create mode 100644 runtime/c/i64_udivmod.c create mode 100644 runtime/c/i64_umod.c create mode 100644 runtime/c/i64_utod.c create mode 100644 runtime/c/i64_utof.c (limited to 'runtime/c') diff --git a/runtime/c/i64.h b/runtime/c/i64.h new file mode 100644 index 00000000..dd584533 --- /dev/null +++ b/runtime/c/i64.h @@ -0,0 +1,43 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +extern unsigned long long __i64_shl(unsigned long long x, int amount); +extern unsigned long long __i64_shr(unsigned long long x, int amount); +extern signed long long __i64_sar(signed long long x, int amount); + +extern unsigned long long __i64_udivmod(unsigned long long n, + unsigned long long d, + unsigned long long * rp); diff --git a/runtime/c/i64_dtos.c b/runtime/c/i64_dtos.c new file mode 100644 index 00000000..d428e744 --- /dev/null +++ b/runtime/c/i64_dtos.c @@ -0,0 +1,74 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Conversion float64 -> signed int64 */ + +long long __i64_dtos(double d) +{ + /* Extract bits of d's representation */ + union { double d; unsigned long long i; } buf; + buf.d = d; + unsigned int h = buf.i >> 32; + /* Extract unbiased exponent */ + int e = ((h & 0x7FF00000) >> 20) - (1023 + 52); + /* Check range of exponent */ + if (e < -52) { + /* |d| is less than 1.0 */ + return 0LL; + } + if (e >= 63 - 52) { + /* |d| is greater or equal to 2^63 */ + if ((int) h < 0) + return -0x8000000000000000LL; /* min signed long long */ + else + return 0x7FFFFFFFFFFFFFFFLL; /* max signed long long */ + } + /* Extract true mantissa */ + unsigned long long m = + (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL; + /* Shift it appropriately */ + if (e >= 0) + m = __i64_shl(m, e); + else + m = __i64_shr(m, -e); + /* Apply sign to result */ + if ((int) h < 0) + return -m; + else + return m; +} diff --git a/runtime/c/i64_dtou.c b/runtime/c/i64_dtou.c new file mode 100644 index 00000000..c5f9df4d --- /dev/null +++ b/runtime/c/i64_dtou.c @@ -0,0 +1,69 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Conversion float64 -> unsigned int64 */ + +unsigned long long __i64_dtou(double d) +{ + /* Extract bits of d's representation */ + union { double d; unsigned long long i; } buf; + buf.d = d; + unsigned int h = buf.i >> 32; + /* Negative FP numbers convert to 0 */ + if ((int) h < 0) return 0ULL; + /* Extract unbiased exponent */ + int e = ((h & 0x7FF00000) >> 20) - (1023 + 52); + /* Check range of exponent */ + if (e < -52) { + /* d is less than 1.0 */ + return 0ULL; + } + if (e >= 64 - 52) { + /* d is greater or equal to 2^64 */ + return 0xFFFFFFFFFFFFFFFFULL; /* max unsigned long long */ + } + /* Extract true mantissa */ + unsigned long long m = + (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL; + /* Shift it appropriately */ + if (e >= 0) + return __i64_shl(m, e); + else + return __i64_shr(m, -e); + +} diff --git a/runtime/c/i64_sar.c b/runtime/c/i64_sar.c new file mode 100644 index 00000000..a5f3364a --- /dev/null +++ b/runtime/c/i64_sar.c @@ -0,0 +1,56 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Shift right signed */ + +signed long long __i64_sar(signed long long x, int amount) +{ + unsigned xl = x; + int xh = x >> 32; + amount = amount & 63; + if (amount == 0) { + return x; + } + else if (amount < 32) { + unsigned rl = (xl >> amount) | (xh << (32 - amount)); + int rh = xh >> amount; + return rl | ((signed long long) rh << 32); + } else { + return (signed long long) (xh >> (amount - 32)); + } +} diff --git a/runtime/c/i64_sdiv.c b/runtime/c/i64_sdiv.c new file mode 100644 index 00000000..3f21d9b7 --- /dev/null +++ b/runtime/c/i64_sdiv.c @@ -0,0 +1,51 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Signed division */ + +signed long long __i64_sdiv(signed long long n, signed long long d) +{ + unsigned long long un, ud, uq, ur; + int nh = n >> 32, dh = d >> 32; + /* Take absolute values of n and d */ + un = nh < 0 ? -n : n; + ud = dh < 0 ? -d : d; + uq = __i64_udivmod(un, ud, &ur); + /* Apply sign to quotient */ + return (nh ^ dh) < 0 ? -uq : uq; +} diff --git a/runtime/c/i64_shl.c b/runtime/c/i64_shl.c new file mode 100644 index 00000000..9b9aae57 --- /dev/null +++ b/runtime/c/i64_shl.c @@ -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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Shift left */ + +unsigned long long __i64_shl(unsigned long long x, int amount) +{ + unsigned xl = x, xh = x >> 32; + amount = amount & 63; + if (amount == 0) { + return x; + } + else if (amount < 32) { + unsigned rl = xl << amount; + unsigned rh = (xh << amount) | (xl >> (32 - amount)); + return rl | ((unsigned long long) rh << 32); + } else { + return ((unsigned long long) (xl << (amount - 32))) << 32; + } +} diff --git a/runtime/c/i64_shr.c b/runtime/c/i64_shr.c new file mode 100644 index 00000000..c1db2a5f --- /dev/null +++ b/runtime/c/i64_shr.c @@ -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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Shift right unsigned */ + +unsigned long long __i64_shr(unsigned long long x, int amount) +{ + unsigned xl = x, xh = x >> 32; + amount = amount & 63; + if (amount == 0) { + return x; + } + else if (amount < 32) { + unsigned rl = (xl >> amount) | (xh << (32 - amount)); + unsigned rh = xh >> amount; + return rl | ((unsigned long long) rh << 32); + } else { + return (unsigned long long) (xh >> (amount - 32)); + } +} diff --git a/runtime/c/i64_smod.c b/runtime/c/i64_smod.c new file mode 100644 index 00000000..ab15b6e6 --- /dev/null +++ b/runtime/c/i64_smod.c @@ -0,0 +1,51 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Signed remainder */ + +signed long long __i64_smod(signed long long n, signed long long d) +{ + unsigned long long un, ud, ur; + int nh = n >> 32, dh = d >> 32; + /* Take absolute values of n and d */ + un = nh < 0 ? -n : n; + ud = dh < 0 ? -d : d; + (void) __i64_udivmod(un, ud, &ur); + /* Apply sign to remainder */ + return nh < 0 ? -ur : ur; +} diff --git a/runtime/c/i64_stod.c b/runtime/c/i64_stod.c new file mode 100644 index 00000000..158b6892 --- /dev/null +++ b/runtime/c/i64_stod.c @@ -0,0 +1,46 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Conversion from signed int64 to float64 */ + +double __i64_stod(signed long long x) +{ + unsigned xl = x; + signed xh = x >> 32; + return (double) xl + 0x1p+32 * (double) xh; +} diff --git a/runtime/c/i64_stof.c b/runtime/c/i64_stof.c new file mode 100644 index 00000000..8410ba13 --- /dev/null +++ b/runtime/c/i64_stof.c @@ -0,0 +1,56 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Conversion from signed int64 to float32 */ + +float __i64_stof(signed long long x) +{ + if (x < -(1LL << 53) || x >= (1LL << 53)) { + /* x is large enough that double rounding can occur. + Nudge x away from the points where double rounding occurs + (the "round to odd" technique) */ + unsigned delta = ((unsigned) x & 0x7FF) + 0x7FF; + x = (x | delta) & ~0x7FFLL; + } + /* Convert to double */ + unsigned xl = x; + signed xh = x >> 32; + double r = (double) xl + 0x1.0p32 * (double) xh; + /* Round to single */ + return (float) r; +} diff --git a/runtime/c/i64_udiv.c b/runtime/c/i64_udiv.c new file mode 100644 index 00000000..91fbf6e4 --- /dev/null +++ b/runtime/c/i64_udiv.c @@ -0,0 +1,45 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Unsigned division */ + +unsigned long long __i64_udiv(unsigned long long n, unsigned long long d) +{ + unsigned long long r; + return __i64_udivmod(n, d, &r); +} diff --git a/runtime/c/i64_udivmod.c b/runtime/c/i64_udivmod.c new file mode 100644 index 00000000..d8f5073a --- /dev/null +++ b/runtime/c/i64_udivmod.c @@ -0,0 +1,158 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include +#include "i64.h" + +static unsigned __i64_udiv6432(unsigned u1, unsigned u0, + unsigned v, unsigned *r); +static int __i64_nlz(unsigned x); + +/* Unsigned division and remainder */ + +unsigned long long __i64_udivmod(unsigned long long n, + unsigned long long d, + unsigned long long * rp) +{ + unsigned dh = d >> 32; + if (dh == 0) { + unsigned nh = n >> 32; + if (nh == 0) { + /* Special case 32 / 32 */ + unsigned nl = n; + unsigned dl = d; + *rp = (unsigned long long) (nl % dl); + return (unsigned long long) (nl / dl); + } else { + /* Special case 64 / 32 */ + unsigned nl = n; + unsigned dl = d; + unsigned qh = nh / dl; + unsigned rl; + unsigned ql = __i64_udiv6432(nh % dl, nl, dl, &rl); + *rp = (unsigned long long) rl; /* high word of remainder is 0 */ + return ((unsigned long long) qh) << 32 | ql; + } + } else { + /* General case 64 / 64 */ + unsigned dl = d; + /* Scale N and D down, giving N' and D' such that 2^31 <= D' < 2^32 */ + int s = 32 - __i64_nlz(dh); /* shift amount, between 1 and 32 */ + unsigned long long np = __i64_shr(n, s); + unsigned dp = (unsigned) __i64_shr(d, s); + /* Divide N' by D' to get an approximate quotient Q */ + unsigned q = __i64_udiv6432(np >> 32, np, dp, NULL); + again: ; + /* Tentative quotient Q is either correct or one too high */ + /* Compute Q * D, checking for overflow */ + unsigned long long p1 = (unsigned long long) dl * q; + unsigned long long p2 = (unsigned long long) (dh * q) << 32; + unsigned long long p = p1 + p2; + if (p < p1) { + /* Overflow occurred: adjust Q down by 1 and redo check */ + q = q - 1; goto again; + } + /* Compute remainder R */ + unsigned long long r = n - p; + if (n < p) { + /* Q is one too high, adjust Q down by 1 and R up by D */ + q = q - 1; r = r + d; + } + *rp = r; + return (unsigned long long) q; + } +} + +/* Unsigned division and remainder for 64 bits divided by 32 bits. */ +/* This is algorithm "divlu" from _Hacker's Delight_, fig 9.3 */ + +static unsigned __i64_udiv6432(unsigned u1, unsigned u0, + unsigned v, unsigned *r) +{ + const unsigned b = 65536; // Number base (16 bits). + unsigned un1, un0, // Norm. dividend LSD's. + vn1, vn0, // Norm. divisor digits. + q1, q0, // Quotient digits. + un32, un21, un10,// Divided digit pairs. + rhat; // A remainder. + int s; // Shift amount for norm. + + if (u1 >= v) { // If overflow, + if (r != NULL) *r = 0xFFFFFFFFU; // set rem to an impossible value, + return 0xFFFFFFFFU; // and return largest possible quotient. + } + s = __i64_nlz(v); // 0 <= s <= 31. + v = v << s; // Normalize divisor. + vn1 = v >> 16; // Break divisor up into + vn0 = v & 0xFFFF; // two 16-bit digits. + un32 = (u1 << s) | ((u0 >> (32 - s)) & (-s >> 31)); + un10 = u0 << s; // Shift dividend left. + un1 = un10 >> 16; // Break right half of + un0 = un10 & 0xFFFF; // dividend into two digits. + q1 = un32/vn1; // Compute the first quotient digit, q1. + rhat = un32 - q1*vn1; + again1: + if (q1 >= b || q1*vn0 > b*rhat + un1) { + q1 = q1 - 1; + rhat = rhat + vn1; + if (rhat < b) goto again1; + } + un21 = un32*b + un1 - q1*v; // Multiply and subtract. + q0 = un21/vn1; // Compute the second quotient digit, q0 + rhat = un21 - q0*vn1; +again2: + if (q0 >= b || q0*vn0 > b*rhat + un0) { + q0 = q0 - 1; + rhat = rhat + vn1; + if (rhat < b) goto again2; + } + if (r != NULL) *r = (un21*b + un0 - q0*v) >> s; + return q1*b + q0; +} + +/* Number of leading zeroes */ + +static int __i64_nlz(unsigned x) +{ + if (x == 0) return 32; + int n = 0; + if (x <= 0x0000FFFF) { n += 16; x <<= 16; } + if (x <= 0x00FFFFFF) { n += 8; x <<= 8; } + if (x <= 0x0FFFFFFF) { n += 4; x <<= 4; } + if (x <= 0x3FFFFFFF) { n += 2; x <<= 2; } + if (x <= 0x7FFFFFFF) { n += 1; x <<= 1; } + return n; +} diff --git a/runtime/c/i64_umod.c b/runtime/c/i64_umod.c new file mode 100644 index 00000000..d30e29c4 --- /dev/null +++ b/runtime/c/i64_umod.c @@ -0,0 +1,46 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Unsigned remainder */ + +unsigned long long __i64_umod(unsigned long long n, unsigned long long d) +{ + unsigned long long r; + (void) __i64_udivmod(n, d, &r); + return r; +} diff --git a/runtime/c/i64_utod.c b/runtime/c/i64_utod.c new file mode 100644 index 00000000..e70820a9 --- /dev/null +++ b/runtime/c/i64_utod.c @@ -0,0 +1,45 @@ +/***************************************************************** + * + * 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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Conversion from unsigned int64 to float64 */ + +double __i64_utod(unsigned long long x) +{ + unsigned xl = x, xh = x >> 32; + return (double) xl + 0x1.0p32 * (double) xh; +} diff --git a/runtime/c/i64_utof.c b/runtime/c/i64_utof.c new file mode 100644 index 00000000..87b85bfc --- /dev/null +++ b/runtime/c/i64_utof.c @@ -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 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 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. Reference C implementation */ + +#include "i64.h" + +/* Conversion from unsigned int64 to float32 */ + +float __i64_utof(unsigned long long x) +{ + if (x >= 1ULL << 53) { + /* x is large enough that double rounding can occur. + Nudge x away from the points where double rounding occurs + (the "round to odd" technique) */ + unsigned delta = ((unsigned) x & 0x7FF) + 0x7FF; + x = (x | delta) & ~0x7FFULL; + } + /* Convert to double */ + unsigned xl = x, xh = x >> 32; + double r = (double) xl + 0x1.0p32 * (double) xh; + /* Round to single */ + return (float) r; +} -- cgit