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

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 <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
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 7104c32..d3d4067 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -28,7 +28,7 @@ let option_falignfunctions = ref (None: int option)
 let option_falignbranchtargets = ref 0
 let option_faligncondbranchs = ref 0
 let option_finline_asm = ref false
-let option_fthumb = ref false
+let option_fthumb = ref (Configuration.model = "armv7m")
 let option_Osize = ref false
 let option_dparse = ref false
 let option_dcmedium = ref false
@@ -49,7 +49,7 @@ let option_v = ref false
 let option_interp = ref false
 let option_small_data = 
   ref (if Configuration.arch = "powerpc"
-       && Configuration.variant = "eabi"
+       && Configuration.abi = "eabi"
        && Configuration.system = "diab"
        then 8 else 0)
 let option_small_const = ref (!option_small_data)
diff --git a/runtime/Makefile b/runtime/Makefile
index 0cdfd3b..1f0ccf2 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -22,7 +22,7 @@ $(LIB): $(OBJS)
 	$(CASMRUNTIME) -o $@ $^
 
 %.o: $(ARCH)/%.S
-	$(CASMRUNTIME) -DVARIANT_$(VARIANT) -DSYS_$(SYSTEM) -o $@ $^
+	$(CASMRUNTIME) -DMODEL_$(MODEL) -DABI_$(ABI) -DSYS_$(SYSTEM) -o $@ $^
 
 clean::
 	rm -f *.o $(LIB)
diff --git a/runtime/arm/i64_dtos.S b/runtime/arm/i64_dtos.S
index 638a5ff..4557eea 100644
--- a/runtime/arm/i64_dtos.S
+++ b/runtime/arm/i64_dtos.S
@@ -39,7 +39,7 @@
 @@@ Conversion from double float to signed 64-bit integer
 	
 FUNCTION(__i64_dtos)
-#ifndef VARIANT_eabi
+#ifndef ABI_eabi
 	vmov r0, r1, d0
 #endif	
         ASR r12, r1, #31       @ save sign of result in r12
diff --git a/runtime/arm/i64_dtou.S b/runtime/arm/i64_dtou.S
index 1c632d2..5764190 100644
--- a/runtime/arm/i64_dtou.S
+++ b/runtime/arm/i64_dtou.S
@@ -39,7 +39,7 @@
 @@@ Conversion from double float to unsigned 64-bit integer	
 
 FUNCTION(__i64_dtou)
-#ifndef VARIANT_eabi
+#ifndef ABI_eabi
 	vmov r0, r1, d0
 #endif	
         cmp r1, #0              @ is double < 0 ?
diff --git a/runtime/arm/i64_sar.S b/runtime/arm/i64_sar.S
index 1bbd8a7..a4d0a1d 100644
--- a/runtime/arm/i64_sar.S
+++ b/runtime/arm/i64_sar.S
@@ -44,7 +44,7 @@ FUNCTION(__i64_sar)
         ble 1f                  @ branch if <= 0, namely if amount >= 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;
 }