diff options
56 files changed, 1051 insertions, 577 deletions
@@ -52,6 +52,7 @@ cparser/tests/generated/*.err backend/CMparser.automaton lib/Readconfig.ml lib/Tokenize.ml +lib/Responsefile.ml driver/Version.ml # Documentation doc/coq2html @@ -202,12 +202,14 @@ 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)"; \ echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ echo "struct_passing_style=$(STRUCT_PASSING)"; \ - echo "struct_return_style=$(STRUCT_RETURN)";) \ + echo "struct_return_style=$(STRUCT_RETURN)"; \ + echo "response_file_style=$(RESPONSEFILE)";) \ > compcert.ini driver/Version.ml: VERSION diff --git a/Makefile.extr b/Makefile.extr index 51dbd767..8fdc9ffe 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -63,7 +63,8 @@ MODORDER=tools/modorder .depend.extr PARSERS=backend/CMparser.mly cparser/pre_parser.mly LEXERS=backend/CMlexer.mll cparser/Lexer.mll \ - lib/Tokenize.mll lib/Readconfig.mll + lib/Tokenize.mll lib/Readconfig.mll \ + lib/Responsefile.mll LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS) LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS))) 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/backend/Regalloc.ml b/backend/Regalloc.ml index e6e07339..0013d91a 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -915,7 +915,12 @@ let spill_instr tospill eqs instr = | false, true -> let eqs1 = add arg1 res (kill res eqs) in let (argl', c1, eqs2) = reload_vars tospill eqs1 argl in - (Xreload(arg1, res) :: c1 @ [Xop(op, res :: argl', res)], + (* PR#113, PR#122: [Xreload] here causes [res] to become + unspillable in the future. This is too strong, hence + the [Xmove]. Alternatively, this [false, true] + case could be removed and the [true, true] case + below used instead. *) + (Xmove(arg1, res) :: c1 @ [Xop(op, res :: argl', res)], kill res eqs2) | true, true -> let tmp = new_temp (typeof res) in diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c33449e4..4049907e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -758,7 +758,7 @@ let rec convertExpr env e = let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) - | _ -> error "argument 1 of '__builtin_debug' must be constant"; (0L, args) in + | _ -> error "argument 1 of '__builtin_debug' must be constant"; (1L, args) in let (text, args2) = match args1 with | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 7933f987..e3e259f7 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -401,7 +401,7 @@ let name_function_parameters fun_name params cconv = | _ -> let rec add_params first = function | [] -> - if cconv.cc_vararg then Buffer.add_string b "..." + if cconv.cc_vararg then Buffer.add_string b ",..." | (id, ty) :: rem -> if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl (extern_atom id) ty); @@ -426,7 +426,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) -> + | Ctypes.External((EF_external _ | EF_runtime _| EF_malloc | EF_free), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | Ctypes.External(_, _, _, _) -> @@ -434,6 +434,14 @@ let print_fundef p id fd = | Ctypes.Internal f -> print_function p id f +let print_fundecl p id fd = + match fd with + | Ctypes.Internal f -> + let linkage = if C2C.atom_is_static id then "static" else "extern" in + fprintf p "%s %s;@ @ " linkage + (name_cdecl (extern_atom id) (Csyntax.type_of_function f)) + | _ -> () + let string_of_init id = let b = Buffer.create (List.length id) in let add_init = function @@ -501,6 +509,17 @@ let print_globvar p id v = end; fprintf p ";@]@ @ " +let print_globvardecl p id v = + let name = extern_atom id in + let name = if v.gvar_readonly then "const "^name else name in + let linkage = if C2C.atom_is_static id then "static" else "extern" in + fprintf p "%s %s;@ @ " linkage (name_cdecl name v.gvar_info) + +let print_globdecl p (id,gd) = + match gd with + | Gfun f -> print_fundecl p id f + | Gvar v -> print_globvardecl p id v + let print_globdef p (id, gd) = match gd with | Gfun f -> print_fundef p id f @@ -524,6 +543,7 @@ let print_program p prog = fprintf p "@[<v 0>"; List.iter (declare_composite p) prog.prog_types; List.iter (define_composite p) prog.prog_types; + List.iter (print_globdecl p) prog.prog_defs; List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." 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='' @@ -20,48 +20,61 @@ target='' has_runtime_lib=true has_standard_headers=true clightgen=false +responsefile="gnu" 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, little endian) + arm-linux (ARM, EABI, little endian) + arm-eabihf (ARM, EABI using hardware FP registers, little endian) + arm-hardfloat (ARM, EABI using hardware FP registers, little endian) + armeb-eabi (ARM, EABI, big endian) + armeb-linux (ARM, EABI, big endian) + armeb-eabihf (ARM, EABI using hardware FP registers, big endian) + armeb-hardfloat (ARM, EABI using hardware FP registers, big endian) + 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 +For ARM targets, the "arm-" or "armeb-" prefix can be refined into: + armv6- ARMv6 + VFPv2 + armv7a- ARMv7-A + VFPv3-d16 (default for arm-) + armv7r- ARMv7-R + VFPv3-d16 + armv7m- ARMv7-M + VFPv3-d16 + + armebv6- ARMv6 + VFPv2 + armebv7a- ARMv7-A + VFPv3-d16 (default for armeb-) + armebv7r- ARMv7-R + VFPv3-d16 + armebv7m- ARMv7-M + VFPv3-d16 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 +96,247 @@ 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";; + armeb-*|armebv7a-*) + arch="arm"; model="armv7a"; endianness="big";; + armebv6-*) + arch="arm"; model="armv6"; endianness="big";; + armebv7r-*) + arch="arm"; model="armv7r"; endianness="big";; + armebv7m-*) + arch="arm"; model="armv7m"; endianness="big";; + 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]*-} + + +# 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" + responsefile="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" + 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" - 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="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 + esac +fi +# +# Finalize Target Configuration +# if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; 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 +345,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 +435,10 @@ if $missingtools; then exit 2 fi -# Generate Makefile.config +# +# Generate Makefile.config +# sharedir="$(dirname "$bindir")"/share rm -f Makefile.config @@ -367,25 +452,27 @@ 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 +RESPONSEFILE=$responsefile EOF else cat >> Makefile.config <<'EOF' @@ -397,40 +484,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 +550,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 @@ -469,19 +566,22 @@ ASM_SUPPORTS_CFI=false # Turn on/off compilation of clightgen CLIGHTGEN=false -EOF +# Whether the other tools support responsefiles in gnu syntax +RESPONSEFILE="none" +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 +593,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 +613,4 @@ CompCert configuration: If anything above looks wrong, please edit file ./Makefile.config to correct. EOF - fi diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 8ee13caf..046ca9b0 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -207,7 +207,7 @@ let rc fmt = cprintf fmt "\x1b[31;1m" let mc fmt = - cprintf fmt "\x1b35;1m" + cprintf fmt "\x1b[35;1m" let pp_key key fmt = let key = match key with @@ -240,7 +240,7 @@ let warning loc ty fmt = | WarningMsg -> incr num_warnings; kfprintf (pp_key key) - err_formatter ("%a %twarning:%tm: %t" ^^ fmt) pp_loc loc mc rsc bc + err_formatter ("%a %twarning:%t: %t" ^^ fmt) pp_loc loc mc rsc bc | SuppressedMsg -> ifprintf err_formatter fmt let error loc fmt = @@ -301,3 +301,7 @@ let warning_help = "Diagnostic options:\n\ \ -Wfatal-errors Turn all errors into fatal errors aborting the compilation\n\ \ -fdiagnostics-color Turn on colored diagnostics\n\ \ -fno-diagnostics-color Turn of colored diagnostics\n" + +let raise_on_errors () = + if !num_errors > 0 then + raise Abort diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index b312931a..b547188a 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -68,3 +68,5 @@ val warning_help : string val warning_options : (Commandline.pattern * Commandline.action) list (** List of all options for diagnostics *) + +val raise_on_errors : unit -> unit diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index b19b1e4b..53142598 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -1034,6 +1034,7 @@ let formatloc pp (filename, lineno) = if filename <> "" then Format.fprintf pp "%s:%d: " filename lineno (* Generate the default initializer for the given type *) +exception No_default_init let rec default_init env ty = match unroll env ty with @@ -1057,11 +1058,11 @@ let rec default_init env ty = | TUnion(id, _) -> let ci = Env.find_union env id in begin match ci.ci_members with - | [] -> assert false + | [] -> raise No_default_init | fld :: _ -> Init_union(id, fld, default_init env fld.fld_typ) end | _ -> - assert false + raise No_default_init (* Substitution of variables by expressions *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index b724f573..7fc6aedd 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -247,6 +247,8 @@ val formatloc: Format.formatter -> location -> unit (* Printer for locations (for Format) *) (* Initializers *) +exception No_default_init + (* Raised if no default initilaizer exists *) val default_init: Env.t -> typ -> init (* Return a default initializer for the given type diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 52426014..728739bf 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -188,8 +188,8 @@ let enter_or_refine_ident local loc env s sto ty = let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref = ref (fun _ _ _ -> assert false) -let elab_funbody_f : (C.typ -> Env.t -> statement -> C.stmt) ref - = ref (fun _ _ _ -> assert false) +let elab_funbody_f : (C.typ -> bool -> Env.t -> statement -> C.stmt) ref + = ref (fun _ _ _ _ -> assert false) (** * Elaboration of constants - C99 section 6.4.4 *) @@ -451,6 +451,7 @@ let elab_attribute env = function error loc "requested alignment is not a power of 2"; [] end | _ -> error loc "requested alignment is not an integer constant"; [] + | exception Wrong_attr_arg -> error loc "bad _Alignas value"; [] end | ALIGNAS_ATTR (_, loc) -> error loc "_Alignas takes no more than 1 argument"; [] @@ -490,7 +491,7 @@ let is_anonymous_composite spec = C99 section 6.7.2. *) -let rec elab_specifier ?(only = false) loc env specifier = +let rec elab_specifier keep_ty ?(only = false) loc env specifier = (* We first divide the parts of the specifier as follows: - a storage class - a set of attributes (const, volatile, restrict) @@ -594,14 +595,14 @@ let rec elab_specifier ?(only = false) loc env specifier = let a' = add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = - elab_struct_or_union only Struct loc id optmembers a' env in + elab_struct_or_union keep_ty only Struct loc id optmembers a' env in (!sto, !inline, !noreturn, !typedef, TStruct(id', !attr), env') | [Cabs.Tstruct_union(UNION, id, optmembers, a)] -> let a' = add_attributes (get_type_attrs()) (elab_attributes env a) in let (id', env') = - elab_struct_or_union only Union loc id optmembers a' env in + elab_struct_or_union keep_ty only Union loc id optmembers a' env in (!sto, !inline, !noreturn, !typedef, TUnion(id', !attr), env') | [Cabs.Tenum(id, optmembers, a)] -> @@ -635,7 +636,7 @@ and elab_return_type loc env ty = error loc "function cannot return function type %a" (print_typ env) ty | _ -> () -and elab_type_declarator loc env ty kr_ok = function +and elab_type_declarator keep_ty loc env ty kr_ok = function | Cabs.JUSTBASE -> ((ty, None), env) | Cabs.ARRAY(d, cv_specs, sz) -> @@ -655,19 +656,20 @@ and elab_type_declarator loc env ty kr_ok = function | None -> error loc "size of array is not a compile-time constant"; Some 1L in (* produces better error messages later *) - elab_type_declarator loc env (TArray(ty, sz', a)) kr_ok d + elab_type_declarator keep_ty loc env (TArray(ty, sz', a)) kr_ok d | Cabs.PTR(cv_specs, d) -> let a = elab_cvspecs env cv_specs in - elab_type_declarator loc env (TPtr(ty, a)) kr_ok d + elab_type_declarator keep_ty loc env (TPtr(ty, a)) kr_ok d | Cabs.PROTO(d, (params, vararg)) -> elab_return_type loc env ty; - let params' = elab_parameters env params in - elab_type_declarator loc env (TFun(ty, Some params', vararg, [])) kr_ok d + let params',env' = elab_parameters keep_ty env params in + let env = if keep_ty then Env.add_types env env' else env in + elab_type_declarator keep_ty loc env (TFun(ty, Some params', vararg, [])) kr_ok d | Cabs.PROTO_OLD(d, params) -> elab_return_type loc env ty; match params with | [] -> - elab_type_declarator loc env (TFun(ty, None, false, [])) kr_ok d + elab_type_declarator keep_ty loc env (TFun(ty, None, false, [])) kr_ok d | _ -> if not kr_ok || d <> Cabs.JUSTBASE then fatal_error loc "illegal old-style K&R function definition"; @@ -675,21 +677,21 @@ and elab_type_declarator loc env ty kr_ok = function (* Elaboration of parameters in a prototype *) -and elab_parameters env params = +and elab_parameters keep_ty env params = (* Prototype introduces a new scope *) - let (vars, _) = mmap elab_parameter (Env.new_scope env) params in + let (vars, env) = mmap (elab_parameter keep_ty) (Env.new_scope env) params in (* Catch special case f(t) where t is void or a typedef to void *) match vars with - | [ ( {C.name=""}, t) ] when is_void_type env t -> [] - | _ -> vars + | [ ( {C.name=""}, t) ] when is_void_type env t -> [],env + | _ -> vars,env (* Elaboration of a function parameter *) -and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = - let (sto, inl, noret, tydef, bty, env1) = elab_specifier loc env spec in +and elab_parameter keep_ty env (PARAM (spec, id, decl, attr, loc)) = + let (sto, inl, noret, tydef, bty, env1) = elab_specifier keep_ty loc env spec in if tydef then error loc "'typedef' used in function parameter"; - let ((ty, _), _) = elab_type_declarator loc env1 bty false decl in + let ((ty, _), _) = elab_type_declarator keep_ty loc env1 bty false decl in let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then error loc @@ -704,23 +706,23 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = (* replace array and function types by pointer types *) let ty1 = argument_conversion env1 ty in let (id', env2) = Env.enter_ident env1 id sto ty1 in - ( (id', ty1) , env2 ) + ( (id', ty1) , env2) (* Elaboration of a (specifier, Cabs "name") pair *) -and elab_fundef_name env spec (Name (id, decl, attr, loc)) = - let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in +and elab_fundef_name keep_ty env spec (Name (id, decl, attr, loc)) = + let (sto, inl, noret, tydef, bty, env') = elab_specifier keep_ty loc env spec in if tydef then error loc "'typedef' is forbidden here"; - let ((ty, kr_params), env'') = elab_type_declarator loc env' bty true decl in + let ((ty, kr_params), env'') = elab_type_declarator keep_ty loc env' bty true decl in let a = elab_attributes env attr in (id, sto, inl, noret, add_attributes_type a ty, kr_params, env'') (* Elaboration of a name group. C99 section 6.7.6 *) -and elab_name_group loc env (spec, namelist) = +and elab_name_group keep_ty loc env (spec, namelist) = let (sto, inl, noret, tydef, bty, env') = - elab_specifier loc env spec in + elab_specifier keep_ty loc env spec in if tydef then error loc "'typedef' is forbidden here"; if inl then @@ -729,19 +731,19 @@ and elab_name_group loc env (spec, namelist) = error loc "'_Noreturn' is forbidden here"; let elab_one_name env (Name (id, decl, attr, loc)) = let ((ty, _), env1) = - elab_type_declarator loc env bty false decl in + elab_type_declarator keep_ty loc env bty false decl in let a = elab_attributes env attr in ((id, add_attributes_type a ty), env1) in (mmap elab_one_name env' namelist, sto) (* Elaboration of an init-name group *) -and elab_init_name_group loc env (spec, namelist) = +and elab_init_name_group keep_ty loc env (spec, namelist) = let (sto, inl, noret, tydef, bty, env') = - elab_specifier ~only:(namelist=[]) loc env spec in + elab_specifier keep_ty ~only:(namelist=[]) loc env spec in let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = let ((ty, _), env1) = - elab_type_declarator loc env bty false decl in + elab_type_declarator keep_ty loc env bty false decl in let a = elab_attributes env attr in if inl && not (is_function_type env ty) then error loc "'inline' can only appear on functions"; @@ -752,7 +754,7 @@ and elab_init_name_group loc env (spec, namelist) = (* Elaboration of a field group *) -and elab_field_group env (Field_group (spec, fieldlist, loc)) = +and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = let fieldlist = List.map ( function @@ -762,7 +764,7 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = in let ((names, env'), sto) = - elab_name_group loc env (spec, List.map fst fieldlist) in + elab_name_group keep_ty loc env (spec, List.map fst fieldlist) in if sto <> Storage_default then error loc "non-default storage in struct or union"; @@ -815,8 +817,8 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = (* Elaboration of a struct or union. C99 section 6.7.2.1 *) -and elab_struct_or_union_info kind loc env members attrs = - let (m, env') = mmap elab_field_group env members in +and elab_struct_or_union_info keep_ty kind loc env members attrs = + let (m, env') = mmap (elab_field_group keep_ty) env members in let m = List.flatten m in (* Check for incomplete types *) let rec check_incomplete = function @@ -831,10 +833,14 @@ and elab_struct_or_union_info kind loc env members attrs = check_incomplete m; (* Warn for empty structs or unions *) if m = [] then - warning loc Celeven_extension "anonymous %s are an extension" (if kind = Struct then "struct" else "union"); + if kind = Struct then begin + warning loc Celeven_extension "anonymous structs are a C11 extension" + end else begin + fatal_error loc "anonymous unions are a C11 extension" + end; (composite_info_def env' kind attrs m, env') -and elab_struct_or_union only kind loc tag optmembers attrs env = +and elab_struct_or_union keep_ty only kind loc tag optmembers attrs env = let warn_attrs () = if attrs <> [] then warning loc Unnamed "attribute declaration must precede definition" in @@ -853,7 +859,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = create a new incomplete composite instead via the case "_, None" below. *) if ci.ci_kind <> kind then - error loc "use of '%s' with tag type that does not match previous declaration" tag; + fatal_error loc "use of '%s' with tag type that does not match previous declaration" tag; warn_attrs(); (tag', env) | Some(tag', ({ci_sizeof = None} as ci)), Some members @@ -861,7 +867,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = if ci.ci_kind <> kind then error loc "use of '%s' with tag type that does not match previous declaration" tag; (* finishing the definition of an incomplete struct or union *) - let (ci', env') = elab_struct_or_union_info kind loc env members attrs in + let (ci', env') = elab_struct_or_union_info keep_ty kind loc env members attrs in (* Emit a global definition for it *) emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.ci_members)); (* Replace infos but keep same ident *) @@ -889,7 +895,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = emit_elab env' loc (Gcompositedecl(kind, tag', attrs)); (* elaborate the members *) let (ci2, env'') = - elab_struct_or_union_info kind loc env' members attrs in + elab_struct_or_union_info keep_ty kind loc env' members attrs in (* emit a definition *) emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.ci_members)); (* Replace infos but keep same ident *) @@ -948,8 +954,8 @@ and elab_enum only loc tag optmembers attrs env = (* Elaboration of a naked type, e.g. in a cast *) let elab_type loc env spec decl = - let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in - let ((ty, _), env'') = elab_type_declarator loc env' bty false decl in + let (sto, inl, noret, tydef, bty, env') = elab_specifier false loc env spec in + let ((ty, _), env'') = elab_type_declarator false loc env' bty false decl in if sto <> Storage_default || inl || noret || tydef then error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast"; (ty, env'') @@ -1304,7 +1310,16 @@ and elab_single zi a il = (* Start with top-level object initialized to default *) -in elab_item (I.top env root ty_root) ie [] +in +if is_function_type env ty_root then begin + error loc "illegal initializer (only variables can be initialized)"; + raise Exit +end; +try + elab_item (I.top env root ty_root) ie [] +with No_default_init -> + error loc "variable has incomplete type %a" Cprint.typ ty_root; + raise Exit (* Elaboration of a top-level initializer *) @@ -1340,7 +1355,7 @@ let elab_initializer loc env root ty ie = (* Elaboration of expressions *) -let elab_expr loc env a = +let elab_expr vararg loc env a = let err fmt = error loc fmt in (* non-fatal error *) let error fmt = fatal_error loc fmt in @@ -1428,6 +1443,8 @@ let elab_expr loc env a = (elaboration) --> __builtin_va_arg(ap, sizeof(ty)) *) | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) -> + if not vararg then + err "'va_start' used in function with fixed args"; let b1,env = elab env a1 in let b2,env = elab env a2 in let _b3,env = elab env a3 in @@ -1491,7 +1508,7 @@ let elab_expr loc env a = (* 6.5.4 Cast operators *) | CAST ((spec, dcl), SINGLE_INIT a1) -> - let (ty, _) = elab_type loc env spec dcl in + let (ty, env) = elab_type loc env spec dcl in let b1,env = elab env a1 in if not (wrap2 valid_cast loc env b1.etyp ty) then begin match unroll env b1.etyp, unroll env ty with @@ -1514,7 +1531,7 @@ let elab_expr loc env a = (* 6.5.2.5 Compound literals *) | CAST ((spec, dcl), ie) -> - let (ty, _) = elab_type loc env spec dcl in + let (ty, env) = elab_type loc env spec dcl in begin match elab_initializer loc env "<compound literal>" ty ie with | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' },env | (ty', None) -> error "ill-formed compound literal" @@ -1525,7 +1542,7 @@ let elab_expr loc env a = | EXPR_SIZEOF a1 -> let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then - err "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; + error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; let bdesc = (* Catch special cases sizeof("string literal") *) match b1.edesc with @@ -1542,19 +1559,19 @@ let elab_expr loc env a = | TYPE_SIZEOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then - err "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) ty; + error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) ty; { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) },env' | EXPR_ALIGNOF a1 -> let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then - err "invalid application of 'alignof' to an incomplete type %a" (print_typ env) b1.etyp; + error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) b1.etyp; { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) },env | TYPE_ALIGNOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then - err "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty; + error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty; { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env' | UNARY(PLUS, a1) -> @@ -1659,9 +1676,9 @@ let elab_expr loc env a = let tyres = binary_conversion env b1.etyp b2.etyp in (tyres, tyres) end else begin - match unroll env b1.etyp, unroll env b2.etyp with + match wrap unroll loc env b1.etyp, wrap unroll loc env b2.etyp with | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> - if not (pointer_arithmetic_ok env ty) then + if not (wrap pointer_arithmetic_ok loc env ty) then err "illegal pointer arithmetic in binary '-'"; (TPtr(ty, []), TPtr(ty, [])) | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> @@ -1935,16 +1952,16 @@ let elab_expr loc env a = in elab env a (* Filling in forward declaration *) -let _ = elab_expr_f := elab_expr +let _ = elab_expr_f := (elab_expr false) -let elab_opt_expr loc env = function +let elab_opt_expr vararg loc env = function | None -> None,env - | Some a -> let a,env = (elab_expr loc env a) in + | Some a -> let a,env = (elab_expr vararg loc env a) in Some a,env -let elab_for_expr loc env = function +let elab_for_expr vararg loc env = function | None -> { sdesc = Sskip; sloc = elab_loc loc },env - | Some a -> let a,env = elab_expr loc env a in + | Some a -> let a,env = elab_expr vararg loc env a in { sdesc = Sdo a; sloc = elab_loc loc },env (* Handling of __func__ (section 6.4.2.2) *) @@ -2000,6 +2017,8 @@ let enter_decdefs local loc env sto dl = initializer can refer to the ident *) let (id, sto', env1, ty, linkage) = enter_or_refine_ident local loc env s sto1 ty in + if not isfun && is_void_type env ty then + fatal_error loc "'%s' has incomplete type" s; (* process the initializer *) let (ty', init') = elab_initializer loc env1 s ty init in (* update environment with refined type *) @@ -2055,7 +2074,7 @@ let elab_KR_function_parameters env params defs loc = let elab_param_def env = function | DECDEF((spec', name_init_list), loc') -> let name_list = List.map extract_name name_init_list in - let (paramsenv, sto) = elab_name_group loc' env (spec', name_list) in + let (paramsenv, sto) = elab_name_group true loc' env (spec', name_list) in if sto <> Storage_default && sto <> Storage_register then error loc' "invalid storage class specifier in function declarator"; paramsenv @@ -2121,7 +2140,7 @@ let inherit_vararg env s sto ty = let elab_fundef env spec name defs body loc = let (s, sto, inline, noret, ty, kr_params, env1) = - elab_fundef_name env spec name in + elab_fundef_name true env spec name in if sto = Storage_register then fatal_error loc "illegal storage class on function"; begin match kr_params, defs with @@ -2159,9 +2178,13 @@ let elab_fundef env spec name defs body loc = (* Enter function in the environment, for recursive references *) let (fun_id, sto1, env1, _, _) = enter_or_refine_ident false loc env1 s sto ty in + let incomplete_param env ty = + if wrap incomplete_type loc env ty then + fatal_error loc "parameter has incomplete type" in (* Enter parameters and extra declarations in the environment *) let env2 = - List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) + List.fold_left (fun e (id, ty) -> incomplete_param e ty; + Env.add_ident e id Storage_default ty) (Env.new_scope env1) params in let env2 = List.fold_left (fun e (sto, id, ty, init) -> Env.add_ident e id sto ty) @@ -2173,7 +2196,7 @@ let elab_fundef env spec name defs body loc = emit_elab ~debuginfo:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) - let body1 = !elab_funbody_f ty_ret env3 body in + let body1 = !elab_funbody_f ty_ret vararg env3 body in (* Special treatment of the "main" function *) let body2 = if s = "main" then begin @@ -2224,7 +2247,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) (* "int x = 12, y[10], *z" *) | DECDEF(init_name_group, loc) -> let ((dl, env1), sto, tydef) = - elab_init_name_group loc env init_name_group in + elab_init_name_group false loc env init_name_group in if tydef then let env2 = enter_typedefs loc env1 sto dl in ([], env2) @@ -2245,9 +2268,9 @@ and elab_definitions local env = function (* Extended asm *) -let elab_asm_operand loc env (ASMOPERAND(label, wide, chars, e)) = +let elab_asm_operand vararg loc env (ASMOPERAND(label, wide, chars, e)) = let s = elab_simple_string loc wide chars in - let e',env = elab_expr loc env e in + let e',env = elab_expr vararg loc env e in (label, s, e'),env @@ -2259,7 +2282,8 @@ type stmt_context = { ctx_return_typ: typ; (**r return type for the function *) ctx_labels: StringSet.t; (**r all labels defined in the function *) ctx_break: bool; (**r is 'break' allowed? *) - ctx_continue: bool (**r is 'continue' allowed? *) + ctx_continue: bool; (**r is 'continue' allowed? *) + ctx_vararg: bool; (**r is this a vararg function? *) } let stmt_labels stmt = @@ -2296,7 +2320,7 @@ let rec elab_stmt env ctx s = (* 6.8.3 Expression statements *) | COMPUTATION(a, loc) -> - let a,env = (elab_expr loc env a) in + let a,env = (elab_expr ctx.ctx_vararg loc env a) in { sdesc = Sdo a; sloc = elab_loc loc },env (* 6.8.1 Labeled statements *) @@ -2306,7 +2330,7 @@ let rec elab_stmt env ctx s = { sdesc = Slabeled(Slabel lbl, s1); sloc = elab_loc loc },env | CASE(a, s1, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in begin match Ceval.integer_expr env a' with | None -> error loc "expression is not an integer constant expression" @@ -2327,7 +2351,7 @@ let rec elab_stmt env ctx s = (* 6.8.4 Conditional statements *) | If(a, s1, s2, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then error loc "statement requires expression of scalar type (%a invalid)" (print_typ env) a'.etyp; @@ -2342,7 +2366,7 @@ let rec elab_stmt env ctx s = (* 6.8.5 Iterative statements *) | WHILE(a, s1, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then error loc "statement requires expression of scalar type (%a invalid)" (print_typ env) a'.etyp; @@ -2351,7 +2375,7 @@ let rec elab_stmt env ctx s = | DOWHILE(a, s1, loc) -> let s1',env = elab_stmt env (ctx_loop ctx) s1 in - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_scalar_type env a'.etyp) then error loc "statement requires expression of scalar type (%a invalid)" (print_typ env) a'.etyp; @@ -2361,10 +2385,10 @@ let rec elab_stmt env ctx s = let (a1', env', decls') = match fc with | Some (FC_EXP a1) -> - let a1,env = elab_for_expr loc env (Some a1) in + let a1,env = elab_for_expr ctx.ctx_vararg loc env (Some a1) in (a1, env, None) | None -> - let a1,env = elab_for_expr loc env None in + let a1,env = elab_for_expr ctx.ctx_vararg loc env None in (a1, env, None) | Some (FC_DECL def) -> let (dcl, env') = elab_definition true (Env.new_scope env) def in @@ -2374,11 +2398,11 @@ let rec elab_stmt env ctx s = let a2',env = match a2 with | None -> intconst 1L IInt,env - | Some a2 -> elab_expr loc env' a2 + | Some a2 -> elab_expr ctx.ctx_vararg loc env' a2 in if not (is_scalar_type env' a2'.etyp) then error loc "statement requires expression of scalar type (%a invalid)" (print_typ env) a2'.etyp; - let a3',env' = elab_for_expr loc env' a3 in + let a3',env' = elab_for_expr ctx.ctx_vararg loc env' a3 in let s1',env' = elab_stmt env' (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in begin match decls' with @@ -2388,7 +2412,7 @@ let rec elab_stmt env ctx s = (* 6.8.4 Switch statement *) | SWITCH(a, s1, loc) -> - let a',env = elab_expr loc env a in + let a',env = elab_expr ctx.ctx_vararg loc env a in if not (is_integer_type env a'.etyp) then error loc "statement requires expression of integer type (%a invalid)" (print_typ env) a'.etyp; @@ -2407,7 +2431,7 @@ let rec elab_stmt env ctx s = (* 6.8.6 Return statements *) | RETURN(a, loc) -> - let a',env = elab_opt_expr loc env a in + let a',env = elab_opt_expr ctx.ctx_vararg loc env a in begin match (unroll env ctx.ctx_return_typ, a') with | TVoid _, None -> () | TVoid _, Some _ -> @@ -2450,8 +2474,8 @@ let rec elab_stmt env ctx s = | ASM(cv_specs, wide, chars, outputs, inputs, flags, loc) -> let a = elab_cvspecs env cv_specs in let s = elab_simple_string loc wide chars in - let outputs,env = mmap (elab_asm_operand loc) env outputs in - let inputs ,env= mmap (elab_asm_operand loc) env inputs in + let outputs,env = mmap (elab_asm_operand ctx.ctx_vararg loc) env outputs in + let inputs ,env= mmap (elab_asm_operand ctx.ctx_vararg loc) env inputs in let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in { sdesc = Sasm(a, s, outputs, inputs, flags); sloc = elab_loc loc },env @@ -2484,12 +2508,13 @@ and elab_block_body env ctx sl = (* Elaboration of a function body. Return the corresponding C statement. *) -let elab_funbody return_typ env b = +let elab_funbody return_typ vararg env b = let ctx = { ctx_return_typ = return_typ; ctx_labels = stmt_labels b; ctx_break = false; - ctx_continue = false } in + ctx_continue = false; + ctx_vararg = vararg;} in fst(elab_stmt env ctx b) (* Filling in forward declaration *) diff --git a/cparser/Env.ml b/cparser/Env.ml index cbfafd48..b2a4e21c 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -251,6 +251,9 @@ let add_enum env id info = { env with env_enum = IdentMap.add id info env.env_enum } info.ei_members +let add_types env_old env_new = + { env_new with env_ident = env_old.env_ident;env_scope = env_old.env_scope;} + (* Error reporting *) open Printf diff --git a/cparser/Env.mli b/cparser/Env.mli index b650f0f8..a794d4a4 100644 --- a/cparser/Env.mli +++ b/cparser/Env.mli @@ -76,3 +76,5 @@ val add_ident : t -> C.ident -> C.storage -> C.typ -> t val add_composite : t -> C.ident -> composite_info -> t val add_typedef : t -> C.ident -> typedef_info -> t val add_enum : t -> C.ident -> enum_info -> t + +val add_types : t -> t -> t 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/cparser/Parse.ml b/cparser/Parse.ml index ebe62621..507aea36 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -74,6 +74,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in + Cerrors.raise_on_errors (); Timing.time2 "Emulations" transform_program t p1 name with | Cerrors.Abort -> diff --git a/driver/Commandline.ml b/driver/Commandline.ml index c5c2b82c..ce5acf9d 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -16,6 +16,7 @@ (* Parsing of command-line flags and arguments *) open Printf +open Responsefile type pattern = | Exact of string @@ -103,4 +104,9 @@ let parse_array spec argv first last = in parse first let parse_cmdline spec = - parse_array spec Sys.argv 1 (Array.length Sys.argv - 1) + try + let argv = expandargv Sys.argv in + parse_array spec argv 1 (Array.length argv - 1) + with Responsefile.Error s -> + eprintf "%s" s; + exit 2 diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e1a02573..87e29e0f 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 @@ -171,3 +176,15 @@ let struct_return_style = | "int1-8" -> SR_int1to8 | "ref" -> SR_ref | v -> bad_config "struct_return_style" [v] + +type response_file_style = + | Gnu (* responsefiles in gnu compatible syntax *) + | Diab (* responsefiles in diab compatible syntax *) + | Unsupported (* responsefiles are not supported *) + +let response_file_style = + match get_config_string "response_file_style" with + | "unsupported" -> Unsupported + | "gnu" -> Gnu + | "diab" -> Diab + | v -> bad_config "response_file_style" [v] diff --git a/driver/Configuration.mli b/driver/Configuration.mli index dde9d6fd..197e8ad2 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 *) @@ -63,3 +66,11 @@ val struct_passing_style: struct_passing_style val struct_return_style: struct_return_style (** Calling conventions to use for returning structs and unions as first-class values *) + +type response_file_style = + | Gnu (* responsefiles in gnu compatible syntax *) + | Diab (* responsefiles in diab compatible syntax *) + | Unsupported (* responsefiles are not supported *) + +val response_file_style: response_file_style + (** Style of supported responsefiles *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 78baed47..8b0cd7ac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -333,13 +333,15 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -dltl Save LTL after register allocation in <file>.ltl\n\ \ -dmach Save generated Mach code in <file>.mach\n\ \ -dasm Save generated assembly in <file>.s\n\ +\ -dall Save all generated intermidate files in <file>.<ext>\n\ \ -sdump Save info for post-linking validation in <file>.json\n\ \ -doptions Save the compiler configurations in <file>.opt.json\n\ General options:\n\ \ -stdlib <dir> Set the path of the Compcert run-time library\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ -\ -version Print the version string and exit\n" ^ +\ -version Print the version string and exit\n\ +\ @<file> Read command line options from <file>\n" ^ Cerrors.warning_help ^ "Interpreter mode:\n\ \ -interp Execute given .c files using the reference interpreter\n\ @@ -442,6 +444,17 @@ let cmdline_actions = Exact "-dalloctrace", Set option_dalloctrace; Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; + Exact "-dall", Self (fun _ -> + option_dprepro := true; + option_dparse := true; + option_dcmedium := true; + option_dclight := true; + option_dcminor := true; + option_drtl := true; + option_dalloctrace := true; + option_dmach := true; + option_dasm := true; + dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); Exact "-doptions", Set dump_options; @@ -515,7 +528,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/driver/Driveraux.ml b/driver/Driveraux.ml index 3fe22fac..d25301d2 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -14,21 +14,20 @@ open Printf open Clflags +(* Is this a gnu based tool chain *) +let gnu_system = Configuration.system <> "diab" + +(* Safe removal of files *) +let safe_remove file = + try Sys.remove file with Sys_error _ -> () + (* Invocation of external tools *) let rec waitpid_no_intr pid = try Unix.waitpid [] pid with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid -let command ?stdout args = - if !option_v then begin - eprintf "+ %s" (String.concat " " args); - begin match stdout with - | None -> () - | Some f -> eprintf " > %s" f - end; - prerr_endline "" - end; +let command stdout args = let argv = Array.of_list args in assert (Array.length argv > 0); try @@ -51,12 +50,37 @@ let command ?stdout args = argv.(0) fn (Unix.error_message err) param; -1 +let command ?stdout args = + if !option_v then begin + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" + end; + let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in + if resp && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then + let quote,prefix = match Configuration.response_file_style with + | Configuration.Unsupported -> assert false + | Configuration.Gnu -> Responsefile.gnu_quote,"@" + | Configuration.Diab -> Responsefile.diab_quote,"-@" in + let file,oc = Filename.open_temp_file "compcert" "" in + let cmd,args = match args with + | cmd::args -> cmd,args + | [] -> assert false (* Should never happen *) in + List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args; + close_out oc; + let arg = prefix^file in + let ret = command stdout [cmd;arg] in + safe_remove file; + ret + else + command stdout args + let command_error n exc = eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc -let safe_remove file = - try Sys.remove file with Sys_error _ -> () - (* Determine names for output files. We use -o option if specified and if this is the final destination file (not a dump file). @@ -94,8 +118,6 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' -let gnu_system = Configuration.system <> "diab" - (* Command-line parsing *) let explode_comma_option s = match Str.split (Str.regexp ",") s with diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 60efcc80..e6bac6e3 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,7 +12,7 @@ (* *********************************************************************) -val command: ?stdout:string -> string list -> int +val command: ?stdout:string -> string list -> int (** Execute the command with the given arguments and an optional file for the stdout. Returns the exit code. *) diff --git a/driver/Interp.ml b/driver/Interp.ml index 5c2158ae..f42bed32 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -387,10 +387,12 @@ let do_external_function id sg ge w args m = match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> - print_string (do_printf m fmt args'); + let fmt' = do_printf m fmt args' in + let len = coqint_of_camlint (Int32.of_int (String.length fmt')) in + print_string fmt'; flush stdout; convert_external_args ge args sg.sig_args >>= fun eargs -> - Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) + Some(((w, [Event_syscall(id, eargs, EVint len)]), Vint len), m) | _ -> None diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index bdbf8be9..f272c3ed 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/lib/Responsefile.mli b/lib/Responsefile.mli new file mode 100644 index 00000000..ada5a15d --- /dev/null +++ b/lib/Responsefile.mli @@ -0,0 +1,31 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + + +val expandargv: string array -> string array + (** Expand responsefile arguments contained in the array and return the full + set of arguments. *) + +exception Error of string + (** Raised by [expandargv] in case of an error *) + +val gnu_quote : string -> string + (** [gnu_quote arg] returns [arg] quoted compatible with the gnu tool chain + quoting conventions. *) + +val diab_quote : string -> string + (** [diab_quote arg] returns [arg] quoted compatible with the diab tool chain + quoting conventions. *) diff --git a/lib/Responsefile.mll b/lib/Responsefile.mll new file mode 100644 index 00000000..35a2dbdb --- /dev/null +++ b/lib/Responsefile.mll @@ -0,0 +1,120 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + + +{ +(* To accumulate the characters in a word or quoted string *) +let buf = Buffer.create 32 + +(* Add the current contents of buf to the list of words seen so far, + taking care not to add empty strings unless warranted (e.g. quoted) *) +let stash inword words = + if inword then begin + let w = Buffer.contents buf in + Buffer.clear buf; + w :: words + end else + words + +} + +let whitespace = [' ' '\t' '\012' '\r' '\n'] + +let backslashes_even = "\\\\"* (* an even number of backslashes *) +let backslashes_odd = "\\\\"* '\\' (* an odd number of backslashes *) + +(* GNU-style quoting *) +(* "Options in file are separated by whitespace. A whitespace + character may be included in an option by surrounding the entire + option in either single or double quotes. Any character (including + a backslash) may be included by prefixing the character to be + included with a backslash. The file may itself contain additional + @file options; any such options will be processed recursively." *) + +rule gnu_unquoted inword words = parse + | eof { List.rev (stash inword words) } + | whitespace+ { gnu_unquoted false (stash inword words) lexbuf } + | '\'' { gnu_single_quote lexbuf; gnu_unquoted true words lexbuf } + | '\"' { gnu_double_quote lexbuf; gnu_unquoted true words lexbuf } + | "" { gnu_one_char lexbuf; gnu_unquoted true words lexbuf } + +and gnu_one_char = parse + | '\\' (_ as c) { Buffer.add_char buf c } + | _ as c { Buffer.add_char buf c } + +and gnu_single_quote = parse + | eof { () (* tolerance *) } + | '\'' { () } + | "" { gnu_one_char lexbuf; gnu_single_quote lexbuf } + +and gnu_double_quote = parse + | eof { () (* tolerance *) } + | '\"' { () } + | "" { gnu_one_char lexbuf; gnu_double_quote lexbuf } + +{ + +let re_responsefile = Str.regexp "@\\(.*\\)$" + +exception Error of string + +let expandargv argv = + let rec expand_arg seen arg k = + if not (Str.string_match re_responsefile arg 0) then + arg :: k + else begin + let filename = Str.matched_group 1 arg in + if List.mem filename seen then + raise (Error ("cycle in response files: " ^ filename)); + let ic = open_in filename in + let words = gnu_unquoted false [] (Lexing.from_channel ic) in + close_in ic; + expand_args (filename :: seen) words k + end + and expand_args seen args k = + match args with + | [] -> k + | a1 :: al -> expand_args seen al (expand_arg seen a1 k) + in + let args = Array.to_list argv in + Array.of_list (List.rev (expand_args [] args [])) + +(* This function reimplements quoting of writeargv from libiberty *) +let gnu_quote arg = + let len = String.length arg in + let buf = Buffer.create len in + String.iter (fun c -> begin match c with + | ' ' | '\t' | '\r' | '\n' | '\\' | '\'' | '"' -> + Buffer.add_char buf '\\' + | _ -> () end; + Buffer.add_char buf c) arg; + Buffer.contents buf + +let re_quote = Str.regexp ".*[ \t\n\r\"]" + +let diab_quote arg = + let buf = Buffer.create ((String.length arg) + 8) in + let doublequote = Str.string_match re_quote arg 0 in + if doublequote then begin + Buffer.add_char buf '"'; + String.iter (fun c -> + if c = '"' then Buffer.add_char buf '\\'; + Buffer.add_char buf c) arg; + if doublequote then Buffer.add_char buf '"'; + Buffer.contents buf + end else + arg +} 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 |