diff options
Diffstat (limited to 'arm')
| -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 |
6 files changed, 25 insertions, 16 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"")". |