diff options
Diffstat (limited to 'runtime/x86_32')
| -rw-r--r-- | runtime/x86_32/i64_dtos.S | 60 | ||||
| -rw-r--r-- | runtime/x86_32/i64_dtou.S | 88 | ||||
| -rw-r--r-- | runtime/x86_32/i64_sar.S | 60 | ||||
| -rw-r--r-- | runtime/x86_32/i64_sdiv.S | 74 | ||||
| -rw-r--r-- | runtime/x86_32/i64_shl.S | 59 | ||||
| -rw-r--r-- | runtime/x86_32/i64_shr.S | 59 | ||||
| -rw-r--r-- | runtime/x86_32/i64_smod.S | 70 | ||||
| -rw-r--r-- | runtime/x86_32/i64_smulh.S | 94 | ||||
| -rw-r--r-- | runtime/x86_32/i64_stod.S | 49 | ||||
| -rw-r--r-- | runtime/x86_32/i64_stof.S | 49 | ||||
| -rw-r--r-- | runtime/x86_32/i64_udiv.S | 52 | ||||
| -rw-r--r-- | runtime/x86_32/i64_udivmod.S | 104 | ||||
| -rw-r--r-- | runtime/x86_32/i64_umod.S | 51 | ||||
| -rw-r--r-- | runtime/x86_32/i64_umulh.S | 74 | ||||
| -rw-r--r-- | runtime/x86_32/i64_utod.S | 55 | ||||
| -rw-r--r-- | runtime/x86_32/i64_utof.S | 55 | ||||
| -rw-r--r-- | runtime/x86_32/sysdeps.h | 75 | ||||
| -rw-r--r-- | runtime/x86_32/vararg.S | 81 |
18 files changed, 1209 insertions, 0 deletions
diff --git a/runtime/x86_32/i64_dtos.S b/runtime/x86_32/i64_dtos.S new file mode 100644 index 00000000..3cc381bf --- /dev/null +++ b/runtime/x86_32/i64_dtos.S @@ -0,0 +1,60 @@ +// ***************************************************************** +// +// 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 float -> signed long + +FUNCTION(__i64_dtos) + subl $4, %esp + // Change rounding mode to "round towards zero" + fnstcw 0(%esp) + movw 0(%esp), %ax + movb $12, %ah + movw %ax, 2(%esp) + fldcw 2(%esp) + // Convert + fldl 8(%esp) + fistpll 8(%esp) + // Restore rounding mode + fldcw 0(%esp) + // Load result in edx:eax + movl 8(%esp), %eax + movl 12(%esp), %edx + addl $4, %esp + ret +ENDFUNCTION(__i64_dtos) + diff --git a/runtime/x86_32/i64_dtou.S b/runtime/x86_32/i64_dtou.S new file mode 100644 index 00000000..4903f847 --- /dev/null +++ b/runtime/x86_32/i64_dtou.S @@ -0,0 +1,88 @@ +// ***************************************************************** +// +// 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 float -> unsigned long + +FUNCTION(__i64_dtou) + subl $4, %esp + // Compare argument with 2^63 + fldl 8(%esp) + flds LC1 + fucomp + fnstsw %ax + sahf + jbe 1f // branch if not (ARG < 2^63) + // Argument < 2^63: convert as is + // Change rounding mode to "round towards zero" + fnstcw 0(%esp) + movw 0(%esp), %ax + movb $12, %ah + movw %ax, 2(%esp) + fldcw 2(%esp) + // Convert + fistpll 8(%esp) + movl 8(%esp), %eax + movl 12(%esp), %edx + // Restore rounding mode + fldcw 0(%esp) + addl $4, %esp + ret + // Argument > 2^63: offset ARG by -2^63, then convert, then offset RES by 2^63 +1: fsubs LC1 + // Change rounding mode to "round towards zero" + fnstcw 0(%esp) + movw 0(%esp), %ax + movb $12, %ah + movw %ax, 2(%esp) + fldcw 2(%esp) + // Convert + fistpll 8(%esp) + movl 8(%esp), %eax + movl 12(%esp), %edx + // Offset result by 2^63 + addl $0x80000000, %edx + // Restore rounding mode + fldcw 0(%esp) + addl $4, %esp + ret + + .p2align 2 +LC1: .long 0x5f000000 // 2^63 in single precision + +ENDFUNCTION(__i64_dtou) +
\ No newline at end of file diff --git a/runtime/x86_32/i64_sar.S b/runtime/x86_32/i64_sar.S new file mode 100644 index 00000000..cf2233b1 --- /dev/null +++ b/runtime/x86_32/i64_sar.S @@ -0,0 +1,60 @@ +// ***************************************************************** +// +// 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" + +// Shift right signed + +// Note: IA32 shift instructions treat their amount (in %cl) modulo 32 + +FUNCTION(__i64_sar) + movl 12(%esp), %ecx // ecx = shift amount, treated mod 64 + testb $32, %cl + jne 1f + // shift amount < 32 + movl 4(%esp), %eax + movl 8(%esp), %edx + shrdl %cl, %edx, %eax // eax = low(XH:XL >> amount) + sarl %cl, %edx // edx = XH >> amount (signed) + ret + // shift amount >= 32 +1: movl 8(%esp), %eax + movl %eax, %edx + sarl %cl, %eax // eax = XH >> (amount - 32) + sarl $31, %edx // edx = sign of X + ret +ENDFUNCTION(__i64_sar) + diff --git a/runtime/x86_32/i64_sdiv.S b/runtime/x86_32/i64_sdiv.S new file mode 100644 index 00000000..f6551c7d --- /dev/null +++ b/runtime/x86_32/i64_sdiv.S @@ -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 <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" + +// Signed division + +FUNCTION(__i64_sdiv) + pushl %ebp + pushl %esi + pushl %edi + movl 20(%esp), %esi // esi = NH + movl %esi, %ebp // save sign of N in ebp + testl %esi, %esi + jge 1f // if N < 0, + negl 16(%esp) // N = -N + adcl $0, %esi + negl %esi + movl %esi, 20(%esp) +1: movl 28(%esp), %esi // esi = DH + xorl %esi, %ebp // sign of result in ebp + testl %esi, %esi + jge 2f // if D < 0, + negl 24(%esp) // D = -D + adcl $0, %esi + negl %esi + movl %esi, 28(%esp) +2: call GLOB(__i64_udivmod) + testl %ebp, %ebp // apply sign to result + jge 3f + negl %esi + adcl $0, %edi + negl %edi +3: movl %esi, %eax + movl %edi, %edx + popl %edi + popl %esi + popl %ebp + ret +ENDFUNCTION(__i64_sdiv) + diff --git a/runtime/x86_32/i64_shl.S b/runtime/x86_32/i64_shl.S new file mode 100644 index 00000000..1fabebce --- /dev/null +++ b/runtime/x86_32/i64_shl.S @@ -0,0 +1,59 @@ +// ***************************************************************** +// +// 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" + +// Shift left + +// Note: IA32 shift instructions treat their amount (in %cl) modulo 32 + +FUNCTION(__i64_shl) + movl 12(%esp), %ecx // ecx = shift amount, treated mod 64 + testb $32, %cl + jne 1f + // shift amount < 32 + movl 4(%esp), %eax + movl 8(%esp), %edx + shldl %cl, %eax, %edx // edx = high(XH:XL << amount) + shll %cl, %eax // eax = XL << amount + ret + // shift amount >= 32 +1: movl 4(%esp), %edx + shll %cl, %edx // edx = XL << (amount - 32) + xorl %eax, %eax // eax = 0 + ret +ENDFUNCTION(__i64_shl) + diff --git a/runtime/x86_32/i64_shr.S b/runtime/x86_32/i64_shr.S new file mode 100644 index 00000000..34196f09 --- /dev/null +++ b/runtime/x86_32/i64_shr.S @@ -0,0 +1,59 @@ +// ***************************************************************** +// +// 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" + +// Shift right unsigned + +// Note: IA32 shift instructions treat their amount (in %cl) modulo 32 + +FUNCTION(__i64_shr) + movl 12(%esp), %ecx // ecx = shift amount, treated mod 64 + testb $32, %cl + jne 1f + // shift amount < 32 + movl 4(%esp), %eax + movl 8(%esp), %edx + shrdl %cl, %edx, %eax // eax = low(XH:XL >> amount) + shrl %cl, %edx // edx = XH >> amount + ret + // shift amount >= 32 +1: movl 8(%esp), %eax + shrl %cl, %eax // eax = XH >> (amount - 32) + xorl %edx, %edx // edx = 0 + ret +ENDFUNCTION(__i64_shr) + diff --git a/runtime/x86_32/i64_smod.S b/runtime/x86_32/i64_smod.S new file mode 100644 index 00000000..28f47ad4 --- /dev/null +++ b/runtime/x86_32/i64_smod.S @@ -0,0 +1,70 @@ +// ***************************************************************** +// +// 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" + +// Signed remainder + +FUNCTION(__i64_smod) + pushl %ebp + pushl %esi + pushl %edi + movl 20(%esp), %esi // esi = NH + movl %esi, %ebp // save sign of result in ebp + testl %esi, %esi + jge 1f // if N < 0, + negl 16(%esp) // N = -N + adcl $0, %esi + negl %esi + movl %esi, 20(%esp) +1: movl 28(%esp), %esi // esi = DH + testl %esi, %esi + jge 2f // if D < 0, + negl 24(%esp) // D = -D + adcl $0, %esi + negl %esi + movl %esi, 28(%esp) +2: call GLOB(__i64_udivmod) + testl %ebp, %ebp // apply sign to result + jge 3f + negl %eax + adcl $0, %edx + negl %edx +3: popl %edi + popl %esi + popl %ebp + ret +ENDFUNCTION(__i64_smod) diff --git a/runtime/x86_32/i64_smulh.S b/runtime/x86_32/i64_smulh.S new file mode 100644 index 00000000..cc0f0167 --- /dev/null +++ b/runtime/x86_32/i64_smulh.S @@ -0,0 +1,94 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, INRIA Paris +// +// Copyright (c) 2016 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" + +// Multiply-high signed + +#define XL 12(%esp) +#define XH 16(%esp) +#define YL 20(%esp) +#define YH 24(%esp) + +// Hacker's Delight section 8.3: +// - compute high 64 bits of the unsigned product X * Y (see i64_umulh.S) +// - subtract X if Y < 0 +// - subtract Y if X < 0 + +FUNCTION(__i64_smulh) + pushl %esi + pushl %edi + movl XL, %eax + mull YL // EDX:EAX = 64-bit product XL.YL + movl %edx, %ecx + xorl %esi, %esi + xorl %edi, %edi // EDI:ESI:ECX accumulatesbits 127:32 of result + movl XH, %eax + mull YL // EDX:EAX = 64-bit product XH.YL + addl %eax, %ecx + adcl %edx, %esi + adcl $0, %edi + movl YH, %eax + mull XL // EDX:EAX = 64-bit product YH.XL + addl %eax, %ecx + adcl %edx, %esi + adcl $0, %edi + movl XH, %eax + mull YH // EDX:EAX = 64-bit product XH.YH + addl %eax, %esi + adcl %edx, %edi +// Here, EDI:ESI is the high 64 bits of the unsigned product X.Y + xorl %eax, %eax + xorl %edx, %edx + cmpl $0, XH + cmovl YL, %eax + cmovl YH, %edx // EDX:EAX = Y if X < 0, = 0 if X >= 0 + subl %eax, %esi + sbbl %edx, %edi // EDI:ESI -= Y if X < 0 + xorl %eax, %eax + xorl %edx, %edx + cmpl $0, YH + cmovl XL, %eax + cmovl XH, %edx // EDX:EAX = X if Y < 0, = 0 if Y >= 0 + subl %eax, %esi + sbbl %edx, %edi // EDI:ESI -= X if Y < 0 +// Now EDI:ESI contains the high 64 bits of the signed product X.Y + movl %esi, %eax + movl %edi, %edx + popl %edi + popl %esi + ret +ENDFUNCTION(__i64_smulh) diff --git a/runtime/x86_32/i64_stod.S b/runtime/x86_32/i64_stod.S new file mode 100644 index 00000000..d020e2fc --- /dev/null +++ b/runtime/x86_32/i64_stod.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 -> 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/x86_32/i64_stof.S b/runtime/x86_32/i64_stof.S new file mode 100644 index 00000000..25b1d4f7 --- /dev/null +++ b/runtime/x86_32/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/x86_32/i64_udiv.S b/runtime/x86_32/i64_udiv.S new file mode 100644 index 00000000..75305433 --- /dev/null +++ b/runtime/x86_32/i64_udiv.S @@ -0,0 +1,52 @@ +// ***************************************************************** +// +// 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" + +// Unsigned division + +FUNCTION(__i64_udiv) + pushl %ebp + pushl %esi + pushl %edi + call GLOB(__i64_udivmod) + movl %esi, %eax + movl %edi, %edx + popl %edi + popl %esi + popl %ebp + ret +ENDFUNCTION(__i64_udiv) diff --git a/runtime/x86_32/i64_udivmod.S b/runtime/x86_32/i64_udivmod.S new file mode 100644 index 00000000..dccfc286 --- /dev/null +++ b/runtime/x86_32/i64_udivmod.S @@ -0,0 +1,104 @@ +// ***************************************************************** +// +// 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" + +// Division and remainder + +// Auxiliary function, never called directly from C code +// Input: 20(esp), 24(esp) is dividend N +// 28(esp), 32(esp) is divisor D +// Output: esi:edi is quotient Q +// eax:edx is remainder R +// ebp is preserved + +FUNCTION(__i64_udivmod) + cmpl $0, 32(%esp) // single-word divisor? (DH = 0) + jne 1f + // Special case 64 bits divided by 32 bits + movl 28(%esp), %ecx // divide NH by DL + movl 24(%esp), %eax // (will trap if D = 0) + xorl %edx, %edx + divl %ecx // eax = quotient, edx = remainder + movl %eax, %edi // high word of quotient in edi + movl 20(%esp), %eax // divide rem : NL by DL + divl %ecx // eax = quotient, edx = remainder + movl %eax, %esi // low word of quotient in esi */ + movl %edx, %eax // low word of remainder in eax + xorl %edx, %edx // high word of remainder is 0, in edx + ret + // The general case +1: movl 28(%esp), %ecx // esi:ecx = D + movl 32(%esp), %esi + movl 20(%esp), %eax // edx:eax = N + movl 24(%esp), %edx + // Scale D and N down, giving D' and N', until D' fits in 32 bits +2: shrl $1, %esi // shift D' right by one + rcrl $1, %ecx + shrl $1, %edx // shift N' right by one + rcrl $1, %eax + testl %esi, %esi // repeat until D'H = 0 + jnz 2b + // Divide N' by D' to get an approximate quotient + divl %ecx // eax = quotient, edx = remainder + movl %eax, %esi // save tentative quotient Q in esi + // Check for off by one quotient + // Compute Q * D +3: movl 32(%esp), %ecx + imull %esi, %ecx // ecx = Q * DH + movl 28(%esp), %eax + mull %esi // edx:eax = Q * DL + add %ecx, %edx // edx:eax = Q * D + jc 5f // overflow in addition means Q is too high + // Compare Q * D with N, computing the remainder in the process + movl %eax, %ecx + movl 20(%esp), %eax + subl %ecx, %eax + movl %edx, %ecx + movl 24(%esp), %edx + sbbl %ecx, %edx // edx:eax = N - Q * D + jnc 4f // no carry: N >= Q * D, we are fine + decl %esi // carry: N < Q * D, adjust Q down by 1 + addl 28(%esp), %eax // and remainder up by D + adcl 32(%esp), %edx + // Finished +4: xorl %edi, %edi // high half of quotient is 0 + ret + // Special case when Q * D overflows +5: decl %esi // adjust Q down by 1 + jmp 3b // and redo check & computation of remainder + +ENDFUNCTION(__i64_udivmod) diff --git a/runtime/x86_32/i64_umod.S b/runtime/x86_32/i64_umod.S new file mode 100644 index 00000000..a019df28 --- /dev/null +++ b/runtime/x86_32/i64_umod.S @@ -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 <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" + +// Unsigned remainder + +FUNCTION(__i64_umod) + pushl %ebp + pushl %esi + pushl %edi + call GLOB(__i64_udivmod) + popl %edi + popl %esi + popl %ebp + ret +ENDFUNCTION(__i64_umod) + diff --git a/runtime/x86_32/i64_umulh.S b/runtime/x86_32/i64_umulh.S new file mode 100644 index 00000000..449a0f8b --- /dev/null +++ b/runtime/x86_32/i64_umulh.S @@ -0,0 +1,74 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, INRIA Paris +// +// Copyright (c) 2016 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" + +// Multiply-high unsigned + +#define XL 12(%esp) +#define XH 16(%esp) +#define YL 20(%esp) +#define YH 24(%esp) + +// X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL + +FUNCTION(__i64_umulh) + pushl %esi + pushl %edi + movl XL, %eax + mull YL // EDX:EAX = 64-bit product XL.YL + movl %edx, %ecx + xorl %esi, %esi + xorl %edi, %edi // EDI:ESI:ECX accumulate bits 127:32 of result + movl XH, %eax + mull YL // EDX:EAX = 64-bit product XH.YL + addl %eax, %ecx + adcl %edx, %esi + adcl $0, %edi + movl YH, %eax + mull XL // EDX:EAX = 64-bit product YH.XL + addl %eax, %ecx + adcl %edx, %esi + adcl $0, %edi + movl XH, %eax + mull YH // EDX:EAX = 64-bit product XH.YH + addl %esi, %eax + adcl %edi, %edx + popl %edi + popl %esi + ret +ENDFUNCTION(__i64_umulh) + diff --git a/runtime/x86_32/i64_utod.S b/runtime/x86_32/i64_utod.S new file mode 100644 index 00000000..428a3b94 --- /dev/null +++ b/runtime/x86_32/i64_utod.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 -> double-precision float + +FUNCTION(__i64_utod) + fildll 4(%esp) // convert as if signed + cmpl $0, 8(%esp) // is argument >= 2^63? + 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 + +ENDFUNCTION(__i64_utod) diff --git a/runtime/x86_32/i64_utof.S b/runtime/x86_32/i64_utof.S new file mode 100644 index 00000000..0b58f48b --- /dev/null +++ b/runtime/x86_32/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) diff --git a/runtime/x86_32/sysdeps.h b/runtime/x86_32/sysdeps.h new file mode 100644 index 00000000..9d957a88 --- /dev/null +++ b/runtime/x86_32/sysdeps.h @@ -0,0 +1,75 @@ +// ***************************************************************** +// +// 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. +// +// ********************************************************************* + +// System dependencies + +#if defined(SYS_linux) || defined(SYS_bsd) + +#define GLOB(x) x +#define FUNCTION(f) \ + .text; \ + .globl f; \ + .align 16; \ +f: + +#define ENDFUNCTION(f) \ + .type f, @function; .size f, . - f + +#endif + +#if defined(SYS_macosx) + +#define GLOB(x) _##x +#define FUNCTION(f) \ + .text; \ + .globl _##f; \ + .align 4; \ +_##f: + +#define ENDFUNCTION(f) + +#endif + +#if defined(SYS_cygwin) + +#define GLOB(x) _##x +#define FUNCTION(f) \ + .text; \ + .globl _##f; \ + .align 16; \ +_##f: + +#define ENDFUNCTION(f) + +#endif diff --git a/runtime/x86_32/vararg.S b/runtime/x86_32/vararg.S new file mode 100644 index 00000000..78666c70 --- /dev/null +++ b/runtime/x86_32/vararg.S @@ -0,0 +1,81 @@ +// ***************************************************************** +// +// 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 variadic functions <stdarg.h>. IA32 version + +#include "sysdeps.h" + +// typedef void * va_list; +// unsigned int __compcert_va_int32(va_list * ap); +// unsigned long long __compcert_va_int64(va_list * ap); +// double __compcert_va_float64(va_list * ap); + +FUNCTION(__compcert_va_int32) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 0(%ecx), %edx // %edx = current argument pointer + movl 0(%edx), %eax // load the int32 value there + addl $4, %edx // increment argument pointer by 4 + movl %edx, 0(%ecx) + ret +ENDFUNCTION(__compcert_va_int32) + +FUNCTION(__compcert_va_int64) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 0(%ecx), %edx // %edx = current argument pointer + movl 0(%edx), %eax // load the int64 value there + movl 4(%edx), %edx + addl $8, 0(%ecx) // increment argument pointer by 8 + ret +ENDFUNCTION(__compcert_va_int64) + +FUNCTION(__compcert_va_float64) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 0(%ecx), %edx // %edx = current argument pointer + fldl 0(%edx) // load the float64 value there + addl $8, %edx // increment argument pointer by 8 + movl %edx, 0(%ecx) + ret +ENDFUNCTION(__compcert_va_float64) + +FUNCTION(__compcert_va_composite) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 8(%esp), %edx // %edx = size of composite in bytes + movl 0(%ecx), %eax // %eax = current argument pointer + leal 3(%eax, %edx), %edx // advance by size + andl $0xfffffffc, %edx // and round up to multiple of 4 + movl %edx, 0(%ecx) // update argument pointer + ret +ENDFUNCTION(__compcert_va_composite) + + |