Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#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

1 files changed, 4 insertions, 4 deletions

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))))).