Support for 64-bit architectures: x86 in 64-bit mode

This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.

To activate x86-64 bit support, configure with "x86_64-linux".

Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode

To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
  (currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.

1 files changed, 35 insertions, 4 deletions

diff --git a/configure b/configure
index c15ce3eb..ccdf6c27 100755
--- a/configure
+++ b/configure
@@ -40,6 +40,7 @@ Supported targets:
   ia32-bsd             (x86 32 bits, BSD)
   ia32-macosx          (x86 32 bits, MacOS X)
   ia32-cygwin          (x86 32 bits, Cygwin environment under Windows)
+  x86_64-linux         (x86 64 bits, Linux)
   manual               (edit configuration file by hand)
 
 For PowerPC targets, the "ppc-" prefix can be refined into:
@@ -118,7 +119,9 @@ case "$target" in
   armebv7m-*)
       arch="arm"; model="armv7m"; endianness="big";;
   ia32-*)
-      arch="ia32"; model="sse2"; endianness="little";;
+      arch="ia32"; model="32sse2"; endianness="little";;
+  x86_64-*)
+      arch="ia32"; model="64"; endianness="little";;
   powerpc-*|ppc-*)
       arch="powerpc"; model="ppc32"; endianness="big";;
   powerpc64-*|ppc64-*)
@@ -239,9 +242,9 @@ fi
 
 
 #
-# IA32 Target Configuration
+# IA32 (32 bits) Target Configuration
 #
-if test "$arch" = "ia32"; then
+if test "$arch" = "ia32" -a "$model" != "64"; then
 
   case "$target" in
     bsd)
@@ -318,6 +321,33 @@ if test "$arch" = "ia32"; then
 fi
 
 #
+# IA32 (64 bits) Target Configuration
+#
+if test "$arch" = "ia32" -a "$model" = "64"; then
+
+  case "$target" in
+    linux)
+        abi="standard"
+        casm="${toolprefix}gcc"
+        casm_options="-m64 -c"
+        cc="${toolprefix}gcc -m64"
+        clinker="${toolprefix}gcc"
+        clinker_options="-m64"
+        cprepro="${toolprefix}gcc"
+        cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
+        libmath="-lm"
+        struct_passing="ref-callee"   # wrong!
+        struct_return="ref"           # to check!
+        system="linux"
+        ;;
+    *)
+        echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2
+        echo "$usage" 1>&2
+        exit 2;;
+  esac
+fi
+
+#
 # Finalize Target Configuration
 #
 if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi
@@ -491,7 +521,8 @@ ARCH=
 # MODEL=armv7a      # for ARM
 # MODEL=armv7r      # for ARM
 # MODEL=armv7m      # for ARM
-# MODEL=sse2        # for IA32
+# MODEL=32sse2      # for IA32 in 32-bit mode
+# MODEL=64          # for IA32 in 64-bit mode
 MODEL=
 
 # Target ABI