Implement support for big endian arm targets.

Adds support for the big endian arm targets by making the target
endianess flag configurable, adding support for the big endian
calling conventions, rewriting memory access patterns and adding
big endian versions of the runtime functions.
Bug 19418

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