diff options
75 files changed, 1871 insertions, 1127 deletions
@@ -202,6 +202,7 @@ compcert.ini: Makefile.config echo "arch=$(ARCH)"; \ echo "model=$(MODEL)"; \ echo "abi=$(ABI)"; \ + echo "endianness=$(ENDIANNESS)"; \ echo "system=$(SYSTEM)"; \ echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \ diff --git a/arm/Archi.v b/arm/Archi.v index 6b282022..fedc55f5 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -20,7 +20,7 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. -Definition big_endian := false. +Parameter big_endian: bool. Notation align_int64 := 8%Z (only parsing). Notation align_float64 := 8%Z (only parsing). @@ -45,8 +45,7 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := false. -Global Opaque big_endian - default_pl_64 choose_binop_pl_64 +Global Opaque default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 855ca9ad..43c26f58 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -185,13 +185,14 @@ let expand_builtin_vload_common chunk base ofs res = | Mint32, BR(IR res) -> emit (Pldr (res, base, SOimm ofs)) | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> - let ofs' = Int.add ofs _4 in + let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in + let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in if base <> res2 then begin - emit (Pldr (res2, base, SOimm ofs)); - emit (Pldr (res1, base, SOimm ofs')) + emit (Pldr (res2, base, SOimm ofs_lo)); + emit (Pldr (res1, base, SOimm ofs_hi)) end else begin - emit (Pldr (res1, base, SOimm ofs')); - emit (Pldr (res2, base, SOimm ofs)) + emit (Pldr (res1, base, SOimm ofs_hi)); + emit (Pldr (res2, base, SOimm ofs_lo)) end | Mfloat32, BR(FR res) -> emit (Pflds (res, base, ofs)) @@ -226,9 +227,10 @@ let expand_builtin_vstore_common chunk base ofs src = | Mint32, BA(IR src) -> emit (Pstr (src, base, SOimm ofs)) | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) -> - let ofs' = Int.add ofs _4 in - emit (Pstr (src2, base, SOimm ofs)); - emit (Pstr (src1, base, SOimm ofs')) + let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in + let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in + emit (Pstr (src2, base, SOimm ofs_lo)); + emit (Pstr (src1, base, SOimm ofs_hi)) | Mfloat32, BA(FR src) -> emit (Pfsts (src, base, ofs)) | Mfloat64, BA(FR src) -> diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 3eae50ef..888861a5 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -85,15 +85,21 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) For the "softfloat" convention, results of FP types should be passed in [R0] or [R0,R1]. This doesn't fit the CompCert register model, - so we have code in [arm/PrintAsm.ml] that inserts additional moves - to/from [F0]. *) + so we have code in [arm/TargetPrinter.ml] that inserts additional moves + to/from [F0]. + + Concerning endianness for 64bit values in register pairs, the contents + of the registers is as if the value had been loaded from memory + representation with a single LDM instruction. *) Definition loc_result (s: signature) : rpair mreg := match s.(sig_res) with | None => One R0 | Some (Tint | Tany32) => One R0 | Some (Tfloat | Tsingle | Tany64) => One F0 - | Some Tlong => Twolong R1 R0 + | Some Tlong => if Archi.big_endian + then Twolong R0 R1 + else Twolong R1 R0 end. (** The result registers have types compatible with that given in the signature. *) @@ -102,7 +108,7 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto. + intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto. Qed. (** The result locations are caller-save registers *) @@ -112,7 +118,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. + unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -124,7 +130,9 @@ Lemma loc_result_pair: | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence. + intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. + intuition congruence. + intuition congruence. Qed. (** ** Location of function arguments *) @@ -176,11 +184,13 @@ Fixpoint loc_arguments_hf then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs else One (S Outgoing ofs Tsingle) :: loc_arguments_hf tys ir fr (ofs + 1) | Tlong :: tys => + let ohi := if Archi.big_endian then 0 else 1 in + let olo := if Archi.big_endian then 1 else 0 in let ir := align ir 2 in if zlt ir 4 - then Twolong (R (ireg_param (ir + 1))) (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 2) fr ofs + then Twolong (R (ireg_param (ir + ohi))) (R (ireg_param (ir + olo))) :: loc_arguments_hf tys (ir + 2) fr ofs else let ofs := align ofs 2 in - Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: loc_arguments_hf tys ir fr (ofs + 2) + Twolong (S Outgoing (ofs + ohi) Tint) (S Outgoing (ofs + olo) Tint) :: loc_arguments_hf tys ir fr (ofs + 2) end. (** For the "softfloat" configuration, as well as for variable-argument functions @@ -218,9 +228,11 @@ Fixpoint loc_arguments_sf One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle) :: loc_arguments_sf tys (ofs + 1) | Tlong :: tys => + let ohi := if Archi.big_endian then 0 else 1 in + let olo := if Archi.big_endian then 1 else 0 in let ofs := align ofs 2 in - Twolong (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint) - (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint) + Twolong (if zlt ofs 0 then R (ireg_param (ofs+ohi+4)) else S Outgoing (ofs+ohi) Tint) + (if zlt ofs 0 then R (ireg_param (ofs+olo+4)) else S Outgoing (ofs+olo) Tint) :: loc_arguments_sf tys (ofs + 2) end. @@ -341,9 +353,9 @@ Proof. set (ir' := align ir 2) in *. assert (ofs <= align ofs 2) by (apply align_le; omega). destruct (zlt ir' 4). - destruct H. subst p. split; apply ireg_param_caller_save. + destruct H. subst p. split; apply ireg_param_caller_save. eapply IHtyl; eauto. - destruct H. subst p. split; (split; [ omega | auto ]). + destruct H. subst p. split; destruct Archi.big_endian; (split; [ omega | auto ]). eapply Y. eapply IHtyl; eauto. omega. - (* single *) destruct (zlt fr 8); destruct H. @@ -396,7 +408,7 @@ Proof. destruct H. destruct (zlt ofs' 0); subst p. split; apply ireg_param_caller_save. - split; (split; [xomega|auto]). + split; destruct Archi.big_endian; (split; [xomega|auto]). eapply Y. eapply IHtyl; eauto. omega. - (* single *) destruct H. @@ -513,6 +525,12 @@ Proof. - (* long *) destruct (zlt (align ir 2) 4). destruct H. discriminate. destruct H. discriminate. eauto. + destruct Archi.big_endian. + destruct H. inv H. + eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + destruct H. inv H. + rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + eauto. destruct H. inv H. rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. destruct H. inv H. @@ -556,9 +574,15 @@ Proof. eauto. - (* long *) destruct H. + destruct Archi.big_endian. + destruct (zlt (align ofs0 2) 0); inv H. + eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. destruct (zlt (align ofs0 2) 0); inv H. rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. destruct H. + destruct Archi.big_endian. + destruct (zlt (align ofs0 2) 0); inv H. + rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. destruct (zlt (align ofs0 2) 0); inv H. eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. eauto. diff --git a/arm/Machregs.v b/arm/Machregs.v index b43f9be6..e97df790 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -58,7 +58,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -161,6 +161,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg := nil. Definition destroyed_at_function_entry: list mreg := R12 :: nil. +Definition destroyed_at_indirect_call: list mreg := + R0 :: R1 :: R2 :: R3 :: nil. + Definition temp_for_parent_frame: mreg := R12. @@ -177,6 +180,7 @@ Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame + destroyed_at_indirect_call mregs_for_operation mregs_for_builtin. (** Two-address operations. Return [true] if the first argument and diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 71e1dfc3..642fff80 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -120,6 +120,7 @@ let print_operation reg pp = function | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 + | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1 | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index d2ea16f7..6d194369 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' -> @@ -378,7 +382,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | (fr, Single, sr) :: act -> let n = fixup_incoming oc act in - if fr = sr then n else begin + if (2*fr) = sr then n else begin fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; 1 + n end @@ -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/RTLgen.v b/backend/RTLgen.v index 49d79fb2..11da630b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -23,7 +23,7 @@ Require Import Registers. Require Import CminorSel. Require Import RTL. -Open Local Scope string_scope. +Local Open Scope string_scope. (** * Translation environments and state *) @@ -112,16 +112,13 @@ Implicit Arguments Error [A s]. Definition mon (A: Type) : Type := forall (s: state), res A s. -Definition ret (A: Type) (x: A) : mon A := +Definition ret {A: Type} (x: A) : mon A := fun (s: state) => OK x s (state_incr_refl s). -Implicit Arguments ret [A]. -Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. +Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. -Implicit Arguments error [A]. - -Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := +Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := fun (s: state) => match f s with | Error msg => Error msg @@ -132,27 +129,21 @@ Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C := +Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := bind f (fun xy => g (fst xy) (snd xy)). -Implicit Arguments bind2 [A B C]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (at level 200, X ident, Y ident, A at level 100, B at level 200). -Definition handle_error (A: Type) (f g: mon A) : mon A := +Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s: state) => match f s with | OK a s' i => OK a s' i | Error _ => g s end. -Implicit Arguments handle_error [A]. - (** ** Operations on state *) (** The initial state (empty CFG). *) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index e6e07339..b91bad27 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -657,9 +657,12 @@ let add_interfs_instr g instr live = | Xstore(chunk, addr, args, src) -> add_interfs_destroyed g live (destroyed_by_store chunk addr) | Xcall(sg, vos, args, res) -> + begin match vos with + | Coq_inl v -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) destroyed_at_indirect_call + | _ -> () end; add_interfs_destroyed g (vset_removelist res live) destroyed_at_call | Xtailcall(sg, Coq_inl v, args) -> - List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs + List.iter (fun r -> IRC.add_interf g (vmreg r) v) (int_callee_save_regs @ destroyed_at_indirect_call) | Xtailcall(sg, Coq_inr id, args) -> () | Xbuiltin(ef, args, res) -> @@ -915,7 +918,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 decbf58b..d7b26322 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -115,13 +115,13 @@ let currentLocation = ref Cutil.no_loc let updateLoc l = currentLocation := l let error msg = - Cerrors.error "%aError: %s" Cutil.formatloc !currentLocation msg + Cerrors.error !currentLocation "%s" msg let unsupported msg = - Cerrors.error "%aUnsupported feature: %s" Cutil.formatloc !currentLocation msg + Cerrors.error !currentLocation "unsupported feature: %s" msg -let warning msg = - Cerrors.warning "%aWarning: %s" Cutil.formatloc !currentLocation msg +let warning t msg = + Cerrors.warning !currentLocation t msg let string_of_errmsg msg = let string_of_err = function @@ -357,11 +357,11 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in + | _ -> error "argument 3 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in + | _ -> error "argument 4 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), @@ -587,15 +587,15 @@ let z_of_str hex str fst = !res -let checkFloatOverflow f = +let checkFloatOverflow f typ = match f with | Fappli_IEEE.B754_finite _ -> () | Fappli_IEEE.B754_zero _ -> - warning "Floating-point literal is so small that it converts to 0" + warning Cerrors.Literal_range "magnitude of floating-point constant too small for type '%s'" typ | Fappli_IEEE.B754_infinity _ -> - warning "Floating-point literal is so large that it converts to infinity" + warning Cerrors.Literal_range "magnitude of floating-point constant too large for type '%s'" typ | Fappli_IEEE.B754_nan _ -> - warning "Floating-point literal converts to Not-a-Number" + warning Cerrors.Literal_range "floating-point converts converts to 'NaN'" let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in @@ -621,11 +621,11 @@ let convertFloat f kind = begin match kind with | FFloat -> let f = Float32.from_parsed base mant exp in - checkFloatOverflow f; + checkFloatOverflow f "float"; Ctyping.econst_single f | FDouble | FLongDouble -> let f = Float.from_parsed base mant exp in - checkFloatOverflow f; + checkFloatOverflow f "double"; Ctyping.econst_float f end @@ -655,7 +655,7 @@ let rec convertExpr env e = else Ctyping.econst_int (convertInt i) sg | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then - unsupported "'long double' floating-point literal"; + unsupported "'long double' floating-point constant"; convertFloat f k | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in @@ -717,8 +717,7 @@ let rec convertExpr env e = let e2' = convertExpr env e2 in if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then - warning "assignment to a l-value of volatile composite type. \ - The 'volatile' qualifier is ignored."; + warning Cerrors.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored"; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| @@ -759,12 +758,12 @@ let rec convertExpr env e = let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) - | _ -> error "ill_formed __builtin_debug"; (0L, args) in + | _ -> error "argument 1 of '__builtin_debug' must be a constant"; (1L, args) in let (text, args2) = match args1 with | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) | {edesc = C.EVar id} :: args2 -> (id.name, args2) - | _ -> error "ill_formed __builtin_debug"; ("", args1) in + | _ -> error "argument 2 of '__builtin_debug' must be either a string literal or a variable"; ("", args1) in let targs2 = convertTypArgs env [] args2 in Ebuiltin( EF_debug(P.of_int64 kind, intern_string text, @@ -779,7 +778,7 @@ let rec convertExpr env e = EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> - error "ill-formed __builtin_annot (first argument must be string literal)"; + error "argument 1 of '__builtin_annot' must be a string literal"; ezero end @@ -792,7 +791,7 @@ let rec convertExpr env e = Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> - error "ill-formed __builtin_annot_intval (first argument must be string literal)"; + error "argument 1 of '__builtin_annot_intval' must be a string literal"; ezero end @@ -839,9 +838,9 @@ let rec convertExpr env e = | Some(tres, targs, va) -> checkFunctionType env tres targs; if targs = None && not !Clflags.option_funprototyped then - unsupported "call to unprototyped function (consider adding option -funprototyped)"; + unsupported "call to unprototyped function (consider adding option [-funprototyped])"; if va && not !Clflags.option_fvararg_calls then - unsupported "call to variable-argument function (consider adding option -fvararg-calls)" + unsupported "call to variable-argument function (consider adding option [-fvararg-calls])" end; ewrap (Ctyping.ecall (convertExpr env fn) (convertExprList env args)) @@ -863,7 +862,7 @@ and convertLvalue env e = let e3' = ewrap (Ctyping.ebinop Oadd e1' e2') in ewrap (Ctyping.ederef e3') | _ -> - error "illegal l-value"; ezero + error "illegal lvalue"; ezero and convertExprList env el = match el with @@ -945,7 +944,7 @@ let rec contains_case s = | C.Sdowhile (s1,_) -> contains_case s1 | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 | C.Slabeled(C.Scase _, _) -> - unsupported "'case' outside of 'switch'" + unsupported "'case' statement not in 'switch' statement" | C.Slabeled(_,s) -> contains_case s | C.Sblock b -> List.iter contains_case b @@ -996,7 +995,7 @@ let rec convertStmt env s = | _ -> Cutil.is_debug_stmt s in if init.sdesc <> C.Sskip && not (init_debug init) then begin - warning "ignored code at beginning of 'switch'"; + warning Cerrors.Unnamed "ignored code at beginning of 'switch'"; contains_case init end; let te = convertExpr env e in @@ -1005,9 +1004,9 @@ let rec convertStmt env s = | C.Slabeled(C.Slabel lbl, s1) -> Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> - unsupported "'case' outside of 'switch'"; Sskip + unsupported "'case' statement not in 'switch' statement"; Sskip | C.Slabeled(C.Sdefault, _) -> - unsupported "'default' outside of 'switch'"; Sskip + unsupported "'default' statement not in 'switch' statement"; Sskip | C.Sgoto lbl -> Sgoto(intern_string lbl) | C.Sreturn None -> @@ -1020,7 +1019,7 @@ let rec convertStmt env s = unsupported "inner declarations"; Sskip | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then - unsupported "inline 'asm' statement (consider adding option -finline-asm)"; + unsupported "inline 'asm' statement (consider adding option [-finline-asm])"; Sdo (convertAsm s.sloc env txt outputs inputs clobber) and convertSwitch env is_64 = function @@ -1034,7 +1033,7 @@ and convertSwitch env is_64 = function None | Case e -> match Ceval.integer_expr env e with - | None -> unsupported "'case' label is not a compile-time integer"; + | None -> unsupported "expression is not an integer constant expression"; None | Some v -> Some (if is_64 then Z.of_uint64 v @@ -1047,7 +1046,7 @@ and convertSwitch env is_64 = function let convertFundef loc env fd = checkFunctionType env fd.fd_ret (Some fd.fd_params); if fd.fd_vararg && not !Clflags.option_fvararg_calls then - unsupported "variable-argument function (consider adding option -fvararg-calls)"; + unsupported "variable-argument function (consider adding option [-fvararg-calls])"; let ret = convertTyp env fd.fd_ret in let params = @@ -1132,7 +1131,7 @@ let convertInitializer env ty i = with | Errors.OK init -> init | Errors.Error msg -> - error (sprintf "Initializer is not a compile-time constant (%s)" + error (sprintf "initializer element is not a compile-time constant (%s)" (string_of_errmsg msg)); [] (** Global variable *) @@ -1185,7 +1184,7 @@ let rec convertGlobdecls env res gl = begin match Cutil.unroll env ty with | TFun(tres, targs, va, a) -> if targs = None then - warning ("'" ^ id.name ^ "' is declared without a function prototype"); + warning Cerrors.Unnamed "'%s' is declared without a function prototype" id.name; convertGlobdecls env (convertFundecl env d :: res) gl' | _ -> convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl' @@ -1199,7 +1198,7 @@ let rec convertGlobdecls env res gl = convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then - warning ("'#pragma " ^ s ^ "' directive ignored"); + warning Cerrors.Unknown_pragmas "unknown pragma ignored"; convertGlobdecls env res gl' (** Convert struct and union declarations. @@ -1308,7 +1307,7 @@ let convertProgram p = let typs = convertCompositedefs env [] p in match build_composite_env typs with | Errors.Error msg -> - error (sprintf "Incorrect struct or union definition: %s" + error (sprintf "incorrect struct or union definition: %s" (string_of_errmsg msg)); None | Errors.OK ce -> diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 0c932170..2a199ff8 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -73,7 +73,7 @@ let process_pragma name = | "section" :: _ -> C2C.error "ill-formed `section' pragma"; true | "use_section" :: classname :: identlist -> - if identlist = [] then C2C.warning "vacuous `use_section' pragma"; + if identlist = [] then C2C.warning Cerrors.Unnamed "empty `use_section' pragma"; List.iter (process_use_section_pragma classname) identlist; true | "use_section" :: _ -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b9deb204..a2bfa6e1 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -15,6 +15,7 @@ Require Import String. Require Import Axioms. Require Import Classical. +Require Import Decidableplus. Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -473,39 +474,11 @@ Definition memcpy_args_ok /\ (sz > 0 -> (al | odst)) /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc). -Remark memcpy_check_args: - forall sz al bdst odst bsrc osrc, - {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}. -Proof with try (right; intuition omega). - intros. - assert (X: {al = 1 \/ al = 2 \/ al = 4 \/ al = 8} + {~(al = 1 \/ al = 2 \/ al = 4 \/ al = 8)}). - destruct (zeq al 1); auto. destruct (zeq al 2); auto. - destruct (zeq al 4); auto. destruct (zeq al 8); auto... - unfold memcpy_args_ok. destruct X... - assert (al > 0) by (intuition omega). - destruct (zle 0 sz)... - destruct (Zdivide_dec al sz); auto... - assert(U: forall x, {sz > 0 -> (al | x)} + {~(sz > 0 -> (al | x))}). - intros. destruct (zeq sz 0). - left; intros; omegaContradiction. - destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega. - destruct (U osrc); auto... - destruct (U odst); auto... - assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc} - +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}). - destruct (eq_block bsrc bdst); auto. - destruct (zeq osrc odst); auto. - destruct (zle (osrc + sz) odst); auto. - destruct (zle (odst + sz) osrc); auto. - right; intuition omega. - destruct Y... left; intuition omega. -Defined. - Definition do_ef_memcpy (sz al: Z) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | Vptr bdst odst :: Vptr bsrc osrc :: nil => - if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then + if decide (memcpy_args_ok sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc)) then do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz; do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes; Some(w, E0, Vundef, m') @@ -581,7 +554,7 @@ Proof with try congruence. split. econstructor; eauto. omega. constructor. (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... - destruct v... destruct vargs... mydestr. red in m0. + destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1. split. econstructor; eauto; tauto. constructor. (* EF_annot *) unfold do_ef_annot. mydestr. @@ -623,7 +596,7 @@ Proof. inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega. (* EF_memcpy *) inv H; unfold do_ef_memcpy. - inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto. + inv H0. rewrite Decidable_complete, H7, H8. auto. red. tauto. (* EF_annot *) inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. 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/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index bfdd8ab9..71b67f67 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -25,7 +25,7 @@ Require Import Cop. Require Import Csyntax. Require Import Clight. -Open Local Scope string_scope. +Local Open Scope string_scope. (** State and error monad for generating fresh identifiers. *) @@ -43,17 +43,13 @@ Implicit Arguments Res [A g]. Definition mon (A: Type) := forall (g: generator), result A g. -Definition ret (A: Type) (x: A) : mon A := +Definition ret {A: Type} (x: A) : mon A := fun g => Res x g (Ple_refl (gen_next g)). -Implicit Arguments ret [A]. - -Definition error (A: Type) (msg: Errors.errmsg) : mon A := +Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun g => Err msg. -Implicit Arguments error [A]. - -Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B := +Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B := fun g => match x g with | Err msg => Err msg @@ -64,13 +60,9 @@ Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (x: mon (A * B)) (f: A -> B -> mon C) : mon C := +Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C := bind x (fun p => f (fst p) (snd p)). -Implicit Arguments bind2 [A B C]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200) : gensym_monad_scope. 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='' @@ -25,44 +25,56 @@ 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) @@ -84,180 +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 @@ -266,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' @@ -354,8 +435,10 @@ if $missingtools; then exit 2 fi -# Generate Makefile.config +# +# Generate Makefile.config +# sharedir="$(dirname "$bindir")"/share rm -f Makefile.config @@ -369,25 +452,26 @@ EOF if test "$target" != "manual"; then cat >> Makefile.config <<EOF -ARCH=$arch -MODEL=$model ABI=$abi -STRUCT_PASSING=$struct_passing -STRUCT_RETURN=$struct_return -SYSTEM=$system -CC=$cc -CPREPRO=$cprepro -CPREPRO_OPTIONS=$cprepro_options +ARCH=$arch +ASM_SUPPORTS_CFI=$asm_supports_cfi CASM=$casm CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime +CC=$cc +CLIGHTGEN=$clightgen CLINKER=$clinker CLINKER_OPTIONS=$clinker_options -LIBMATH=$libmath +CPREPRO=$cprepro +CPREPRO_OPTIONS=$cprepro_options +ENDIANNESS=$endianness HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers -ASM_SUPPORTS_CFI=$asm_supports_cfi -CLIGHTGEN=$clightgen +LIBMATH=$libmath +MODEL=$model +STRUCT_PASSING=$struct_passing +STRUCT_RETURN=$struct_return +SYSTEM=$system RESPONSEFILE=$responsefile EOF else @@ -400,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 @@ -456,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 @@ -476,18 +570,18 @@ CLIGHTGEN=false 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|"` @@ -499,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 @@ -518,5 +613,4 @@ CompCert configuration: If anything above looks wrong, please edit file ./Makefile.config to correct. EOF - fi diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index d55a6d36..9f38abc6 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -67,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n = else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members then true else begin - Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n; + Cerrors.warning Cutil.no_loc Cerrors.Unnamed "not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n; false end diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index a4d1a3f8..9ca04a62 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -16,8 +16,12 @@ (* Management of errors and warnings *) open Format +open Commandline -let warn_error = ref false +let error_fatal = ref false +let color_diagnostics = + let term = try Sys.getenv "TERM" with Not_found -> "" in + ref (Unix.isatty Unix.stderr && term <> "dumb" && term <>"") let num_errors = ref 0 let num_warnings = ref 0 @@ -38,35 +42,269 @@ let fatal_error_raw fmt = stderr (fmt ^^ "Fatal error; compilation aborted.\n%!") -let fatal_error fmt = +type msg_class = + | WarningMsg + | ErrorMsg + | FatalErrorMsg + | SuppressedMsg + +type warning_type = + | Unnamed + | Unknown_attribute + | Zero_length_array + | Celeven_extension + | Gnu_empty_struct + | Missing_declarations + | Constant_conversion + | Int_conversion + | Varargs + | Implicit_function_declaration + | Pointer_type_mismatch + | Compare_distinct_pointer_types + | Pedantic + | Main_return_type + | Invalid_noreturn + | Return_type + | Literal_range + | Unknown_pragmas + | CompCert_conformance + +let active_warnings: warning_type list ref = ref [ + Unnamed; + Unknown_attribute; + Celeven_extension; + Gnu_empty_struct; + Missing_declarations; + Constant_conversion; + Int_conversion; + Varargs; + Implicit_function_declaration; + Pointer_type_mismatch; + Compare_distinct_pointer_types; + Main_return_type; + Invalid_noreturn; + Return_type; + Literal_range; +] + +let error_warnings: warning_type list ref = ref [] + +let string_of_warning = function + | Unnamed -> "" + | Unknown_attribute -> "unknown-attributes" + | Zero_length_array -> "zero-length-array" + | Celeven_extension -> "c11-extensions" + | Gnu_empty_struct -> "gnu-empty-struct" + | Missing_declarations -> "missing-declarations" + | Constant_conversion -> "constant-conversion" + | Int_conversion -> "int-conversion" + | Varargs -> "varargs" + | Implicit_function_declaration -> "implicit-function-declaration" + | Pointer_type_mismatch -> "pointer-type-mismatch" + | Compare_distinct_pointer_types -> "compare-distinct-pointer-types" + | Pedantic -> "pedantic" + | Main_return_type -> "main-return-type" + | Invalid_noreturn -> "invalid-noreturn" + | Return_type -> "return-type" + | Literal_range -> "literal-range" + | Unknown_pragmas -> "unknown-pragmas" + | CompCert_conformance -> "compcert-conformance" + +let activate_warning w () = + if not (List.mem w !active_warnings) then + active_warnings:=w::!active_warnings + +let deactivate_warning w () = + active_warnings:=List.filter ((<>) w) !active_warnings; + error_warnings:= List.filter ((<>) w) !error_warnings + +let warning_as_error w ()= + activate_warning w (); + if not (List.mem w !error_warnings) then + error_warnings := w::!error_warnings + +let warning_not_as_error w () = + error_warnings:= List.filter ((<>) w) !error_warnings + +let wall () = + active_warnings:=[ + Unnamed; + Unknown_attribute; + Zero_length_array; + Celeven_extension; + Gnu_empty_struct; + Missing_declarations; + Constant_conversion; + Int_conversion; + Varargs; + Implicit_function_declaration; + Pointer_type_mismatch; + Compare_distinct_pointer_types; + Pedantic; + Main_return_type; + Invalid_noreturn; + Return_type; + Literal_range; + Unknown_pragmas; + ] + +let werror () = + error_warnings:=[ + Unnamed; + Unknown_attribute; + Zero_length_array; + Celeven_extension; + Gnu_empty_struct; + Missing_declarations; + Constant_conversion; + Int_conversion; + Varargs; + Implicit_function_declaration; + Pointer_type_mismatch; + Compare_distinct_pointer_types; + Pedantic; + Main_return_type; + Invalid_noreturn; + Return_type; + Literal_range; + Unknown_pragmas; + ] + + +let key_of_warning w = + match w with + | Unnamed -> None + | _ -> Some ("-W"^(string_of_warning w)) + +let key_add_werror = function + | None -> Some ("-Werror") + | Some s -> Some ("-Werror,"^s) + +let classify_warning w = + let key = key_of_warning w in + if List.mem w !active_warnings then + if List.mem w !error_warnings then + let key = key_add_werror key in + if !error_fatal then + FatalErrorMsg,key + else + ErrorMsg,key + else + WarningMsg,key + else + SuppressedMsg,None + +let cprintf fmt c = + if Unix.isatty Unix.stderr && !color_diagnostics then + fprintf fmt c + else + ifprintf fmt c + +let rsc fmt = + cprintf fmt "\x1b[0m" + +let bc fmt = + cprintf fmt "\x1b[1m" + +let rc fmt = + cprintf fmt "\x1b[31;1m" + +let mc fmt = + cprintf fmt "\x1b[35;1m" + +let pp_key key fmt = + let key = match key with + | None -> "" + | Some s -> " ["^s^"]" in + fprintf fmt "%s%t@." key rsc + +let pp_loc fmt (filename,lineno) = + if filename <> "" then + fprintf fmt "%t%s:%d:%t" bc filename lineno rsc + +let error key loc fmt = incr num_errors; - kfprintf - (fun _ -> raise Abort) - err_formatter - ("@[<hov 2>" ^^ fmt ^^ ".@]@.@[<hov 0>Fatal error; compilation aborted.@]@.") + kfprintf (pp_key key) + err_formatter ("%a %terror:%t %t" ^^ fmt) pp_loc loc rc rsc bc -let error fmt = +let fatal_error key loc fmt = incr num_errors; - eprintf ("@[<hov 2>" ^^ fmt ^^ ".@]@.") + kfprintf + (fun fmt -> pp_key key fmt;raise Abort) + err_formatter ("%a %terror:%t %t" ^^ fmt) pp_loc loc rc rsc bc -let warning fmt = - incr num_warnings; - eprintf ("@[<hov 2>" ^^ fmt ^^ ".@]@.") +let warning loc ty fmt = + let kind,key = classify_warning ty in + match kind with + | ErrorMsg -> + error key loc fmt + | FatalErrorMsg -> + fatal_error key loc fmt + | WarningMsg -> + incr num_warnings; + kfprintf (pp_key key) + err_formatter ("%a %twarning:%t %t" ^^ fmt) pp_loc loc mc rsc bc + | SuppressedMsg -> ifprintf err_formatter fmt -let info fmt = - eprintf ("@[<hov 2>" ^^ fmt ^^ ".@]@.") +let error loc fmt = + if !error_fatal then + fatal_error None loc fmt + else + error None loc fmt + +let fatal_error loc fmt = + fatal_error None loc fmt let check_errors () = if !num_errors > 0 then eprintf "@[<hov 0>%d error%s detected.@]@." !num_errors (if !num_errors = 1 then "" else "s"); - if !warn_error && !num_warnings > 0 then - eprintf "@[<hov 0>%d error-enabled warning%s detected.@]@." - !num_warnings - (if !num_warnings = 1 then "" else "s"); - !num_errors > 0 || (!warn_error && !num_warnings > 0) + !num_errors > 0 + +let error_option w = + let key = string_of_warning w in + [Exact ("-W"^key), Unit (activate_warning w); + Exact ("-Wno"^key), Unit (deactivate_warning w); + Exact ("-Werror="^key), Unit ( warning_as_error w); + Exact ("-Wno-error="^key), Unit ( warning_not_as_error w)] + +let warning_options = + error_option Unnamed @ + error_option Unknown_attribute @ + error_option Zero_length_array @ + error_option Celeven_extension @ + error_option Gnu_empty_struct @ + error_option Missing_declarations @ + error_option Constant_conversion @ + error_option Int_conversion @ + error_option Varargs @ + error_option Implicit_function_declaration @ + error_option Pointer_type_mismatch @ + error_option Compare_distinct_pointer_types @ + error_option Pedantic @ + error_option Main_return_type @ + error_option Invalid_noreturn @ + error_option Return_type @ + error_option Literal_range @ + error_option Unknown_pragmas @ + [Exact ("-Wfatal-errors"), Set error_fatal; + Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) + Exact ("-fno-diagnostics-color"), Unset color_diagnostics; + Exact ("-Werror"), Unit werror; + Exact ("-Wall"), Unit wall;] + +let warning_help = "Diagnostic options:\n\ +\ -W<warning> Enable the specific <warning>\n\ +\ -Wno-<warning> Disable the specific <warning>\n\ +\ -Werror Make all warnings into errors\n\ +\ -Werror=<warning> Turn <warning> into an error\n\ +\ -Wno-error=<warning> Turn <warning> into a warning even if -Werror is\n\ + specified\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 || (!warn_error && !num_warnings > 0) then + if !num_errors > 0 then raise Abort diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 313573c3..1ef8bb21 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -13,13 +13,61 @@ (* *) (* *********************************************************************) -val warn_error : bool ref +(* Printing of warnings and error messages *) + val reset : unit -> unit + (** Reset the error counters. *) + exception Abort -val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a -val fatal_error : ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a -val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -val info : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a + (** Exception raised upon fatal errors *) + val check_errors : unit -> bool + (** Check whether errors occured *) + +type warning_type = + | Unnamed (** warnings which cannot be turned off *) + | Unknown_attribute (** usage of unsupported/unknown attributes *) + | Zero_length_array (** gnu extension for zero lenght arrays *) + | Celeven_extension (** C11 fetatures *) + | Gnu_empty_struct (** gnu extension for empty struct *) + | Missing_declarations (** declation which do not declare anything *) + | Constant_conversion (** dangerous constant conversions *) + | Int_conversion (** pointer <-> int conversions *) + | Varargs (** promotable vararg argument *) + | Implicit_function_declaration (** deprecated implicit function declaration *) + | Pointer_type_mismatch (** pointer type mismatch in ?: operator *) + | Compare_distinct_pointer_types (** comparison between different pointer types *) + | Pedantic (** non C99 code *) + | Main_return_type (** wrong return type for main *) + | Invalid_noreturn (** noreturn function containing return *) + | Return_type (** void return in non-void function *) + | Literal_range (** literal ranges *) + | Unknown_pragmas (** unknown/unsupported pragma *) + | CompCert_conformance (** features that are not part of the CompCert C core language *) + +val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +(** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w] *) + +val error : (string * int) -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +(** [error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w]. *) + +val fatal_error : (string * int) -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a +(** [fatal_error (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as error according to + the format string [fmt] and outputs the result on [stderr] with additional file [f] and column [c] + and warning key for [w]. Additionally raises the excpetion [Abort] after printing the error message *) + +val fatal_error_raw : ('a, out_channel, unit, 'b) format4 -> 'a +(** [fatal_error_raw] is identical to fatal_error, except it uses [Printf] and does not automatically + introduce indentation *) + +val warning_help : string +(** Help string for all warning options *) + +val warning_options : (Commandline.pattern * Commandline.action) list +(** List of all options for diagnostics *) + val raise_on_errors : unit -> unit diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index e80a4c8e..2a110104 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -126,7 +126,7 @@ let name_of_fkind = function | FDouble -> "double" | FLongDouble -> "long double" -let rec dcl pp ty n = +let rec dcl ?(pp_indication=true) pp ty n = match ty with | TVoid a -> fprintf pp "void%a%t" attributes a n @@ -160,7 +160,8 @@ let rec dcl pp ty n = | [] -> n pp | _ -> fprintf pp " (%a%t)" attributes a n end; - fprintf pp "(@[<hov 0>"; + fprintf pp "("; + if pp_indication then fprintf pp "@[<hov 0>"; begin match args with | None -> () | Some [] -> if vararg then fprintf pp "..." else fprintf pp "void" @@ -169,7 +170,8 @@ let rec dcl pp ty n = List.iter (fun a -> fprintf pp ",@ "; param a) al; if vararg then fprintf pp ",@ ..." end; - fprintf pp "@])" in + if pp_indication then fprintf pp "@]"; + fprintf pp ")" in dcl pp tres n' | TNamed(id, a) -> fprintf pp "%a%a%t" ident id attributes a n @@ -183,6 +185,9 @@ let rec dcl pp ty n = let typ pp ty = dcl pp ty (fun _ -> ()) +let typ_raw pp ty = + dcl ~pp_indication:false pp ty (fun _ -> ()) + type associativity = LtoR | RtoL | NA let precedence = function (* H&S section 7.2 *) diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli index 349b5f9a..fe71e4fe 100644 --- a/cparser/Cprint.mli +++ b/cparser/Cprint.mli @@ -20,6 +20,7 @@ val print_debug_idents : bool ref val location : Format.formatter -> C.location -> unit val attributes : Format.formatter -> C.attributes -> unit val typ : Format.formatter -> C.typ -> unit +val typ_raw : Format.formatter -> C.typ -> unit val simple_decl : Format.formatter -> C.ident * C.typ -> unit val full_decl: Format.formatter -> C.decl -> unit val const : Format.formatter -> C.constant -> unit diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 4b4e1b81..19a32a7e 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -20,6 +20,11 @@ open C open Env open Machine + +(* Empty location *) + +let no_loc = ("", -1) + (* Set and Map structures over identifiers *) module Ident = struct @@ -478,7 +483,7 @@ let rec sizeof env t = | Some s -> match cautious_mul n s with | Some sz -> Some sz - | None -> error "sizeof(%a) overflows" Cprint.typ t'; Some 1 + | None -> error no_loc "sizeof(%a) overflows" Cprint.typ t'; Some 1 end | TFun(_, _, _, _) -> !config.sizeof_fun | TNamed(_, _) -> sizeof env (unroll env t) @@ -941,6 +946,14 @@ let valid_cast env tfrom tto = | TUnion(s1, _), TUnion(s2, _) -> s1 = s2 | _, _ -> false +(* Check that the cast from tfrom to tto is an integer to pointer conversion *) + +let int_pointer_conversion env tfrom tto = + match unroll env tfrom, unroll env tto with + | (TInt _ | TEnum _),(TPtr _) + | (TPtr _),(TInt _ | TEnum _) -> true + | _,_ -> false + (* Construct an integer constant *) let intconst v ik = @@ -1007,10 +1020,6 @@ let sseq loc s1 s2 = let sassign loc lv rv = { sdesc = Sdo (eassign lv rv); sloc = loc } -(* Empty location *) - -let no_loc = ("", -1) - (* Dummy skip statement *) let sskip = { sdesc = Sskip; sloc = no_loc } @@ -1026,6 +1035,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 @@ -1049,11 +1059,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 91b073ab..3f988f7c 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -198,6 +198,9 @@ val valid_assignment : Env.t -> exp -> typ -> bool the given type is allowed. *) val valid_cast : Env.t -> typ -> typ -> bool (* Check that a cast from the first type to the second is allowed. *) +val int_pointer_conversion : Env.t -> typ -> typ -> bool + (* Check that the cast from tfrom to tto is an integer to pointer + conversion *) val fundef_typ: fundef -> typ (* Return the function type for the given function definition. *) val int_representable: int64 -> int -> bool -> bool @@ -244,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 2b5b4591..9cdf6c29 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -22,6 +22,7 @@ open Machine open !Cabs open Cabshelper open !C +open Cerrors open Cutil open Env @@ -30,13 +31,19 @@ open Env (* Error reporting *) let fatal_error loc fmt = - Cerrors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + fatal_error (loc.filename,loc.lineno) fmt let error loc fmt = - Cerrors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + error (loc.filename,loc.lineno) fmt -let warning loc fmt = - Cerrors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc +let warning loc = + warning (loc.filename,loc.lineno) + +let print_typ env fmt ty = + match ty with + | TNamed _ -> + Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ_raw ty Cprint.typ_raw (Cutil.unroll env ty) + | _ -> Format.fprintf fmt "'%a'" Cprint.typ_raw ty (* Error reporting for Env functions *) @@ -115,12 +122,9 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Some new_ty -> new_ty | None -> - let id = Env.fresh_ident s in error loc - "redefinition of '%s' with incompatible type.@ \ - Previous declaration: %a.@ \ - New declaration: %a" - s Cprint.simple_decl (id, old_ty) Cprint.simple_decl (id, ty); + "redefinition of '%s' with a different type: %a vs %a" + s (print_typ env) old_ty (print_typ env) ty; ty in let new_sto = (* The only case not allowed is removing static *) @@ -130,8 +134,8 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = | Storage_register,Storage_register | Storage_default,Storage_default -> sto | _,Storage_static -> - error loc "static redefinition of '%s' after non-static definition" s; - sto + error loc "static declaration of '%s' follows non-static declaration" s; + sto | Storage_static,_ -> Storage_static (* Static stays static *) | Storage_extern,_ -> sto | Storage_default,Storage_extern -> Storage_extern @@ -149,14 +153,14 @@ let enter_or_refine_ident local loc env s sto ty = - an enum that was already declared in the same scope. Redefinition of a variable at global scope (or extern) is treated below. *) if redef Env.lookup_typedef env s then - error loc "redefinition of typedef '%s' as different kind of symbol" s; + error loc "redefinition of '%s' as different kind of symbol" s; begin match previous_def Env.lookup_ident env s with | Some(id, II_ident(old_sto, old_ty)) when local && Env.in_current_scope env id && not (sto = Storage_extern && old_sto = Storage_extern) -> - error loc "redefinition of local variable '%s'" s + error loc "redefinition of '%s'" s | Some(id, II_enum _) when Env.in_current_scope env id -> - error loc "redefinition of enumerator '%s'" s + error loc "redefinition of '%s' as different kind of symbol" s; | _ -> () end; @@ -184,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 *) @@ -277,7 +281,7 @@ let elab_int_constant loc s0 = try parse_int base s with | Overflow -> - error loc "integer literal '%s' is too large" s0; + error loc "integer literal '%s' is too large to be represented in any integer type" s0; 0L | Bad_digit -> (*error loc "bad digit in integer literal '%s'" s0;*) (* Is caught earlier *) @@ -313,17 +317,23 @@ let elab_char_constant loc wide chars = (* Treat multi-char constants as a number in base 2^nbits *) let max_digit = Int64.shift_left 1L nbits in let max_val = Int64.shift_left 1L (64 - nbits) in - let v = + let v,_ = List.fold_left - (fun acc d -> - if acc < 0L || acc >= max_val then - error loc "character constant overflows"; - if d < 0L || d >= max_digit then - error loc "escape sequence is out of range (code 0x%LX)" d; - Int64.add (Int64.shift_left acc nbits) d) - 0L chars in + (fun (acc,err) d -> + if not err then begin + let overflow = acc < 0L || acc >= max_val + and out_of_range = d < 0L || d >= max_digit in + if overflow then + error loc "character constant too long for its type"; + if out_of_range then + error loc "escape sequence is out of range (code 0x%LX)" d; + Int64.add (Int64.shift_left acc nbits) d,overflow || out_of_range + end else + Int64.add (Int64.shift_left acc nbits) d,true + ) + (0L,false) chars in if not (integer_representable v IInt) then - warning loc "character constant cannot be represented at type 'int'"; + warning loc Unnamed "character constant too long for its type"; (* C99 6.4.4.4 item 10: single character -> represent at type char or wchar_t *) Ceval.normalize_int v @@ -365,7 +375,7 @@ let elab_constant loc = function let elab_simple_string loc wide chars = match elab_string_literal loc wide chars with | CStr s -> s - | _ -> error loc "wide character string not allowed here"; "" + | _ -> error loc "cannot use wide string literal in 'asm'"; "" (** * Elaboration of type expressions, type specifiers, name declarations *) @@ -406,7 +416,8 @@ let elab_gcc_attr loc env = function begin try [Attr(v, List.map (elab_attr_arg loc env) args)] with Wrong_attr_arg -> - warning loc "cannot parse '%s' attribute, ignored" v; [] + warning loc Unknown_attribute + "unknown attribute '%s' ignored" v; [] end let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L @@ -415,8 +426,11 @@ let extract_alignas loc a = match a with | Attr(("aligned"|"__aligned__"), args) -> begin match args with - | [AInt n] when is_power_of_two n -> AAlignas (Int64.to_int n) - | _ -> warning loc "bad 'aligned' attribute, ignored"; a + | [AInt n] when is_power_of_two n -> AAlignas (Int64.to_int n) + | [AInt n] -> error loc "requested alignment is not a power of 2"; a + | [_] -> error loc "requested alignment is not an integer constant"; a + | [] -> a (* Use the default alignment as the gcc does *) + | _ -> error loc "'aligned' attribute takes no more than 1 argument"; a end | _ -> a @@ -431,12 +445,17 @@ let elab_attribute env = function [Attr("__packed__", List.map (elab_attr_arg loc env) args)] | ALIGNAS_ATTR ([a], loc) -> begin match elab_attr_arg loc env a with - | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] - | _ -> warning loc "bad _Alignas value, ignored"; [] - | exception Wrong_attr_arg -> warning loc "bad _Alignas value, ignored"; [] + | AInt n -> + if is_power_of_two n then + [AAlignas (Int64.to_int n)] + else begin + 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) -> - warning loc "_Alignas takes exactly one parameter, ignored"; [] + error loc "_Alignas takes no more than 1 argument"; [] let elab_attributes env al = List.fold_left add_attributes [] (List.map (elab_attribute env) al) @@ -473,7 +492,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) @@ -490,7 +509,7 @@ let rec elab_specifier ?(only = false) loc env specifier = attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> if !sto <> Storage_default && st <> TYPEDEF then - error loc "multiple storage specifiers"; + error loc "multiple storage-classes in declaration specifier"; begin match st with | AUTO -> () | STATIC -> sto := Storage_static @@ -577,14 +596,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)] -> @@ -610,8 +629,15 @@ and elab_cvspecs env cv_specs = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) (* Elaboration of a type declarator. C99 section 6.7.5. *) +and elab_return_type loc env ty = + match unroll env ty with + | TArray _ -> + error loc "function cannot return array type %a" (print_typ env) ty + | TFun _ -> + 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) -> @@ -624,59 +650,53 @@ and elab_type_declarator loc env ty kr_ok = function let expr,env = (!elab_expr_f loc env sz) in match Ceval.integer_expr env expr with | Some n -> - if n < 0L then error loc "array size is negative"; - if n = 0L then warning loc "array of size 0"; + if n < 0L then error loc "size of array is negative"; + if n = 0L then warning loc Zero_length_array + "zero size arrays are an extension"; Some n | None -> - error loc "array size is not a compile-time constant"; + 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)) -> - begin match unroll env ty with - | TArray _ | TFun _ -> - error loc "Illegal function return type@ %a" Cprint.typ ty - | _ -> () - end; - let params' = elab_parameters env params in - elab_type_declarator loc env (TFun(ty, Some params', vararg, [])) kr_ok d + elab_return_type loc env ty; + 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) -> - begin match unroll env ty with - | TArray _ | TFun _ -> - error loc "Illegal function return type@ %a" Cprint.typ ty - | _ -> () - end; + 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"; + fatal_error loc "illegal old-style K&R function definition"; ((TFun(ty, None, false, []), Some params), env) (* 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 - "'extern' or 'static' storage not supported for function parameter"; + "invalid storage-class specifier in function declarator"; if inl then error loc "'inline' can only appear on functions"; if noret then @@ -687,23 +707,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 @@ -712,19 +732,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"; @@ -735,7 +755,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 @@ -745,15 +765,16 @@ 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"; if fieldlist = [] then if is_anonymous_composite spec then - warning loc "ISO C99 does not support anonymous structs/unions" + warning loc Celeven_extension "anonymous structs/unions are a C11 extension" else - warning loc "declaration does not declare any members"; + (* This should actually never be triggered, empty structs are captured earlier *) + warning loc Missing_declarations "declaration does not declare anything"; let elab_bitfield (Name (_, _, _, loc), optbitsize) (id, ty) = let optbitsize' = @@ -767,28 +788,28 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = | _ -> ILongLong (* trigger next error message *) in if integer_rank ik > integer_rank IInt then begin error loc - "the type of bitfield '%s' must be an integer type \ - no bigger than 'int'" id; + "the type of bit-field '%s' must be an integer type no bigger than 'int'" id; None end else begin let expr,env' =(!elab_expr_f loc env sz) in match Ceval.integer_expr env' expr with | Some n -> if n < 0L then begin - error loc "bit size of '%s' (%Ld) is negative" id n; + error loc "bit-field '%s' has negative width (%Ld)" id n; None end else - if n > Int64.of_int(sizeof_ikind ik * 8) then begin - error loc "bit size of '%s' (%Ld) exceeds its type" id n; - None + let max = Int64.of_int(sizeof_ikind ik * 8) in + if n > max then begin + error loc "size of bit-field '%s' (%Ld bits) exceeds its type (%Ld bits)" id n max; + None end else if n = 0L && id <> "" then begin - error loc "member '%s' has zero size" id; + error loc "named bit-field '%s' has zero width" id; None end else Some(Int64.to_int n) | None -> - error loc "bit size of '%s' is not a compile-time constant" id; + error loc "bit-field '%s' width not an integer constant" id; None end in { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } @@ -797,9 +818,17 @@ 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 + ignore (List.fold_left (fun acc fld -> + let n = fld.fld_name in + if n <> "" then begin + if List.exists ((=) n) acc then + error loc "duplicate member '%s'" n; + n::acc + end else + acc) [] m); (* Check for incomplete types *) let rec check_incomplete = function | [] -> () @@ -814,16 +843,16 @@ and elab_struct_or_union_info kind loc env members attrs = (* Warn for empty structs or unions *) if m = [] then if kind = Struct then begin - warning loc "empty struct" + warning loc Gnu_empty_struct "empty struct is a GNU extension" end else begin - fatal_error loc "empty union" + fatal_error loc "empty union is a GNU 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 "attributes over struct/union ignored in this context" in + warning loc Unnamed "attribute declaration must precede definition" in let optbinding, tag = match tag with | None -> None, "" @@ -838,14 +867,16 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = and the composite was bound in another scope, create a new incomplete composite instead via the case "_, None" below. *) + if ci.ci_kind <> kind then + 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 when Env.in_current_scope env tag' -> if ci.ci_kind <> kind then - error loc "struct/union mismatch on tag '%s'" tag; + 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 *) @@ -873,7 +904,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 *) @@ -892,15 +923,15 @@ and elab_enum_item env ((s, exp), loc) nextval = | Some n -> (n, Some exp') | None -> error loc - "value of enumerator '%s' is not a compile-time constant" s; + "value of enumerator '%s' is not an integer constant" s; (nextval, Some exp') in if redef Env.lookup_ident env s then - error loc "redefinition of identifier '%s'" s; + error loc "'%s' redeclared as different kind of symbol" s; if redef Env.lookup_typedef env s then - error loc "redefinition of typedef '%s' as different kind of symbol" s; + error loc "'%s' redeclared as different kind of symbol" s; if not (int_representable v (8 * sizeof_ikind enum_ikind) (is_signed_ikind enum_ikind)) then - warning loc "the value of '%s' is not representable with type %a" - s Cprint.typ (TInt(enum_ikind, [])); + warning loc Constant_conversion "integer literal '%Ld' is too large to be represented in any integer type" + v; let (id, env') = Env.enter_enum_item env s v in ((id, v, exp'), Int64.succ v, env') @@ -932,8 +963,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'') @@ -972,13 +1003,18 @@ let init_int_array_wstring opt_size s = let check_init_type loc env a ty = if wrap2 valid_assignment loc env a ty then () else if wrap2 valid_cast loc env a.etyp ty then - warning loc - "initializer has type@ %a@ instead of the expected type @ %a" - Cprint.typ a.etyp Cprint.typ ty + if wrap2 int_pointer_conversion loc env a.etyp ty then + warning loc Int_conversion + "incompatible integer-pointer conversion initializer has type %a instead of the expected type %a" + (print_typ env) a.etyp (print_typ env) ty + else + warning loc Unnamed + "incompatible conversion initializer has type %a instead of the expected type %a" + (print_typ env) a.etyp (print_typ env) ty else error loc - "initializer has type@ %a@ instead of the expected type @ %a" - Cprint.typ a.etyp Cprint.typ ty + "initializer has type %a instead of the expected type %a" + (print_typ env) a.etyp (print_typ env) ty (* Representing initialization state using zippers *) @@ -1171,16 +1207,14 @@ let rec elab_designator loc env zi desig = let expr,env = (!elab_expr_f loc env a) in begin match Ceval.integer_expr env expr with | None -> - error loc "array element designator for %s is not a compile-time constant" - (I.name zi); + error loc "array element designator for %s is not an integer constant expression" (I.name zi); raise Exit | Some n -> match I.index env zi n with | Some zi' -> elab_designator loc env zi' desig' | None -> - error loc "bad array element designator %Ld within %s" - n (I.name zi); + error loc "array index %Ld within %s exceeds array bounds" n (I.name zi); raise Exit end @@ -1203,7 +1237,7 @@ let rec elab_list zi il first = match (if first then I.first env zi else I.next zi) with | None -> - warning loc "excess elements at end of initializer for %s, ignored" + warning loc Unnamed "excess elements in initializer for %s" (I.name zi); I.to_init zi | Some zi' -> @@ -1226,16 +1260,14 @@ and elab_item zi item il = begin match elab_string_literal loc w s, unroll env ty_elt with | CStr s, TInt((IChar | ISChar | IUChar), _) -> if not (I.index_below (Int64.of_int(String.length s - 1)) sz) then - warning loc "initializer string for array of chars %s is too long" - (I.name zi); + warning loc Unnamed "initializer string for array of chars %s is too long" (I.name zi); elab_list (I.set zi (init_char_array_string sz s)) il false | CStr _, _ -> error loc "initialization of an array of non-char elements with a string literal"; elab_list zi il false | CWStr s, TInt(_, _) when compatible_types AttrIgnoreTop env ty_elt (TInt(wchar_ikind(), [])) -> if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then - warning loc "initializer string for array of wide chars %s is too long" - (I.name zi); + warning loc Unnamed "initializer string for array of wide chars %s is too long" (I.name zi); elab_list (I.set zi (init_int_array_wstring sz s)) il false | CWStr _, _ -> error loc "initialization of an array of non-wchar_t elements with a wide string literal"; @@ -1281,13 +1313,22 @@ and elab_single zi a il = raise Exit end | _ -> - error loc "impossible to initialize %s of type@ %a" - (I.name zi) Cprint.typ ty; + error loc "impossible to initialize %s of type %a" + (I.name zi) (print_typ env) ty; raise Exit (* 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 *) @@ -1307,7 +1348,7 @@ let elab_initial loc env root ty ie = let fixup_typ loc env ty init = match unroll env ty, init with | TArray(ty_elt, None, attr), Init_array il -> - if il = [] then warning loc "array of size 0"; + if il = [] then warning loc Zero_length_array "zero size arrays are an extension"; TArray(ty_elt, Some(Int64.of_int(List.length il)), attr) | _ -> ty @@ -1323,11 +1364,22 @@ 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 - let warning fmt = warning loc fmt in + let warning t fmt = + warning loc t fmt in + + let check_ptr_arith env ty s = + match unroll env ty with + | TVoid _ -> + err "illegal arithmetic on a pointer to void in binary '%c'" s + | TFun _ -> + err "illegal arithmetic on a pointer to the function type %a in binary '%c'" (print_typ env) ty s + | _ -> if incomplete_type env ty then + err "arithmetic on a pointer to an incomplete type %a in binary '%c'" (print_typ env) ty s + in let rec elab env = function @@ -1354,7 +1406,7 @@ let elab_expr loc env a = match (unroll env b1.etyp, unroll env b2.etyp) with | (TPtr(t, _) | TArray(t, _, _)), (TInt _ | TEnum _) -> t | (TInt _ | TEnum _), (TPtr(t, _) | TArray(t, _, _)) -> t - | t1, t2 -> error "incorrect types for array subscripting" in + | t1, t2 -> error "subscripted value is neither an array nor pointer" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres },env | MEMBEROF(a1, fieldname) -> @@ -1366,7 +1418,7 @@ let elab_expr loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "left-hand side of '.' is not a struct or union" in + error "request for member '%s' in something not a structure or union" fieldname in (* A field of a const/volatile struct or union is itself const/volatile *) { edesc = EUnop(Odot fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) @@ -1383,10 +1435,10 @@ let elab_expr loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "left-hand side of '->' is not a pointer to a struct or union" + error "request for member '%s' in something not a structure or union" fieldname end | _ -> - error "left-hand side of '->' is not a pointer " in + error "member reference type %a is not a pointer" (print_typ env) b1.etyp in { edesc = EUnop(Oarrow fieldname, b1); etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) (type_of_member env fld) },env @@ -1400,6 +1452,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 @@ -1417,9 +1471,8 @@ let elab_expr loc env a = let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in let ty' = default_argument_conversion env ty in if not (compatible_types AttrIgnoreTop env ty ty') then - warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'" - Cprint.typ ty Cprint.typ ty' - Cprint.typ ty' Cprint.typ ty; + warning Varargs "%a is promoted to %a when passed through '...'. You should pass %a, not %a, to 'va_arg'" + (print_typ env) ty (print_typ env) ty' (print_typ env) ty' (print_typ env) ty; { edesc = ECall(ident, [b2; b3]); etyp = ty },env | CALL(a1, al) -> @@ -1428,7 +1481,7 @@ let elab_expr loc env a = having declared it *) match a1 with | VARIABLE n when not (Env.ident_is_bound env n) -> - warning "implicit declaration of function '%s'" n; + warning Implicit_function_declaration "implicit declaration of function '%s' is invalid in C99" n; let ty = TFun(TInt(IInt, []), None, false, []) in (* Check against other definitions and enter in env *) let (id, sto, env, ty, linkage) = @@ -1445,9 +1498,9 @@ let elab_expr loc env a = | TPtr(ty, a) -> begin match unroll env ty with | TFun(res, args, vararg, a) -> (res, args, vararg) - | _ -> error "the function part of a call does not have a function type" + | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp end - | _ -> error "the function part of a call does not have a function type" + | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp in (* Type-check the arguments against the prototype *) let bl',env = @@ -1457,23 +1510,37 @@ let elab_expr loc env a = { edesc = ECall(b1, bl'); etyp = res },env | UNARY(POSINCR, a1) -> - elab_pre_post_incr_decr Opostincr "postfix '++'" a1 + elab_pre_post_incr_decr Opostincr "increment" a1 | UNARY(POSDECR, a1) -> - elab_pre_post_incr_decr Opostdecr "postfix '--'" a1 + elab_pre_post_incr_decr Opostdecr "decrement" a1 (* 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 - err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty; + begin match unroll env b1.etyp, unroll env ty with + | _, (TStruct _|TUnion _ | TVoid _) -> + err "used type %a where arithmetic or pointer type is required" + (print_typ env) ty + | (TStruct _| TUnion _ | TVoid _),_ -> + err "operand of type %a where arithmetic or pointer type is required" + (print_typ env) b1.etyp + | TFloat _, TPtr _ -> + err "operand of type %a cannot be cast to a pointer type" + (print_typ env) b1.etyp + | TPtr _ , TFloat _ -> + err "pointer cannot be cast to type %a" (print_typ env) ty + | _ -> + err "illegal cast from %a to %a" (print_typ env) b1.etyp (print_typ env) ty + end; { edesc = ECast(ty, b1); etyp = ty },env (* 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" @@ -1484,7 +1551,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 "incomplete type %a" Cprint.typ 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 @@ -1501,49 +1568,49 @@ 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 "incomplete type %a" Cprint.typ 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 "incomplete type %a" Cprint.typ 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 "incomplete type %a" Cprint.typ ty; - { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env + 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) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - err "argument of unary '+' is not an arithmetic type"; + error "invalid argument type %a to unary '+'" (print_typ env) b1.etyp; { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(MINUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - err "argument of unary '-' is not an arithmetic type"; + error "invalid argument type %a to unary '-'" (print_typ env) b1.etyp; { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp },env | UNARY(BNOT, a1) -> let b1,env = elab env a1 in if not (is_integer_type env b1.etyp) then - err "argument of '~' is not an integer type"; + error "invalid argument type %a to unary '~'" (print_typ env) b1.etyp; { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp },env | UNARY(NOT, a1) -> let b1,env = elab env a1 in if not (is_scalar_type env b1.etyp) then - err "argument of '!' is not a scalar type"; + error "invalid argument type %a to unary '!'" (print_typ env) b1.etyp; { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) },env | UNARY(ADDROF, a1) -> let b1,env = elab env a1 in if not (is_lvalue b1 || is_function_type env b1.etyp) then - err "argument of '&' is not an l-value"; + err "argument of '&' is not an lvalue (invalid %a)" (print_typ env) b1.etyp; begin match b1.edesc with | EVar id -> begin match wrap Env.find_ident loc env id with @@ -1571,13 +1638,14 @@ let elab_expr loc env a = | TPtr(ty, _) | TArray(ty, _, _) -> { edesc = EUnop(Oderef, b1); etyp = ty },env | _ -> - error "argument of unary '*' is not a pointer" + error "arguemnt of unary '*' is not a pointer (%a invalid)" + (print_typ env) b1.etyp end | UNARY(PREINCR, a1) -> - elab_pre_post_incr_decr Opreincr "prefix '++'" a1 + elab_pre_post_incr_decr Opreincr "increment" a1 | UNARY(PREDECR, a1) -> - elab_pre_post_incr_decr Opredecr "prefix '--'" a1 + elab_pre_post_incr_decr Opredecr "decrement" a1 (* 6.5.5 to 6.5.12 Binary operator expressions *) @@ -1588,7 +1656,7 @@ let elab_expr loc env a = elab_binary_arithmetic "/" Odiv a1 a2 | BINARY(MOD, a1, a2) -> - elab_binary_integer "/" Omod a1 a2 + elab_binary_integer "%" Omod a1 a2 | BINARY(ADD, a1, a2) -> let b1,env = elab env a1 in @@ -1601,9 +1669,10 @@ let elab_expr loc env a = match unroll env b1.etyp, unroll env b2.etyp with | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty - | _, _ -> error "type error in binary '+'" in - if not (pointer_arithmetic_ok env ty) then - err "illegal pointer arithmetic in binary '+'"; + | _, _ -> error "invalid operands to binary '+' (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp + in + check_ptr_arith env ty '+'; TPtr(ty, []) end in { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres },env @@ -1616,25 +1685,25 @@ 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)) -> - if not (pointer_arithmetic_ok env ty) then - err "illegal pointer arithmetic in binary '-'"; + check_ptr_arith env ty '-'; (TPtr(ty, []), TPtr(ty, [])) | (TPtr(ty1, a1) | TArray(ty1, _, a1)), (TPtr(ty2, a2) | TArray(ty2, _, a2)) -> if not (compatible_types AttrIgnoreAll env ty1 ty2) then - err "mismatch between pointer types in binary '-'"; - if not (pointer_arithmetic_ok env ty1) then - err "illegal pointer arithmetic in binary '-'"; + err "%a and %a are not pointers to compatible types" + (print_typ env) b1.etyp (print_typ env) b1.etyp; + check_ptr_arith env ty1 '-'; if wrap sizeof loc env ty1 = Some 0 then err "subtraction between two pointers to zero-sized objects"; (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) - | _, _ -> error "type error in binary '-'" + | _, _ -> error "invalid operands to binary '-' (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp end in { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres },env @@ -1677,12 +1746,13 @@ let elab_expr loc env a = let b2,env = elab env a2 in let b3,env = elab env a3 in if not (is_scalar_type env b1.etyp) then - err ("the first argument of '? :' is not a scalar type"); + err "first argument of '?:' is not a scalar type (invalid %a)" + (print_typ env) b1.etyp; begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> { edesc = EConditional(b1, b2, b3); etyp = binary_conversion env b2.etyp b3.etyp },env - | TPtr(ty1, a1), TPtr(ty2, a2) -> + | (TPtr(ty1, a1) as pty1), (TPtr(ty2, a2) as pty2) -> let tyres = if is_void_type env ty1 || is_void_type env ty2 then TPtr(TVoid (add_attributes a1 a2), []) @@ -1690,8 +1760,8 @@ let elab_expr loc env a = match combine_types AttrIgnoreAll env (TPtr(ty1, a1)) (TPtr(ty2, a2)) with | None -> - warning "the second and third arguments of '? :' \ - have incompatible pointer types"; + warning Pointer_type_mismatch "the second and third argument of '?:' have incompatible pointer types (%a and %a)" + (print_typ env) pty1 (print_typ env) pty2; (* tolerance *) TPtr(TVoid (add_attributes a1 a2), []) | Some ty -> ty @@ -1704,7 +1774,8 @@ let elab_expr loc env a = | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with | None -> - error ("the second and third arguments of '? :' have incompatible types") + error "the second and third argument of '?:' incompatible types (%a and %a)" + (print_typ env) ty1 (print_typ env) ty2 | Some tyres -> { edesc = EConditional(b1, b2, b3); etyp = tyres },env end @@ -1715,16 +1786,22 @@ let elab_expr loc env a = let b1,env = elab env a1 in let b2,env = elab env a2 in if List.mem AConst (attributes_of_type env b1.etyp) then - err "left-hand side of assignment has 'const' type"; + error "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then - err "left-hand side of assignment is not a modifiable l-value"; + err "expression is not assignable"; if not (wrap2 valid_assignment loc env b2 b1.etyp) then begin if wrap2 valid_cast loc env b2.etyp b1.etyp then - warning "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ b2.etyp Cprint.typ b1.etyp + if wrap2 int_pointer_conversion loc env b2.etyp b1.etyp then + warning Int_conversion + "incompatible integer-pointer conversion: assigning to %a from %a" + (print_typ env) b1.etyp (print_typ env) b2.etyp + else + warning Unnamed + "incompatible conversion assigning to %a from %a" + (print_typ env) b1.etyp (print_typ env) b2.etyp else - err "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ b2.etyp Cprint.typ b1.etyp; + err "assigning to %a from incompatible type %a" + (print_typ env) b1.etyp (print_typ env) b2.etyp; end; { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp },env @@ -1749,14 +1826,20 @@ let elab_expr loc env a = if List.mem AConst (attributes_of_type env b1.etyp) then err "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then - err ("left-hand side of assignment is not a modifiable l-value"); + err "expression is not assignable"; if not (wrap2 valid_assignment loc env b b1.etyp) then begin if wrap2 valid_cast loc env ty b1.etyp then - warning "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ ty Cprint.typ b1.etyp + if wrap2 int_pointer_conversion loc env ty b1.etyp then + warning Int_conversion + "incompatible integer-pointer conversion: assigning to %a from %a" + (print_typ env) b1.etyp (print_typ env) ty + else + warning Unnamed + "incompatible conversion assigning to %a from %a" + (print_typ env) b1.etyp (print_typ env) ty else - err "assigning a value of type@ %a@ to a lvalue of type@ %a" - Cprint.typ ty Cprint.typ b1.etyp; + err "assigning to %a from incompatible type %a" + (print_typ env) b1.etyp (print_typ env) ty; end; { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp },env | _ -> assert false @@ -1771,45 +1854,42 @@ let elab_expr loc env a = (* Elaboration of pre- or post- increment/decrement *) and elab_pre_post_incr_decr op msg a1 = - let b1,env = elab env a1 in - if not (is_modifiable_lvalue env b1) then - err "the argument of %s is not a modifiable l-value" msg; - if not (is_scalar_type env b1.etyp) then - err "the argument of %s must be an arithmetic or pointer type" msg; - { edesc = EUnop(op, b1); etyp = b1.etyp },env + let b1,env = elab env a1 in + if not (is_modifiable_lvalue env b1) then + err "expression is not assignable"; + if not (is_scalar_type env b1.etyp) then + err "cannot %s value of type %a" msg (print_typ env) b1.etyp; + { edesc = EUnop(op, b1); etyp = b1.etyp },env (* Elaboration of binary operators over integers *) and elab_binary_integer msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_integer_type env b1.etyp) then - error "the first argument of '%s' is not an integer type" msg; - let b2,env = elab env a2 in - if not (is_integer_type env b2.etyp) then - error "the second argument of '%s' is not an integer type" msg; - let tyres = binary_conversion env b1.etyp b2.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then + error "invalid operands to binary '%s' (%a and %a)" msg + (print_typ env) b1.etyp (print_typ env) b2.etyp; + let tyres = binary_conversion env b1.etyp b2.etyp in + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of binary operators over arithmetic types *) and elab_binary_arithmetic msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_arith_type env b1.etyp) then - error "the first argument of '%s' is not an arithmetic type" msg; - let b2,env = elab env a2 in - if not (is_arith_type env b2.etyp) then - error "the second argument of '%s' is not an arithmetic type" msg; - let tyres = binary_conversion env b1.etyp b2.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_arith_type env b1.etyp) && (is_arith_type env b2.etyp)) then + error "invalid operands to binary '%s' (%a and %a)" msg + (print_typ env) b1.etyp (print_typ env) b2.etyp; + let tyres = binary_conversion env b1.etyp b2.etyp in + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of shift operators *) and elab_shift msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_integer_type env b1.etyp) then - error "the first argument of '%s' is not an integer type" msg; - let b2,env = elab env a2 in - if not (is_integer_type env b2.etyp) then - error "the second argument of '%s' is not an integer type" msg; - let tyres = unary_conversion env b1.etyp in - { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_integer_type env b1.etyp) && (is_integer_type env b2.etyp)) then + error "invalid operands to '%s' (%a and %a)" msg + (print_typ env) b1.etyp (print_typ env) b2.etyp; + let tyres = unary_conversion env b1.etyp in + { edesc = EBinop(op, b1, b2, tyres); etyp = tyres },env (* Elaboration of comparisons *) and elab_comparison op a1 a2 = @@ -1831,66 +1911,76 @@ let elab_expr loc env a = EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr(ty1, _), TPtr(ty2, _) -> if not (compatible_types AttrIgnoreAll env ty1 ty2) then - warning "comparison between incompatible pointer types"; + warning Compare_distinct_pointer_types "comparison of distinct pointer types (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr _, (TInt _ | TEnum _) | (TInt _ | TEnum _), TPtr _ -> - warning "comparison between integer and pointer"; + warning Unnamed "comparison between pointer and integer (%a and %a)" + (print_typ env) b1.etyp (print_typ env) b2.etyp; EBinop(op, b1, b2, TPtr(TVoid [], [])) - | _, _ -> + | ty1, ty2 -> error "illegal comparison between types@ %a@ and %a" - Cprint.typ b1.etyp Cprint.typ b2.etyp in + (print_typ env) b1.etyp (print_typ env) b2.etyp; in { edesc = resdesc; etyp = TInt(IInt, []) },env (* Elaboration of && and || *) and elab_logical_operator msg op a1 a2 = - let b1,env = elab env a1 in - if not (is_scalar_type env b1.etyp) then - err "the first argument of '%s' is not a scalar type" msg; - let b2,env = elab env a2 in - if not (is_scalar_type env b2.etyp) then - err "the second argument of '%s' is not a scalar type" msg; - { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) },env + let b1,env = elab env a1 in + let b2,env = elab env a2 in + if not ((is_scalar_type env b1.etyp) && (is_scalar_type env b2.etyp)) then + error "invalid operands to binary %s (%a and %a)" msg + (print_typ env) b1.etyp (print_typ env) b2.etyp; + { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) },env (* Type-checking of function arguments *) and elab_arguments argno args params vararg = match args, params with | ([],env), [] -> [],env - | ([],env), _::_ -> err "not enough arguments in function call"; [], env - | (_::_,env), [] -> + | ([],env), _::_ -> + let found = argno - 1 in + let expected = List.length params + found in + err "too few arguments to function call, expected %d, have %d" expected found; [],env + | (_::_,env), [] -> if vararg then args - else (err "too many arguments in function call"; args) + else + let expected = argno - 1 in + let found = List.length (fst args) + expected in + (err "too many arguments to function call, expected %d, have %d" expected found; args) | (arg1 :: argl,env), (_, ty_p) :: paraml -> let ty_a = argument_conversion env arg1.etyp in if not (wrap2 valid_assignment loc env {arg1 with etyp = ty_a} ty_p) then begin - if wrap2 valid_cast loc env ty_a ty_p then - warning - "argument #%d of function call has type@ %a@ \ - instead of the expected type@ %a" - argno Cprint.typ ty_a Cprint.typ ty_p + if wrap2 valid_cast loc env ty_a ty_p then begin + if wrap2 int_pointer_conversion loc env ty_a ty_p then + warning Int_conversion + "incompatible integer-pointer conversion: passing %a to parameter %d of type %a" + (print_typ env) ty_a argno (print_typ env) ty_p + else + warning Unnamed + "incompatible conversion passing %a to parameter %d of type %a" + (print_typ env) ty_a argno (print_typ env) ty_p end else err - "argument #%d of function call has type@ %a@ \ - instead of the expected type@ %a" - argno Cprint.typ ty_a Cprint.typ ty_p + "passing %a to parameter %d of incompatible type %a" + (print_typ env) ty_a argno (print_typ env) ty_p end; let rest,env = elab_arguments (argno + 1) (argl,env) paraml vararg in arg1 :: rest,env 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) *) @@ -1904,22 +1994,23 @@ let __func__type_and_init s = let enter_typedefs loc env sto dl = if sto <> Storage_default then - error loc "Non-default storage on 'typedef' definition"; + error loc "non-default storage-class on 'typedef' definition"; List.fold_left (fun env (s, ty, init) -> if init <> NO_INIT then error loc "initializer in typedef"; match previous_def Env.lookup_typedef env s with | Some (s',ty') -> if equal_types env ty ty' then begin - warning loc "redefinition of typedef '%s'" s; + warning loc Cerrors.Celeven_extension "redefinition of typedef '%s' is C11 extension" s; env end else begin - error loc "redefinition of typedef '%s' with different type" s; + error loc "typedef redefinition with different types (%a vs %a)" + (print_typ env) ty (print_typ env) ty'; env end | None -> if redef Env.lookup_ident env s then - error loc "redefinition of identifier '%s' as different kind of symbol" s; + error loc "redefinition of '%s' as different kind of symbol" s; let (id, env') = Env.enter_typedef env s ty in emit_elab env loc (Gtypedef(id, ty)); env') env dl @@ -1927,15 +2018,19 @@ let enter_typedefs loc env sto dl = let enter_decdefs local loc env sto dl = (* Sanity checks on storage class *) if sto = Storage_register && not local then - fatal_error loc "'register' on global declaration"; - if sto <> Storage_default && dl = [] then - warning loc "Storage class specifier on empty declaration"; + fatal_error loc "'register' storage-class on file-scoped variable"; + if dl = [] then + warning loc Missing_declarations "declaration does not declare anything"; let enter_decdef (decls, env) (s, ty, init) = let isfun = is_function_type env ty in if sto = Storage_extern && init <> NO_INIT then - error loc "'extern' declaration cannot have an initializer"; - if local && isfun && (sto = Storage_static || sto = Storage_register) then - error loc "invalid storage class for '%s'" s; + error loc "'extern' declaration variable has an initializer"; + if local && isfun then begin + match sto with + | Storage_static -> error loc "function declared in block scope cannot have 'static' storage-class"; + | Storage_register -> error loc "invalid 'register' storage-class on function"; + | _ -> () + end; (* Local function declarations are always treated as extern *) let sto1 = if local && isfun then Storage_extern else sto in (* enter ident in environment with declared type, because @@ -1952,7 +2047,7 @@ let enter_decdefs local loc env sto dl = if local && sto' <> Storage_extern && not isfun && wrap incomplete_type loc env ty' then - error loc "'%s' has incomplete type" s; + error loc "variable has incomplete type %a" (print_typ env) ty'; if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then (* Local definition *) ((sto', id, ty', init') :: decls, env2) @@ -1985,40 +2080,46 @@ let elab_KR_function_parameters env params defs loc = (* Check that the parameters have unique names *) List.iter (fun id -> if List.length (List.filter ((=) id) params) > 1 then - error loc "Parameter '%s' appears more than once in function declaration" id) + fatal_error loc "redefinition of parameter '%s'" id) params; (* Check that the declarations only declare parameters *) let extract_name (Init_name(Name(s, dty, attrs, loc') as name, ie)) = if not (List.mem s params) then error loc' "Declaration of '%s' which is not a function parameter" s; if ie <> NO_INIT then - error loc' "Illegal initialization of function parameter '%s'" s; + error loc' "illegal initialization of parameter '%s'" s; name in (* Extract names and types from the declarations *) 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 - if sto <> Storage_default && sto <> Storage_register then - error loc' "'extern' or 'static' storage not supported for function parameter"; + let (paramsenv, sto) = elab_name_group true loc' env (spec', name_list) in + begin match sto with + | Storage_extern -> + error loc' "invalid 'extern' storage-class specifier for function parameter" + | Storage_static -> + error loc' "invalid 'static' storage-class specifier for function parameter" + | _ -> () + end; paramsenv | d -> (* Should never be produced by the parser *) fatal_error (get_definitionloc d) "Illegal declaration of function parameter" in - let kr_params_defs = - List.concat (fst (mmap elab_param_def env defs)) in + let kr_params_defs,paramsenv = + let params,paramsenv = mmap elab_param_def env defs in + List.concat params,paramsenv in (* Find the type of a parameter *) let type_of_param param = match List.filter (fun (p, _) -> p = param) kr_params_defs with | [] -> (* Parameter is not declared, defaults to "int" in ISO C90, is an error in ISO C99. Just emit a warning. *) - warning loc "Type of '%s' defaults to 'int'" param; + warning loc Pedantic "type of '%s' defaults to 'int'" param; TInt (IInt, []) | (_, ty) :: rem -> if rem <> [] then - error loc "Parameter '%s' defined more than once" param; + error loc "redefinition of parameter '%s'" param; ty in (* Match parameters against declarations *) let rec match_params params' extra_decls = function @@ -2044,7 +2145,8 @@ let elab_KR_function_parameters env params defs loc = ps end in - match_params [] [] params + let a,b = match_params [] [] params in + a,b,paramsenv (* Look for varargs flag in previous definitions of a function *) @@ -2065,30 +2167,30 @@ 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 "A function definition cannot have 'register' storage class"; + fatal_error loc "invalid 'register' storage-class on function"; begin match kr_params, defs with - | None, d :: _ -> - error (get_definitionloc d) - "Old-style parameter declaration in a new-style function definition" + | None, d::_ -> + error (get_definitionloc d) + "old-style parameter declarations in prototyped function definition" | _ -> () end; (* Process the parameters and the K&R declarations, if any, to obtain: - [ty]: the full, prototyped type of the function - [extra_decls]: extra declarations to be inserted at the beginning of the function *) - let (ty, extra_decls) = + let (ty, extra_decls,env1) = match ty, kr_params with | TFun(ty_ret, None, vararg, attr), None -> - (TFun(ty_ret, Some [], vararg, attr), []) + (TFun(ty_ret, Some [], vararg, attr), [],env1) | ty, None -> - (ty, []) + (ty, [],env1) | TFun(ty_ret, None, false, attr), Some params -> - warning loc "Non-prototype, pre-standard function definition.@ Converting to prototype form"; - let (params', extra_decls) = + warning loc Cerrors.CompCert_conformance "non-prototype, pre-standard function definition, converting to prototype form"; + let (params', extra_decls,env) = elab_KR_function_parameters env params defs loc in - (TFun(ty_ret, Some params', inherit_vararg env s sto ty, attr), extra_decls) + (TFun(ty_ret, Some params', inherit_vararg env s sto ty, attr), extra_decls,env) | _, Some params -> assert false in @@ -2096,18 +2198,21 @@ let elab_fundef env spec name defs body loc = let (ty_ret, params, vararg, attr) = match ty with | TFun(ty_ret, Some params, vararg, attr) -> - if wrap incomplete_type loc env1 ty_ret - && not (is_void_type env ty_ret) - then error loc "return type is an incomplete type"; - (ty_ret, params, vararg, attr) - | _ -> - fatal_error loc "wrong type for function definition" in + if wrap incomplete_type loc env1 ty_ret && not (is_void_type env ty_ret) then + fatal_error loc "incomplete result type %a in function definition" + (print_typ env) ty_ret; + (ty_ret, params, vararg, attr) + | _ -> fatal_error loc "wrong type for function definition" in (* 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) @@ -2119,7 +2224,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 @@ -2129,7 +2234,7 @@ let elab_fundef env spec name defs body loc = sseq no_loc body1 {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} | _ -> - warning loc "return type of 'main' should be 'int'"; + warning loc Main_return_type "return type of 'main' should be 'int'"; body1 end else body1 in (* Add the extra declarations if any *) @@ -2140,7 +2245,7 @@ let elab_fundef env spec name defs body loc = sloc = no_loc } end in if noret && contains_return body1 then - warning loc "function '%s' declared 'noreturn' should not return" s; + warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) let fn = { fd_storage = sto1; @@ -2163,14 +2268,14 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) (* "int f(int x) { ... }" *) (* "int f(x, y) double y; { ... }" *) | FUNDEF(spec, name, defs, body, loc) -> - if local then error loc "local definition of a function"; + if local then error loc "function definition is not allowed here"; let env1 = elab_fundef env spec name defs body loc in ([], env1) (* "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) @@ -2191,9 +2296,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 @@ -2205,7 +2310,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 = @@ -2222,7 +2328,7 @@ let stmt_labels stmt = | DEFAULT(s1, _) -> do_stmt s1 | LABEL(lbl, s1, loc) -> if StringSet.mem lbl !lbls then - error loc "multiply-defined label '%s'\n" lbl; + error loc "redefinition of label '%s'\n" lbl; lbls := StringSet.add lbl !lbls; do_stmt s1 | _ -> () @@ -2242,7 +2348,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 *) @@ -2252,10 +2358,10 @@ 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 "argument of 'case' must be an integer compile-time constant" + error loc "expression of 'case' label is not an integer constant expression" | Some n -> () end; let s1,env = elab_stmt env ctx s1 in @@ -2273,9 +2379,10 @@ 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 "the condition of 'if' does not have scalar type"; + error loc "controlling expression of 'if' does not have scalar type (%a invalid)" + (print_typ env) a'.etyp; let s1',env = elab_stmt env ctx s1 in let s2',env = match s2 with @@ -2287,27 +2394,29 @@ 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 "the condition of 'while' does not have scalar type"; + error loc "controlling expression of 'while' does not have scalar type (%a invalid)" + (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_loop ctx) s1 in { sdesc = Swhile(a', s1'); sloc = elab_loc loc },env | 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 "the condition of 'while' does not have scalar type"; + error loc "controlling expression of 'while' does not have scalar type (%a invalid)" + (print_typ env) a'.etyp; { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc },env | FOR(fc, a2, a3, s1, loc) -> 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 @@ -2317,11 +2426,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 "the condition of 'for' does not have scalar type"; - let a3',env' = elab_for_expr loc env' a3 in + error loc "controlling expression of 'for' does not have scalar type (%a invalid)" (print_typ env) a2'.etyp; + 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 @@ -2331,47 +2440,50 @@ 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 "the argument of 'switch' is not an integer"; + error loc "controlling expression of 'switch' does not have integer type (%a invalid)" + (print_typ env) a'.etyp; let s1',env = elab_stmt env (ctx_switch ctx) s1 in { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env (* 6.8.6 Break and continue statements *) | BREAK loc -> if not ctx.ctx_break then - error loc "'break' outside of a loop or a 'switch'"; + error loc "'break' statement not in loop or switch statement"; { sdesc = Sbreak; sloc = elab_loc loc },env | CONTINUE loc -> if not ctx.ctx_continue then - error loc "'continue' outside of a loop"; + error loc "'continue' statement not in loop statement"; { sdesc = Scontinue; sloc = elab_loc loc },env (* 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 _ -> error loc - "'return' with a value in a function of return type 'void'" + "'return' with a value in a function returning void" | _, None -> - warning loc - "'return' without a value in a function of return type@ %a" - Cprint.typ ctx.ctx_return_typ + warning loc Return_type + "'return' with no value, in a function returning non-void" | _, Some b -> if not (wrap2 valid_assignment loc env b ctx.ctx_return_typ) then begin if wrap2 valid_cast loc env b.etyp ctx.ctx_return_typ then - warning loc - "return value has type@ %a@ \ - instead of the expected type@ %a" - Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ + if wrap2 int_pointer_conversion loc env b.etyp ctx.ctx_return_typ then + warning loc Int_conversion + "incompatible integer-pointer conversion: returning %a from a function with result type %a" + (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ + else + warning loc Unnamed + "incompatible conversion returning %a from a function with result type %a" + (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ else error loc - "return value has type@ %a@ \ - instead of the expected type@ %a" - Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ + "returning %a from a function with incompatible result type %a" + (print_typ env) b.etyp (print_typ env) ctx.ctx_return_typ end end; { sdesc = Sreturn a'; sloc = elab_loc loc },env @@ -2379,7 +2491,7 @@ let rec elab_stmt env ctx s = (* 6.8.6 Goto statements *) | GOTO(lbl, loc) -> if not (StringSet.mem lbl ctx.ctx_labels) then - error loc "unknown 'goto' label %s" lbl; + error loc "use of undeclared label '%s'" lbl; { sdesc = Sgoto lbl; sloc = elab_loc loc },env (* 6.8.3 Null statements *) @@ -2390,8 +2502,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 @@ -2424,12 +2536,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 dae79ef2..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 @@ -260,17 +263,17 @@ let composite_tag_name name = let error_message = function | Unbound_identifier name -> - sprintf "Unbound identifier '%s'" name + sprintf "use of undeclared identifier '%s'" name | Unbound_tag(name, kind) -> - sprintf "Unbound %s '%s'" kind (composite_tag_name name) + sprintf "unbound %s '%s'" kind (composite_tag_name name) | Tag_mismatch(name, expected, actual) -> sprintf "'%s' was declared as a %s but is used as a %s" (composite_tag_name name) actual expected | Unbound_typedef name -> - sprintf "Unbound typedef '%s'" name + sprintf "unbound typedef '%s'" name | No_member(compname, compkind, memname) -> - sprintf "%s '%s' has no member named '%s'" - compkind (composite_tag_name compname) memname + sprintf "no member named '%s' in '%s %s'" + memname compkind (composite_tag_name compname) let _ = Printexc.register_printer 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/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index fc228aca..30d1a0cc 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -104,14 +104,14 @@ let rec transf_inputs loc env accu pos pos' subst = function let n = match Ceval.integer_expr env e with | Some n -> n - | None -> error "%aError: asm argument of kind '%s' is not a constant" - formatloc loc cstr; + | None -> error loc "asm argument of kind '%s' is not a constant" + cstr; 0L in transf_inputs loc env accu (pos + 1) pos' (set_label_const lbl pos n subst) inputs end else begin - error "%aUnsupported feature: asm argument of kind '%s'" - formatloc loc cstr; + error loc "unsupported feature: asm argument of kind '%s'" + cstr; transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1) (set_label_reg lbl pos pos' subst) inputs end @@ -127,7 +127,7 @@ let transf_outputs loc env = function (None, [], StringMap.empty, 0, 0) | [(lbl, cstr, e)] -> if not (is_modifiable_lvalue env e) then - error "%aError: asm output is not a modifiable l-value" formatloc loc; + error loc "asm output is not a modifiable l-value"; let valid = Str.string_match re_valid_output cstr 0 in if valid && String.contains cstr 'r' then if is_reg_pair env e.etyp then @@ -139,13 +139,12 @@ let transf_outputs loc env = function (None, [eaddrof e], set_label_mem lbl 0 0 StringMap.empty, 1, 1) else begin - error "%aUnsupported feature: asm result of kind '%s'" - formatloc loc cstr; + error loc "unsupported feature: asm result of kind '%s'" + cstr; (None, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1) end | outputs -> - error "%aUnsupported feature: asm statement with 2 or more outputs" - formatloc loc; + error loc "unsupported feature: asm statement with 2 or more outputs"; (* Bind the outputs so that we don't get another error when substituting the text *) let rec bind_outputs pos subst = function @@ -163,8 +162,7 @@ let check_clobbers loc clob = || Machregsaux.is_scratch_register c || c = "memory" || c = "cc" (* GCC does not accept MEMORY or CC *) then () - else error "%aError: unrecognized asm register clobber '%s'" - formatloc loc c) + else error loc "unrecognized asm register clobber '%s'" c) clob (* Renaming of the %nnn and %[ident] placeholders in the asm text *) @@ -178,8 +176,7 @@ let rename_placeholders loc template subst = try StringMap.find p subst with Not_found -> - error "%aError: '%s' in asm text does not designate any operand" - formatloc loc p; + error loc"'%s' in asm text does not designate any operand" p; "%<error>" in Str.global_substitute re_asm_placeholder diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index d3747e22..71aad604 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -126,16 +126,16 @@ let currentLoc = (* Error reporting *) let fatal_error lb fmt = - Cerrors.fatal_error ("%s:%d: Error:@ " ^^ fmt) - lb.lex_curr_p.pos_fname lb.lex_curr_p.pos_lnum + Cerrors.fatal_error + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let error lb fmt = - Cerrors.error ("%s:%d: Error:@ " ^^ fmt) - lb.lex_curr_p.pos_fname lb.lex_curr_p.pos_lnum + Cerrors.error + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt let warning lb fmt = - Cerrors.warning ("%s:%d: Warning:@ " ^^ fmt) - lb.lex_curr_p.pos_fname lb.lex_curr_p.pos_lnum + Cerrors.warning + (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Cerrors.Unnamed ("warning: " ^^ fmt) (* Simple character escapes *) 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/PackedStructs.ml b/cparser/PackedStructs.ml index aafa1caa..a921e2d8 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -48,7 +48,7 @@ let safe_alignof loc env ty = match alignof env ty with | Some al -> al | None -> - error "%aError: incomplete type for a struct field" formatloc loc; 1 + error loc "incomplete type for a struct field"; 1 (* Remove existing [_Alignas] attributes and add the given [_Alignas] attr. *) @@ -61,14 +61,13 @@ let set_alignas_attr al attrs = let transf_field_decl mfa swapped loc env struct_id f = if f.fld_bitfield <> None then - error "%aError: bitfields in packed structs not allowed" - formatloc loc; + error loc "bitfields in packed structs not allowed"; (* Register as byte-swapped if needed *) if swapped then begin let (can_swap, must_swap) = can_byte_swap env f.fld_typ in if not can_swap then - error "%aError: cannot byte-swap field of type '%a'" - formatloc loc Cprint.typ f.fld_typ; + error loc "cannot byte-swap field of type '%a'" + Cprint.typ f.fld_typ; if must_swap then Hashtbl.add byteswapped_fields (struct_id, f.fld_name) () end; @@ -99,11 +98,11 @@ let is_pow2 n = n > 0 && n land (n - 1) = 0 let packed_param_value loc n = let m = Int64.to_int n in if n <> Int64.of_int m then - (error "%a: __packed__ parameter `%Ld' is too large" formatloc loc n; 0) + (error loc "__packed__ parameter `%Ld' is too large" n; 0) else if m = 0 || is_pow2 m then m else - (error "%a: __packed__ parameter `%Ld' must be a power of 2" formatloc loc n; 0) + (error loc "__packed__ parameter `%Ld' must be a power of 2" n; 0) let transf_composite loc env su id attrs ml = match su with @@ -117,8 +116,7 @@ let transf_composite loc env su id attrs ml = | [[AInt n; AInt p]] -> (n, p, false) | [[AInt n; AInt p; AInt q]] -> (n, p, q <> 0L) | _ -> - error "%a: ill-formed or ambiguous __packed__ attribute" - formatloc loc; + error loc "ill-formed or ambiguous __packed__ attribute"; (0L, 0L, false) in let mfa = packed_param_value loc mfa in let msa = packed_param_value loc msa in @@ -140,7 +138,7 @@ let accessor_type loc env ty = | TEnum(_,_) -> (8 * sizeof_ikind enum_ikind, TInt(unsigned_ikind_of enum_ikind,[])) | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind(),[])) | _ -> - error "%a: unsupported type for byte-swapped field access" formatloc loc; + error loc "unsupported type for byte-swapped field access"; (32, TVoid []) (* (ty) e *) @@ -175,7 +173,7 @@ let bswap_read loc env lval = ecast_opt env ty call end with Env.Error msg -> - fatal_error "%aError: %s" formatloc loc (Env.error_message msg) + fatal_error loc "%s" (Env.error_message msg) (* __builtin_write_intNN_reversed(&lhs,rhs) or lhs = __builtin_bswapNN(rhs) *) @@ -202,7 +200,7 @@ let bswap_write loc env lhs rhs = eassign lhs (ecast_opt env ty call) end with Env.Error msg -> - fatal_error "%aError: %s" formatloc loc (Env.error_message msg) + fatal_error loc "%s" (Env.error_message msg) (* Expressions *) @@ -248,7 +246,7 @@ let transf_expr loc env ctx e = | EUnop(Oaddrof, e1) -> let (e1', swap) = lvalue e1 in if swap then - error "%aError: & over byte-swapped field" formatloc loc; + error loc "& over byte-swapped field"; {edesc = EUnop(Oaddrof, e1'); etyp = e.etyp} | EUnop((Opreincr|Opredecr) as op, e1) -> @@ -349,8 +347,8 @@ let transf_init loc env i = let n' = byteswap_int (sizeof_ikind ik) n in Init_single {edesc = EConst(CInt(n', ik, "")); etyp = e.etyp} | _ -> - error "%aError: initializer for byte-swapped field is not \ - a compile-time integer constant" formatloc loc; i + error loc "initializer for byte-swapped field is not \ + a compile-time integer constant"; i end | Init_array il -> let swap_elt = diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 3f60ebb4..507aea36 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -70,7 +70,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Cerrors.fatal_error "Internal error while parsing" + Cerrors.fatal_error Cutil.no_loc "Internal error while parsing" | 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 diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 664f6a28..c62c6763 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -94,7 +94,7 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" + Cerrors.fatal_error no_loc "internal error: rename: %s__%d unbound" id.name id.stamp let rec typ env = function @@ -292,4 +292,3 @@ let program p file = globdecls (reserve_public (reserve_builtins()) file p) [] p - diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 0669be6e..87b2f9bb 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -32,7 +32,7 @@ let rec local_initializer env path init k = let (ty_elt, sz) = match unroll env path.etyp with | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) - | _ -> fatal_error "Wrong type for array initializer" in + | _ -> fatal_error no_loc "Wrong type for array initializer" in let rec array_init pos il = if pos >= sz then k else begin let (i1, il') = diff --git a/driver/Commandline.ml b/driver/Commandline.ml index d125736a..c0dd6257 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -32,6 +32,8 @@ type action = | Self of (string -> unit) | String of (string -> unit) | Integer of (int -> unit) + | Ignore + | Unit of (unit -> unit) let match_pattern text = function | Exact s -> @@ -96,6 +98,13 @@ let parse_array spec argv first last = end else begin eprintf "Option `%s' expects an argument\n" s; exit 2 end + | Some (Ignore) -> + if i + 1 <= last then begin + parse (i+2) + end else begin + eprintf "Option `%s' expects an argument\n" s; exit 2 + end + | Some (Unit f) -> f (); parse (i+1) end in parse first diff --git a/driver/Commandline.mli b/driver/Commandline.mli index 79786678..197d0b04 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -33,6 +33,8 @@ type action = | Self of (string -> unit) (** call the function with the matched string *) | String of (string -> unit) (** read next arg as a string, call function *) | Integer of (int -> unit) (** read next arg as an int, call function *) + | Ignore (** ignore the next arg *) + | Unit of (unit -> unit) (** call the function with unit as argument *) val parse_cmdline: (pattern * action) list -> unit diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 0a2b3eec..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 diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 7087c3c2..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 *) diff --git a/driver/Driver.ml b/driver/Driver.ml index eccd233c..b89d93c1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -23,6 +23,7 @@ let dump_options = ref false (* Optional sdump suffix *) let sdump_suffix = ref ".json" +let sdump_folder = ref "" (* Dump Asm code in asm format for the validator *) @@ -59,8 +60,11 @@ let compile_c_ast sourcename csyntax ofile = eprintf "%s: %a" sourcename print_error msg; exit 2 in (* Dump Asm in binary and JSON format *) - if !option_sdump then - dump_jasm asm sourcename (output_filename sourcename ".c" !sdump_suffix); + if !option_sdump then begin + let sf = output_filename sourcename ".c" !sdump_suffix in + let csf = Filename.concat !sdump_folder sf in + dump_jasm asm sourcename csf + end; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm; @@ -341,18 +345,19 @@ General options:\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\ -\ @<file> Read command line options from <file>\n\ -Interpreter mode:\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\ \ -quiet Suppress diagnostic messages for the interpreter\n\ \ -trace Have the interpreter produce a detailed trace of reductions\n\ \ -random Randomize execution order\n\ \ -all Simulate all possible execution orders\n" -let print_usage_and_exit _ = +let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit _ = +let print_version_and_exit () = printf "%s" version_string; exit 0 let language_support_options = [ @@ -365,8 +370,8 @@ let optimization_options = [ option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy ] -let set_all opts = List.iter (fun r -> r := true) opts -let unset_all opts = List.iter (fun r -> r := false) opts +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts let num_source_files = ref 0 @@ -375,13 +380,16 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in + let dwarf_version version () = + option_g:=true; + option_gdwarf := version in [ (* Getting help *) - Exact "-help", Self print_usage_and_exit; - Exact "--help", Self print_usage_and_exit; + Exact "-help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit; (* Getting version info *) - Exact "-version", Self print_version_and_exit; - Exact "--version", Self print_version_and_exit; + Exact "-version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; @@ -392,17 +400,15 @@ let cmdline_actions = (* Preprocessing options *) @ prepro_actions @ (* Language support options -- more below *) - [ Exact "-fall", Self (fun _ -> set_all language_support_options); - Exact "-fnone", Self (fun _ -> unset_all language_support_options); + [ Exact "-fall", Unit (set_all language_support_options); + Exact "-fnone", Unit (unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; - option_gdwarf := 3);] @ + Exact "-g", Unit (dwarf_version 3);] @ (if gnu_system then - [ Exact "-gdwarf-2", Self (fun s -> option_g:=true; - option_gdwarf := 2); - Exact "-gdwarf-3", Self (fun s -> option_g := true; - option_gdwarf := 3);] else []) @ - [ Exact "-frename-static", Self (fun s -> option_rename_static:= true); + [ Exact "-gdwarf-2", Unit (dwarf_version 2); + Exact "-gdwarf-3", Unit (dwarf_version 3);] + else []) @ + [ Exact "-frename-static", Set option_rename_static; Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin @@ -410,9 +416,9 @@ let cmdline_actions = option_gdepth := if n > 3 then 3 else n end); (* Code generation options -- more below *) - Exact "-O0", Self (fun _ -> unset_all optimization_options); - Exact "-O", Self (fun _ -> set_all optimization_options); - _Regexp "-O[123]$", Self (fun _ -> set_all optimization_options); + Exact "-O0", Unit (unset_all optimization_options); + Exact "-O", Unit (set_all optimization_options); + _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); @@ -421,8 +427,8 @@ let cmdline_actions = Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) - Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-target", String (fun _ -> ());] @ (* Ignore option since it is already handled *) + Exact "-conf", Ignore; (* Ignore option since it is already handled *) + Exact "-target", Ignore;] @ (* Ignore option since it is already handled *) (if Configuration.arch = "arm" then [ Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; ] @@ -455,18 +461,20 @@ let cmdline_actions = dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); + Exact "-sdump-folder", String (fun s -> sdump_folder := s); Exact "-doptions", Set dump_options; (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-timings", Set option_timings; - Exact "-Werror", Set Cerrors.warn_error; + Exact "-timings", Set option_timings;] @ +(* Diagnostic options *) + Cerrors.warning_options @ (* Interpreter mode *) - Exact "-interp", Set option_interp; - Exact "-quiet", Self (fun _ -> Interp.trace := 0); - Exact "-trace", Self (fun _ -> Interp.trace := 2); - Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); - Exact "-all", Self (fun _ -> Interp.mode := Interp.All) + [ Exact "-interp", Set option_interp; + Exact "-quiet", Unit (fun () -> Interp.trace := 0); + Exact "-trace", Unit (fun () -> Interp.trace := 2); + Exact "-random", Unit (fun () -> Interp.mode := Interp.Random); + Exact "-all", Unit (fun () -> Interp.mode := Interp.All) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @@ -525,7 +533,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 33cd9215..d25301d2 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -28,14 +28,6 @@ let rec waitpid_no_intr 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 argv = Array.of_list args in assert (Array.length argv > 0); try @@ -59,6 +51,14 @@ let command stdout args = -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 diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 0a586acd..f272c3ed 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -98,10 +98,10 @@ Tracing options:\n\ General options:\n\ \ -v Print external commands before invoking them\n" -let print_usage_and_exit _ = +let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit _ = +let print_version_and_exit () = printf "%s" version_string; exit 0 let language_support_options = [ @@ -110,26 +110,26 @@ let language_support_options = [ option_fpacked_structs; option_finline_asm ] -let set_all opts = List.iter (fun r -> r := true) opts -let unset_all opts = List.iter (fun r -> r := false) opts +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ (* Getting help *) - Exact "-help", Self print_usage_and_exit; - Exact "--help", Self print_usage_and_exit; + Exact "-help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit; (* Getting version info *) - Exact "-version", Self print_version_and_exit; - Exact "--version", Self print_version_and_exit; + Exact "-version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit; (* Processing options *) Exact "-E", Set option_E;] (* Preprocessing options *) @ prepro_actions @ (* Language support options -- more below *) - [Exact "-fall", Self (fun _ -> set_all language_support_options); - Exact "-fnone", Self (fun _ -> unset_all language_support_options); + [Exact "-fall", Unit (set_all language_support_options); + Exact "-fnone", Unit (unset_all language_support_options); (* Tracing options *) Exact "-dparse", Set option_dparse; Exact "-dc", Set option_dcmedium; @@ -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/extraction/extraction.v b/extraction/extraction.v index e7f2e2fc..8e13264c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -12,6 +12,7 @@ Require Coqlib. Require Wfsimpl. +Require DecidableClass Decidableplus. Require AST. Require Iteration. Require Floats. @@ -39,6 +40,12 @@ Require Import ExtrOcamlString. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". +(* Decidable *) + +Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide + Decidableplus.Decidable_and Decidableplus.Decidable_or + Decidableplus.Decidable_not Decidableplus.Decidable_implies. + (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. @@ -159,12 +166,13 @@ Separate Extraction Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr Ctypes.make_program - Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs - Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs + Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs + Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg + Machregs.destroyed_at_indirect_call AST.signature_main Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol @@ -151,6 +151,7 @@ Inductive instruction: Type := | Pimul_ri (rd: ireg) (n: int) | Pimul_r (r1: ireg) | Pmul_r (r1: ireg) + | Pcltd | Pdiv (r1: ireg) | Pidiv (r1: ireg) | Pand_rr (rd: ireg) (r1: ireg) @@ -618,17 +619,25 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmul_r r1 => Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1) #EDX <- (Val.mulhu rs#EAX rs#r1))) m + | Pcltd => + Next (nextinstr_nf (rs#EDX <- (Val.shr rs#EAX (Vint (Int.repr 31))))) m | Pdiv r1 => - let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in - match Val.divu vn vd, Val.modu vn vd with - | Some vq, Some vr => Next (nextinstr_nf (rs#EAX <- vq #EDX <- vr)) m - | _, _ => Stuck + match rs#EDX, rs#EAX, rs#r1 with + | Vint nh, Vint nl, Vint d => + match Int.divmodu2 nh nl d with + | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m + | None => Stuck + end + | _, _, _ => Stuck end | Pidiv r1 => - let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in - match Val.divs vn vd, Val.mods vn vd with - | Some vq, Some vr => Next (nextinstr_nf (rs#EAX <- vq #EDX <- vr)) m - | _, _ => Stuck + match rs#EDX, rs#EAX, rs#r1 with + | Vint nh, Vint nl, Vint d => + match Int.divmods2 nh nl d with + | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m + | None => Stuck + end + | _, _, _ => Stuck end | Pand_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.and rs#rd rs#r1))) m diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index fd0d5bc5..1d718c26 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -315,22 +315,22 @@ Definition transl_op assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res AX); - OK(Pidiv ECX :: k) + OK(Pcltd :: Pidiv ECX :: k) | Odivu, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res AX); - OK(Pdiv ECX :: k) + OK(Pxor_r EDX :: Pdiv ECX :: k) | Omod, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res DX); - OK(Pidiv ECX :: k) + OK(Pcltd :: Pidiv ECX :: k) | Omodu, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); assertion (mreg_eq res DX); - OK(Pdiv ECX :: k) + OK(Pxor_r EDX :: Pdiv ECX :: k) | Oand, a1 :: a2 :: nil => assertion (mreg_eq a1 res); do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pand_rr r r2 :: k) diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 60cc266e..9703d419 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -121,28 +121,44 @@ Qed. (** Properties of division *) -Remark divs_mods_exist: +Lemma divu_modu_exists: forall v1 v2, - match Val.divs v1 v2, Val.mods v1 v2 with - | Some _, Some _ => True - | None, None => True - | _, _ => False - end. + Val.divu v1 v2 <> None \/ Val.modu v1 v2 <> None -> + exists n d q r, + v1 = Vint n /\ v2 = Vint d + /\ Int.divmodu2 Int.zero n d = Some(q, r) + /\ Val.divu v1 v2 = Some (Vint q) /\ Val.modu v1 v2 = Some (Vint r). Proof. - intros. unfold Val.divs, Val.mods. destruct v1; auto. destruct v2; auto. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto. + intros v1 v2; unfold Val.divu, Val.modu. + destruct v1; try (intuition discriminate). + destruct v2; try (intuition discriminate). + predSpec Int.eq Int.eq_spec i0 Int.zero ; try (intuition discriminate). + intros _. exists i, i0, (Int.divu i i0), (Int.modu i i0); intuition auto. + apply Int.divmodu2_divu_modu; auto. Qed. -Remark divu_modu_exist: +Lemma divs_mods_exists: forall v1 v2, - match Val.divu v1 v2, Val.modu v1 v2 with - | Some _, Some _ => True - | None, None => True - | _, _ => False - end. + Val.divs v1 v2 <> None \/ Val.mods v1 v2 <> None -> + exists nh nl d q r, + Val.shr v1 (Vint (Int.repr 31)) = Vint nh /\ v1 = Vint nl /\ v2 = Vint d + /\ Int.divmods2 nh nl d = Some(q, r) + /\ Val.divs v1 v2 = Some (Vint q) /\ Val.mods v1 v2 = Some (Vint r). Proof. - intros. unfold Val.divu, Val.modu. destruct v1; auto. destruct v2; auto. - destruct (Int.eq i0 Int.zero); auto. + intros v1 v2; unfold Val.divs, Val.mods. + destruct v1; try (intuition discriminate). + destruct v2; try (intuition discriminate). + destruct (Int.eq i0 Int.zero + || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:OK; + try (intuition discriminate). + intros _. + InvBooleans. + exists (Int.shr i (Int.repr 31)), i, i0, (Int.divs i i0), (Int.mods i i0); intuition auto. + rewrite Int.shr_lt_zero. apply Int.divmods2_divs_mods. + red; intros; subst i0; rewrite Int.eq_true in H; discriminate. + revert H0. predSpec Int.eq Int.eq_spec i (Int.repr Int.min_signed); auto. + predSpec Int.eq Int.eq_spec i0 Int.mone; auto. + discriminate. Qed. (** Smart constructor for [shrx] *) @@ -1031,32 +1047,52 @@ Transparent destroyed_by_op. apply SAME. TranslOp. destruct H1. Simplifs. (* div *) apply SAME. - specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.mods (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divs_mods_exists (rs EAX) (rs ECX)). left; congruence. + intros (nh & nl & d & q & r & A & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- (Vint nh))). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint q = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* divu *) apply SAME. - specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.modu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divu_modu_exists (rs EAX) (rs ECX)). left; congruence. + intros (n & d & q & r & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- Vzero)). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint q = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* mod *) apply SAME. - specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.divs (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divs_mods_exists (rs EAX) (rs ECX)). right; congruence. + intros (nh & nl & d & q & r & A & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- (Vint nh))). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint r = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* modu *) apply SAME. - specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. - destruct (Val.divu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. - TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. - auto. auto. - simpl in H3. destruct H3; Simplifs. + exploit (divu_modu_exists (rs EAX) (rs ECX)). right; congruence. + intros (n & d & q & r & B & C & D & E & F). + set (rs1 := nextinstr_nf (rs#EDX <- Vzero)). + econstructor; split. + eapply exec_straight_two with (rs2 := rs1). reflexivity. + simpl. change (rs1 EAX) with (rs EAX); rewrite B. + change (rs1 ECX) with (rs ECX); rewrite C. + rewrite D. reflexivity. auto. auto. + split. change (Vint r = v). congruence. + simpl; intros. destruct H2. unfold rs1; Simplifs. (* shrximm *) apply SAME. eapply mk_shrximm_correct; eauto. (* lea *) diff --git a/ia32/Machregs.v b/ia32/Machregs.v index fb80a1fd..3a6ae674 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -55,7 +55,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -166,6 +166,9 @@ Definition destroyed_at_function_entry: list mreg := (* must include [destroyed_by_setstack ty] *) DX :: FP0 :: nil. +Definition destroyed_at_indirect_call: list mreg := + nil. + Definition destroyed_by_setstack (ty: typ): list mreg := match ty with | Tfloat | Tsingle => FP0 :: nil @@ -210,6 +213,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_indirect_call destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame mregs_for_operation mregs_for_builtin. diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 979ac800..4ffb701b 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -421,11 +421,11 @@ module Target(System: SYSTEM):TARGET = fprintf oc " imull %a\n" ireg r1 | Pmul_r(r1) -> fprintf oc " mull %a\n" ireg r1 + | Pcltd -> + fprintf oc " cltd\n" | Pdiv(r1) -> - fprintf oc " xorl %%edx, %%edx\n"; fprintf oc " divl %a\n" ireg r1 | Pidiv(r1) -> - fprintf oc " cltd\n"; fprintf oc " idivl %a\n" ireg r1 | Pand_rr(rd, r1) -> fprintf oc " andl %a, %a\n" ireg r1 ireg rd diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 6fa82492..18d4d7e1 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1200,7 +1200,7 @@ Proof. subst; exists b1; auto. exploit IHlist_forall2; eauto. intros (x2 & U & V); exists x2; auto. Qed. - + Lemma list_forall2_in_right: forall x2 l1 l2, list_forall2 l1 l2 -> In x2 l2 -> exists x1, In x1 l1 /\ P x1 x2. @@ -1209,7 +1209,7 @@ Proof. subst; exists a1; auto. exploit IHlist_forall2; eauto. intros (x1 & U & V); exists x1; auto. Qed. - + End FORALL2. Lemma list_forall2_imply: @@ -1277,11 +1277,9 @@ Qed. (** * Definitions and theorems over boolean types *) -Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := +Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool := if a then true else false. -Implicit Arguments proj_sumbool [P Q]. - Coercion proj_sumbool: sumbool >-> bool. Lemma proj_sumbool_true: diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 932b885a..3bb6eee7 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -19,56 +19,9 @@ of Coq 8.5 with more instances of decidable properties, including universal and existential quantification over finite types. *) -(** Temporarily and for compatibility with Coq 8.4, this file includes - a copy of the relevant definitions from the Coq 8.5 [DecidableClass] - library. This library is copyright INRIA. *) - +Require Export DecidableClass. Require Import Coqlib. -Class Decidable (P : Prop) := { - Decidable_witness : bool; - Decidable_spec : Decidable_witness = true <-> P -}. - -Lemma Decidable_sound : forall P (H : Decidable P), - Decidable_witness = true -> P. -Proof. - intros. rewrite <- Decidable_spec. auto. -Qed. - -Lemma Decidable_complete : forall P (H : Decidable P), - P -> Decidable_witness = true. -Proof. - intros. rewrite Decidable_spec. auto. -Qed. - -Lemma Decidable_sound_alt : forall P (H : Decidable P), - ~ P -> Decidable_witness = false. -Proof. - intros. destruct Decidable_witness eqn:E; auto. elim H0. eapply Decidable_sound; eauto. -Qed. - -Lemma Decidable_complete_alt : forall P (H : Decidable P), - Decidable_witness = false -> ~ P. -Proof. - intros; red; intros. rewrite (Decidable_complete P H) in H0 by auto. discriminate. -Qed. - -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). - -Ltac _decide_ P H := - let b := fresh "b" in - set (b := decide P) in *; - assert (H : decide P = b) by reflexivity; - clearbody b; - destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H]. - -Tactic Notation "decide" constr(P) "as" ident(H) := - _decide_ P H. - -Tactic Notation "decide" constr(P) := - let H := fresh "H" in _decide_ P H. - Ltac decide_goal := eapply Decidable_sound; reflexivity. (** Deciding logical connectives *) @@ -169,6 +122,34 @@ Next Obligation. apply Z.ltb_lt. Qed. +Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { + Decidable_witness := Z.geb x y +}. +Next Obligation. + rewrite Z.geb_le. intuition omega. +Qed. + +Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { + Decidable_witness := Z.gtb x y +}. +Next Obligation. + rewrite Z.gtb_lt. intuition omega. +Qed. + +Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { + Decidable_witness := Z.eqb y ((y / x) * x)%Z +}. +Next Obligation. + split. + intros. apply Z.eqb_eq in H. exists (y / x). auto. + intros [k EQ]. apply Z.eqb_eq. + destruct (Z.eq_dec x 0). + subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity. + assert (k = y / x). + { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. } + congruence. +Qed. + (** Deciding properties over lists *) Program Instance Decidable_forall_in_list : diff --git a/lib/Integers.v b/lib/Integers.v index 316dfb52..16c95e01 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -403,6 +403,18 @@ Definition is_false (x: int) : Prop := x = zero. Definition is_true (x: int) : Prop := x <> zero. Definition notbool (x: int) : int := if eq x zero then one else zero. +(** x86-style extended division and modulus *) + +Definition divmodu2 (nhi nlo: int) (d: int) : option (int * int) := + if eq_dec d zero then None else + (let (q, r) := Z.div_eucl (unsigned nhi * modulus + unsigned nlo) (unsigned d) in + if zle q max_unsigned then Some(repr q, repr r) else None). + +Definition divmods2 (nhi nlo: int) (d: int) : option (int * int) := + if eq_dec d zero then None else + (let (q, r) := Z.quotrem (signed nhi * modulus + unsigned nlo) (signed d) in + if zle min_signed q && zle q max_signed then Some(repr q, repr r) else None). + (** * Properties of integers and integer arithmetic *) (** ** Properties of [modulus], [max_unsigned], etc. *) @@ -1193,6 +1205,86 @@ Proof. rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. Qed. +Theorem divmodu2_divu_modu: + forall n d, + d <> zero -> divmodu2 zero n d = Some (divu n d, modu n d). +Proof. + unfold divmodu2, divu, modu; intros. + rewrite dec_eq_false by auto. + set (N := unsigned zero * modulus + unsigned n). + assert (E1: unsigned n = N) by (unfold N; rewrite unsigned_zero; ring). rewrite ! E1. + set (D := unsigned d). + set (Q := N / D); set (R := N mod D). + assert (E2: Z.div_eucl N D = (Q, R)). + { unfold Q, R, Z.div, Z.modulo. destruct (Z.div_eucl N D); auto. } + rewrite E2. rewrite zle_true. auto. + assert (unsigned d <> 0). + { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. } + assert (0 < D). + { unfold D. generalize (unsigned_range d); intros. omega. } + assert (0 <= Q <= max_unsigned). + { unfold Q. apply Zdiv_interval_2. + rewrite <- E1; apply unsigned_range_2. + omega. unfold max_unsigned; generalize modulus_pos; omega. omega. } + omega. +Qed. + +Lemma unsigned_signed: + forall n, unsigned n = if lt n zero then signed n + modulus else signed n. +Proof. + intros. unfold lt. rewrite signed_zero. unfold signed. + generalize (unsigned_range n). rewrite half_modulus_modulus. intros. + destruct (zlt (unsigned n) half_modulus). +- rewrite zlt_false by omega. auto. +- rewrite zlt_true by omega. ring. +Qed. + +Theorem divmods2_divs_mods: + forall n d, + d <> zero -> n <> repr min_signed \/ d <> mone -> + divmods2 (if lt n zero then mone else zero) n d = Some (divs n d, mods n d). +Proof. + unfold divmods2, divs, mods; intros. + rewrite dec_eq_false by auto. + set (N := signed (if lt n zero then mone else zero) * modulus + unsigned n). + set (D := signed d). + assert (D <> 0). + { unfold D; red; intros. elim H. rewrite <- (repr_signed d). rewrite H1; auto. } + assert (N = signed n). + { unfold N. rewrite unsigned_signed. destruct (lt n zero). + rewrite signed_mone. ring. + rewrite signed_zero. ring. } + set (Q := Z.quot N D); set (R := Z.rem N D). + assert (E2: Z.quotrem N D = (Q, R)). + { unfold Q, R, Z.quot, Z.rem. destruct (Z.quotrem N D); auto. } + rewrite E2. + assert (min_signed <= N <= max_signed) by (rewrite H2; apply signed_range). + assert (min_signed <= Q <= max_signed). + { unfold Q. destruct (zeq D 1); [ | destruct (zeq D (-1))]. + - (* D = 1 *) + rewrite e. rewrite Z.quot_1_r; auto. + - (* D = -1 *) + rewrite e. change (-1) with (Z.opp 1). rewrite Z.quot_opp_r by omega. + rewrite Z.quot_1_r. + assert (N <> min_signed). + { red; intros; destruct H0. + + elim H0. rewrite <- (repr_signed n). rewrite <- H2. rewrite H4. auto. + + elim H0. rewrite <- (repr_signed d). unfold D in e; rewrite e; auto. } + unfold min_signed, max_signed in *. omega. + - (* |D| > 1 *) + assert (Z.abs (Z.quot N D) < half_modulus). + { rewrite <- Z.quot_abs by omega. apply Zquot_lt_upper_bound. + xomega. xomega. + apply Zle_lt_trans with (half_modulus * 1). + rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega. + apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. } + rewrite Z.abs_lt in H4. + unfold min_signed, max_signed; omega. + } + unfold proj_sumbool; rewrite ! zle_true by omega; simpl. + unfold Q, R; rewrite H2; auto. +Qed. + (** ** Bit-level properties *) (** ** Properties of bit-level operations over [Z] *) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 24065254..ce9c3542 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -76,7 +76,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -210,6 +210,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg := Definition destroyed_at_function_entry: list mreg := nil. +Definition destroyed_at_indirect_call: list mreg := + nil. + Definition temp_for_parent_frame: mreg := R11. @@ -230,6 +233,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_at_indirect_call destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame mregs_for_operation mregs_for_builtin. 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 |