From 769589fb4f72edf46c16a396de6777d8e2fbb9bf Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jul 2014 13:42:11 +0000 Subject: 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 +1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- configure | 82 ++++++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 55 insertions(+), 27 deletions(-) (limited to 'configure') 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 Install in /bin and /lib/compcert -bindir Install binaries in @@ -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 <> 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 <