diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-27 11:06:09 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-27 11:06:09 +0200 |
commit | 883341719d7d6868f8165541e7e13ac45192a358 (patch) | |
tree | 368ad6e0f2d8e4c99c13a68da0e92c7f00408ae5 /configure | |
parent | 88c717e497e0e8a2e6df12418833e46c56291724 (diff) | |
download | compcert-883341719d7d6868f8165541e7e13ac45192a358.tar.gz compcert-883341719d7d6868f8165541e7e13ac45192a358.zip |
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).
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 58 |
1 files changed, 33 insertions, 25 deletions
@@ -103,31 +103,31 @@ done # case "$target" in arm-*|armv7a-*) - arch="arm"; model="armv7a"; endianness="little";; + arch="arm"; model="armv7a"; endianness="little"; bitsize=32;; armv6-*) - arch="arm"; model="armv6"; endianness="little";; + arch="arm"; model="armv6"; endianness="little"; bitsize=32;; armv7r-*) - arch="arm"; model="armv7r"; endianness="little";; + arch="arm"; model="armv7r"; endianness="little"; bitsize=32;; armv7m-*) - arch="arm"; model="armv7m"; endianness="little";; + arch="arm"; model="armv7m"; endianness="little"; bitsize=32;; armeb-*|armebv7a-*) - arch="arm"; model="armv7a"; endianness="big";; + arch="arm"; model="armv7a"; endianness="big"; bitsize=32;; armebv6-*) - arch="arm"; model="armv6"; endianness="big";; + arch="arm"; model="armv6"; endianness="big"; bitsize=32;; armebv7r-*) - arch="arm"; model="armv7r"; endianness="big";; + arch="arm"; model="armv7r"; endianness="big"; bitsize=32;; armebv7m-*) - arch="arm"; model="armv7m"; endianness="big";; - ia32-*) - arch="ia32"; model="32sse2"; endianness="little";; + arch="arm"; model="armv7m"; endianness="big"; bitsize=32;; + x86_32-*|ia32-*) + arch="x86"; model="32sse2"; endianness="little"; bitsize=32;; x86_64-*) - arch="ia32"; model="64"; endianness="little";; + arch="x86"; model="64"; endianness="little"; bitsize=64;; powerpc-*|ppc-*) - arch="powerpc"; model="ppc32"; endianness="big";; + arch="powerpc"; model="ppc32"; endianness="big"; bitsize=32;; powerpc64-*|ppc64-*) - arch="powerpc"; model="ppc64"; endianness="big";; + arch="powerpc"; model="ppc64"; endianness="big"; bitsize=32;; e5500-*) - arch="powerpc"; model="e5500"; endianness="big";; + arch="powerpc"; model="e5500"; endianness="big"; bitsize=32;; manual) ;; "") @@ -242,9 +242,9 @@ fi # -# IA32 (32 bits) Target Configuration +# x86 (32 bits) Target Configuration # -if test "$arch" = "ia32" -a "$model" != "64"; then +if test "$arch" = "x86" -a "$bitsize" = "32"; then case "$target" in bsd) @@ -323,7 +323,7 @@ fi # # IA32 (64 bits) Target Configuration # -if test "$arch" = "ia32" -a "$model" = "64"; then +if test "$arch" = "x86" -a "$bitsize" = "64"; then case "$target" in linux) @@ -501,6 +501,7 @@ cat >> Makefile.config <<EOF ABI=$abi ARCH=$arch ASM_SUPPORTS_CFI=$asm_supports_cfi +BITSIZE=$bitsize CASM=$casm CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime @@ -526,7 +527,7 @@ cat >> Makefile.config <<'EOF' # Target architecture # ARCH=powerpc # ARCH=arm -# ARCH=ia32 +# ARCH=x86 ARCH= # Hardware variant @@ -537,20 +538,25 @@ ARCH= # MODEL=armv7a # for ARM # MODEL=armv7r # for ARM # MODEL=armv7m # for ARM -# MODEL=32sse2 # for IA32 in 32-bit mode -# MODEL=64 # for IA32 in 64-bit mode +# MODEL=32sse2 # for x86 in 32-bit mode +# MODEL=64 # for x86 in 64-bit mode MODEL= # Target ABI # ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms # ABI=eabi # for ARM # ABI=hardfloat # for ARM -# ABI=standard # for IA32 +# ABI=standard # for x86 ABI= +# Target bit width +# BITSIZE=64 # for x86 in 64-bit mode +# BITSIZE=32 # otherwise +BITSIZE= + # Target endianness # ENDIANNESS=big # for ARM or PowerPC -# ENDIANNESS=little # for ARM or IA32 +# ENDIANNESS=little # for ARM or x86 ENDIANNESS= # Default calling conventions for passing structs and unions by value @@ -575,7 +581,7 @@ STRUCT_RETURN=ref # Possible choices for ARM: # SYSTEM=linux # -# Possible choices for IA32: +# Possible choices for x86: # SYSTEM=linux # SYSTEM=bsd # SYSTEM=macosx @@ -619,6 +625,10 @@ RESPONSEFILE="none" EOF fi +# +# Clean up target-dependent files to force their recompilation +# +rm -f .depend $arch/Archi.vo ${arch}_${bitsize}/Archi.vo runtime/*.o # # Summarize Configuration @@ -657,7 +667,5 @@ CompCert configuration: Standard headers installed in. $libdirexp/include Build command to use.......... $make -If anything above looks wrong, please edit file ./Makefile.config to correct. - EOF fi |