diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Bitfields.ml | 28 | ||||
-rw-r--r-- | cparser/Cutil.ml | 3 | ||||
-rw-r--r-- | cparser/Elab.ml | 33 | ||||
-rw-r--r-- | cparser/Machine.ml | 4 | ||||
-rw-r--r-- | cparser/Machine.mli | 1 | ||||
-rw-r--r-- | cparser/Parse.ml | 2 | ||||
-rw-r--r-- | cparser/Rename.ml | 28 | ||||
-rw-r--r-- | cparser/Rename.mli | 2 | ||||
-rw-r--r-- | cparser/StructReturn.ml | 14 | ||||
-rw-r--r-- | cparser/validator/Tuples.v | 7 |
10 files changed, 93 insertions, 29 deletions
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, [])); 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/Elab.ml b/cparser/Elab.ml index d6b79780..9ff7823f 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 @@ -1822,12 +1827,12 @@ let enter_or_refine_ident local loc env s sto ty = | _,Storage_register | Storage_register,_ -> Storage_register in - (id, new_sto, Env.add_ident env id new_sto new_ty) + (id, new_sto, Env.add_ident env id new_sto new_ty,new_ty) | Some(id, II_enum v) when Env.in_current_scope env id -> error loc "redefinition of enumerator '%s'" s; - (id, sto, Env.add_ident env id sto ty) + (id, sto, Env.add_ident env id sto ty,ty) | _ -> - let (id, env') = Env.enter_ident env s sto ty in (id, sto, env') + let (id, env') = Env.enter_ident env s sto ty in (id, sto, env',ty) let enter_decdefs local loc env sto dl = (* Sanity checks on storage class *) @@ -1845,7 +1850,7 @@ let enter_decdefs local loc env sto dl = let sto1 = if local && isfun then Storage_extern else sto in (* enter ident in environment with declared type, because initializer can refer to the ident *) - let (id, sto', env1) = enter_or_refine_ident local loc env s sto1 ty in + let (id, sto', env1,ty) = enter_or_refine_ident local loc env s sto1 ty in (* process the initializer *) let (ty', init') = elab_initializer loc env1 s ty init in (* update environment with refined type *) @@ -1882,18 +1887,30 @@ let elab_fundef env spec name body loc = | TFun(ty_ret, Some params, vararg, attr) -> (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 env s sto ty in + let (fun_id, sto1, env1,ty) = enter_or_refine_ident false loc env1 s sto ty in (* Enter parameters in the environment *) let env2 = List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) (Env.new_scope env1) params in (* Define "__func__" and enter it in the environment *) let (func_ty, func_init) = __func__type_and_init s in - let (func_id, _, env3) = + let (func_id, _, env3,func_ty) = enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in 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; @@ -1904,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 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 diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 317847a7..c9564c08 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -29,7 +29,7 @@ let transform_program t p name = Some (CtoDwarf.program_to_dwarf p p1 name) else None in - (Rename.program p1),debug + (Rename.program p1 (Filename.chop_suffix name ".c")),debug let parse_transformations s = let t = ref CharSet.empty in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 0d533b56..cf82bc9f 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -42,6 +42,16 @@ let enter_public env id = { re_id = IdentMap.add id id env.re_id; re_public = StringMap.add id.name id env.re_public; re_used = StringSet.add id.name env.re_used } + +let enter_static env id file = + try + let id' = StringMap.find id.name env.re_public in + { env with re_id = IdentMap.add id id' env.re_id } + with Not_found -> + let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in + { re_id = IdentMap.add id id' env.re_id; + re_public = env.re_public; + re_used = StringSet.add id'.name env.re_used } (* For static or local identifiers, we make up a new name if needed *) (* If the same identifier has already been declared, @@ -249,7 +259,7 @@ let reserve_builtins () = (* Reserve global declarations with public visibility *) -let rec reserve_public env = function +let rec reserve_public env file = function | [] -> env | dcl :: rem -> let env' = @@ -257,22 +267,28 @@ let rec reserve_public env = function | Gdecl(sto, id, _, _) -> begin match sto with | Storage_default | Storage_extern -> enter_public env id - | Storage_static -> env + | Storage_static -> if !Clflags.option_rename_static then + enter_static env id file + else + env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with | Storage_default | Storage_extern -> enter_public env f.fd_name - | Storage_static -> env + | Storage_static -> if !Clflags.option_rename_static then + enter_static env f.fd_name file + else + env | _ -> assert false end | _ -> env in - reserve_public env' rem + reserve_public env' file rem (* Rename the program *) -let program p = +let program p file = globdecls - (reserve_public (reserve_builtins()) p) + (reserve_public (reserve_builtins()) file p) [] p diff --git a/cparser/Rename.mli b/cparser/Rename.mli index 818a51bc..c4ef2228 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val program : C.program -> C.program +val program : C.program -> string -> C.program 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) 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 := |