Generalize load-immediate operations on ARM

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)