From f1644570a07f668f3ef654fdaba4e3260274d55b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gerg=C3=B6=20Barany?= Date: Fri, 15 Sep 2017 09:51:13 +0200 Subject: [PATCH 1/4] 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. --- arm/TargetPrinter.ml | 8 ++++---- configure | 10 +++++----- runtime/arm/sysdeps.h | 4 ++-- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 89215f719c..a50682760c 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -854,10 +854,10 @@ 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" + | "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/configure b/configure index eb4423e837..17b2325638 100755 --- a/configure +++ b/configure @@ -54,12 +54,12 @@ 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- ARMv6T2 + VFPv2 armv7a- ARMv7-A + VFPv3-d16 (default for arm-) armv7r- ARMv7-R + VFPv3-d16 armv7m- ARMv7-M + VFPv3-d16 - armebv6- ARMv6 + VFPv2 + armebv6- ARMv6T2 + VFPv2 armebv7a- ARMv7-A + VFPv3-d16 (default for armeb-) armebv7r- ARMv7-R + VFPv3-d16 armebv7m- ARMv7-M + VFPv3-d16 @@ -114,7 +114,7 @@ case "$target" in arm-*|armv7a-*) arch="arm"; model="armv7a"; endianness="little"; bitsize=32;; armv6-*) - arch="arm"; model="armv6"; endianness="little"; bitsize=32;; + arch="arm"; model="armv6t2"; endianness="little"; bitsize=32;; armv7r-*) arch="arm"; model="armv7r"; endianness="little"; bitsize=32;; armv7m-*) @@ -122,7 +122,7 @@ case "$target" in armeb-*|armebv7a-*) arch="arm"; model="armv7a"; endianness="big"; bitsize=32;; armebv6-*) - arch="arm"; model="armv6"; endianness="big"; bitsize=32;; + arch="arm"; model="armv6t2"; endianness="big"; bitsize=32;; armebv7r-*) arch="arm"; model="armv7r"; endianness="big"; bitsize=32;; armebv7m-*) @@ -662,7 +662,7 @@ ARCH= # MODEL=ppc32 # for plain PowerPC # 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/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h index ae59f977ef..5907f15079 100644 --- a/runtime/arm/sysdeps.h +++ b/runtime/arm/sysdeps.h @@ -84,8 +84,8 @@ #define SUB THUMB_S(sub) .syntax unified -#if defined(MODEL_armv6) - .arch armv6 +#if defined(MODEL_armv6t2) + .arch armv6t2 #elif defined(MODEL_armv7a) .arch armv7-a #elif defined(MODEL_armv7r) From 323b2cff64e97a58549e0188020adc95e7e1db87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gerg=C3=B6=20Barany?= Date: Fri, 15 Sep 2017 09:19:39 +0200 Subject: [PATCH 2/4] 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. --- arm/Asmgen.v | 8 ++------ arm/Asmgenproof.v | 4 +--- arm/Asmgenproof1.v | 18 +----------------- 3 files changed, 4 insertions(+), 26 deletions(-) diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 1b96416d94..68e52f9ea5 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,12 +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 Nat.leb l1 l2 then - iterate_op (Pmov r) (Porr r r) d1 k else - iterate_op (Pmvn r) (Pbic r r) d2 k. + loadimm_word r n k. Definition addimm (r1 r2: ireg) (n: int) (k: code) := if Int.ltu (Int.repr (-256)) n then diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 71a0e04915..4fd10b5e20 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -165,14 +165,12 @@ Hint Resolve iterate_op_label: labels. Remark loadimm_label: forall r n k, tail_nolabel k (loadimm r n k). Proof. - intros. unfold loadimm. + intros. unfold loadimm, loadimm_word. set (l1 := length (decompose_int n)). 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 (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel. - destruct (Nat.leb l1 l2); auto with labels. Qed. Hint Resolve loadimm_label: labels. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 7084336e71..2ab4e635fc 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -344,9 +344,8 @@ Proof. econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. split; intros; Simpl. } - destruct (thumb tt). { (* 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. @@ -360,21 +359,6 @@ Proof. rewrite andb_true_r, orb_false_r; auto. rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. -} - destruct (Nat.leb l1 l2). -{ (* mov - orr* *) - replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). - apply iterate_op_correct. - auto. - intros; simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. - rewrite decompose_int_or. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. -} -{ (* mvn - bic* *) - replace (Vint n) with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (Vint Int.mone)). - apply iterate_op_correct. - auto. - intros. simpl. rewrite Int.and_commut; rewrite Int.and_mone; auto. - rewrite decompose_int_bic. simpl. rewrite Int.not_involutive. rewrite Int.and_commut. rewrite Int.and_mone; auto. } Qed. From f77c94520dd597ab0114f27bd3af446645825212 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gerg=C3=B6=20Barany?= Date: Fri, 15 Sep 2017 16:08:26 +0200 Subject: [PATCH 3/4] 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) --- arm/Archi.v | 3 +++ arm/Asmgen.v | 6 +++++- arm/Asmgenproof.v | 4 +++- arm/Asmgenproof1.v | 16 ++++++++++++++++ arm/TargetPrinter.ml | 1 + arm/extractionMachdep.v | 4 ++++ configure | 11 +++++++++-- driver/Driver.ml | 6 ++++-- runtime/arm/sysdeps.h | 4 +++- 9 files changed, 48 insertions(+), 7 deletions(-) diff --git a/arm/Archi.v b/arm/Archi.v index 64afb3ec87..3dfabcfc40 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -65,3 +65,6 @@ Global Opaque ptr64 big_endian splitlong Inductive abi_kind := Softfloat | Hardfloat. Parameter abi: abi_kind. + +(** Whether to generate [movw] and [movt] instructions. *) +Parameter move_imm: bool. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 68e52f9ea5..c795704cf4 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -177,8 +177,12 @@ 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 Archi.move_imm then + loadimm_word r n k + else if Nat.leb l1 l2 then + iterate_op (Pmov r) (Porr r r) d1 k else - loadimm_word r n k. + iterate_op (Pmvn r) (Pbic r r) d2 k. Definition addimm (r1 r2: ireg) (n: int) (k: code) := if Int.ltu (Int.repr (-256)) n then diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 4fd10b5e20..dc0889c258 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -165,12 +165,14 @@ Hint Resolve iterate_op_label: labels. Remark loadimm_label: forall r n k, tail_nolabel k (loadimm r n k). Proof. - intros. unfold loadimm, loadimm_word. + intros. unfold loadimm. set (l1 := length (decompose_int n)). set (l2 := length (decompose_int (Int.not n))). destruct (Nat.leb l1 1%nat). TailNoLabel. destruct (Nat.leb l2 1%nat). TailNoLabel. + destruct Archi.move_imm. unfold loadimm_word. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel. + destruct (Nat.leb l1 l2); auto with labels. Qed. Hint Resolve loadimm_label: labels. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 2ab4e635fc..2e8408ee0e 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -344,6 +344,7 @@ Proof. econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. split; intros; Simpl. } + destruct Archi.move_imm. { (* movw / movt *) unfold loadimm_word. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero). econstructor; split. @@ -359,6 +360,21 @@ Proof. rewrite andb_true_r, orb_false_r; auto. rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. +} + destruct (Nat.leb l1 l2). +{ (* mov - orr* *) + replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). + apply iterate_op_correct. + auto. + intros; simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. + rewrite decompose_int_or. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. +} +{ (* mvn - bic* *) + replace (Vint n) with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (Vint Int.mone)). + apply iterate_op_correct. + auto. + intros. simpl. rewrite Int.and_commut; rewrite Int.and_mone; auto. + rewrite decompose_int_bic. simpl. rewrite Int.not_involutive. rewrite Int.and_commut. rewrite Int.and_mone; auto. } Qed. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index a50682760c..fa612047f5 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -854,6 +854,7 @@ struct fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" (match Configuration.model with + | "armv6" -> "armv6" | "armv6t2" -> "armv6t2" | "armv7a" -> "armv7-a" | "armv7r" -> "armv7-r" diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index fb75435f75..36e4e44d0b 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 to generate [movw] and [movt] instructions. *) +Extract Constant Archi.move_imm => + "(Configuration.model = ""armv6t2"" || Configuration.model >= ""armv7"")". diff --git a/configure b/configure index 17b2325638..cc6731ecf7 100755 --- a/configure +++ b/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- ARMv6T2 + 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- ARMv6T2 + 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 @@ -114,6 +116,8 @@ case "$target" in arm-*|armv7a-*) 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;; @@ -122,6 +126,8 @@ case "$target" in armeb-*|armebv7a-*) 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;; @@ -662,6 +668,7 @@ ARCH= # MODEL=ppc32 # for plain PowerPC # 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 diff --git a/driver/Driver.ml b/driver/Driver.ml index 45a5c769e9..9467e826bf 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -372,8 +372,10 @@ 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 [] (* 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 5907f15079..0c873f951d 100644 --- a/runtime/arm/sysdeps.h +++ b/runtime/arm/sysdeps.h @@ -84,7 +84,9 @@ #define SUB THUMB_S(sub) .syntax unified -#if defined(MODEL_armv6t2) +#if defined(MODEL_armv6) + .arch armv6 +#elif defined(MODEL_armv6t2) .arch armv6t2 #elif defined(MODEL_armv7a) .arch armv7-a From 619da5d61ffdf1d1421984dac240f751d6df57ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gerg=C3=B6=20Barany?= Date: Fri, 15 Sep 2017 19:20:25 +0200 Subject: [PATCH 4/4] 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 | 5 +++-- arm/Asmgen.v | 6 +++--- arm/Asmgenproof.v | 6 +++--- arm/Asmgenproof1.v | 6 +++--- arm/extractionMachdep.v | 4 ++-- driver/Driver.ml | 6 ++++-- 6 files changed, 18 insertions(+), 15 deletions(-) diff --git a/arm/Archi.v b/arm/Archi.v index 3dfabcfc40..353731e0be 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -66,5 +66,6 @@ Global Opaque ptr64 big_endian splitlong Inductive abi_kind := Softfloat | Hardfloat. Parameter abi: abi_kind. -(** Whether to generate [movw] and [movt] instructions. *) -Parameter move_imm: bool. +(** 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 c795704cf4..ed64e2f0b9 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -177,7 +177,7 @@ 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 Archi.move_imm then + 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 @@ -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 dc0889c258..c1c3900cb5 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 Archi.move_imm. unfold loadimm_word. + 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 2e8408ee0e..c1015a8c1f 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -344,7 +344,7 @@ Proof. econstructor; split. apply exec_straight_one. simpl. rewrite Int.not_involutive. reflexivity. auto. split; intros; Simpl. } - destruct Archi.move_imm. + destruct Archi.thumb2_support. { (* movw / movt *) unfold loadimm_word. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero). 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/extractionMachdep.v b/arm/extractionMachdep.v index 36e4e44d0b..9d243413b6 100644 --- a/arm/extractionMachdep.v +++ b/arm/extractionMachdep.v @@ -29,6 +29,6 @@ Extract Constant Archi.abi => Extract Constant Archi.big_endian => "Configuration.is_big_endian". -(* Whether to generate [movw] and [movt] instructions. *) -Extract Constant Archi.move_imm => +(* Whether the model is ARMv6T2 or above and hence supports Thumb2. *) +Extract Constant Archi.thumb2_support => "(Configuration.model = ""armv6t2"" || Configuration.model >= ""armv7"")". diff --git a/driver/Driver.ml b/driver/Driver.ml index 9467e826bf..a09aa95df8 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,7 +373,8 @@ 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 - if Configuration.model = "armv6" then [] (* Thumb needs ARMv6T2 or ARMv7 *) + if Configuration.model = "armv6" then + [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *) else [ Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; ]