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

1 files changed, 60 insertions, 0 deletions

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