aboutsummaryrefslogtreecommitdiffstats
path: root/arm
diff options
context:
space:
mode:
Diffstat (limited to 'arm')
-rw-r--r--arm/Archi.v5
-rw-r--r--arm/Asmexpand.ml18
-rw-r--r--arm/Conventions1.v50
-rw-r--r--arm/TargetPrinter.ml12
-rw-r--r--arm/extractionMachdep.v4
5 files changed, 60 insertions, 29 deletions
diff --git a/arm/Archi.v b/arm/Archi.v
index 6b282022..fedc55f5 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -20,7 +20,7 @@ Require Import ZArith.
Require Import Fappli_IEEE.
Require Import Fappli_IEEE_bits.
-Definition big_endian := false.
+Parameter big_endian: bool.
Notation align_int64 := 8%Z (only parsing).
Notation align_float64 := 8%Z (only parsing).
@@ -45,8 +45,7 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p
Definition float_of_single_preserves_sNaN := false.
-Global Opaque big_endian
- default_pl_64 choose_binop_pl_64
+Global Opaque default_pl_64 choose_binop_pl_64
default_pl_32 choose_binop_pl_32
float_of_single_preserves_sNaN.
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 855ca9ad..43c26f58 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -185,13 +185,14 @@ let expand_builtin_vload_common chunk base ofs res =
| Mint32, BR(IR res) ->
emit (Pldr (res, base, SOimm ofs))
| Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
- let ofs' = Int.add ofs _4 in
+ let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in
+ let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in
if base <> res2 then begin
- emit (Pldr (res2, base, SOimm ofs));
- emit (Pldr (res1, base, SOimm ofs'))
+ emit (Pldr (res2, base, SOimm ofs_lo));
+ emit (Pldr (res1, base, SOimm ofs_hi))
end else begin
- emit (Pldr (res1, base, SOimm ofs'));
- emit (Pldr (res2, base, SOimm ofs))
+ emit (Pldr (res1, base, SOimm ofs_hi));
+ emit (Pldr (res2, base, SOimm ofs_lo))
end
| Mfloat32, BR(FR res) ->
emit (Pflds (res, base, ofs))
@@ -226,9 +227,10 @@ let expand_builtin_vstore_common chunk base ofs src =
| Mint32, BA(IR src) ->
emit (Pstr (src, base, SOimm ofs))
| Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) ->
- let ofs' = Int.add ofs _4 in
- emit (Pstr (src2, base, SOimm ofs));
- emit (Pstr (src1, base, SOimm ofs'))
+ let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in
+ let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in
+ emit (Pstr (src2, base, SOimm ofs_lo));
+ emit (Pstr (src1, base, SOimm ofs_hi))
| Mfloat32, BA(FR src) ->
emit (Pfsts (src, base, ofs))
| Mfloat64, BA(FR src) ->
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index 3eae50ef..888861a5 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -85,15 +85,21 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *)
For the "softfloat" convention, results of FP types should be passed
in [R0] or [R0,R1]. This doesn't fit the CompCert register model,
- so we have code in [arm/PrintAsm.ml] that inserts additional moves
- to/from [F0]. *)
+ so we have code in [arm/TargetPrinter.ml] that inserts additional moves
+ to/from [F0].
+
+ Concerning endianness for 64bit values in register pairs, the contents
+ of the registers is as if the value had been loaded from memory
+ representation with a single LDM instruction. *)
Definition loc_result (s: signature) : rpair mreg :=
match s.(sig_res) with
| None => One R0
| Some (Tint | Tany32) => One R0
| Some (Tfloat | Tsingle | Tany64) => One F0
- | Some Tlong => Twolong R1 R0
+ | Some Tlong => if Archi.big_endian
+ then Twolong R0 R1
+ else Twolong R1 R0
end.
(** The result registers have types compatible with that given in the signature. *)
@@ -102,7 +108,7 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
- intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
+ intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto.
Qed.
(** The result locations are caller-save registers *)
@@ -112,7 +118,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
- unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+ unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -124,7 +130,9 @@ Lemma loc_result_pair:
| Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
end.
Proof.
- intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence.
+ intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto.
+ intuition congruence.
+ intuition congruence.
Qed.
(** ** Location of function arguments *)
@@ -176,11 +184,13 @@ Fixpoint loc_arguments_hf
then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs
else One (S Outgoing ofs Tsingle) :: loc_arguments_hf tys ir fr (ofs + 1)
| Tlong :: tys =>
+ let ohi := if Archi.big_endian then 0 else 1 in
+ let olo := if Archi.big_endian then 1 else 0 in
let ir := align ir 2 in
if zlt ir 4
- then Twolong (R (ireg_param (ir + 1))) (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 2) fr ofs
+ then Twolong (R (ireg_param (ir + ohi))) (R (ireg_param (ir + olo))) :: loc_arguments_hf tys (ir + 2) fr ofs
else let ofs := align ofs 2 in
- Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: loc_arguments_hf tys ir fr (ofs + 2)
+ Twolong (S Outgoing (ofs + ohi) Tint) (S Outgoing (ofs + olo) Tint) :: loc_arguments_hf tys ir fr (ofs + 2)
end.
(** For the "softfloat" configuration, as well as for variable-argument functions
@@ -218,9 +228,11 @@ Fixpoint loc_arguments_sf
One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle)
:: loc_arguments_sf tys (ofs + 1)
| Tlong :: tys =>
+ let ohi := if Archi.big_endian then 0 else 1 in
+ let olo := if Archi.big_endian then 1 else 0 in
let ofs := align ofs 2 in
- Twolong (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint)
- (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint)
+ Twolong (if zlt ofs 0 then R (ireg_param (ofs+ohi+4)) else S Outgoing (ofs+ohi) Tint)
+ (if zlt ofs 0 then R (ireg_param (ofs+olo+4)) else S Outgoing (ofs+olo) Tint)
:: loc_arguments_sf tys (ofs + 2)
end.
@@ -341,9 +353,9 @@ Proof.
set (ir' := align ir 2) in *.
assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct (zlt ir' 4).
- destruct H. subst p. split; apply ireg_param_caller_save.
+ destruct H. subst p. split; apply ireg_param_caller_save.
eapply IHtyl; eauto.
- destruct H. subst p. split; (split; [ omega | auto ]).
+ destruct H. subst p. split; destruct Archi.big_endian; (split; [ omega | auto ]).
eapply Y. eapply IHtyl; eauto. omega.
- (* single *)
destruct (zlt fr 8); destruct H.
@@ -396,7 +408,7 @@ Proof.
destruct H.
destruct (zlt ofs' 0); subst p.
split; apply ireg_param_caller_save.
- split; (split; [xomega|auto]).
+ split; destruct Archi.big_endian; (split; [xomega|auto]).
eapply Y. eapply IHtyl; eauto. omega.
- (* single *)
destruct H.
@@ -513,6 +525,12 @@ Proof.
- (* long *)
destruct (zlt (align ir 2) 4).
destruct H. discriminate. destruct H. discriminate. eauto.
+ destruct Archi.big_endian.
+ destruct H. inv H.
+ eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega.
+ destruct H. inv H.
+ rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above.
+ eauto.
destruct H. inv H.
rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above.
destruct H. inv H.
@@ -556,9 +574,15 @@ Proof.
eauto.
- (* long *)
destruct H.
+ destruct Archi.big_endian.
+ destruct (zlt (align ofs0 2) 0); inv H.
+ eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega.
destruct (zlt (align ofs0 2) 0); inv H.
rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above.
destruct H.
+ destruct Archi.big_endian.
+ destruct (zlt (align ofs0 2) 0); inv H.
+ rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above.
destruct (zlt (align ofs0 2) 0); inv H.
eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega.
eauto.
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index d2ea16f7..95cae3f7 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -220,10 +220,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
fprintf oc " .balign 4\n";
Hashtbl.iter
(fun bf lbl ->
- (* Little-endian floats *)
+ (* Big or little-endian floats *)
let bfhi = Int64.shift_right_logical bf 32
and bflo = Int64.logand bf 0xFFFF_FFFFL in
- fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bflo bfhi)
+ if Archi.big_endian
+ then fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bfhi bflo
+ else fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bflo bfhi)
float_labels;
Hashtbl.iter
(fun bf lbl ->
@@ -310,7 +312,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
| (Tfloat | Tany64) :: tyl' ->
let i = (i + 1) land (-2) in
if i >= 4 then 0 else begin
- fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1));
+ if Archi.big_endian
+ then fixup_double oc dir (freg_param i) (ireg_param (i+1)) (ireg_param i)
+ else fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1));
1 + fixup (i+2) tyl'
end
| Tsingle :: tyl' ->
@@ -855,14 +859,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
cfi_section oc
end
-
let print_epilogue oc =
if !Clflags.option_g then begin
Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
section oc Section_text;
end
-
let default_falignment = 4
let label = elf_label
diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v
index 121deb4c..fb75435f 100644
--- a/arm/extractionMachdep.v
+++ b/arm/extractionMachdep.v
@@ -24,3 +24,7 @@ Extract Constant Archi.abi =>
| ""hardfloat"" -> Hardfloat
| _ -> assert false
end".
+
+(* Choice of endianness *)
+Extract Constant Archi.big_endian =>
+ "Configuration.is_big_endian".
generated by cgit (git 2.34.1) at 2024-07-01 15:43:47 +0000