Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mo…

…de (#203)

* Clarify that ARMv6 is in fact ARMv6T2

The ARMv6 comes in two flavors depending on the version of the Thumb
instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2.
CompCert only supports Thumb2, so its ARMv6 architecture should really be
called ARMv6T2. This makes a difference: the GNU assembler rejects most of
the instructions CompCert generates for ARMv6 with "-mthumb" if the
architecture is specified as ".arch armv6" as opposed to ".arch armv6t2".

This patch fixes the architecture specification in the target printer and
the internal name of the architecture. It does not change the configure
script's flags to avoid breaking changes.

* Always use ARM movw/movt to load large immediates

These move-immediate instructions used to be only emitted in Thumb mode, not
in ARM mode. As far as I understand ARM's documentation, these instructions
are available in *both* modes in ARMv6T2 and above. This should cover all of
CompCert's ARM targets.

Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is
now identical to Clang, and the GNU assembler accepts these instructions in
all configurations.

* Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6

- define separate architecture models for ARMv6 and ARMv6T2
- introduce `Archi.move_imm` parameter on ARM to identify models with
  `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM
  and Thumb mode)

* Fixes for support for architectures with Thumb2

- rename relevant parameter to `Archi.thumb2_support`
- on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb)
- allow generation of `sbfx` in ARM mode if Thumb2 is supported

arm/Archi.v

@@ -65,3 +65,7 @@ Global Opaque ptr64 big_endian splitlong
 
 Inductive abi_kind := Softfloat | Hardfloat.
 Parameter abi: abi_kind.
+
+(** Whether instructions added with Thumb2 are supported. True for ARMv6T2
+  and above. *)
+Parameter thumb2_support: bool.

arm/Asmgen.v

@@ -162,7 +162,7 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code)
 
 (** Smart constructors for integer immediate arguments. *)
 
-Definition loadimm_thumb (r: ireg) (n: int) (k: code) :=
+Definition loadimm_word (r: ireg) (n: int) (k: code) :=
   let hi := Int.shru n (Int.repr 16) in
   if Int.eq hi Int.zero
   then Pmovw r n :: k
@@ -177,8 +177,8 @@ Definition loadimm (r: ireg) (n: int) (k: code) :=
     Pmov r (SOimm n) :: k
   else if Nat.leb l2 1%nat then
     Pmvn r (SOimm (Int.not n)) :: k
-  else if thumb tt then
-    loadimm_thumb r n k
+  else if Archi.thumb2_support then
+    loadimm_word r n k
   else if Nat.leb l1 l2 then
     iterate_op (Pmov r) (Porr r r) d1 k
   else
@@ -365,14 +365,14 @@ Definition transl_op
       OK (addimm r IR13 (Ptrofs.to_int n) k)
   | Ocast8signed, a1 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1;
-      OK (if thumb tt then
+      OK (if Archi.thumb2_support then
             Psbfx r r1 Int.zero (Int.repr 8) :: k
           else
             Pmov r (SOlsl r1 (Int.repr 24)) ::
             Pmov r (SOasr r (Int.repr 24)) :: k)
   | Ocast16signed, a1 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1;
-      OK (if thumb tt then
+      OK (if Archi.thumb2_support then
             Psbfx r r1 Int.zero (Int.repr 16) :: k
           else
             Pmov r (SOlsl r1 (Int.repr 16)) ::

arm/Asmgenproof.v

@@ -170,7 +170,7 @@ Proof.
   set (l2 := length (decompose_int (Int.not n))).
   destruct (Nat.leb l1 1%nat). TailNoLabel.
   destruct (Nat.leb l2 1%nat). TailNoLabel.
-  destruct (thumb tt). unfold loadimm_thumb.
+  destruct Archi.thumb2_support. unfold loadimm_word.
   destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel.
   destruct (Nat.leb l1 l2); auto with labels.
 Qed.
@@ -264,8 +264,8 @@ Proof.
 Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
   destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-  destruct (thumb tt); TailNoLabel.
-  destruct (thumb tt); TailNoLabel.
+  destruct Archi.thumb2_support; TailNoLabel.
+  destruct Archi.thumb2_support; TailNoLabel.
   eapply tail_nolabel_trans; TailNoLabel.
   eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
 Qed.

arm/Asmgenproof1.v

@@ -344,9 +344,9 @@ Proof.
   econstructor; split. apply exec_straight_one.
   simpl. rewrite Int.not_involutive. reflexivity. auto.
   split; intros; Simpl. }
-  destruct (thumb tt).
+  destruct Archi.thumb2_support.
 { (* movw / movt *)
-  unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero).
+  unfold loadimm_word. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero).
   econstructor; split.
   apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl.
   econstructor; split.
@@ -1193,7 +1193,7 @@ Proof.
   (* Oaddrstack *)
   contradiction.
   (* Ocast8signed *)
-  destruct (thumb tt).
+  destruct Archi.thumb2_support.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   destruct (rs x0); auto; simpl. rewrite Int.shru_zero. reflexivity.
   set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 24))))).
@@ -1206,7 +1206,7 @@ Proof.
   f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto.
   intros. unfold rs2, rs1; Simpl.
   (* Ocast16signed *)
-  destruct (thumb tt).
+  destruct Archi.thumb2_support.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   destruct (rs x0); auto; simpl. rewrite Int.shru_zero. reflexivity.
   set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 16))))).

arm/TargetPrinter.ml

@@ -854,10 +854,11 @@ struct
     fprintf oc "	.syntax	unified\n";
     fprintf oc "	.arch	%s\n"
       (match Configuration.model with
-       | "armv6" -> "armv6"
-       | "armv7a" -> "armv7-a"
-       | "armv7r" -> "armv7-r"
-       | "armv7m" -> "armv7-m"
+       | "armv6"   -> "armv6"
+       | "armv6t2" -> "armv6t2"
+       | "armv7a"  -> "armv7-a"
+       | "armv7r"  -> "armv7-r"
+       | "armv7m"  -> "armv7-m"
        | _ -> "armv7");
     fprintf oc "	.fpu	%s\n"
       (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2");

arm/extractionMachdep.v

@@ -28,3 +28,7 @@ Extract Constant Archi.abi =>
 (* Choice of endianness *)
 Extract Constant Archi.big_endian =>
   "Configuration.is_big_endian".
+
+(* Whether the model is ARMv6T2 or above and hence supports Thumb2. *)
+Extract Constant Archi.thumb2_support =>
+  "(Configuration.model = ""armv6t2"" || Configuration.model >= ""armv7"")".

configure

@@ -54,12 +54,14 @@ For PowerPC targets, the "ppc-" prefix can be refined into:
   e5500-               Freescale e5500 core (PowerPC 64 bit, EREF extensions)
 
 For ARM targets, the "arm-" or "armeb-" prefix can be refined into:
-  armv6-               ARMv6   + VFPv2
+  armv6-               ARMv6   + VFPv2       (Thumb mode not supported)
+  armv6t2-             ARMv6T2 + VFPv2
   armv7a-              ARMv7-A + VFPv3-d16   (default for arm-)
   armv7r-              ARMv7-R + VFPv3-d16
   armv7m-              ARMv7-M + VFPv3-d16
 
-  armebv6-             ARMv6   + VFPv2
+  armebv6-             ARMv6   + VFPv2       (Thumb mode not supported)
+  armebv6t2-           ARMv6T2 + VFPv2
   armebv7a-            ARMv7-A + VFPv3-d16   (default for armeb-)
   armebv7r-            ARMv7-R + VFPv3-d16
   armebv7m-            ARMv7-M + VFPv3-d16
@@ -115,6 +117,8 @@ case "$target" in
       arch="arm"; model="armv7a"; endianness="little"; bitsize=32;;
   armv6-*)
       arch="arm"; model="armv6"; endianness="little"; bitsize=32;;
+  armv6t2-*)
+      arch="arm"; model="armv6t2"; endianness="little"; bitsize=32;;
   armv7r-*)
       arch="arm"; model="armv7r"; endianness="little"; bitsize=32;;
   armv7m-*)
@@ -123,6 +127,8 @@ case "$target" in
       arch="arm"; model="armv7a"; endianness="big"; bitsize=32;;
   armebv6-*)
       arch="arm"; model="armv6"; endianness="big"; bitsize=32;;
+  armebv6t2-*)
+      arch="arm"; model="armv6t2"; endianness="big"; bitsize=32;;
   armebv7r-*)
       arch="arm"; model="armv7r"; endianness="big"; bitsize=32;;
   armebv7m-*)
@@ -663,6 +669,7 @@ ARCH=
 # MODEL=ppc64       # for PowerPC with 64-bit instructions
 # MODEL=e5500       # for Freescale e5500 PowerPC variant
 # MODEL=armv6       # for ARM
+# MODEL=armv6t2     # for ARM
 # MODEL=armv7a      # for ARM
 # MODEL=armv7r      # for ARM
 # MODEL=armv7m      # for ARM

driver/Driver.ml

@@ -205,7 +205,8 @@ let version_string =
   else
     "The CompCert C verified compiler, version "^ Version.version ^ "\n"
 
-let target_help = if Configuration.arch = "arm" then
+let target_help =
+  if Configuration.arch = "arm" && Configuration.model <> "armv6" then
 {|Target processor options:
   -mthumb        Use Thumb2 instruction encoding
   -marm          Use classic ARM instruction encoding
@@ -372,8 +373,11 @@ let cmdline_actions =
   Exact "-conf", Ignore; (* Ignore option since it is already handled *)
   Exact "-target", Ignore;] @ (* Ignore option since it is already handled *)
   (if Configuration.arch = "arm" then
-    [ Exact "-mthumb", Set option_mthumb;
-      Exact "-marm", Unset option_mthumb; ]
+    if Configuration.model = "armv6" then
+      [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *)
+    else
+      [ Exact "-mthumb", Set option_mthumb;
+        Exact "-marm", Unset option_mthumb; ]
   else []) @
 (* Assembling options *)
   assembler_actions @

runtime/arm/sysdeps.h

@@ -86,6 +86,8 @@
 	.syntax unified
 #if defined(MODEL_armv6)
         .arch   armv6
+#elif defined(MODEL_armv6t2)
+        .arch   armv6t2
 #elif defined(MODEL_armv7a)
         .arch   armv7-a
 #elif defined(MODEL_armv7r)