configure: distinguish between ABI and processor model.

ARM: various tweaks, incl. support for SDIV and UDIV insns when available.
test/regression/funptr2.c: Thumb does weird things with <function ptr>+1.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 55 insertions, 27 deletions

diff --git a/configure b/configure
index c7e7847..603b30a 100755
--- a/configure
+++ b/configure
@@ -27,14 +27,20 @@ Supported targets:
   ppc-eabi-diab    (PowerPC, EABI with Diab tools)
   arm-linux        (ARM, EABI)
   arm-eabi         (ARM, EABI)
-  arm-eabihf       (ARM, EABI with hardware floating point)
-  arm-hardfloat    (ARM, EABI with hardware floating point)
+  arm-eabihf       (ARM, EABI using hardware FP registers)
+  arm-hardfloat    (ARM, EABI using hardware FP registers)
   ia32-linux       (x86 32 bits, Linux)
   ia32-bsd         (x86 32 bits, BSD)
   ia32-macosx      (x86 32 bits, MacOS X)
   ia32-cygwin      (x86 32 bits, Cygwin environment under Windows)
   manual           (edit configuration file by hand)
 
+For ARM targets, the "arm-" prefix can be refined into:
+  armv6-           ARMv6 + VFPv2
+  armv7a-          ARMv7a + VFPv3-d16   (default)
+  armv7r-          ARMv7r + VFPv3-d16
+  armv7m-          ARMv7m + VFPv3-d16
+
 Options:
   -prefix <dir>    Install in <dir>/bin and <dir>/lib/compcert
   -bindir <dir>    Install binaries in <dir>
@@ -74,7 +80,8 @@ asm_supports_cfi=""
 case "$target" in
   powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi)
     arch="powerpc"
-    variant="eabi"
+    model="standard"
+    abi="eabi"
     system="linux"
     cc="${toolprefix}gcc"
     cprepro="${toolprefix}gcc -U__GNUC__ -E"
@@ -85,7 +92,8 @@ case "$target" in
     cchecklink=true;;
   powerpc-eabi-diab|ppc-eabi-diab)
     arch="powerpc"
-    variant="eabi"
+    model="standard"
+    abi="eabi"
     system="diab"
     cc="${toolprefix}dcc"
     cprepro="${toolprefix}dcc -E"
@@ -94,18 +102,22 @@ case "$target" in
     clinker="${toolprefix}dcc"
     libmath="-lm"
     cchecklink=true;;
-  arm-linux|arm-eabi)
+  arm*-*)
     arch="arm"
-    variant="eabi"
-    system="linux"
-    cc="${toolprefix}gcc"
-    cprepro="${toolprefix}gcc -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
-    casm="${toolprefix}gcc -c"
-    clinker="${toolprefix}gcc"
-    libmath="-lm";;
-  arm-eabihf|arm-hardfloat)
-    arch="arm"
-    variant="hardfloat"
+    case "$target" in
+      armv6-*) model="armv6";;
+      arm-*|armv7a-*) model="armv7a";;
+      armv7r-*) model="armv7r";;
+      armv7m-*) model="armv7m";;
+      *)
+        echo "Unknown target '$target'." 1>&2
+        echo "$usage" 1>&2
+        exit 2;;
+    esac
+    case "$target" in
+      *-eabi) abi="eabi";;
+      *-eabihf|*-hf|*-hardfloat) abi="hardfloat";;
+    esac
     system="linux"
     cc="${toolprefix}gcc"
     cprepro="${toolprefix}gcc -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
@@ -114,7 +126,8 @@ case "$target" in
     libmath="-lm";;
   ia32-linux)
     arch="ia32"
-    variant="standard"
+    model="sse2"
+    abi="standard"
     system="linux"
     cc="${toolprefix}gcc -m32"
     cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E"
@@ -123,7 +136,8 @@ case "$target" in
     libmath="-lm";;
   ia32-bsd)
     arch="ia32"
-    variant="standard"
+    model="sse2"
+    abi="standard"
     system="bsd"
     cc="${toolprefix}gcc -m32"
     cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E"
@@ -132,7 +146,8 @@ case "$target" in
     libmath="-lm";;
   ia32-macosx)
     arch="ia32"
-    variant="standard"
+    model="sse2"
+    abi="standard"
     system="macosx"
     cc="${toolprefix}gcc -arch i386"
     cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' -E"
@@ -146,7 +161,8 @@ case "$target" in
     libmath="";;
   ia32-cygwin)
     arch="ia32"
-    variant="standard"
+    model="sse2"
+    abi="standard"
     system="cygwin"
     cc="${toolprefix}gcc -m32"
     cprepro="${toolprefix}gcc -m32 -U__GNUC__ -E"
@@ -199,11 +215,11 @@ case "$coq_ver" in
         echo "version $coq_ver -- good!";;
   ?.*)
         echo "version $coq_ver -- UNSUPPORTED"
-        echo "Error: CompCert requires Coq version 8.4pl1 or 8.4pl2 or 8.4pl3."
+        echo "Error: CompCert requires Coq version 8.4, pl1 and up."
         missingtools=true;;
   *)
         echo "NOT FOUND"
-        echo "Error: make sure Coq version 8.4pl3 is installed."
+        echo "Error: make sure Coq version 8.4pl4 is installed."
         missingtools=true;;
 esac
 
@@ -264,7 +280,8 @@ EOF
 if test "$target" != "manual"; then
 cat >> Makefile.config <<EOF
 ARCH=$arch
-VARIANT=$variant
+MODEL=$model
+ABI=$abi
 SYSTEM=$system
 CC=$cc
 CPREPRO=$cprepro
@@ -285,11 +302,21 @@ cat >> Makefile.config <<'EOF'
 # ARCH=ia32
 ARCH=
 
+# Hardware variant
+# MODEL=standard  # for PowerPC
+# MODEL=armv6     # for ARM
+# MODEL=armv7a    # for ARM
+# MODEL=armv7r    # for ARM
+# MODEL=armv7m    # for ARM
+# MODEL=sse2      # for IA32
+MODEL=
+
 # Target ABI
-# VARIANT=eabi     # for PowerPC / Linux and other SVR4 or EABI platforms
-# VARIANT=linux    # for ARM
-# VARIANT=standard # for IA32
-VARIANT=
+# ABI=eabi     # for PowerPC / Linux and other SVR4 or EABI platforms
+# ABI=eabi     # for ARM
+# ABI=hardfloat # for ARM
+# ABI=standard # for IA32
+ABI=
 
 # Target operating system and development environment
 # Possible choices for PowerPC:
@@ -355,7 +382,8 @@ cat <<EOF
 
 CompCert configuration:
     Target architecture........... $arch
-    Application binary interface.. $variant
+    Hardware model................ $model
+    Application binary interface.. $abi
     OS and development env........ $system
     C compiler.................... $cc
     C preprocessor................ $cprepro