diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:38:24 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:38:24 +0200 |
commit | a14b9578ee5297d954103e05d7b2d322816ddd8f (patch) | |
tree | 93b7c2b6bd7de8a4dedaf399088257e0660959b8 /configure | |
parent | 3bef0962079cf971673b4267b0142bd5fe092509 (diff) | |
download | compcert-a14b9578ee5297d954103e05d7b2d322816ddd8f.tar.gz compcert-a14b9578ee5297d954103e05d7b2d322816ddd8f.zip |
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.
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 39 |
1 files changed, 35 insertions, 4 deletions
@@ -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 |