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 --- Makefile | 3 +- arm/PrintAsm.ml | 39 +++++++++++++++----- arm/extractionMachdep.v | 2 +- configure | 82 +++++++++++++++++++++++++++-------------- driver/Clflags.ml | 4 +- runtime/Makefile | 2 +- runtime/arm/i64_dtos.S | 2 +- runtime/arm/i64_dtou.S | 2 +- runtime/arm/i64_sar.S | 2 +- runtime/arm/i64_stod.S | 2 +- runtime/arm/i64_stof.S | 2 +- runtime/arm/i64_utod.S | 2 +- runtime/arm/i64_utof.S | 2 +- runtime/arm/sysdeps.h | 19 ++++++++-- runtime/arm/vararg.S | 2 +- test/regression/Results/funptr2 | 2 +- test/regression/funptr2.c | 2 +- 17 files changed, 116 insertions(+), 55 deletions(-) diff --git a/Makefile b/Makefile index f698381..5bac694 100644 --- a/Makefile +++ b/Makefile @@ -226,7 +226,8 @@ driver/Configuration.ml: Makefile.config VERSION echo let asm = "\"$(CASM)\""; \ echo let linker = "\"$(CLINKER)\""; \ echo let arch = "\"$(ARCH)\""; \ - echo let variant = "\"$(VARIANT)\""; \ + echo let model = "\"$(MODEL)\""; \ + echo let abi = "\"$(ABI)\""; \ echo let system = "\"$(SYSTEM)\""; \ echo let has_runtime_lib = $(HAS_RUNTIME_LIB); \ echo let asm_supports_cfi = $(ASM_SUPPORTS_CFI); \ diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7dd7e48..e1988cc 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -20,10 +20,16 @@ open AST open Memdata open Asm -(* Code generation options. To be turned into proper options. *) +(* Code generation options. *) -let vfpv3 = ref true -let literals_in_code = ref true +let vfpv3 = Configuration.model >= "armv7" + +let hardware_idiv () = + match Configuration.model with + | "armv7r" | "armv7m" -> !Clflags.option_fthumb + | _ -> false + +let literals_in_code = ref true (* to be turned into a proper option *) (* On-the-fly label renaming *) @@ -729,7 +735,7 @@ module FixupHF = struct end let (fixup_arguments, fixup_result) = - match Configuration.variant with + match Configuration.abi with | "eabi" -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result) | "hardfloat" -> (FixupHF.fixup_arguments, FixupHF.fixup_result) | _ -> assert false @@ -835,7 +841,11 @@ let print_instruction oc = function | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Psdiv -> - fprintf oc " bl __aeabi_idiv\n"; 1 + if hardware_idiv() then begin + fprintf oc " sdiv r0, r0, r1\n"; 1 + end else begin + fprintf oc " bl __aeabi_idiv\n"; 1 + end | Psbfx(r1, r2, lsb, sz) -> fprintf oc " sbfx %a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1 | Psmull(r1, r2, r3, r4) -> @@ -844,7 +854,11 @@ let print_instruction oc = function fprintf oc " sub%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 | Pudiv -> - fprintf oc " bl __aeabi_uidiv\n"; 1 + if hardware_idiv() then begin + fprintf oc " udiv r0, r0, r1\n"; 1 + end else begin + fprintf oc " bl __aeabi_uidiv\n"; 1 + end | Pumull(r1, r2, r3, r4) -> fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 (* Floating-point VFD instructions *) @@ -864,7 +878,7 @@ let print_instruction oc = function fprintf oc " vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 | Pflid(r1, f) -> let f = camlint64_of_coqint(Floats.Float.to_bits f) in - if !vfpv3 && is_immediate_float64 f then begin + if vfpv3 && is_immediate_float64 f then begin fprintf oc " vmov.f64 %a, #%F\n" freg r1 (Int64.float_of_bits f); 1 (* immediate floats have at most 4 bits of fraction, so they @@ -912,7 +926,7 @@ let print_instruction oc = function fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 | Pflis(r1, f) -> let f = camlint_of_coqint(Floats.Float32.to_bits f) in - if !vfpv3 && is_immediate_float32 f then begin + if vfpv3 && is_immediate_float32 f then begin fprintf oc " vmov.f32 %a, #%F\n" freg_single r1 (Int32.float_of_bits f); 1 (* immediate floats have at most 4 bits of fraction, so they @@ -1171,9 +1185,14 @@ let print_program oc p = Hashtbl.clear filename_num; fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" - (if !Clflags.option_fthumb then "armv7" else "armv6"); + (match Configuration.model with + | "armv6" -> "armv6" + | "armv7a" -> "armv7-a" + | "armv7r" -> "armv7-r" + | "armv7m" -> "armv7-m" + | _ -> "armv7"); fprintf oc " .fpu %s\n" - (if !vfpv3 then "vfpv3-d16" else "vfpv2"); + (if vfpv3 then "vfpv3-d16" else "vfpv2"); fprintf oc " .%s\n" (if !Clflags.option_fthumb then "thumb" else "arm"); List.iter (print_globdef oc) p.prog_defs diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index 0c9b705..121deb4 100644 --- a/arm/extractionMachdep.v +++ b/arm/extractionMachdep.v @@ -19,7 +19,7 @@ Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". (* Choice of calling conventions *) Extract Constant Archi.abi => - "begin match Configuration.variant with + "begin match Configuration.abi with | ""eabi"" -> Softfloat | ""hardfloat"" -> Hardfloat | _ -> assert false 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 <= 32 LSR r0, r0, r2 LSL r3, r1, r3 - ORR r0, r1, r3 + ORR r0, r0, r3 ASR r1, r1, r2 bx lr 1: diff --git a/runtime/arm/i64_stod.S b/runtime/arm/i64_stod.S index 81e43e2..e38b466 100644 --- a/runtime/arm/i64_stod.S +++ b/runtime/arm/i64_stod.S @@ -46,7 +46,7 @@ __i64_stod: vcvt.f64.s32 d1, s2 @ convert high half to double (signed) vldr d2, .LC1 @ d2 = 2^32 vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 -#ifdef VARIANT_eabi +#ifdef ABI_eabi vmov r0, r1, d0 @ return result in r0, r1 #endif bx lr diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S index f1051f5..bb5e05c 100644 --- a/runtime/arm/i64_stof.S +++ b/runtime/arm/i64_stof.S @@ -66,7 +66,7 @@ FUNCTION(__i64_stof) vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 @ Round to single vcvt.f32.f64 s0, d0 -#ifdef VARIANT_eabi +#ifdef ABI_eabi @ Return result in r0 vmov r0, s0 #endif diff --git a/runtime/arm/i64_utod.S b/runtime/arm/i64_utod.S index b12d7c2..b4c3075 100644 --- a/runtime/arm/i64_utod.S +++ b/runtime/arm/i64_utod.S @@ -46,7 +46,7 @@ __i64_stod: vcvt.f64.u32 d1, s2 @ convert high half to double (unsigned) vldr d2, .LC1 @ d2 = 2^32 vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 -#ifdef VARIANT_eabi +#ifdef ABI_eabi vmov r0, r1, d0 @ return result in r0, r1 #endif bx lr diff --git a/runtime/arm/i64_utof.S b/runtime/arm/i64_utof.S index 711cda0..fbd325c 100644 --- a/runtime/arm/i64_utof.S +++ b/runtime/arm/i64_utof.S @@ -62,7 +62,7 @@ FUNCTION(__i64_utof) vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 @ Round to single vcvt.f32.f64 s0, d0 -#ifdef VARIANT_eabi +#ifdef ABI_eabi @ Return result in r0 vmov r0, s0 #endif diff --git a/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h index b72af0f..85404cf 100644 --- a/runtime/arm/sysdeps.h +++ b/runtime/arm/sysdeps.h @@ -34,6 +34,13 @@ // System dependencies +#if defined(MODEL_armv7r) +// Thumb2-only +#define THUMB +#else +#undef THUMB +#endif + #ifdef THUMB #define FUNCTION(f) \ .text; \ @@ -76,9 +83,15 @@ f: #define SUB THUMB_S(sub) .syntax unified -#ifdef THUMB - .arch armv7 +#if defined(MODEL_armv6) + .arch armv6 +#elif defined(MODEL_armv7a) + .arch armv7-a +#elif defined(MODEL_armv7r) + .arch armv7-r +#elif defined(MODEL_armv7m) + .arch armv7-m #else - .arch armv6 + .arch armv7 #endif .fpu vfpv2 diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S index e352582..ae06e36 100644 --- a/runtime/arm/vararg.S +++ b/runtime/arm/vararg.S @@ -67,7 +67,7 @@ FUNCTION(__compcert_va_float64) ADD r1, r1, #15 @ 8-align and advance by 8 BIC r1, r1, #7 str r1, [r0, #0] @ update ap -#ifdef VARIANT_eabi +#ifdef ABI_eabi ldr r0, [r1, #-8] @ load next argument and return it in r0,r1 ldr r1, [r1, #-4] #else diff --git a/test/regression/Results/funptr2 b/test/regression/Results/funptr2 index f364c59..9574355 100644 --- a/test/regression/Results/funptr2 +++ b/test/regression/Results/funptr2 @@ -1,3 +1,3 @@ f == f is 1 f == g is 0 -f + 1 == f is 0 +f + 2 == f is 0 diff --git a/test/regression/funptr2.c b/test/regression/funptr2.c index 5c31dd2..8086eae 100644 --- a/test/regression/funptr2.c +++ b/test/regression/funptr2.c @@ -9,6 +9,6 @@ int main(void) { printf ("f == f is %d\n", &f == &f); printf ("f == g is %d\n", &f == &g); /* The following is undefined behavior */ - printf ("f + 1 == f is %d\n", ((char *) &f) + 1 == (char *) &f); + printf ("f + 2 == f is %d\n", ((char *) &f) + 2 == (char *) &f); return 0; } -- cgit v1.2.3