Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 -> x86/x86_32/x86_64

Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.

This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true).  Unlike previous approaches, no other file is duplicated between these two variants of x86.

While we are at it, I renamed "ia32" into "x86" everywhere.  "ia32" is Intel speak for the 32-bit architecture.  It is not a good name to describe both the 32 and 64 bit architectures.

Finally, .depend is no longer under version control and is regenerated when the target architecture changes.  That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).

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)
+        
+