From a28cb16aeb266fd41c0ce2ddbe0a0d8d2cbf20de Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 7 Jul 2015 17:50:55 +0200 Subject: Diab defines w_char to be unsigned short. --- cparser/Cutil.ml | 3 ++- cparser/Machine.ml | 4 ++++ cparser/Machine.mli | 1 + 3 files changed, 7 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 221bd7cc..a3c05c34 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -721,7 +721,8 @@ let type_of_member env fld = let find_matching_unsigned_ikind sz = assert (sz > 0); - if sz = !config.sizeof_int then IUInt + if sz = !config.sizeof_short then IUShort + else if sz = !config.sizeof_int then IUInt else if sz = !config.sizeof_long then IULong else if sz = !config.sizeof_longlong then IULongLong else assert false diff --git a/cparser/Machine.ml b/cparser/Machine.ml index bd6489fd..7a12c649 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -170,6 +170,10 @@ let ppc_32_bigendian = bitfields_msb_first = true; supports_unaligned_accesses = true } +let ppc_32_diab_bigendian = + { ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false } + + let arm_littleendian = { ilp32ll64 with name = "arm" } diff --git a/cparser/Machine.mli b/cparser/Machine.mli index fb7321f9..277ac3fb 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -62,6 +62,7 @@ val x86_64 : t val win32 : t val win64 : t val ppc_32_bigendian : t +val ppc_32_diab_bigendian : t val arm_littleendian : t val gcc_extensions : t -> t -- cgit From 4717443c519f5d6426c165de545952b2b7ef50f9 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Tue, 7 Jul 2015 18:07:31 +0200 Subject: Change the definition of Typles.tuple --- cparser/validator/Tuples.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'cparser') diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v index 88dc46e9..3fd2ec03 100644 --- a/cparser/validator/Tuples.v +++ b/cparser/validator/Tuples.v @@ -26,8 +26,11 @@ Definition arrows_right: Type -> list Type -> Type := fold_right (fun A B => A -> B). (** A tuple is a heterogeneous list. For convenience, we use pairs. **) -Definition tuple (types:list Type) : Type := - fold_right prod unit types. +Fixpoint tuple (types : list Type) : Type := + match types with + | nil => unit + | t::q => prod t (tuple q) + end. Fixpoint uncurry {args:list Type} {res:Type}: arrows_left args res -> tuple args -> res := -- cgit From 2b1c0aa69adafac185dd6c4e460d83517bcc8884 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 8 Jul 2015 10:16:53 +0200 Subject: Fix issue with bit fields of type _Bool cparser/Bitfields.ml: when assigning to a bit field of type _Bool, the right-hand side must be normalized to 0 or 1 via a cast to _Bool. test/regression/bitfields{1,9}.c: add corresponding test cases. --- cparser/Bitfields.ml | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) (limited to 'cparser') diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 570572fa..6569bb4c 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -31,7 +31,8 @@ type bitfield_info = bf_pos: int; (* start bit *) bf_size: int; (* size in bit *) bf_signed: bool; (* is field signed or unsigned? *) - bf_signed_res: bool (* is result of extracting field signed or unsigned? *) + bf_signed_res: bool; (* is result of extracting field signed or unsigned? *) + bf_bool: bool (* does field have type _Bool? *) } (* invariants: @@ -100,7 +101,13 @@ let pack_bitfields env sid ml = match unroll env (type_of_member env m) with | TInt(ik, _) -> is_signed_ikind ik | _ -> assert false (* should never happen, checked in Elab *) in - pack ((m.fld_name, pos, n, signed, signed2) :: accu) (pos + n) ms + let is_bool = + match unroll env m.fld_typ with + | TInt(IBool, _) -> true + | _ -> false in + + pack ((m.fld_name, pos, n, signed, signed2, is_bool) :: accu) + (pos + n) ms end in pack [] 0 ml @@ -121,7 +128,7 @@ let rec transf_members env id count = function let carrier_typ = TInt(carrier_ikind, []) in (* Enter each field with its bit position, size, signedness *) List.iter - (fun (name, pos, sz, signed, signed2) -> + (fun (name, pos, sz, signed, signed2, is_bool) -> if name <> "" then begin let pos' = if !config.bitfields_msb_first @@ -131,7 +138,8 @@ let rec transf_members env id count = function (id, name) {bf_carrier = carrier; bf_carrier_typ = carrier_typ; bf_pos = pos'; bf_size = sz; - bf_signed = signed; bf_signed_res = signed2} + bf_signed = signed; bf_signed_res = signed2; + bf_bool = is_bool} end) bitfields; { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None} @@ -208,13 +216,16 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y) return (x & ~mask) | ((y << ofs) & mask); } +If the bitfield is of type _Bool, the new value (y above) must be converted +to _Bool to normalize it to 0 or 1. *) let bitfield_assign env bf carrier newval = let msk = insertion_mask bf in let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in let newval_casted = - ecast (TInt(IUInt,[])) newval in + ecast (TInt(IUInt,[])) + (if bf.bf_bool then ecast (TInt(IBool,[])) newval else newval) in let newval_shifted = eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in let newval_masked = ebinint env Oand newval_shifted msk @@ -230,17 +241,22 @@ unsigned int bitfield_init(int ofs, int sz, unsigned int y) unsigned int mask = (1U << sz) - 1; return (y & mask) << ofs; } + +If the bitfield is of type _Bool, the new value (y above) must be converted +to _Bool to normalize it to 0 or 1. *) let bitfield_initializer bf i = match i with | Init_single e -> let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in + let e_cast = + if bf.bf_bool then ecast (TInt(IBool,[])) e else e in let e_mask = {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])} in let e_and = - {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[])); + {edesc = EBinop(Oand, e_cast, e_mask, TInt(IUInt,[])); etyp = TInt(IUInt,[])} in {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, TInt(IUInt, [])); -- cgit From cbcf2f8950d0ea7208d9c021422946433f90e745 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 8 Jul 2015 10:49:36 +0200 Subject: Turn "redefinition with an incompatible type" warning into an error. Also: improve error message by showing old and new types. --- cparser/Elab.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d6b79780..5be4c598 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1805,7 +1805,12 @@ let enter_or_refine_ident local loc env s sto ty = | Some new_ty -> new_ty | None -> - warning loc "redefinition of '%s' with incompatible type" s; ty in + error loc + "redefinition of '%s' with incompatible type.@ \ + Previous type: %a.@ \ + New type: %a" + s Cprint.typ old_ty Cprint.typ ty; + ty in let new_sto = (* The only case not allowed is removing static *) match old_sto,sto with -- cgit From 3eb2b3b7bb464d9844f7c161fbcff53f597348b9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 8 Jul 2015 11:24:09 +0200 Subject: Add implicit "return 0;" at end of function "main". As per ISO C99, "hosted environment". "return 0" is added at the end of any function named "main" that has "int" as return type. If the name is "main" but the return type is not "int", emit a warning and do not add anything. --- cparser/Elab.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 5be4c598..5533105a 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1899,6 +1899,18 @@ let elab_fundef env spec name body loc = emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body' = !elab_funbody_f ty_ret env3 body in + (* Special treatment of the "main" function *) + let body'' = + if s = "main" then begin + match unroll env ty_ret with + | TInt(IInt, []) -> + (* Add implicit "return 0;" at end of function body *) + sseq no_loc body' + {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + | _ -> + warning loc "return type of 'main' should be 'int'"; + body' + end else body' in (* Build and emit function definition *) let fn = { fd_storage = sto1; @@ -1909,7 +1921,7 @@ let elab_fundef env spec name body loc = fd_params = params; fd_vararg = vararg; fd_locals = []; - fd_body = body' } in + fd_body = body'' } in emit_elab loc (Gfundef fn); env1 -- cgit From f869da75c970aec78975f7154c806f29e3012b7a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 8 Jul 2015 11:42:39 +0200 Subject: Turn off copy optimization when returning a composite by reference. The copy optimization is not correct in case of overlap between destination and source. We would need to use an hypothetical __builtin_memmove_aligned that can cope with overlap to implement the copy at return of callee. --- cparser/StructReturn.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'cparser') diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 660f1d9b..5e5602f3 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -299,10 +299,15 @@ let rec transf_expr env ctx e = transf_call env ctx None fn args e.etyp (* Function calls returning a composite by reference: add first argument. - ctx = Effects: lv = f(...) -> f(&lv, ...) [copy optimization] + ctx = Effects: lv = f(...) -> f(&newtemp, ...), lv = newtemp f(...) -> f(&newtemp, ...) ctx = Val: lv = f(...) -> f(&newtemp, ...), lv = newtemp f(...) -> f(&newtemp, ...), newtemp + + We used to do a copy optimization: + ctx = Effects: lv = f(...) -> f(&lv, ...) + but it is not correct in case of overlap (see test/regression/struct12.c) + Function calls returning a composite by value: ctx = Effects: lv = f(...) -> newtemp = f(...), lv = newtemp f(...) -> f(...) @@ -332,13 +337,14 @@ and transf_call env ctx opt_lhs fn args ty = | Effects, None -> let tmp = new_temp ~name:"_res" ty in {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} - | Effects, Some lhs -> - {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []} + (* Copy optimization, turned off as explained above *) + (* | Effects, Some lhs -> + {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []} *) | Val, None -> let tmp = new_temp ~name:"_res" ty in ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} tmp - | Val, Some lhs -> + | _, Some lhs -> let tmp = new_temp ~name:"_res" ty in ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} (eassign lhs tmp) -- cgit