diff options
| -rw-r--r-- | arm/Archi.v | 4 | ||||
| -rw-r--r-- | arm/Asmgen.v | 10 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 6 | ||||
| -rw-r--r-- | arm/Asmgenproof1.v | 8 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 9 | ||||
| -rw-r--r-- | arm/extractionMachdep.v | 4 | ||||
| -rwxr-xr-x | configure | 11 | ||||
| -rw-r--r-- | driver/Driver.ml | 10 | ||||
| -rw-r--r-- | runtime/arm/sysdeps.h | 2 |
9 files changed, 43 insertions, 21 deletions
diff --git a/arm/Archi.v b/arm/Archi.v index 64afb3ec..353731e0 100644 --- a/arm/Archi.v +++ b/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. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 1b96416d..ed64e2f0 100644 --- a/arm/Asmgen.v +++ b/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)) :: diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 71a0e049..c1c3900c 100644 --- a/arm/Asmgenproof.v +++ b/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. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 7084336e..c1015a8c 100644 --- a/arm/Asmgenproof1.v +++ b/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))))). diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 89215f71..fa612047 100644 --- a/arm/TargetPrinter.ml +++ b/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"); diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index fb75435f..9d243413 100644 --- a/arm/extractionMachdep.v +++ b/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"")". @@ -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 diff --git a/driver/Driver.ml b/driver/Driver.ml index 45a5c769..a09aa95d 100644 --- a/driver/Driver.ml +++ b/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 @ diff --git a/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h index ae59f977..0c873f95 100644 --- a/runtime/arm/sysdeps.h +++ b/runtime/arm/sysdeps.h @@ -86,6 +86,8 @@ f: .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) |