diff options
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 196 |
1 files changed, 121 insertions, 75 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1bfc2d11..ea85ad04 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -17,14 +17,11 @@ (* Numbered references are to sections of the ISO C99 standard *) -open Format open Machine -open !Cabs -open Cabshelper -open !C +open Cabs +open C open Cerrors open Cutil -open Env (** * Utility functions *) @@ -42,7 +39,7 @@ let warning loc = 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' (aka '%a')" Cprint.typ_raw ty Cprint.typ_raw (unroll env ty) | _ -> Format.fprintf fmt "'%a'" Cprint.typ_raw ty (* Error reporting for Env functions *) @@ -155,11 +152,11 @@ let enter_or_refine_ident local loc env s sto ty = if redef Env.lookup_typedef env s then 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)) + | Some(id, Env.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 '%s'" s - | Some(id, II_enum _) when Env.in_current_scope env id -> + | Some(id, Env.II_enum _) when Env.in_current_scope env id -> error loc "redefinition of '%s' as different kind of symbol" s; | _ -> () @@ -174,7 +171,7 @@ let enter_or_refine_ident local loc env s sto ty = prior declarations of this variable with internal or external linkage. The variable has linkage. *) match previous_def Env.lookup_ident !top_environment s with - | Some(id, II_ident(old_sto, old_ty)) -> + | Some(id, Env.II_ident(old_sto, old_ty)) -> let (new_sto, new_ty) = combine_toplevel_definitions loc env s old_sto old_ty sto ty in (id, new_sto, Env.add_ident env id new_sto new_ty, new_ty, true) @@ -389,8 +386,8 @@ let elab_attr_arg loc env a = | VARIABLE s -> begin try match Env.lookup_ident env s with - | (id, II_ident(sto, ty)) -> AIdent s - | (id, II_enum v) -> AInt v + | (id, Env.II_ident(sto, ty)) -> AIdent s + | (id, Env.II_enum v) -> AInt v with Env.Error _ -> AIdent s end @@ -477,13 +474,19 @@ let typespec_rank = function (* Don't change this *) let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) -(* Is a specifier an anonymous struct/union in the sense of ISO C2011? *) +(* Auxiliary for type declarator elaboration. Remove the non-type-related + attributes from the given type and return those attributes separately. + If the type is a function type, keep function-related attributes + attached to the type. *) -let is_anonymous_composite spec = - List.exists - (function SpecType(Tstruct_union(_, None, Some _, _)) -> true - | _ -> false) - spec +let get_nontype_attrs env ty = + let to_be_removed a = + match class_of_attribute a with + | Attr_type -> false + | Attr_function -> not (is_function_type env ty) + | _ -> true in + let nta = List.filter to_be_removed (attributes_of_type env ty) in + (remove_attributes_type env nta ty, nta) (* Elaboration of a type specifier. Returns 5-tuple: (storage class, "inline" flag, "typedef" flag, elaborated type, new env) @@ -528,14 +531,15 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = let simple ty = (!sto, !inline, !noreturn ,!typedef, add_attributes_type !attr ty, env) in - (* As done in CIL, partition !attr into type-related attributes, + (* As done in CIL, partition !attr into struct-related attributes, which are returned, and other attributes, which are left in !attr. - The returned type-related attributes are applied to the + The returned struct-related attributes are applied to the struct/union/enum being defined. - The leftover non-type-related attributes will be applied + The leftover non-struct-related attributes will be applied to the variable being defined. *) - let get_type_attrs () = - let (ta, nta) = List.partition attr_is_type_related !attr in + let get_struct_attrs () = + let (ta, nta) = + List.partition (fun a -> class_of_attribute a = Attr_struct) !attr in attr := nta; ta in @@ -594,21 +598,21 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = | [Cabs.Tstruct_union(STRUCT, id, optmembers, a)] -> let a' = - add_attributes (get_type_attrs()) (elab_attributes env a) in + add_attributes (get_struct_attrs()) (elab_attributes env a) in let (id', env') = 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 + add_attributes (get_struct_attrs()) (elab_attributes env a) in let (id', env') = 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)] -> let a' = - add_attributes (get_type_attrs()) (elab_attributes env a) in + add_attributes (get_struct_attrs()) (elab_attributes env a) in let (id', env') = elab_enum only loc id optmembers a' env in (!sto, !inline, !noreturn, !typedef, TEnum(id', !attr), env') @@ -641,7 +645,8 @@ and elab_type_declarator keep_ty loc env ty kr_ok = function | Cabs.JUSTBASE -> ((ty, None), env) | Cabs.ARRAY(d, cv_specs, sz) -> - let a = elab_cvspecs env cv_specs in + let (ty, a) = get_nontype_attrs env ty in + let a = add_attributes a (elab_cvspecs env cv_specs) in let sz' = match sz with | None -> @@ -659,22 +664,25 @@ and elab_type_declarator keep_ty loc env ty kr_ok = function Some 1L in (* produces better error messages later *) 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 + let (ty, a) = get_nontype_attrs env ty in + let a = add_attributes a (elab_cvspecs env cv_specs) in elab_type_declarator keep_ty loc env (TPtr(ty, a)) kr_ok d | Cabs.PROTO(d, (params, vararg)) -> elab_return_type loc env ty; + let (ty, a) = get_nontype_attrs env ty in 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 + elab_type_declarator keep_ty loc env (TFun(ty, Some params', vararg, a)) kr_ok d | Cabs.PROTO_OLD(d, params) -> elab_return_type loc env ty; + let (ty, a) = get_nontype_attrs env ty in match params with | [] -> - elab_type_declarator keep_ty loc env (TFun(ty, None, false, [])) kr_ok d + elab_type_declarator keep_ty loc env (TFun(ty, None, false, a)) kr_ok d | _ -> if not kr_ok || d <> Cabs.JUSTBASE then fatal_error loc "illegal old-style K&R function definition"; - ((TFun(ty, None, false, []), Some params), env) + ((TFun(ty, None, false, a), Some params), env) (* Elaboration of parameters in a prototype *) @@ -748,12 +756,14 @@ and elab_init_name_group keep_ty loc env (spec, namelist) = let a = elab_attributes env attr in if inl && not (is_function_type env ty) then error loc "'inline' can only appear on functions"; - if noret then begin - warning loc Celeven_extension "_Noreturn functions are a C11 extension"; - if not (is_function_type env ty) then - error loc "'_Noreturn' can only appear on functions"; - end; - ((id, add_attributes_type a ty, init), env1) in + let a' = + if noret then begin + warning loc Celeven_extension "_Noreturn functions are a C11 extension"; + if not (is_function_type env ty) then + error loc "'_Noreturn' can only appear on functions"; + add_attributes [Attr("noreturn",[])] a + end else a in + ((id, add_attributes_type a' ty, init), env1) in (mmap elab_one_name env' namelist, sto, tydef) (* Elaboration of a field group *) @@ -772,9 +782,6 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = 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 Celeven_extension "anonymous structs/unions are a C11 extension" - else (* This should actually never be triggered, empty structs are captured earlier *) warning loc Missing_declarations "declaration does not declare anything"; @@ -814,7 +821,7 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = error loc "bit-field '%s' width not an integer constant" id; None end in - let anon_composite = Cutil.is_anonymous_composite ty in + let anon_composite = is_anonymous_composite ty in if id = "" && not anon_composite && optbitsize = None then warning loc Missing_declarations "declaration does not declare anything"; { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize'; fld_anonymous = id = "" && anon_composite} @@ -836,17 +843,15 @@ and elab_struct_or_union_info keep_ty kind loc env members attrs = | [] -> () | fld::rest -> if fld.fld_anonymous then begin - let warn () = - warning loc Celeven_extension "anonymous structs/unions are a C11 extension" in let rest = match unroll env fld.fld_typ with | TStruct (id,_) -> - warn (); + warning loc Celeven_extension "anonymous structs/unions are a C11 extension"; let str = Env.find_struct env' id in - str.ci_members@rest + str.Env.ci_members@rest | TUnion (id,_) -> - warn (); + warning loc Celeven_extension "anonymous structs/unions are a C11 extension"; let union = Env.find_union env' id in - union.ci_members@rest + union.Env.ci_members@rest | _ -> rest in duplicate acc rest end else if fld.fld_name <> "" then begin @@ -894,21 +899,21 @@ and elab_struct_or_union keep_ty 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 + if ci.Env.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 + | Some(tag', ({Env.ci_sizeof = None} as ci)), Some members when Env.in_current_scope env tag' -> - if ci.ci_kind <> kind then + if ci.Env.ci_kind <> kind then error loc "use of '%s' with tag type that does not match previous declaration" tag; (* finishing the definition of an incomplete struct or union *) let (ci', env') = elab_struct_or_union_info 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)); + emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.Env.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env' tag' ci') - | Some(tag', {ci_sizeof = Some _}), Some _ + | Some(tag', {Env.ci_sizeof = Some _}), Some _ when Env.in_current_scope env tag' -> error loc "redefinition of struct or union '%s'" tag; (tag', env) @@ -933,7 +938,7 @@ and elab_struct_or_union keep_ty only kind loc tag optmembers attrs env = let (ci2, env'') = 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)); + emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.Env.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env'' tag' ci2) @@ -982,7 +987,7 @@ and elab_enum only loc tag optmembers attrs env = let (dcl2, env2) = elab_members env1 nextval1 tl in (dcl1 :: dcl2, env2) in let (dcls, env') = elab_members env 0L members in - let info = { ei_members = dcls; ei_attr = attrs } in + let info = { Env.ei_members = dcls; ei_attr = attrs } in let (tag', env'') = Env.enter_enum env' tag info in emit_elab env' loc (Genumdef(tag', attrs, dcls)); (tag', env'') @@ -1098,11 +1103,11 @@ module I = struct let rec zipname = function | Ztop(name, ty) -> name | Zarray(z, ty, sz, dfl, before, idx, after) -> - sprintf "%s[%Ld]" (zipname z) idx + Printf.sprintf "%s[%Ld]" (zipname z) idx | Zstruct(z, id, before, fld, after) -> - sprintf "%s.%s" (zipname z) fld.fld_name + Printf.sprintf "%s.%s" (zipname z) fld.fld_name | Zunion(z, id, fld) -> - sprintf "%s.%s" (zipname z) fld.fld_name + Printf.sprintf "%s.%s" (zipname z) fld.fld_name let name (z, i) = zipname z @@ -1146,7 +1151,7 @@ module I = struct | TStruct(id, _), Init_struct(id', (fld1, i1) :: flds) -> Some(Zstruct(z, id, [], fld1, flds), i1) | TUnion(id, _), Init_union(id', fld, i) -> - begin match (Env.find_union env id).ci_members with + begin match (Env.find_union env id).Env.ci_members with | [] -> None | fld1 :: _ -> Some(Zunion(z, id, fld1), @@ -1225,7 +1230,7 @@ module I = struct member env zi name else find rem - in find (Env.find_union env id).ci_members + in find (Env.find_union env id).Env.ci_members end | (TStruct _ | TUnion _), Init_single a -> member env (z, default_init env ty) name @@ -1432,9 +1437,9 @@ let elab_expr vararg loc env a = | VARIABLE s -> begin match wrap Env.lookup_ident loc env s with - | (id, II_ident(sto, ty)) -> + | (id, Env.II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty },env - | (id, II_enum v) -> + | (id, Env.II_enum v) -> { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) },env end @@ -1522,7 +1527,7 @@ let elab_expr vararg loc env a = | BUILTIN_VA_ARG (a2, a3) -> let ident = match wrap Env.lookup_ident loc env "__builtin_va_arg" with - | (id, II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty } + | (id, Env.II_ident(sto, ty)) -> { edesc = EVar id; etyp = ty } | _ -> assert false in let b2,env = elab env a2 in @@ -1642,6 +1647,45 @@ let elab_expr vararg loc env a = error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty; { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) },env' + | BUILTIN_OFFSETOF ((spec,dcl), mem) -> + let (ty,env) = elab_type loc env spec dcl in + if incomplete_type env ty then + error "offsetof of incomplete type %a" (print_typ env) ty; + let members env ty mem = + match ty with + | TStruct (id,_) -> wrap Env.find_struct_member loc env (id,mem) + | TUnion (id,_) -> wrap Env.find_union_member loc env (id,mem) + | _ -> error "request for member '%s' in something not a structure or union" mem in + let rec offset_of_list acc env ty = function + | [] -> acc,ty + | fld::rest -> let off = offsetof env ty fld in + offset_of_list (acc+off) env fld.fld_typ rest in + let offset_of_member (env,off_accu,ty) mem = + match mem,unroll env ty with + | INFIELD_INIT mem,ty -> + let flds = members env ty mem in + let flds = List.rev flds in + let off,ty = offset_of_list 0 env ty flds in + env,off_accu + off,ty + | ATINDEX_INIT e,TArray (sub_ty,_,_) -> + let e,env = elab env e in + let e = match Ceval.integer_expr env e with + | None -> error "array element designator for is not an integer constant expression" + | Some n-> n in + let size = match sizeof env sub_ty with + | None -> assert false (* We expect only complete types *) + | Some s -> s in + let off_accu = match cautious_mul e size with + | None -> error "'offsetof' overflows" + | Some s -> off_accu + s in + env,off_accu,sub_ty + | ATINDEX_INIT _,_ -> error "subscripted value is not an array" in + let env,offset,_ = List.fold_left offset_of_member (env,0,ty) mem in + let size_t = size_t_ikind () in + let offset = Ceval.normalize_int (Int64.of_int offset) size_t in + let offsetof_const = EConst (CInt(offset,size_t,"")) in + { edesc = offsetof_const; etyp = TInt(size_t, []) },env + | UNARY(PLUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then @@ -1674,7 +1718,7 @@ let elab_expr vararg loc env a = | EVar id -> begin match wrap Env.find_ident loc env id with | Env.II_ident(Storage_register, _) -> - err "address of register variable '%s' requested" id.name + err "address of register variable '%s' requested" id.C.name | _ -> () end | EUnop(Odot f, b2) -> @@ -2061,7 +2105,7 @@ let enter_typedefs loc env sto dl = match previous_def Env.lookup_typedef env s with | Some (s',ty') -> if equal_types env ty ty' then begin - warning loc Cerrors.Celeven_extension "redefinition of typedef '%s' is C11 extension" s; + warning loc Celeven_extension "redefinition of typedef '%s' is C11 extension" s; env end else begin error loc "typedef redefinition with different types (%a vs %a)" @@ -2164,7 +2208,7 @@ let elab_KR_function_parameters env params defs loc = end; paramsenv | d -> (* Should never be produced by the parser *) - fatal_error (get_definitionloc d) + fatal_error (Cabshelper.get_definitionloc d) "Illegal declaration of function parameter" in let kr_params_defs,paramsenv = let params,paramsenv = mmap elab_param_def env defs in @@ -2213,7 +2257,7 @@ let elab_KR_function_parameters env params defs loc = let inherit_vararg env s sto ty = match previous_def Env.lookup_ident env s with - | Some(id, II_ident(_, old_ty)) + | Some(id, Env.II_ident(_, old_ty)) when sto = Storage_extern || Env.in_current_scope env id -> begin match old_ty, ty with @@ -2232,7 +2276,7 @@ let elab_fundef env spec name defs body loc = fatal_error loc "invalid 'register' storage-class on function"; begin match kr_params, defs with | None, d::_ -> - error (get_definitionloc d) + error (Cabshelper.get_definitionloc d) "old-style parameter declarations in prototyped function definition" | _ -> () end; @@ -2247,7 +2291,7 @@ let elab_fundef env spec name defs body loc = | ty, None -> (ty, [],env1) | TFun(ty_ret, None, false, attr), Some params -> - warning loc Cerrors.CompCert_conformance "non-prototype, pre-standard function definition, converting to prototype form"; + warning loc 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,env) @@ -2304,17 +2348,19 @@ let elab_fundef env spec name defs body loc = { sdesc = Sblock (List.map mkdecl extra_decls @ [body2]); sloc = no_loc } end in - if noret then begin + (* Handling of _Noreturn and of attribute("noreturn") *) + if noret then warning loc Celeven_extension "_Noreturn functions are a C11 extension"; - if contains_return body1 then - warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; - end; + if (noret || find_custom_attributes ["noreturn"; "__noreturn__"] attr <> []) + && contains_return body1 then + warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) let fn = { fd_storage = sto1; fd_inline = inline; fd_name = fun_id; - fd_attrib = attr; + fd_attrib = if noret then add_attributes [Attr("noreturn",[])] attr + else attr; fd_ret = ty_ret; fd_params = params; fd_vararg = vararg; @@ -2483,7 +2529,7 @@ let rec elab_stmt env ctx s = (a1, env, None) | Some (FC_DECL def) -> let (dcl, env') = elab_definition true (Env.new_scope env) def in - let loc = elab_loc (get_definitionloc def) in + let loc = elab_loc (Cabshelper.get_definitionloc def) in (sskip, env', Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in let a2',env = @@ -2573,7 +2619,7 @@ let rec elab_stmt env ctx s = (* Unsupported *) | DEFINITION def -> - error (get_definitionloc def) "ill-placed definition"; + error (Cabshelper.get_definitionloc def) "ill-placed definition"; sskip,env and elab_block loc env ctx b = @@ -2586,7 +2632,7 @@ and elab_block_body env ctx sl = [],env | DEFINITION def :: sl1 -> let (dcl, env') = elab_definition true env def in - let loc = elab_loc (get_definitionloc def) in + let loc = elab_loc (Cabshelper.get_definitionloc def) in let dcl = List.map (fun ((sto,id,ty,_) as d) -> Debug.insert_local_declaration sto id ty loc; {sdesc = Sdecl d; sloc = loc}) dcl in |