diff options
37 files changed, 667 insertions, 472 deletions
@@ -202,6 +202,7 @@ compcert.ini: Makefile.config echo "arch=$(ARCH)"; \ echo "model=$(MODEL)"; \ echo "abi=$(ABI)"; \ + echo "endianness=$(ENDIANNESS)"; \ echo "system=$(SYSTEM)"; \ echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \ 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". diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 154c1e2e..47dac12f 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1890,7 +1890,8 @@ Proof. { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. eapply reg_unconstrained_satisf. eauto. eapply add_equations_satisf; eauto. assumption. - rewrite Regmap.gss. apply Val.lessdef_trans with v1'; auto. + rewrite Regmap.gss. + apply Val.lessdef_trans with v1'; unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). @@ -1906,7 +1907,8 @@ Proof. assert (SAT4: satisf (rs#dst <- v) ls4 e0). { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. assumption. - rewrite Regmap.gss. apply Val.lessdef_trans with v2'; auto. + rewrite Regmap.gss. + apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. } exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]]. econstructor; split. @@ -1938,7 +1940,8 @@ Proof. set (ls2 := Locmap.set (R dst') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e0). { eapply parallel_assignment_satisf; eauto. - apply Val.lessdef_trans with v1'; auto. + apply Val.lessdef_trans with v1'; + unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. @@ -1968,7 +1971,7 @@ Proof. set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e0). { eapply parallel_assignment_satisf; eauto. - apply Val.lessdef_trans with v2'; auto. + apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a8d0512c..2a8d6d97 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -864,11 +864,12 @@ Proof. with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). - eapply store_zeros_unchanged; eauto. intros; omega. + eapply store_zeros_unchanged; eauto. intros; omega. intros; omega. - change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). + replace (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). change 1 with (size_chunk Mint8unsigned). eapply Mem.loadbytes_store_same; eauto. + unfold encode_val; unfold encode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. eapply IHo; eauto. omega. omega. omega. omega. + eapply IHo; eauto. omega. omega. - discriminate. @@ -973,7 +974,7 @@ Proof. transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))). apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. - f_equal. destruct chunk; reflexivity. + f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. Qed. Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop := @@ -12,7 +12,7 @@ # # ####################################################################### -prefix=/usr/local +prefix='/usr/local' bindir='$(PREFIX)/bin' libdir='$(PREFIX)/lib/compcert' toolprefix='' @@ -24,44 +24,51 @@ clightgen=false usage='Usage: ./configure [options] target Supported targets: - ppc-eabi (PowerPC, EABI with GNU/Unix tools) - ppc-eabi-diab (PowerPC, EABI with Diab tools) - ppc-linux (PowerPC, Linux) - arm-eabi (ARM, EABI) - arm-linux (ARM, EABI) - arm-eabihf (ARM, EABI using hardware FP registers) - arm-hardfloat (ARM, EABI using hardware FP registers) - ia32-linux (x86 32 bits, Linux) - ia32-bsd (x86 32 bits, BSD) - ia32-macosx (x86 32 bits, MacOS X) - ia32-cygwin (x86 32 bits, Cygwin environment under Windows) - manual (edit configuration file by hand) + ppc-eabi (PowerPC, EABI with GNU/Unix tools) + ppc-eabi-diab (PowerPC, EABI with Diab tools) + ppc-linux (PowerPC, Linux) + arm-eabi (ARM, EABI) + arm-linux (ARM, EABI) + arm-eabihf (ARM, EABI using hardware FP registers) + arm-hardfloat (ARM, EABI using hardware FP registers) + ia32-linux (x86 32 bits, Linux) + ia32-bsd (x86 32 bits, BSD) + ia32-macosx (x86 32 bits, MacOS X) + ia32-cygwin (x86 32 bits, Cygwin environment under Windows) + manual (edit configuration file by hand) For PowerPC targets, the "ppc-" prefix can be refined into: - ppc64- PowerPC 64 bits - e5500- Freescale e5500 core (PowerPC 64 bits + EREF extensions) + ppc64- PowerPC 64 bits + e5500- Freescale e5500 core (PowerPC 64 bit, EREF extensions) For ARM targets, the "arm-" prefix can be refined into: - armv6- ARMv6 + VFPv2 - armv7a- ARMv7-A + VFPv3-d16 (default) - armv7r- ARMv7-R + VFPv3-d16 - armv7m- ARMv7-M + VFPv3-d16 + armv6- ARMv6 + VFPv2 + armv7a- ARMv7-A + VFPv3-d16 (default) + armv7r- ARMv7-R + VFPv3-d16 + armv7m- ARMv7-M + VFPv3-d16 + +For ARM targets, the endianness can optionally be speficied as a suffix: + -big Big endian + -little Little endian (default) Options: - -prefix <dir> Install in <dir>/bin and <dir>/lib/compcert - -bindir <dir> Install binaries in <dir> - -libdir <dir> Install libraries in <dir> - -toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref> - -no-runtime-lib Do not compile nor install the runtime support library + -prefix <dir> Install in <dir>/bin and <dir>/lib/compcert + -bindir <dir> Install binaries in <dir> + -libdir <dir> Install libraries in <dir> + -toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref> + -no-runtime-lib Do not compile nor install the runtime support library -no-standard-headers Do not install nor use the standard .h headers - -clightgen Also compile the clightgen tool + -clightgen Also compile the clightgen tool ' -# Parse command-line arguments +# +# Parse Command-Line Arguments +# while : ; do case "$1" in - "") break;; + "") + break;; -prefix|--prefix) prefix="$2"; shift;; -bindir|--bindir) @@ -83,179 +90,260 @@ while : ; do shift done -# Per-target configuration -casmruntime="" +# +# Extract Architecture, Model and Default Endianness +# +case "$target" in + arm-*|armv7a-*) + arch="arm"; model="armv7a"; endianness="little";; + armv6-*) + arch="arm"; model="armv6"; endianness="little";; + armv7r-*) + arch="arm"; model="armv7r"; endianness="little";; + armv7m-*) + arch="arm"; model="armv7m"; endianness="little";; + ia32-*) + arch="ia32"; model="sse2"; endianness="little";; + powerpc-*|ppc-*) + arch="powerpc"; model="ppc32"; endianness="big";; + powerpc64-*|ppc64-*) + arch="powerpc"; model="ppc64"; endianness="big";; + e5500-*) + arch="powerpc"; model="e5500"; endianness="big";; + manual) + ;; + "") + echo "Error: no target architecture specified." 1>&2 + echo "$usage" 1>&2 + exit 2 + ;; + *) + echo "Error: unknown target architecture: '$target'." 1>&2 + echo "$usage" 1>&2 + exit 2 + ;; +esac + +target=${target#[a-zA-Z0-9]*-} + + +# +# ARM: Optional Endianness Specification +# +if test "$arch" = "arm"; then + case "$target" in + *-big) + endianness="big"; + target=${target%"-big"} + ;; + *-little) + endianness="little"; + target=${target%"-little"} + ;; + esac +else + case "$target" in + *-big|*-little) + echo "Error: endianness may only be specified for ARM architecture." 1>&2 + echo "$usage" 1>&2 + exit 2 + ;; + *) + ;; + esac +fi + + +# Per-target configuration asm_supports_cfi="" -struct_passing="" -struct_return="" casm_options="" -cprepro_options="" +casmruntime="" clinker_options="" +cprepro_options="" +struct_passing="" +struct_return="" -case "$target" in - powerpc-*|ppc-*|powerpc64-*|ppc64-*|e5500-*) - arch="powerpc" - case "$target" in - powerpc64-*|ppc64-*) model="ppc64";; - e5500-*) model="e5500";; - *) model="ppc32";; - esac - abi="eabi" - struct_passing="ref-caller" - case "$target" in - *-linux) struct_return="ref";; - *) struct_return="int1-8";; - esac - case "$target" in - *-eabi-diab) - system="diab" - cc="${toolprefix}dcc" - cprepro="${toolprefix}dcc" - cprepro_options="-E -D__GNUC__" + +# +# ARM Target Configuration +# +if test "$arch" = "arm"; then + + case "$target" in + eabi|linux) + abi="eabi" + ;; + eabihf|hf|hardfloat) + abi="hardfloat" + ;; + *) + echo "Error: invalid eabi/system '$target' for architecture ARM." 1>&2 + echo "$usage" 1>&2 + exit 2;; + esac + + casm="${toolprefix}gcc" + casm_options="-c" + cc="${toolprefix}gcc" + clinker="${toolprefix}gcc" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" + libmath="-lm" + struct_passing="ints" + struct_return="int1-4" + system="linux" +fi + + +# +# PowerPC Target Configuration +# +if test "$arch" = "powerpc"; then + + case "$target" in + eabi|eabi-diab|linux) + ;; + *) + echo "Error: invalid eabi/system '$target' for architecture PowerPC." 1>&2 + echo "$usage" 1>&2 + exit 2;; + esac + + case "$target" in + linux) + struct_return="ref" + ;; + *) + struct_return="int1-8" + ;; + esac + + case "$target" in + eabi-diab) + abi="eabi" + asm_supports_cfi=false casm="${toolprefix}das" casm_options="-Xalign-value" - asm_supports_cfi=false + cc="${toolprefix}dcc" clinker="${toolprefix}dcc" + cprepro="${toolprefix}dcc" + cprepro_options="-E -D__GNUC__" libmath="-lm" + struct_passing="ref-caller" + system="diab" ;; - *) - system="linux" + *) + abi="eabi" + casm="${toolprefix}gcc" + casm_options="-c" + casmruntime="${toolprefix}gcc -c -Wa,-mregnames" cc="${toolprefix}gcc" + clinker="${toolprefix}gcc" cprepro="${toolprefix}gcc" cprepro_options="-std=c99 -U__GNUC__ -E" + libmath="-lm" + struct_passing="ref-caller" + system="linux" + ;; + esac +fi + + +# +# IA32 Target Configuration +# +if test "$arch" = "ia32"; then + + case "$target" in + bsd) + abi="standard" casm="${toolprefix}gcc" - casm_options="-c" - casmruntime="${toolprefix}gcc -c -Wa,-mregnames" + casm_options="-m32 -c" + cc="${toolprefix}gcc -m32" clinker="${toolprefix}gcc" + clinker_options="-m32" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m32 -U__GNUC__ -E" libmath="-lm" - esac;; - arm*-*) - arch="arm" - case "$target" in - armv6-*) model="armv6";; - arm-*|armv7a-*) model="armv7a";; - armv7r-*) model="armv7r";; - armv7m-*) model="armv7m";; - *) - echo "Unknown target '$target'." 1>&2 - echo "$usage" 1>&2 - exit 2;; - esac - case "$target" in - *-eabi|*-linux) abi="eabi";; - *-eabihf|*-hf|*-hardfloat) abi="hardfloat";; - *) - echo "Unknown target '$target'." 1>&2 + struct_passing="ints" + struct_return="int1248" # to check! + system="bsd" + ;; + cygwin) + abi="standard" + casm="${toolprefix}gcc" + casm_options="-m32 -c" + cc="${toolprefix}gcc -m32" + clinker="${toolprefix}gcc" + clinker_options="-m32" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m32 -U__GNUC__ -E" + libmath="-lm" + struct_passing="ints" + struct_return="ref" + system="cygwin" + ;; + linux) + abi="standard" + casm="${toolprefix}gcc" + casm_options="-m32 -c" + cc="${toolprefix}gcc -m32" + clinker="${toolprefix}gcc" + clinker_options="-m32" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m32 -U__GNUC__ -E" + libmath="-lm" + struct_passing="ints" + struct_return="ref" + system="linux" + ;; + macosx) + # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11 + kernel_major=`uname -r | cut -d "." -f 1` + + abi="macosx" + casm="${toolprefix}gcc" + casm_options="-arch i386 -c" + cc="${toolprefix}gcc -arch i386" + clinker="${toolprefix}gcc" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" + libmath="" + struct_passing="ints" + struct_return="int1248" + system="macosx" + + if [[ $kernel_major -gt 11 ]]; then + # OSX >= 10.8 + clinker_options="-arch i386 -Wl,-no_pie" + else + # OSX <= 10.7 + clinker_options="-arch i386" + fi + ;; + *) + echo "Error: invalid eabi/system '$target' for architecture IA32." 1>&2 echo "$usage" 1>&2 exit 2;; - esac - struct_passing="ints" - struct_return="int1-4" - system="linux" - cc="${toolprefix}gcc" - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" - casm="${toolprefix}gcc" - casm_options="-c" - clinker="${toolprefix}gcc" - libmath="-lm";; - ia32-linux) - arch="ia32" - model="sse2" - abi="standard" - struct_passing="ints" - struct_return="ref" - system="linux" - cc="${toolprefix}gcc -m32" - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -m32 -U__GNUC__ -E" - casm="${toolprefix}gcc" - casm_options="-m32 -c" - clinker="${toolprefix}gcc" - clinker_options="-m32" - libmath="-lm";; - ia32-bsd) - arch="ia32" - model="sse2" - abi="standard" - struct_passing="ints" - struct_return="int1248" # to check! - system="bsd" - cc="${toolprefix}gcc -m32" - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -m32 -U__GNUC__ -E" - casm="${toolprefix}gcc" - casm_options="-m32 -c" - clinker="${toolprefix}gcc" - clinker_options="-m32" - libmath="-lm";; - ia32-macosx) - # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11 - kernel_major=`uname -r | cut -d "." -f 1` - arch="ia32" - model="sse2" - abi="macosx" - struct_passing="ints" - struct_return="int1248" - system="macosx" - cc="${toolprefix}gcc -arch i386" - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" - casm="${toolprefix}gcc" - casm_options="-arch i386 -c" - clinker="${toolprefix}gcc" - if [[ $kernel_major -gt 11 ]] - then - # OSX >= 10.8 - clinker_options="-arch i386 -Wl,-no_pie" - else - # OSX <= 10.7 - clinker_options="-arch i386" - fi - libmath="";; - ia32-cygwin) - arch="ia32" - model="sse2" - abi="standard" - struct_passing="ints" - struct_return="ref" - system="cygwin" - cc="${toolprefix}gcc -m32" - cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -m32 -U__GNUC__ -E" - casm="${toolprefix}gcc" - casm_options="-m32 -c" - clinker="${toolprefix}gcc" - clinker_options="-m32" - libmath="-lm";; - manual) - ;; - "") - echo "No target specified." 1>&2 - echo "$usage" 1>&2 - exit 2;; - *) - echo "Unknown target '$target'." 1>&2 - echo "$usage" 1>&2 - exit 2;; -esac - -if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi + esac +fi -# Test assembler support for CFI directives +# +# Test Assembler Support for CFI Directives +# if test "$target" != "manual" && test -z "$asm_supports_cfi"; then echo "Testing assembler support for CFI directives... " | tr -d '\n' f=/tmp/compcert-configure-$$.s rm -f $f cat >> $f <<EOF testfun: - .file 1 "testfun.c" - .loc 1 1 - .cfi_startproc - .cfi_adjust_cfa_offset 16 - .cfi_endproc + .file 1 "testfun.c" + .loc 1 1 + .cfi_startproc + .cfi_adjust_cfa_offset 16 + .cfi_endproc EOF if $casm $casm_options -o /dev/null $f 2>/dev/null then echo "yes"; asm_supports_cfi=true @@ -264,8 +352,10 @@ EOF rm -f $f fi -# Testing availability of required tools +# +# Test Availability of Required Tools +# missingtools=false echo "Testing Coq... " | tr -d '\n' @@ -352,8 +442,10 @@ if $missingtools; then exit 2 fi -# Generate Makefile.config +# +# Generate Makefile.config +# sharedir="$(dirname "$bindir")"/share rm -f Makefile.config @@ -367,25 +459,26 @@ EOF if test "$target" != "manual"; then cat >> Makefile.config <<EOF -ARCH=$arch -MODEL=$model ABI=$abi -STRUCT_PASSING=$struct_passing -STRUCT_RETURN=$struct_return -SYSTEM=$system -CC=$cc -CPREPRO=$cprepro -CPREPRO_OPTIONS=$cprepro_options +ARCH=$arch +ASM_SUPPORTS_CFI=$asm_supports_cfi CASM=$casm CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime +CC=$cc +CLIGHTGEN=$clightgen CLINKER=$clinker CLINKER_OPTIONS=$clinker_options -LIBMATH=$libmath +CPREPRO=$cprepro +CPREPRO_OPTIONS=$cprepro_options +ENDIANNESS=$endianness HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers -ASM_SUPPORTS_CFI=$asm_supports_cfi -CLIGHTGEN=$clightgen +LIBMATH=$libmath +MODEL=$model +STRUCT_PASSING=$struct_passing +STRUCT_RETURN=$struct_return +SYSTEM=$system EOF else cat >> Makefile.config <<'EOF' @@ -397,40 +490,50 @@ cat >> Makefile.config <<'EOF' ARCH= # Hardware variant -# MODEL=ppc32 # for plain PowerPC -# MODEL=ppc64 # for PowerPC with 64-bit instructions -# MODEL=e5500 # for Freescale e5500 PowerPC variant -# MODEL=armv6 # for ARM -# MODEL=armv7a # for ARM -# MODEL=armv7r # for ARM -# MODEL=armv7m # for ARM -# MODEL=sse2 # for IA32 +# MODEL=ppc32 # for plain PowerPC +# MODEL=ppc64 # for PowerPC with 64-bit instructions +# MODEL=e5500 # for Freescale e5500 PowerPC variant +# MODEL=armv6 # for ARM +# MODEL=armv7a # for ARM +# MODEL=armv7r # for ARM +# MODEL=armv7m # for ARM +# MODEL=sse2 # for IA32 MODEL= # Target ABI -# ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms -# ABI=eabi # for ARM -# ABI=hardfloat # for ARM -# ABI=standard # for IA32 +# ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms +# ABI=eabi # for ARM +# ABI=hardfloat # for ARM +# ABI=standard # for IA32 ABI= +# Target endianness +# ENDIANNESS=big # for ARM or PowerPC +# ENDIANNESS=little # for ARM or IA32 +ENDIANNESS= + # Default calling conventions for passing structs and unions by value # See options -fstruct-passing=<style> and -fstruct-return=<style> # in the CompCert user's manual +# STRUCT_PASSING=ref_callee # STRUCT_PASSING=ref_caller # STRUCT_PASSING=ints +# STRUCT_RETURN=ref # STRUCT_RETURN=int1248 # STRUCT_RETURN=int1-4 # STRUCT_RETURN=int1-8 # Target operating system and development environment +# # Possible choices for PowerPC: # SYSTEM=linux # SYSTEM=diab +# # Possible choices for ARM: # SYSTEM=linux +# # Possible choices for IA32: # SYSTEM=linux # SYSTEM=bsd @@ -453,7 +556,7 @@ CASMRUNTIME=gcc -c # Linker CLINKER=gcc -# Math library. Set to empty under MacOS X +# Math library. Set to empty under MacOS X LIBMATH=-lm # Turn on/off the installation and use of the runtime support library @@ -470,18 +573,18 @@ ASM_SUPPORTS_CFI=false CLIGHTGEN=false EOF - fi -# Summarize configuration +# +# Summarize Configuration +# if test "$target" = "manual"; then cat <<EOF Please finish the configuration by editing file ./Makefile.config. EOF - else bindirexp=`echo "$bindir" | sed -e "s|\\\$(PREFIX)|$prefix|"` @@ -493,6 +596,7 @@ CompCert configuration: Target architecture........... $arch Hardware model................ $model Application binary interface.. $abi + Endianness.................... $endianness Composite passing conventions. arguments: $struct_passing, return values: $struct_return OS and development env........ $system C compiler.................... $cc @@ -512,5 +616,4 @@ CompCert configuration: If anything above looks wrong, please edit file ./Makefile.config to correct. EOF - fi diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 7a12c649..364ebf28 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -173,10 +173,13 @@ let ppc_32_bigendian = let ppc_32_diab_bigendian = { ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false } - let arm_littleendian = { ilp32ll64 with name = "arm" } +let arm_bigendian = + { arm_littleendian with bigendian = true; + bitfields_msb_first = true } + (* Add GCC extensions re: sizeof and alignof *) let gcc_extensions c = diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 277ac3fb..8ca1e989 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -64,6 +64,7 @@ val win64 : t val ppc_32_bigendian : t val ppc_32_diab_bigendian : t val arm_littleendian : t +val arm_bigendian : t val gcc_extensions : t -> t val compcert_interpreter : t -> t diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e1a02573..765b075a 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -121,6 +121,11 @@ let arch = | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" +let is_big_endian = + match get_config_string "endianness" with + | "big" -> true + | "little" -> false + | v -> bad_config "endianness" [v] let system = get_config_string "system" let has_runtime_lib = match get_config_string "has_runtime_lib" with diff --git a/driver/Configuration.mli b/driver/Configuration.mli index dde9d6fd..4b9c64a9 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -19,6 +19,9 @@ val model: string val abi: string (** ABI to use *) +val is_big_endian: bool + (** Endianness to use *) + val system: string (** Flavor of operating system that runs CompCert *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 68615727..9c07dba1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -524,7 +524,9 @@ let _ = | "powerpc" -> if Configuration.system = "linux" then Machine.ppc_32_bigendian else Machine.ppc_32_diab_bigendian - | "arm" -> Machine.arm_littleendian + | "arm" -> if Configuration.is_big_endian + then Machine.arm_bigendian + else Machine.arm_littleendian | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx else Machine.x86_32 diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 0a586acd..7d1b0657 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -165,7 +165,9 @@ let _ = Machine.config := begin match Configuration.arch with | "powerpc" -> Machine.ppc_32_bigendian - | "arm" -> Machine.arm_littleendian + | "arm" -> if Configuration.is_big_endian + then Machine.arm_bigendian + else Machine.arm_littleendian | "ia32" -> Machine.x86_32 | _ -> assert false end; diff --git a/runtime/Makefile b/runtime/Makefile index e49bf3c7..c01ef38d 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -34,7 +34,7 @@ $(LIB): $(OBJS) $(CASMRUNTIME) -o $@ $^ %.o: %.S - $(CASMRUNTIME) -DMODEL_$(MODEL) -DABI_$(ABI) -DSYS_$(SYSTEM) -o $@ $^ + $(CASMRUNTIME) -DMODEL_$(MODEL) -DABI_$(ABI) -DENDIANNESS_$(ENDIANNESS) -DSYS_$(SYSTEM) -o $@ $^ clean:: rm -f *.o $(LIB) diff --git a/runtime/arm/i64_dtos.S b/runtime/arm/i64_dtos.S index 4557eeab..e31f3f34 100644 --- a/runtime/arm/i64_dtos.S +++ b/runtime/arm/i64_dtos.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -34,19 +34,19 @@ @ Helper functions for 64-bit integer arithmetic. ARM version. -#include "sysdeps.h" +#include "sysdeps.h" @@@ Conversion from double float to signed 64-bit integer - + FUNCTION(__i64_dtos) #ifndef ABI_eabi - vmov r0, r1, d0 -#endif - ASR r12, r1, #31 @ save sign of result in r12 + vmov Reg0LO, Reg0HI, d0 +#endif + ASR r12, Reg0HI, #31 @ save sign of result in r12 @ extract unbiased exponent ((HI & 0x7FF00000) >> 20) - (1023 + 52) in r2 @ note: 1023 + 52 = 1075 = 1024 + 51 @ note: (HI & 0x7FF00000) >> 20 = (HI << 1) >> 21 - LSL r2, r1, #1 + LSL r2, Reg0HI, #1 LSR r2, r2, #21 SUB r2, r2, #51 SUB r2, r2, #1024 @@ -56,45 +56,45 @@ FUNCTION(__i64_dtos) cmp r2, #11 @ if EXP >= 63 - 52, |double| is >= 2^63 bge 2f @ extract true mantissa - BIC r1, r1, #0xFF000000 - BIC r1, r1, #0x00F00000 @ HI &= ~0xFFF00000 - ORR r1, r1, #0x00100000 @ HI |= 0x00100000 + BIC Reg0HI, Reg0HI, #0xFF000000 + BIC Reg0HI, Reg0HI, #0x00F00000 @ HI &= ~0xFFF00000 + ORR Reg0HI, Reg0HI, #0x00100000 @ HI |= 0x00100000 @ shift it appropriately cmp r2, #0 blt 3f - @ EXP >= 0: shift left by EXP. Note that EXP < 12 + @ EXP >= 0: shift left by EXP. Note that EXP < 12 rsb r3, r2, #32 @ r3 = 32 - amount - LSL r1, r1, r2 - LSR r3, r0, r3 - ORR r1, r1, r3 - LSL r0, r0, r2 + LSL Reg0HI, Reg0HI, r2 + LSR r3, Reg0LO, r3 + ORR Reg0HI, Reg0HI, r3 + LSL Reg0LO, Reg0LO, r2 b 4f - @ EXP < 0: shift right by -EXP. Note that -EXP <= 52 but can be >= 32 + @ EXP < 0: shift right by -EXP. Note that -EXP <= 52 but can be >= 32 3: RSB r2, r2, #0 @ r2 = -EXP = shift amount RSB r3, r2, #32 @ r3 = 32 - amount - LSR r0, r0, r2 - LSL r3, r1, r3 - ORR r0, r0, r3 - SUB r3, r2, #32 @ r3 = amount - 32 (see i64_shr.s) - LSR r3, r1, r3 - ORR r0, r0, r3 - LSR r1, r1, r2 + LSR Reg0LO, Reg0LO, r2 + LSL r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + SUB r3, r2, #32 @ r3 = amount - 32 (see i64_shr.s) + LSR r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + LSR Reg0HI, Reg0HI, r2 @ apply sign to result -4: EOR r0, r0, r12 - EOR r1, r1, r12 - subs r0, r0, r12 - sbc r1, r1, r12 +4: EOR Reg0LO, Reg0LO, r12 + EOR Reg0HI, Reg0HI, r12 + subs Reg0LO, Reg0LO, r12 + sbc Reg0HI, Reg0HI, r12 bx lr @ special cases -1: MOV r0, #0 @ result is 0 - MOV r1, #0 +1: MOV Reg0LO, #0 @ result is 0 + MOV Reg0HI, #0 bx lr 2: cmp r12, #0 blt 6f - mvn r0, #0 @ result is 0x7F....FF (MAX_SINT) - LSR r1, r0, #1 + mvn Reg0LO, #0 @ result is 0x7F....FF (MAX_SINT) + LSR Reg0HI, Reg0LO, #1 bx lr -6: MOV r0, #0 @ result is 0x80....00 (MIN_SINT) - MOV r1, #0x80000000 +6: MOV Reg0LO, #0 @ result is 0x80....00 (MIN_SINT) + MOV Reg0HI, #0x80000000 bx lr ENDFUNCTION(__i64_dtos) diff --git a/runtime/arm/i64_dtou.S b/runtime/arm/i64_dtou.S index 57641909..6e47f3de 100644 --- a/runtime/arm/i64_dtou.S +++ b/runtime/arm/i64_dtou.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -36,18 +36,18 @@ #include "sysdeps.h" -@@@ Conversion from double float to unsigned 64-bit integer +@@@ Conversion from double float to unsigned 64-bit integer FUNCTION(__i64_dtou) #ifndef ABI_eabi - vmov r0, r1, d0 -#endif - cmp r1, #0 @ is double < 0 ? + vmov Reg0LO, Reg0HI, d0 +#endif + cmp Reg0HI, #0 @ is double < 0 ? blt 1f @ then it converts to 0 @ extract unbiased exponent ((HI & 0x7FF00000) >> 20) - (1023 + 52) in r2 @ note: 1023 + 52 = 1075 = 1024 + 51 @ note: (HI & 0x7FF00000) >> 20 = (HI << 1) >> 21 - LSL r2, r1, #1 + LSL r2, Reg0HI, #1 LSR r2, r2, #21 SUB r2, r2, #51 SUB r2, r2, #1024 @@ -57,35 +57,35 @@ FUNCTION(__i64_dtou) cmp r2, #12 @ if EXP >= 64 - 52, double is >= 2^64 bge 2f @ extract true mantissa - BIC r1, r1, #0xFF000000 - BIC r1, r1, #0x00F00000 @ HI &= ~0xFFF00000 - ORR r1, r1, #0x00100000 @ HI |= 0x00100000 + BIC Reg0HI, Reg0HI, #0xFF000000 + BIC Reg0HI, Reg0HI, #0x00F00000 @ HI &= ~0xFFF00000 + ORR Reg0HI, Reg0HI, #0x00100000 @ HI |= 0x00100000 @ shift it appropriately cmp r2, #0 blt 3f - @ EXP >= 0: shift left by EXP. Note that EXP < 12 + @ EXP >= 0: shift left by EXP. Note that EXP < 12 rsb r3, r2, #32 @ r3 = 32 - amount - LSL r1, r1, r2 - LSR r3, r0, r3 - ORR r1, r1, r3 - LSL r0, r0, r2 + LSL Reg0HI, Reg0HI, r2 + LSR r3, Reg0LO, r3 + ORR Reg0HI, Reg0HI, r3 + LSL Reg0LO, Reg0LO, r2 bx lr - @ EXP < 0: shift right by -EXP. Note that -EXP <= 52 but can be >= 32 + @ EXP < 0: shift right by -EXP. Note that -EXP <= 52 but can be >= 32 3: RSB r2, r2, #0 @ r2 = -EXP = shift amount RSB r3, r2, #32 @ r3 = 32 - amount - LSR r0, r0, r2 - LSL r3, r1, r3 - ORR r0, r0, r3 - SUB r3, r2, #32 @ r3 = amount - 32 (see i64_shr.s) - LSR r3, r1, r3 - ORR r0, r0, r3 - LSR r1, r1, r2 + LSR Reg0LO, Reg0LO, r2 + LSL r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + SUB r3, r2, #32 @ r3 = amount - 32 (see i64_shr.s) + LSR r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + LSR Reg0HI, Reg0HI, r2 bx lr @ special cases -1: MOV r0, #0 @ result is 0 - MOV r1, #0 +1: MOV Reg0LO, #0 @ result is 0 + MOV Reg0HI, #0 bx lr -2: mvn r0, #0 @ result is 0xFF....FF (MAX_UINT) - MOV r1, r0 +2: mvn Reg0LO, #0 @ result is 0xFF....FF (MAX_UINT) + MOV Reg0HI, Reg0LO bx lr ENDFUNCTION(__i64_dtou) diff --git a/runtime/arm/i64_sar.S b/runtime/arm/i64_sar.S index a4d0a1df..dcaff1ac 100644 --- a/runtime/arm/i64_sar.S +++ b/runtime/arm/i64_sar.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -42,16 +42,16 @@ FUNCTION(__i64_sar) AND r2, r2, #63 @ normalize amount to 0...63 rsbs r3, r2, #32 @ r3 = 32 - amount ble 1f @ branch if <= 0, namely if amount >= 32 - LSR r0, r0, r2 - LSL r3, r1, r3 - ORR r0, r0, r3 - ASR r1, r1, r2 + LSR Reg0LO, Reg0LO, r2 + LSL r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + ASR Reg0HI, Reg0HI, r2 bx lr 1: SUB r2, r2, #32 - ASR r0, r1, r2 - ASR r1, r1, #31 + ASR Reg0LO, Reg0HI, r2 + ASR Reg0HI, Reg0HI, #31 bx lr ENDFUNCTION(__i64_sar) - + diff --git a/runtime/arm/i64_sdiv.S b/runtime/arm/i64_sdiv.S index dd88c12a..358312da 100644 --- a/runtime/arm/i64_sdiv.S +++ b/runtime/arm/i64_sdiv.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -36,26 +36,26 @@ #include "sysdeps.h" -@@@ Signed division - +@@@ Signed division + FUNCTION(__i64_sdiv) push {r4, r5, r6, r7, r8, r10, lr} - ASR r4, r1, #31 @ r4 = sign of N - ASR r5, r3, #31 @ r5 = sign of D + ASR r4, Reg0HI, #31 @ r4 = sign of N + ASR r5, Reg1HI, #31 @ r5 = sign of D EOR r10, r4, r5 @ r10 = sign of result - EOR r0, r0, r4 @ take absolute value of N - EOR r1, r1, r4 @ N = (N ^ (N >>s 31)) - (N >>s 31) - subs r0, r0, r4 - sbc r1, r1, r4 - EOR r2, r2, r5 @ take absolute value of D - EOR r3, r3, r5 - subs r2, r2, r5 - sbc r3, r3, r5 + EOR Reg0LO, Reg0LO, r4 @ take absolute value of N + EOR Reg0HI, Reg0HI, r4 @ N = (N ^ (N >>s 31)) - (N >>s 31) + subs Reg0LO, Reg0LO, r4 + sbc Reg0HI, Reg0HI, r4 + EOR Reg1LO, Reg1LO, r5 @ take absolute value of D + EOR Reg1HI, Reg1HI, r5 + subs Reg1LO, Reg1LO, r5 + sbc Reg1HI, Reg1HI, r5 bl __i64_udivmod @ do unsigned division - EOR r0, r4, r10 @ apply expected sign - EOR r1, r5, r10 - subs r0, r0, r10 - sbc r1, r1, r10 + EOR Reg0LO, Reg2LO, r10 @ apply expected sign + EOR Reg0HI, Reg2HI, r10 + subs Reg0LO, Reg0LO, r10 + sbc Reg0HI, Reg0HI, r10 pop {r4, r5, r6, r7, r8, r10, lr} bx lr ENDFUNCTION(__i64_sdiv) diff --git a/runtime/arm/i64_shl.S b/runtime/arm/i64_shl.S index 66569d34..2b558cfe 100644 --- a/runtime/arm/i64_shl.S +++ b/runtime/arm/i64_shl.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -34,38 +34,38 @@ @ Helper functions for 64-bit integer arithmetic. ARM version. -#include "sysdeps.h" +#include "sysdeps.h" -@@@ Shift left +@@@ Shift left @ Note on ARM shifts: the shift amount is taken modulo 256. @ If shift amount mod 256 >= 32, the shift produces 0. @ Algorithm: @ RH = (XH << N) | (XL >> (32-N) | (XL << (N-32)) -@ RL = XL << N +@ RL = XL << N @ If N = 0: @ RH = XH | 0 | 0 @ RL = XL @ If 1 <= N <= 31: 1 <= 32-N <= 31 and 2s5 <= N-32 mod 256 <= 255 @ RH = (XH << N) | (XL >> (32-N) | 0 -@ RL = XL << N +@ RL = XL << N @ If N = 32: @ RH = 0 | XL | 0 @ RL = 0 @ If 33 <= N <= 63: 225 <= 32-N mod 256 <= 255 and 1 <= N-32 <= 31 @ RH = 0 | 0 | (XL << (N-32)) @ RL = 0 - + FUNCTION(__i64_shl) AND r2, r2, #63 @ normalize amount to 0...63 RSB r3, r2, #32 @ r3 = 32 - amount - LSL r1, r1, r2 - LSR r3, r0, r3 - ORR r1, r1, r3 - SUB r3, r2, #32 @ r3 = amount - 32 - LSL r3, r0, r3 - ORR r1, r1, r3 - LSL r0, r0, r2 + LSL Reg0HI, Reg0HI, r2 + LSR r3, Reg0LO, r3 + ORR Reg0HI, Reg0HI, r3 + SUB r3, r2, #32 @ r3 = amount - 32 + LSL r3, Reg0LO, r3 + ORR Reg0HI, Reg0HI, r3 + LSL Reg0LO, Reg0LO, r2 bx lr ENDFUNCTION(__i64_shl) diff --git a/runtime/arm/i64_shr.S b/runtime/arm/i64_shr.S index a5418f4a..43325092 100644 --- a/runtime/arm/i64_shr.S +++ b/runtime/arm/i64_shr.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -36,20 +36,20 @@ #include "sysdeps.h" -@@@ Shift right unsigned +@@@ Shift right unsigned @ Note on ARM shifts: the shift amount is taken modulo 256. @ If shift amount mod 256 >= 32, the shift produces 0. @ Algorithm: @ RL = (XL >> N) | (XH << (32-N) | (XH >> (N-32)) -@ RH = XH >> N +@ RH = XH >> N @ If N = 0: @ RL = XL | 0 | 0 @ RH = XH @ If 1 <= N <= 31: 1 <= 32-N <= 31 and 255 <= N-32 mod 256 <= 255 @ RL = (XL >> N) | (XH >> (32-N) | 0 -@ RH = XH >> N +@ RH = XH >> N @ If N = 32: @ RL = 0 | XH | 0 @ RH = 0 @@ -60,12 +60,12 @@ FUNCTION(__i64_shr) AND r2, r2, #63 @ normalize amount to 0...63 RSB r3, r2, #32 @ r3 = 32 - amount - LSR r0, r0, r2 - LSL r3, r1, r3 - ORR r0, r0, r3 - SUB r3, r2, #32 @ r3 = amount - 32 - LSR r3, r1, r3 - ORR r0, r0, r3 - LSR r1, r1, r2 + LSR Reg0LO, Reg0LO, r2 + LSL r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + SUB r3, r2, #32 @ r3 = amount - 32 + LSR r3, Reg0HI, r3 + ORR Reg0LO, Reg0LO, r3 + LSR Reg0HI, Reg0HI, r2 bx lr ENDFUNCTION(__i64_shr) diff --git a/runtime/arm/i64_smod.S b/runtime/arm/i64_smod.S index b109ecc3..34c33c1c 100644 --- a/runtime/arm/i64_smod.S +++ b/runtime/arm/i64_smod.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -37,25 +37,25 @@ #include "sysdeps.h" @@@ Signed modulus - + FUNCTION(__i64_smod) push {r4, r5, r6, r7, r8, r10, lr} - ASR r4, r1, #31 @ r4 = sign of N - ASR r5, r3, #31 @ r5 = sign of D + ASR r4, Reg0HI, #31 @ r4 = sign of N + ASR r5, Reg1HI, #31 @ r5 = sign of D MOV r10, r4 @ r10 = sign of result - EOR r0, r0, r4 @ take absolute value of N - EOR r1, r1, r4 @ N = (N ^ (N >>s 31)) - (N >>s 31) - subs r0, r0, r4 - sbc r1, r1, r4 - EOR r2, r2, r5 @ take absolute value of D - EOR r3, r3, r5 - subs r2, r2, r5 - sbc r3, r3, r5 + EOR Reg0LO, Reg0LO, r4 @ take absolute value of N + EOR Reg0HI, Reg0HI, r4 @ N = (N ^ (N >>s 31)) - (N >>s 31) + subs Reg0LO, Reg0LO, r4 + sbc Reg0HI, Reg0HI, r4 + EOR Reg1LO, Reg1LO, r5 @ take absolute value of D + EOR Reg1HI, Reg1HI, r5 + subs Reg1LO, Reg1LO, r5 + sbc Reg1HI, Reg1HI, r5 bl __i64_udivmod @ do unsigned division - EOR r0, r0, r10 @ apply expected sign - EOR r1, r1, r10 - subs r0, r0, r10 - sbc r1, r1, r10 + EOR Reg0LO, Reg0LO, r10 @ apply expected sign + EOR Reg0HI, Reg0HI, r10 + subs Reg0LO, Reg0LO, r10 + sbc Reg0HI, Reg0HI, r10 pop {r4, r5, r6, r7, r8, r10, lr} bx lr ENDFUNCTION(__i64_smod) diff --git a/runtime/arm/i64_stod.S b/runtime/arm/i64_stod.S index e38b466b..82ea9242 100644 --- a/runtime/arm/i64_stod.S +++ b/runtime/arm/i64_stod.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -37,17 +37,17 @@ #include "sysdeps.h" @@@ Conversion from signed 64-bit integer to double float - + FUNCTION(__i64_stod) __i64_stod: - vmov s0, r0 - vcvt.f64.u32 d0, s0 @ convert low half to double (unsigned) - vmov s2, r1 - vcvt.f64.s32 d1, s2 @ convert high half to double (signed) - vldr d2, .LC1 @ d2 = 2^32 - vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 -#ifdef ABI_eabi - vmov r0, r1, d0 @ return result in r0, r1 + vmov s0, Reg0LO + vcvt.f64.u32 d0, s0 @ convert low half to double (unsigned) + vmov s2, Reg0HI + vcvt.f64.s32 d1, s2 @ convert high half to double (signed) + vldr d2, .LC1 @ d2 = 2^32 + vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 +#ifdef ABI_eabi + vmov Reg0LO, Reg0HI, d0 @ return result in register pair r0:r1 #endif bx lr ENDFUNCTION(__i64_stod) diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S index bb5e05c0..d8a250c8 100644 --- a/runtime/arm/i64_stof.S +++ b/runtime/arm/i64_stof.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -37,11 +37,11 @@ #include "sysdeps.h" @@@ Conversion from signed 64-bit integer to single float - + FUNCTION(__i64_stof) @ Check whether -2^53 <= X < 2^53 - ASR r2, r1, #21 - ASR r3, r1, #31 @ (r2,r3) = X >> 53 + ASR r2, Reg0HI, #21 + ASR r3, Reg0HI, #31 @ (r2,r3) = X >> 53 adds r2, r2, #1 adc r3, r3, #0 @ (r2,r3) = X >> 53 + 1 cmp r3, #2 @@ -49,29 +49,29 @@ FUNCTION(__i64_stof) @ X is large enough that double rounding can occur. @ Avoid it by nudging X away from the points where double rounding @ occurs (the "round to odd" technique) - MOV r2, #0x700 + MOV r2, #0x700 ORR r2, r2, #0xFF @ r2 = 0x7FF - AND r3, r0, r2 @ extract bits 0 to 11 of X + AND r3, Reg0LO, r2 @ extract bits 0 to 11 of X ADD r3, r3, r2 @ r3 = (X & 0x7FF) + 0x7FF @ bit 12 of r3 is 0 if all low 12 bits of X are 0, 1 otherwise @ bits 13-31 of r3 are 0 - ORR r0, r0, r3 @ correct bit number 12 of X - BIC r0, r0, r2 @ set to 0 bits 0 to 11 of X + ORR Reg0LO, Reg0LO, r3 @ correct bit number 12 of X + BIC Reg0LO, Reg0LO, r2 @ set to 0 bits 0 to 11 of X @ Convert to double -1: vmov s0, r0 +1: vmov s0, Reg0LO vcvt.f64.u32 d0, s0 @ convert low half to double (unsigned) - vmov s2, r1 + vmov s2, Reg0HI vcvt.f64.s32 d1, s2 @ convert high half to double (signed) vldr d2, .LC1 @ d2 = 2^32 vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 @ Round to single vcvt.f32.f64 s0, d0 -#ifdef ABI_eabi +#ifdef ABI_eabi @ Return result in r0 - vmov r0, s0 -#endif + vmov r0, s0 +#endif bx lr ENDFUNCTION(__i64_stof) - + .balign 8 .LC1: .quad 0x41f0000000000000 @ 2^32 in double precision diff --git a/runtime/arm/i64_udiv.S b/runtime/arm/i64_udiv.S index 3b599442..316b7647 100644 --- a/runtime/arm/i64_udiv.S +++ b/runtime/arm/i64_udiv.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -36,13 +36,13 @@ #include "sysdeps.h" -@@@ Unsigned division - +@@@ Unsigned division + FUNCTION(__i64_udiv) push {r4, r5, r6, r7, r8, lr} bl __i64_udivmod - MOV r0, r4 - MOV r1, r5 + MOV Reg0LO, Reg2LO + MOV Reg0HI, Reg2HI pop {r4, r5, r6, r7, r8, lr} bx lr -ENDFUNCTION(__i64_udiv) +ENDFUNCTION(__i64_udiv) diff --git a/runtime/arm/i64_udivmod.S b/runtime/arm/i64_udivmod.S index e5373ad4..4ba99bc9 100644 --- a/runtime/arm/i64_udivmod.S +++ b/runtime/arm/i64_udivmod.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -38,42 +38,42 @@ @@@ Auxiliary function for division and modulus. Don't call from C -@ On entry: N = (r0, r1) numerator D = (r2, r3) divisor -@ On exit: Q = (r4, r5) quotient R = (r0, r1) remainder -@ Locals: M = (r6, r7) mask TMP = r8 temporary - +@ On entry: N = (r0, r1) numerator D = (r2, r3) divisor +@ On exit: Q = (r4, r5) quotient R = (r0, r1) remainder +@ Locals: M = (r6, r7) mask TMP = r8 temporary + FUNCTION(__i64_udivmod) - orrs r8, r2, r3 @ is D == 0? - it eq - bxeq lr @ if so, return with unspecified results - MOV r4, #0 @ Q = 0 - MOV r5, #0 - MOV r6, #1 @ M = 1 - MOV r7, #0 -1: cmp r3, #0 @ while ((signed) D >= 0) ... + orrs r8, Reg1LO, Reg1HI @ is D == 0? + it eq + bxeq lr @ if so, return with unspecified results + MOV Reg2LO, #0 @ Q = 0 + MOV Reg2HI, #0 + MOV Reg3LO, #1 @ M = 1 + MOV Reg3HI, #0 +1: cmp Reg1HI, #0 @ while ((signed) D >= 0) ... blt 2f - subs r8, r0, r2 @ ... and N >= D ... - sbcs r8, r1, r3 + subs r8, Reg0LO, Reg1LO @ ... and N >= D ... + sbcs r8, Reg0HI, Reg1HI blo 2f - adds r2, r2, r2 @ D = D << 1 - adc r3, r3, r3 - adds r6, r6, r6 @ M = M << 1 - adc r7, r7, r7 + adds Reg1LO, Reg1LO, Reg1LO @ D = D << 1 + adc Reg1HI, Reg1HI, Reg1HI + adds Reg3LO, Reg3LO, Reg3LO @ M = M << 1 + adc Reg3HI, Reg3HI, Reg3HI b 1b -2: subs r0, r0, r2 @ N = N - D - sbcs r1, r1, r3 - orr r4, r4, r6 @ Q = Q | M - orr r5, r5, r7 - bhs 3f @ if N was >= D, continue - adds r0, r0, r2 @ otherwise, undo what we just did - adc r1, r1, r3 @ N = N + D - bic r4, r4, r6 @ Q = Q & ~M - bic r5, r5, r7 -3: lsrs r7, r7, #1 @ M = M >> 1 - rrx r6, r6 - lsrs r3, r3, #1 @ D = D >> 1 - rrx r2, r2 - orrs r8, r6, r7 @ repeat while (M != 0) ... +2: subs Reg0LO, Reg0LO, Reg1LO @ N = N - D + sbcs Reg0HI, Reg0HI, Reg1HI + orr Reg2LO, Reg2LO, Reg3LO @ Q = Q | M + orr Reg2HI, Reg2HI, Reg3HI + bhs 3f @ if N was >= D, continue + adds Reg0LO, Reg0LO, Reg1LO @ otherwise, undo what we just did + adc Reg0HI, Reg0HI, Reg1HI @ N = N + D + bic Reg2LO, Reg2LO, Reg3LO @ Q = Q & ~M + bic Reg2HI, Reg2HI, Reg3HI +3: lsrs Reg3HI, Reg3HI, #1 @ M = M >> 1 + rrx Reg3LO, Reg3LO + lsrs Reg1HI, Reg1HI, #1 @ D = D >> 1 + rrx Reg1LO, Reg1LO + orrs r8, Reg3LO, Reg3HI @ repeat while (M != 0) ... bne 2b bx lr ENDFUNCTION(__i64_udivmod) diff --git a/runtime/arm/i64_utod.S b/runtime/arm/i64_utod.S index b4c30754..593f8543 100644 --- a/runtime/arm/i64_utod.S +++ b/runtime/arm/i64_utod.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -37,17 +37,17 @@ #include "sysdeps.h" @@@ Conversion from unsigned 64-bit integer to double float - + FUNCTION(__i64_utod) -__i64_stod: - vmov s0, r0 - vcvt.f64.u32 d0, s0 @ convert low half to double (unsigned) - vmov s2, r1 - vcvt.f64.u32 d1, s2 @ convert high half to double (unsigned) - vldr d2, .LC1 @ d2 = 2^32 - vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 -#ifdef ABI_eabi - vmov r0, r1, d0 @ return result in r0, r1 +__i64_utod: + vmov s0, Reg0LO + vcvt.f64.u32 d0, s0 @ convert low half to double (unsigned) + vmov s2, Reg0HI + vcvt.f64.u32 d1, s2 @ convert high half to double (unsigned) + vldr d2, .LC1 @ d2 = 2^32 + vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 +#ifdef ABI_eabi + vmov Reg0LO, Reg0HI, d0 @ return result in register pair r0:r1 #endif bx lr ENDFUNCTION(__i64_utod) diff --git a/runtime/arm/i64_utof.S b/runtime/arm/i64_utof.S index fbd325c8..be0ecc6a 100644 --- a/runtime/arm/i64_utof.S +++ b/runtime/arm/i64_utof.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -37,35 +37,35 @@ #include "sysdeps.h" @@@ Conversion from unsigned 64-bit integer to single float - + FUNCTION(__i64_utof) @ Check whether X < 2^53 - lsrs r2, r1, #21 @ test if X >> 53 == 0 + lsrs r2, Reg0HI, #21 @ test if X >> 53 == 0 beq 1f @ X is large enough that double rounding can occur. @ Avoid it by nudging X away from the points where double rounding @ occurs (the "round to odd" technique) - MOV r2, #0x700 + MOV r2, #0x700 ORR r2, r2, #0xFF @ r2 = 0x7FF - AND r3, r0, r2 @ extract bits 0 to 11 of X + AND r3, Reg0LO, r2 @ extract bits 0 to 11 of X ADD r3, r3, r2 @ r3 = (X & 0x7FF) + 0x7FF @ bit 12 of r3 is 0 if all low 12 bits of X are 0, 1 otherwise @ bits 13-31 of r3 are 0 - ORR r0, r0, r3 @ correct bit number 12 of X - BIC r0, r0, r2 @ set to 0 bits 0 to 11 of X + ORR Reg0LO, Reg0LO, r3 @ correct bit number 12 of X + BIC Reg0LO, Reg0LO, r2 @ set to 0 bits 0 to 11 of X @ Convert to double -1: vmov s0, r0 +1: vmov s0, Reg0LO vcvt.f64.u32 d0, s0 @ convert low half to double (unsigned) - vmov s2, r1 + vmov s2, Reg0HI vcvt.f64.u32 d1, s2 @ convert high half to double (unsigned) vldr d2, .LC1 @ d2 = 2^32 vmla.f64 d0, d1, d2 @ d0 = d0 + d1 * d2 = double value of int64 @ Round to single vcvt.f32.f64 s0, d0 -#ifdef ABI_eabi +#ifdef ABI_eabi @ Return result in r0 - vmov r0, s0 -#endif + vmov r0, s0 +#endif bx lr ENDFUNCTION(__i64_utof) diff --git a/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h index 3d6a702c..fd4ea61d 100644 --- a/runtime/arm/sysdeps.h +++ b/runtime/arm/sysdeps.h @@ -95,3 +95,43 @@ f: .arch armv7 #endif .fpu vfpv2 + + + +// Endianness dependencies + +// Location of high and low word of first register pair (r0:r1) +#ifdef ENDIANNESS_big +#define Reg0HI r0 +#define Reg0LO r1 +#else +#define Reg0HI r1 +#define Reg0LO r0 +#endif + +// Location of high and low word of second register pair (r2:r3) +#ifdef ENDIANNESS_big +#define Reg1HI r2 +#define Reg1LO r3 +#else +#define Reg1HI r3 +#define Reg1LO r2 +#endif + +// Location of high and low word of third register pair (r4:r5) +#ifdef ENDIANNESS_big +#define Reg2HI r4 +#define Reg2LO r5 +#else +#define Reg2HI r5 +#define Reg2LO r4 +#endif + +// Location of high and low word of fourth register pair (r6:r7) +#ifdef ENDIANNESS_big +#define Reg3HI r6 +#define Reg3LO r7 +#else +#define Reg3HI r7 +#define Reg3LO r6 +#endif diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S index 5e319b8b..6f446ca8 100644 --- a/runtime/arm/vararg.S +++ b/runtime/arm/vararg.S @@ -17,7 +17,7 @@ @ * Neither the name of the <organization> nor the @ names of its contributors may be used to endorse or promote products @ derived from this software without specific prior written permission. -@ +@ @ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS @ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT @ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR @@ -70,9 +70,9 @@ FUNCTION(__compcert_va_float64) #ifdef ABI_eabi ldr r0, [r1, #-8] @ load next argument and return it in r0,r1 ldr r1, [r1, #-4] -#else +#else vldr d0, [r1, #-8] @ load next argument and return it in d0 -#endif +#endif bx lr ENDFUNCTION(__compcert_va_float64) diff --git a/test/c/aes.c b/test/c/aes.c index 88b3de4a..053324f3 100644 --- a/test/c/aes.c +++ b/test/c/aes.c @@ -32,11 +32,11 @@ #define MAXKB (256/8) #define MAXNR 14 -typedef unsigned char u8; -typedef unsigned short u16; +typedef unsigned char u8; +typedef unsigned short u16; typedef unsigned int u32; -#if defined(__ppc__) || defined(__PPC__) +#if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__) #define ARCH_BIG_ENDIAN #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) #undef ARCH_BIG_ENDIAN @@ -1295,7 +1295,7 @@ void rijndaelEncryptRound(const u32 rk[/*4*(Nr + 1)*/], int Nr, u8 block[16], in (Te4[(s1 >> 8) & 0xff] & 0x0000ff00) ^ (Te4[(s2 ) & 0xff] & 0x000000ff) ^ rk[3]; - + s0 = t0; s1 = t1; s2 = t2; @@ -1433,7 +1433,7 @@ static void do_bench(int nblocks) int main(int argc, char ** argv) { - do_test(128, + do_test(128, (u8 *)"\x00\x01\x02\x03\x04\x05\x06\x07\x08\x09\x0A\x0B\x0C\x0D\x0E\x0F", (u8 *)"\x00\x11\x22\x33\x44\x55\x66\x77\x88\x99\xAA\xBB\xCC\xDD\xEE\xFF", (u8 *)"\x69\xC4\xE0\xD8\x6A\x7B\x04\x30\xD8\xCD\xB7\x80\x70\xB4\xC5\x5A", diff --git a/test/c/sha1.c b/test/c/sha1.c index dff32a8e..3eab9b3d 100644 --- a/test/c/sha1.c +++ b/test/c/sha1.c @@ -178,7 +178,7 @@ static void do_test(unsigned char * txt, unsigned char * expected_output) SHA1_add_data(&ctx, txt, strlen((char *) txt)); SHA1_finish(&ctx, output); ok = memcmp(output, expected_output, 20) == 0; - printf("Test `%s': %s\n", + printf("Test `%s': %s\n", (char *) txt, (ok ? "passed" : "FAILED")); } @@ -197,7 +197,7 @@ unsigned char test_output_1[20] = { 0xA9, 0x99, 0x3E, 0x36, 0x47, 0x06, 0x81, 0x6A, 0xBA, 0x3E , 0x25, 0x71, 0x78, 0x50, 0xC2, 0x6C, 0x9C, 0xD0, 0xD8, 0x9D }; -unsigned char test_input_2[] = +unsigned char test_input_2[] = "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"; unsigned char test_output_2[20] = @@ -214,7 +214,7 @@ static void do_bench(int nblocks) for (i = 0; i < 64; i++) data[i] = i; SHA1_init(&ctx); - for (; nblocks > 0; nblocks--) + for (; nblocks > 0; nblocks--) SHA1_add_data(&ctx, data, 64); SHA1_finish(&ctx, output); } diff --git a/test/cminor/aes.cmp b/test/cminor/aes.cmp index 510e59f8..050c4966 100644 --- a/test/cminor/aes.cmp +++ b/test/cminor/aes.cmp @@ -1,6 +1,6 @@ /* AES cipher. To be preprocessed with cpp -P. */ -#if defined(__ppc__) || defined(__PPC__) +#if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__) #define ARCH_BIG_ENDIAN #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) #undef ARCH_BIG_ENDIAN @@ -111,7 +111,7 @@ rk(13) = rk( 5) ^ rk(12); rk(14) = rk( 6) ^ rk(13); rk(15) = rk( 7) ^ rk(14); - + rk_ = rk_ + 8 * 4; } }} } @@ -316,7 +316,7 @@ Td2((s1 >>u 8) & 0xff) ^ Td3((s0 ) & 0xff) ^ rk(7); - + rk_ = rk_ + 8 * 4; r = r - 1; if (r == 0) exit; diff --git a/test/cminor/sha1.cmp b/test/cminor/sha1.cmp index 98a6b51a..96e3c038 100644 --- a/test/cminor/sha1.cmp +++ b/test/cminor/sha1.cmp @@ -6,7 +6,7 @@ extern "memcpy" : int -> int -> int -> void extern "memset" : int -> int -> int -> void -#if defined(__ppc__) || defined(__PPC__) +#if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__) #define ARCH_BIG_ENDIAN #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) #undef ARCH_BIG_ENDIAN diff --git a/test/regression/floats-basics.c b/test/regression/floats-basics.c index 0a4c69d1..5aa91d14 100644 --- a/test/regression/floats-basics.c +++ b/test/regression/floats-basics.c @@ -4,7 +4,7 @@ #define STR_EXPAND(tok) #tok #define STR(tok) STR_EXPAND(tok) -#if defined(__ppc__) || defined(__PPC__) +#if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__) #define ARCH_BIG_ENDIAN #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) #undef ARCH_BIG_ENDIAN @@ -69,7 +69,7 @@ int main(void) { compd(15./16, 0x.Fp0, STR(__LINE__)); compd(15./16, 0x.fP0, STR(__LINE__)); compd(15./16, 0X.fp0, STR(__LINE__)); - + printf("%d error(s) detected.\n", num_errors); return 0; } diff --git a/test/regression/floats.c b/test/regression/floats.c index a3514fb5..68d60f65 100644 --- a/test/regression/floats.c +++ b/test/regression/floats.c @@ -3,7 +3,7 @@ #define STR_EXPAND(tok) #tok #define STR(tok) STR_EXPAND(tok) -#if defined(__ppc__) || defined(__PPC__) +#if defined(__ppc__) || defined(__PPC__) || defined(__ARMEB__) #define ARCH_BIG_ENDIAN #elif defined(__i386__) || defined(__x86_64__) || defined(__ARMEL__) #undef ARCH_BIG_ENDIAN |