diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Archi.v | 5 | ||||
-rw-r--r-- | arm/Asmexpand.ml | 18 | ||||
-rw-r--r-- | arm/Conventions1.v | 50 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 12 | ||||
-rw-r--r-- | arm/extractionMachdep.v | 4 |
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". |