diff options
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 985 |
1 files changed, 666 insertions, 319 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index a1f85886..718261b4 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -69,6 +69,20 @@ let top_declarations = ref ([] : globdecl list) let top_environment = ref Env.empty +(* Set of all globals with a definitions *) + +module StringSet = Set.Make(String) + +let global_defines = ref StringSet.empty + +let add_global_define loc name = + if StringSet.mem name !global_defines then + error loc "redefinition of '%s'" name; + global_defines := StringSet.add name !global_defines + +let is_global_defined name = + StringSet.mem name !global_defines + let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td = let loc = elab_loc loc in let dec ={ gdesc = td; gloc = loc } in @@ -84,7 +98,7 @@ let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td = | _ -> () end -let reset() = top_declarations := []; top_environment := Env.empty +let reset() = top_declarations := []; top_environment := Env.empty; global_defines := StringSet.empty let elaborated_program () = let p = !top_declarations in @@ -101,6 +115,15 @@ let rec mmap f env = function let (tl', env2) = mmap f env1 tl in (hd' :: tl', env2) +let rec mmap2 f env l1 l2 = + match l1,l2 with + | [],[] -> [],env + | a1::l1,a2::l2 -> + let hd,env1 = f env a1 a2 in + let tl,env2 = mmap2 f env1 l1 l2 in + (hd::tl,env2) + | _, _ -> invalid_arg "mmap2" + (* To detect redefinitions within the same scope *) let previous_def fn env arg = @@ -116,6 +139,13 @@ let redef fn env arg = (* Auxiliaries for handling declarations and redeclarations *) +let name_of_storage_class = function + | Storage_default -> "<default>" + | Storage_extern -> "'extern'" + | Storage_static -> "'static'" + | Storage_auto -> "'auto'" + | Storage_register -> "'register'" + let combine_toplevel_definitions loc env s old_sto old_ty sto ty = let new_ty = match combine_types AttrCompat env old_ty ty with @@ -126,26 +156,43 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty = "redefinition of '%s' with a different type: %a vs %a" s (print_typ env) old_ty (print_typ env) ty; ty in + if is_global_defined s then begin + let old_attrs = attributes_of_type env old_ty + and new_attrs = attributes_of_type env ty in + if not (Cutil.incl_attributes new_attrs old_attrs) then + warning loc Ignored_attributes "attribute declaration must precede definition" + end; let new_sto = (* The only case not allowed is removing static *) match old_sto,sto with | Storage_static,Storage_static | Storage_extern,Storage_extern - | Storage_register,Storage_register | Storage_default,Storage_default -> sto | _,Storage_static -> 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 + | Storage_default,Storage_extern -> + if is_global_defined s && is_function_type env ty then + warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored"; + Storage_extern | _,Storage_extern -> old_sto + (* "auto" and "register" don't appear in toplevel definitions. + Normally this was checked earlier. Generate error message + instead of "assert false", just in case. *) + | _,Storage_auto + | Storage_auto,_ | _,Storage_register - | Storage_register,_ -> Storage_register + | Storage_register,_ -> + error loc "unexpected %s declaration of '%s'" + (name_of_storage_class sto) s; + sto in (new_sto, new_ty) -let enter_or_refine_ident local loc env s sto ty = +let enter_or_refine_ident_base local loc env new_id sto ty = + let s = new_id.C.name in (* Check for illegal redefinitions: - a name that was previously a typedef - a variable that was already declared in the same local scope @@ -155,41 +202,67 @@ 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, Env.II_ident(old_sto, old_ty)) - when local && Env.in_current_scope env id + | Some(old_id, Env.II_ident(old_sto, old_ty)) + when local && Env.in_current_scope env old_id && not (sto = Storage_extern && old_sto = Storage_extern) -> error loc "redefinition of '%s'" s - | Some(id, Env.II_enum _) when Env.in_current_scope env id -> + | Some(old_id, Env.II_enum _) when Env.in_current_scope env old_id -> error loc "redefinition of '%s' as different kind of symbol" s; | _ -> () end; - (* For a block-scoped, non-"extern" variable, a new declaration - is entered, and it has no linkage. *) - if local && sto <> Storage_extern then begin - let (id, env') = Env.enter_ident env s sto ty in - (id, sto, env', ty, false) + (* For a block-scoped, "static" or "auto" or "register" variable, + a new declaration is entered, and it has no linkage. *) + if local + && (sto = Storage_auto || sto = Storage_register || sto = Storage_static) + then begin + (new_id, sto, Env.add_ident env new_id sto ty, ty, false) end else begin (* For a file-scoped or "extern" variable, we need to check against 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, Env.II_ident(old_sto, old_ty)) -> + | Some(old_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) + (old_id, new_sto, Env.add_ident env old_id new_sto new_ty, new_ty, true) | _ -> - let (id, env') = Env.enter_ident env s sto ty in - (id, sto, env', ty, true) + (new_id, sto, Env.add_ident env new_id sto ty, ty, true) end +(* We use two variants of [enter_or_refine]: + + - [enter_or_refine_ident] is to be used for all declarations, + block-scoped ([local = true]) or top-level ([local = false]). + The name of the declared thing is given as a string [s]. If a + previous declaration with this name exists in the current scope, + its unique identifier is returned. Otherwise a fresh identifier + named [s] is created in the current scope of [env] and returned. + + - [enter_or_refine_function] is to be used for function definitions. + Such definitions are always global, hence the [local] parameter + defaults to [false] and is omitted. The function name is given + as an identifier, created in advance by the caller. This + identifier is used if no previous declaration exists for the + function. Otherwise, the identifier of the previous declaration is + used. By creating the identifier in advance, [elab_fundef] makes + sure that it is properly scoped to file scope and not to the local + scope of function parameters. +*) + +let enter_or_refine_ident local loc env s sto ty = + enter_or_refine_ident_base local loc env (Env.fresh_ident s) sto ty + +let enter_or_refine_function loc env id sto ty = + enter_or_refine_ident_base false loc env id sto ty + (* Forward declarations *) let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref = ref (fun _ _ _ -> assert false) -let elab_funbody_f : (C.typ -> bool -> Env.t -> statement -> C.stmt) ref - = ref (fun _ _ _ _ -> assert false) +let elab_funbody_f : (C.typ -> bool -> bool -> Env.t -> statement -> C.stmt) ref + = ref (fun _ _ _ _ _ -> assert false) (** * Elaboration of constants - C99 section 6.4.4 *) @@ -422,35 +495,53 @@ let elab_gcc_attr loc env = function let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L -let extract_alignas loc a = +(* Check alignment parameter *) +let check_alignment loc n = + if not (is_power_of_two n || n = 0L) then begin + error loc "requested alignment %Ld is not a power of 2" n; false + end else + if n <> Int64.of_int (Int64.to_int n) then begin + error loc "requested alignment %Ld is too large" n; false + end else + true + +(* Process GCC attributes that have special significance. Currently we + have two: "aligned" and "packed". *) +let enter_gcc_attr 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) - | [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 + | [AInt n] -> if check_alignment loc n then [a] else [] + | [_] -> error loc "requested alignment is not an integer constant"; [] + | [] -> [] (* Use default alignment, like gcc does *) + | _ -> error loc "'aligned' attribute takes no more than 1 argument"; [] + end + | Attr(("packed"|"__packed__"), args) -> + begin match args with + | [] -> [a] + | [AInt n] -> if check_alignment loc n then [a] else [] + | [AInt n; AInt p] -> + if check_alignment loc n && check_alignment loc p then [a] else [] + | [AInt n; AInt p; AInt q] when q = 0L || q = 1L -> + if check_alignment loc n && check_alignment loc p then [a] else [] + | _ -> error loc "ill-formed 'packed' attribute"; [] end - | _ -> a + | _ -> [a] let elab_attribute env = function | GCC_ATTR (l, loc) -> List.fold_left add_attributes [] - (List.map (fun attr -> [attr]) - (List.map (extract_alignas loc) - (List.flatten - (List.map (elab_gcc_attr loc env) l)))) + (List.map (enter_gcc_attr loc) + (List.flatten + (List.map (elab_gcc_attr loc env) l))) | PACKED_ATTR (args, loc) -> - [Attr("__packed__", List.map (elab_attr_arg loc env) args)] + enter_gcc_attr loc + (Attr("__packed__", List.map (elab_attr_arg loc env) args)) | ALIGNAS_ATTR ([a], loc) -> + warning loc Celeven_extension "'_Alignas' is a C11 extension"; begin match elab_attr_arg loc env a with | 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 + if check_alignment loc n then [AAlignas (Int64.to_int n)] else [] | _ -> error loc "requested alignment is not an integer constant"; [] | exception Wrong_attr_arg -> error loc "bad _Alignas value"; [] end @@ -460,6 +551,22 @@ let elab_attribute env = function let elab_attributes env al = List.fold_left add_attributes [] (List.map (elab_attribute env) al) +(* Warning for alignment requests that reduce the alignment below the + natural alignment. *) + +let warn_if_reduced_alignment loc ~actual ~natural = + match actual, natural with + | Some act, Some nat when act < nat -> + warning loc Reduced_alignment + "requested alignment (%d) is less than natural alignment (%d)" + act nat + | _, _ -> () + +let check_reduced_alignment loc env typ = + warn_if_reduced_alignment loc + ~actual: (wrap alignof loc env typ) + ~natural: (wrap alignof loc env (erase_attributes_type env typ)) + (* Auxiliary for typespec elaboration *) let typespec_rank = function (* Don't change this *) @@ -491,14 +598,15 @@ let get_nontype_attrs env ty = 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) +(* Elaboration of a type specifier. Returns 6-tuple: + (storage class, "inline" flag, "noreturn" flag, "typedef" flag, + elaborated type, new env) Optional argument "only" is true if this is a standalone struct or union declaration, without variable names. C99 section 6.7.2. *) -let rec elab_specifier keep_ty ?(only = false) loc env specifier = +let rec elab_specifier ?(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) @@ -506,18 +614,20 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = let sto = ref Storage_default and inline = ref false and noreturn = ref false + and restrict = ref false and attr = ref [] and tyspecs = ref [] and typedef = ref false in let do_specifier = function | SpecCV cv -> + restrict := cv = CV_RESTRICT; attr := add_attributes (elab_cvspec env cv) !attr | SpecStorage st -> if !sto <> Storage_default && st <> TYPEDEF then - error loc "multiple storage-classes in declaration specifier"; + error loc "multiple storage classes in declaration specifier"; begin match st with - | AUTO -> () + | AUTO -> sto := Storage_auto | STATIC -> sto := Storage_static | EXTERN -> sto := Storage_extern | REGISTER -> sto := Storage_register @@ -530,9 +640,18 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = | SpecFunction NORETURN -> noreturn := true | SpecType tys -> tyspecs := tys :: !tyspecs in + let restrict_check ty = + if !restrict then + if not (is_pointer_type env ty) then + error loc "restrict requires a pointer type (%a is invalid)" (print_typ env) ty + else if is_function_pointer_type env ty then + error loc "pointer to function type %a may not be 'restrict' qualified" (print_typ env) ty in + List.iter do_specifier specifier; - let simple ty = (!sto, !inline, !noreturn ,!typedef, add_attributes_type !attr ty, env) in + let simple ty = + restrict_check ty; + (!sto, !inline, !noreturn ,!typedef, add_attributes_type !attr ty, env) in (* As done in CIL, partition !attr into struct-related attributes, which are returned, and other attributes, which are left in !attr. @@ -603,22 +722,28 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = let a' = 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') + elab_struct_or_union only Struct loc id optmembers a' env in + let ty = TStruct(id', !attr) in + restrict_check ty; + (!sto, !inline, !noreturn, !typedef, ty, env') | [Cabs.Tstruct_union(UNION, id, optmembers, a)] -> let a' = 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') + elab_struct_or_union only Union loc id optmembers a' env in + let ty = TUnion(id', !attr) in + restrict_check ty; + (!sto, !inline, !noreturn, !typedef, ty, env') | [Cabs.Tenum(id, optmembers, a)] -> let a' = 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') + let ty = TEnum (id', !attr) in + restrict_check ty; + (!sto, !inline, !noreturn, !typedef, ty, env') (* Specifier doesn't make sense *) | _ -> @@ -644,12 +769,23 @@ and elab_return_type loc env ty = error loc "function cannot return function type %a" (print_typ env) ty | _ -> () -and elab_type_declarator keep_ty loc env ty kr_ok = function +(* The [?fundef] parameter is true if we're elaborating a function definition + and false otherwise. When [fundef = true], K&R function declarators + are allowed, and the returned environment includes bindings for the + function parameters and the struct/unions they may define. + When [fundef = false], K&R function declarators are rejected + and declarations in parameters are not returned. *) + +and elab_type_declarator ?(fundef = false) loc env ty = function | Cabs.JUSTBASE -> ((ty, None), env) | Cabs.ARRAY(d, cv_specs, sz) -> let (ty, a) = get_nontype_attrs env ty in let a = add_attributes a (elab_cvspecs env cv_specs) in + if wrap incomplete_type loc env ty then + error loc "array type has incomplete element type %a" (print_typ env) ty; + if wrap contains_flex_array_mem loc env ty then + warning loc Flexible_array_extensions "%a may not be used as an array element due to flexible array member" (print_typ env) ty; let sz' = match sz with | None -> @@ -666,33 +802,45 @@ and elab_type_declarator keep_ty loc env ty kr_ok = function | None -> error loc "size of array is not a compile-time constant"; Some 1L in (* produces better error messages later *) - elab_type_declarator keep_ty loc env (TArray(ty, sz', a)) kr_ok d + elab_type_declarator ~fundef loc env (TArray(ty, sz', a)) d | Cabs.PTR(cv_specs, d) -> 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 + if is_function_type env ty && incl_attributes [ARestrict] a then + error loc "pointer to function type %a may not be 'restrict' qualified" (print_typ env) ty; + elab_type_declarator ~fundef loc env (TPtr(ty, a)) 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, a)) kr_ok d + let (params', env') = elab_parameters env params in + (* For a function declaration (fundef = false), the scope introduced + to treat parameters ends here, so we discard the extended + environment env' returned by elab_parameters. + For a function definition (fundef = true) we return the + extended environment env' so that it can serve as the basis + to elaborating the function body. *) + let env'' = if fundef then env' else env in + elab_type_declarator ~fundef loc env'' (TFun(ty, Some params', vararg, a)) d | Cabs.PROTO_OLD(d, params) -> elab_return_type loc env ty; let (ty, a) = get_nontype_attrs env ty in + (* For consistency with the PROTO case above, for a function definition + (fundef = true) we open a new scope, even though we do not + add any bindings for the parameters. *) + let env'' = if fundef then Env.new_scope env else env in match params with | [] -> - elab_type_declarator keep_ty loc env (TFun(ty, None, false, a)) kr_ok d + elab_type_declarator ~fundef loc env'' (TFun(ty, None, false, a)) d | _ -> - if not kr_ok || d <> Cabs.JUSTBASE then + if not fundef || d <> Cabs.JUSTBASE then fatal_error loc "illegal old-style K&R function definition"; - ((TFun(ty, None, false, a), Some params), env) + ((TFun(ty, None, false, a), Some params), env'') (* Elaboration of parameters in a prototype *) -and elab_parameters keep_ty env params = +and elab_parameters env params = (* Prototype introduces a new scope *) - let (vars, env) = mmap (elab_parameter keep_ty) (Env.new_scope env) params in + let (vars, env) = mmap elab_parameter (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 -> [],env @@ -700,42 +848,62 @@ and elab_parameters keep_ty env params = (* Elaboration of a function parameter *) -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 +and elab_parameter env (PARAM (spec, id, decl, attr, loc)) = + let (sto, inl, noret, tydef, bty, env1) = elab_specifier loc env spec in if tydef then error loc "'typedef' used in function parameter"; - let ((ty, _), _) = elab_type_declarator keep_ty loc env1 bty false decl in + let ((ty, _), _) = elab_type_declarator loc env1 bty decl in let ty = add_attributes_type (elab_attributes env attr) ty in if sto <> Storage_default && sto <> Storage_register then - error loc - "invalid storage-class specifier in function declarator"; + error loc (* NB: 'auto' not allowed *) + "invalid storage class %s for function parameter" + (name_of_storage_class sto); if inl then error loc "'inline' can only appear on functions"; if noret then error loc "'_Noreturn' can only appear on functions"; let id = match id with None -> "" | Some id -> id in + if id <> "" && is_void_type env1 ty then + error loc "argument '%s' may not have 'void' type" id; if id <> "" && redef Env.lookup_ident env id then error loc "redefinition of parameter '%s'" id; (* replace array and function types by pointer types *) let ty1 = argument_conversion env1 ty in + if is_qualified_array ty1 then + error loc "type qualifier used in non-outermost array type derivation"; + if has_std_alignas env ty then begin + if id <> "" then + error loc "alignment specified for parameter '%s'" id + else + error loc "alignment specified for unnamed parameter" + end; let (id', env2) = Env.enter_ident env1 id sto ty1 in ( (id', ty1) , env2) -(* Elaboration of a (specifier, Cabs "name") pair *) - -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 +(* Elaboration of a (specifier, Cabs "name") pair as found in a function + definition. Returns two environments: the first is [env] + enriched with struct/union definitions from the return type, + as usual; the second is like the first, plus a new scope. + For a prototyped function ([kr_params = None]) the new scope + includes bindings for the function parameters and the struct/unions + they may define. For a K&R function ([kr_params <> None]) the new + scope is empty. *) + +and elab_fundef_name env spec (Name (s, decl, attr, loc)) = + let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in if tydef then error loc "'typedef' is forbidden here"; - let ((ty, kr_params), env'') = elab_type_declarator keep_ty loc env' bty true decl in + let id = Env.fresh_ident s in + let ((ty, kr_params), env'') = + elab_type_declarator ~fundef:true loc env' bty decl in let a = elab_attributes env attr in - (id, sto, inl, noret, add_attributes_type a ty, kr_params, env'') + (id, sto, inl, noret, add_attributes_type a ty, kr_params, env', env'') (* Elaboration of a name group. C99 section 6.7.6 *) -and elab_name_group keep_ty loc env (spec, namelist) = +and elab_name_group loc env (spec, namelist) = let (sto, inl, noret, tydef, bty, env') = - elab_specifier keep_ty loc env spec in + elab_specifier loc env spec in if tydef then error loc "'typedef' is forbidden here"; if inl then @@ -744,35 +912,40 @@ and elab_name_group keep_ty 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 keep_ty loc env bty false decl in + elab_type_declarator loc env bty 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 keep_ty loc env (spec, namelist) = +and elab_init_name_group loc env (spec, namelist) = let (sto, inl, noret, tydef, bty, env') = - elab_specifier keep_ty ~only:(namelist=[]) loc env spec in + elab_specifier ~only:(namelist=[]) loc env spec in + if noret && tydef then + error loc "'_Noreturn' can only appear on functions"; let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = let ((ty, _), env1) = - elab_type_declarator keep_ty loc env bty false decl in + elab_type_declarator loc env bty decl in let a = elab_attributes env attr in - if inl && not (is_function_type env ty) then + let has_fun_typ = is_function_type env ty in + if inl && not has_fun_typ then error loc "'inline' can only appear on functions"; let a' = if noret then begin warning loc Celeven_extension "_Noreturn functions are a C11 extension"; - if not (is_function_type env ty) then + if not has_fun_typ then error loc "'_Noreturn' can only appear on functions"; add_attributes [Attr("noreturn",[])] a end else a in + if has_std_alignas env ty && has_fun_typ then + error loc "alignment specified for function '%s'" id; ((id, add_attributes_type a' ty, init), env1) in (mmap elab_one_name env' namelist, sto, tydef) (* Elaboration of a field group *) -and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = +and elab_field_group env (Field_group (spec, fieldlist, loc)) = let fieldlist = List.map (function (None, x) -> (Name ("", JUSTBASE, [], loc), x) @@ -781,7 +954,7 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = in let ((names, env'), sto) = - elab_name_group keep_ty loc env (spec, List.map fst fieldlist) in + elab_name_group loc env (spec, List.map fst fieldlist) in if sto <> Storage_default then error loc "non-default storage in struct or union"; @@ -789,10 +962,10 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = (* 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' = + let elab_bitfield env (Name (_, _, _, loc), optbitsize) (id, ty) = + let optbitsize',env' = match optbitsize with - | None -> None + | None -> None,env | Some sz -> let ik = match unroll env' ty with @@ -802,40 +975,45 @@ and elab_field_group keep_ty env (Field_group (spec, fieldlist, loc)) = if integer_rank ik > integer_rank IInt then begin error loc "the type of bit-field '%a' must be an integer type no bigger than 'int'" pp_field id; - None + None,env + end else if has_std_alignas env' ty then begin + error loc "alignment specified for bit-field '%a'" pp_field id; + None, env 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-field '%a' has negative width (%Ld)" pp_field id n; - None + None,env end else let max = Int64.of_int(sizeof_ikind ik * 8) in if n > max then begin error loc "size of bit-field '%a' (%Ld bits) exceeds its type (%Ld bits)" pp_field id n max; - None + None,env end else if n = 0L && id <> "" then begin error loc "named bit-field '%a' has zero width" pp_field id; - None + None,env end else - Some(Int64.to_int n) + Some(Int64.to_int n),env' | None -> error loc "bit-field '%a' width not an integer constant" pp_field id; - None + None,env end in + if is_qualified_array ty then + error loc "type qualifier used in array declarator outside of function prototype"; 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} + { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize'; fld_anonymous = id = "" && anon_composite},env' in - (List.map2 elab_bitfield fieldlist names, env') + (mmap2 elab_bitfield env' fieldlist names) (* Elaboration of a struct or union. C99 section 6.7.2.1 *) -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 +and elab_struct_or_union_info kind loc env members attrs = + let (m, env') = mmap elab_field_group env members in let m = List.flatten m in let m,_ = mmap (fun c fld -> if fld.fld_anonymous then @@ -866,16 +1044,22 @@ and elab_struct_or_union_info keep_ty kind loc env members attrs = duplicate acc rest in duplicate [] m; (* Check for incomplete types *) - let rec check_incomplete = function + let rec check_incomplete only = function | [] -> () - | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> () - (* C99: ty[] allowed as last field of a struct *) + | [ { fld_typ = TArray(ty_elt, None, _) as typ; fld_name = name } ] when kind = Struct -> + (* C99: ty[] allowed as last field of a struct, provided this is not the only field *) + if only then + error loc "flexible array member '%a' not allowed in otherwise empty struct" pp_field name; + check_reduced_alignment loc env' typ | fld :: rem -> if wrap incomplete_type loc env' fld.fld_typ then (* Must be fatal otherwise we get problems constructing the init *) fatal_error loc "member '%a' has incomplete type" pp_field fld.fld_name; - check_incomplete rem in - check_incomplete m; + if wrap contains_flex_array_mem loc env' fld.fld_typ && kind = Struct then + warning loc Flexible_array_extensions "%a may not be used as a struct member due to flexible array member" (print_typ env) fld.fld_typ; + check_reduced_alignment loc env' fld.fld_typ; + check_incomplete false rem in + check_incomplete true m; (* Warn for empty structs or unions *) if m = [] then if kind = Struct then begin @@ -883,16 +1067,26 @@ and elab_struct_or_union_info keep_ty kind loc env members attrs = end else begin fatal_error loc "empty union is a GNU extension" end; + let ci = composite_info_def env' kind attrs m in + (* Warn for reduced alignment *) + if attrs <> [] then begin + let ci_nat = composite_info_def env' kind [] m in + warn_if_reduced_alignment loc + ~actual:ci.Env.ci_alignof ~natural:ci_nat.Env.ci_alignof + end; + (* Final result *) (composite_info_def env' kind attrs m, env') -and elab_struct_or_union keep_ty only kind loc tag optmembers attrs env = +and elab_struct_or_union only kind loc tag optmembers attrs env = let warn_attrs () = if attrs <> [] then - warning loc Unnamed "attribute declaration must precede definition" in + warning loc Ignored_attributes "attribute declaration must precede definition" in let optbinding, tag = match tag with | None -> None, "" | Some s -> + if redef Env.lookup_enum env s then + error loc "'%s' redeclared as different kind of symbol" s; Env.lookup_composite env s, s in match optbinding, optmembers with @@ -910,9 +1104,9 @@ and elab_struct_or_union keep_ty only kind loc tag optmembers attrs env = | Some(tag', ({Env.ci_sizeof = None} as ci)), Some members when Env.in_current_scope env tag' -> if ci.Env.ci_kind <> kind then - error loc "use of '%s' with tag type that does not match previous declaration" tag; + fatal_error loc "use of '%s' with tag type that does not match previous declaration" tag; (* 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 + let (ci', env') = elab_struct_or_union_info kind loc env members attrs in (* Emit a global definition for it *) emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.Env.ci_members)); (* Replace infos but keep same ident *) @@ -939,7 +1133,7 @@ and elab_struct_or_union keep_ty 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 keep_ty kind loc env' members attrs in + elab_struct_or_union_info kind loc env' members attrs in (* emit a definition *) emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.Env.ci_members)); (* Replace infos but keep same ident *) @@ -965,7 +1159,7 @@ and elab_enum_item env ((s, exp), loc) nextval = if redef Env.lookup_typedef env s then 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 Constant_conversion "integer literal '%Ld' is too large to be represented in any integer type" + warning loc Constant_conversion "integer literal '%Ld' is too large to be represented in the enumeration integer type" v; let (id, env') = Env.enter_enum_item env s v in ((id, v, exp'), Int64.succ v, env') @@ -973,10 +1167,15 @@ and elab_enum_item env ((s, exp), loc) nextval = (* Elaboration of an enumeration declaration. C99 section 6.7.2.2 *) and elab_enum only loc tag optmembers attrs env = - let tag = match tag with None -> "" | Some s -> s in + let tag = match tag with + | None -> "" + | Some s -> + if redef Env.lookup_struct env s || redef Env.lookup_union env s then + error loc "'%s' redeclared as different kind of symbol" s; + s in match optmembers with | None -> - if only then + if only && not (redef Env.lookup_enum env tag) then fatal_error loc "forward declaration of 'enum %s' is not allowed in ISO C" tag; let (tag', info) = wrap Env.lookup_enum loc env tag in (tag', env) @@ -998,10 +1197,12 @@ 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 false loc env spec in - let ((ty, _), env'') = elab_type_declarator false loc env' bty false decl in + let (sto, inl, noret, tydef, bty, env') = elab_specifier loc env spec in + let ((ty, _), env'') = elab_type_declarator loc env' bty decl in + (* NB: it seems the parser doesn't accept any of the specifiers below. + We keep the error message as extra safety. *) if sto <> Storage_default || inl || noret || tydef then - error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast"; + error loc "'typedef', 'extern', 'static', 'auto', 'register' and 'inline' are meaningless in cast"; (ty, env'') @@ -1040,11 +1241,11 @@ let check_init_type loc env a ty = else if wrap2 valid_cast loc env a.etyp ty then 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" + "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" + "incompatible conversion: initializer has type %a instead of the expected type %a" (print_typ env) a.etyp (print_typ env) ty else error loc @@ -1087,6 +1288,9 @@ module I = struct (* Change the initializer for the current point *) let set (z, i) i' = (z, i') + (* Is the current point at top? *) + let at_top = function Ztop(_, _), _ -> true | _, _ -> false + (* Put the current point back to the top *) let rec to_top = function | Ztop(name, ty), i as zi -> zi @@ -1372,7 +1576,13 @@ and elab_single zi a il = from the expression: do as above *) elab_list (I.set zi (Init_single a)) il false | TStruct _ | TUnion _ | TArray _ -> - (* This is an aggregate: we need to drill into it, recursively *) + (* This is an aggregate. + At top, explicit { } are required. *) + if I.at_top zi then begin + error loc "invalid initializer, an initializer list was expected"; + raise Exit + end; + (* Otherwise we need to drill into the aggregate, recursively *) begin match I.first env zi with | I.OK zi' -> elab_single zi' a il @@ -1434,23 +1644,51 @@ let elab_initializer loc env root ty ie = (fixup_typ loc env ty init, Some init) +(* Contexts for elaborating statements and expressions *) + +type elab_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_in_switch: bool; (**r are 'case' and 'default' allowed? *) + ctx_vararg: bool; (**r is this a vararg function? *) + ctx_nonstatic_inline: bool (**r is this a nonstatic inline function? *) +} + +(* Context for evaluating compile-time constant expressions. + Only the [ctx_vararg] and [ctx_nonstatic_inline] fields matter. *) +let ctx_constexp = { + ctx_return_typ = TVoid []; + ctx_labels = StringSet.empty; + ctx_break = false; ctx_continue = false; ctx_in_switch = false; + ctx_vararg = false; ctx_nonstatic_inline = false +} + + (* Elaboration of expressions *) -let elab_expr vararg loc env a = +let elab_expr ctx loc env a = - let err fmt = error loc fmt in (* non-fatal error *) - let error fmt = fatal_error loc fmt in - let warning t fmt = - warning loc t fmt in + let error fmt = error loc fmt in + let fatal_error fmt = fatal_error 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 + error "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 + error "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 + error "arithmetic on a pointer to an incomplete type %a in binary '%c'" (print_typ env) ty s + in + + let check_static_var id sto ty = + if ctx.ctx_nonstatic_inline + && sto = Storage_static + && List.mem AConst (attributes_of_type env ty) + then warning Static_in_inline "static variable '%s' is used in an inline function with external linkage" id.C.name in let rec elab env = function @@ -1459,7 +1697,8 @@ let elab_expr vararg loc env a = | VARIABLE s -> begin match wrap Env.lookup_ident loc env s with - | (id, Env.II_ident(sto, ty)) -> + | (id, Env.II_ident(sto, ty)) -> + check_static_var id sto ty; { edesc = EVar id; etyp = ty },env | (id, Env.II_enum v) -> { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) },env @@ -1478,7 +1717,7 @@ let elab_expr vararg 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 "subscripted value is neither an array nor pointer" in + | t1, t2 -> fatal_error "subscripted value is neither an array nor pointer" in { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres },env | MEMBEROF(a1, fieldname) -> @@ -1490,7 +1729,7 @@ let elab_expr vararg loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "request for member '%s' in something not a structure or union" fieldname in + fatal_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 *) let rec access = function | [] -> b1 @@ -1512,10 +1751,10 @@ let elab_expr vararg loc env a = | TUnion(id, attrs) -> (wrap Env.find_union_member loc env (id, fieldname), attrs) | _ -> - error "request for member '%s' in something not a structure or union" fieldname + fatal_error "request for member '%s' in something not a structure or union" fieldname end | _ -> - error "member reference type %a is not a pointer" (print_typ env) b1.etyp in + fatal_error "member reference type %a is not a pointer" (print_typ env) b1.etyp in let rec access = function | [] -> assert false | [fld] -> @@ -1538,8 +1777,8 @@ let elab_expr vararg 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"; + if not ctx.ctx_vararg then + error "'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 @@ -1584,9 +1823,9 @@ let elab_expr vararg loc env a = | TPtr(ty, a) -> begin match unroll env ty with | TFun(res, args, vararg, a) -> (res, args, vararg) - | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp + | _ -> fatal_error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp end - | _ -> error "called object type %a is neither a function nor function pointer" (print_typ env) b1.etyp + | _ -> fatal_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 = @@ -1608,18 +1847,18 @@ let elab_expr vararg loc env a = if not (wrap2 valid_cast loc env b1.etyp ty) then begin match unroll env b1.etyp, unroll env ty with | _, (TStruct _|TUnion _ | TVoid _) -> - err "used type %a where arithmetic or pointer type is required" + error "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" + error "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" + error "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 + error "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 + error "illegal cast from %a to %a" (print_typ env) b1.etyp (print_typ env) ty end; { edesc = ECast(ty, b1); etyp = ty },env @@ -1629,7 +1868,7 @@ let elab_expr vararg loc env a = 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" + | (ty', None) -> fatal_error "ill-formed compound literal" end (* 6.5.3 Unary expressions *) @@ -1637,54 +1876,39 @@ let elab_expr vararg loc env a = | EXPR_SIZEOF a1 -> let b1,env = elab env a1 in if wrap incomplete_type loc env b1.etyp then - error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; + fatal_error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) b1.etyp; if wrap is_bitfield loc env b1 then - error "invalid application of 'sizeof' to a bit-field"; - let bdesc = - (* Catch special cases sizeof("string literal") *) - match b1.edesc with - | EConst(CStr s) -> - let sz = String.length s + 1 in - EConst(CInt(Int64.of_int sz, size_t_ikind(), "")) - | EConst(CWStr s) -> - let sz = (!config).sizeof_wchar * (List.length s + 1) in - EConst(CInt(Int64.of_int sz, size_t_ikind(), "")) - | _ -> - ESizeof b1.etyp in - { edesc = bdesc; etyp = TInt(size_t_ikind(), []) },env + fatal_error "invalid application of 'sizeof' to a bit-field"; + { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind(), []) },env | TYPE_SIZEOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then - error "invalid application of 'sizeof' to an incomplete type %a" (print_typ env) ty; + fatal_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 - error "invalid application of '_Alignof' to an incomplete type %a" (print_typ env) b1.etyp; - if wrap is_bitfield loc env b1 then - error "invalid application of '_Alignof' to a bit-field"; - { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) },env - - | TYPE_ALIGNOF (spec, dcl) -> + | ALIGNOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in + warning Celeven_extension "'_Alignof' is a C11 extension"; if wrap incomplete_type loc env' ty then - error "invalid application of 'alignof' to an incomplete type %a" (print_typ env) ty; + fatal_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; + fatal_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 + | _ -> fatal_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 + | fld::rest -> + if fld.fld_bitfield <> None then + fatal_error "cannot compute offset of bit-field '%s'" fld.fld_name; + 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 @@ -1696,16 +1920,16 @@ let elab_expr vararg loc env a = | 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" + | None -> fatal_error "array element designator 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" + | None -> fatal_error "'offsetof' overflows" | Some s -> off_accu + s in env,off_accu,sub_ty - | ATINDEX_INIT _,_ -> error "subscripted value is not an array" in + | ATINDEX_INIT _,_ -> fatal_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 @@ -1715,46 +1939,46 @@ let elab_expr vararg loc env a = | UNARY(PLUS, a1) -> let b1,env = elab env a1 in if not (is_arith_type env b1.etyp) then - error "invalid argument type %a to unary '+'" (print_typ env) b1.etyp; + fatal_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 - error "invalid argument type %a to unary '-'" (print_typ env) b1.etyp; + fatal_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 - error "invalid argument type %a to unary '~'" (print_typ env) b1.etyp; + fatal_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 - error "invalid argument type %a to unary '!'" (print_typ env) b1.etyp; + fatal_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 lvalue (invalid %a)" (print_typ env) b1.etyp; + error "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 | Env.II_ident(Storage_register, _) -> - err "address of register variable '%s' requested" id.C.name + error "address of register variable '%s' requested" id.C.name | _ -> () end | EUnop(Odot f, b2) -> let fld = wrap2 field_of_dot_access loc env b2.etyp f in if fld.fld_bitfield <> None then - err "address of bit-field '%s' requested" f + error "address of bit-field '%s' requested" f | EUnop(Oarrow f, b2) -> let fld = wrap2 field_of_arrow_access loc env b2.etyp f in if fld.fld_bitfield <> None then - err "address of bit-field '%s' requested" f + error "address of bit-field '%s' requested" f | _ -> () end; { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) },env @@ -1767,7 +1991,7 @@ let elab_expr vararg loc env a = | TPtr(ty, _) | TArray(ty, _, _) -> { edesc = EUnop(Oderef, b1); etyp = ty },env | _ -> - error "arguemnt of unary '*' is not a pointer (%a invalid)" + fatal_error "argument of unary '*' is not a pointer (%a invalid)" (print_typ env) b1.etyp end @@ -1798,7 +2022,7 @@ let elab_expr vararg 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 "invalid operands to binary '+' (%a and %a)" + | _, _ -> fatal_error "invalid operands to binary '+' (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp in check_ptr_arith env ty '+'; @@ -1817,21 +2041,19 @@ let elab_expr vararg loc env a = match wrap unroll loc env b1.etyp, wrap unroll loc env b2.etyp with | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> 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)) -> - check_ptr_arith env ty '-'; + error "illegal pointer arithmetic in binary '-'"; (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 "%a and %a are not pointers to compatible types" + error "%a and %a are not pointers to compatible types" (print_typ env) b1.etyp (print_typ env) b1.etyp; check_ptr_arith env ty1 '-'; + check_ptr_arith env ty2 '-'; if wrap sizeof loc env ty1 = Some 0 then - err "subtraction between two pointers to zero-sized objects"; + error "subtraction between two pointers to zero-sized objects"; (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) - | _, _ -> error "invalid operands to binary '-' (%a and %a)" + | _, _ -> fatal_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 @@ -1875,7 +2097,7 @@ let elab_expr vararg 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 "first argument of '?:' is not a scalar type (invalid %a)" + error "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 _) -> @@ -1903,7 +2125,7 @@ let elab_expr vararg loc env a = | ty1, ty2 -> match combine_types AttrIgnoreAll env ty1 ty2 with | None -> - error "the second and third argument of '?:' incompatible types (%a and %a)" + fatal_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 @@ -1917,7 +2139,7 @@ let elab_expr vararg loc env a = if List.mem AConst (attributes_of_type env b1.etyp) then error "left-hand side of assignment has 'const' type"; if not (is_modifiable_lvalue env b1) then - err "expression is not assignable"; + error "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 if wrap2 int_pointer_conversion loc env b2.etyp b1.etyp then @@ -1926,10 +2148,10 @@ let elab_expr vararg loc env a = (print_typ env) b1.etyp (print_typ env) b2.etyp else warning Unnamed - "incompatible conversion assigning to %a from %a" + "incompatible conversion: assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) b2.etyp else - err "assigning to %a from incompatible type %a" + error "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 @@ -1953,9 +2175,9 @@ let elab_expr vararg loc env a = begin match elab env (BINARY(sop, a1, a2)) with | ({ edesc = EBinop(_, b1, b2, _); etyp = ty } as b),env -> 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 "expression is not assignable"; + error "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 if wrap2 int_pointer_conversion loc env ty b1.etyp then @@ -1964,10 +2186,10 @@ let elab_expr vararg loc env a = (print_typ env) b1.etyp (print_typ env) ty else warning Unnamed - "incompatible conversion assigning to %a from %a" + "incompatible conversion: assigning to %a from %a" (print_typ env) b1.etyp (print_typ env) ty else - err "assigning to %a from incompatible type %a" + error "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 @@ -1986,9 +2208,9 @@ let elab_expr vararg loc env a = 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 "expression is not assignable"; + error "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; + error "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 *) @@ -1996,7 +2218,7 @@ let elab_expr vararg loc env a = 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 + fatal_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 @@ -2006,7 +2228,7 @@ let elab_expr vararg loc env a = 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 + fatal_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 @@ -2016,7 +2238,7 @@ let elab_expr vararg loc env a = 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 + fatal_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 @@ -2043,6 +2265,10 @@ let elab_expr vararg loc env a = if not (compatible_types AttrIgnoreAll env ty1 ty2) then warning Compare_distinct_pointer_types "comparison of distinct pointer types (%a and %a)" (print_typ env) b1.etyp (print_typ env) b2.etyp; + let incomp_ty1 = wrap incomplete_type loc env ty1 + and incomp_ty2 = wrap incomplete_type loc env ty2 in + if incomp_ty1 <> incomp_ty2 then + warning Unnamed "comparison of complete and incomplete pointers"; EBinop(op, b1, b2, TPtr(ty1, [])) | TPtr _, (TInt _ | TEnum _) | (TInt _ | TEnum _), TPtr _ -> @@ -2050,7 +2276,7 @@ let elab_expr vararg loc env 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" + fatal_error "illegal comparison between types@ %a@ and %a" (print_typ env) b1.etyp (print_typ env) b2.etyp; in { edesc = resdesc; etyp = TInt(IInt, []) },env @@ -2059,7 +2285,7 @@ let elab_expr vararg loc env a = 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 + fatal_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 @@ -2071,14 +2297,14 @@ let elab_expr vararg loc env a = let found = argno - 1 in let expected = List.length params + found in let vararg = if vararg then "at least " else "" in - err "too few arguments to function call, expected %s%d, have %d" vararg expected found; [],env + error "too few arguments to function call, expected %s%d, have %d" vararg expected found; [],env | (_::_,env), [] -> if vararg then 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) + (error "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) @@ -2090,10 +2316,10 @@ let elab_expr vararg loc env 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" + "incompatible conversion: passing %a to parameter %d of type %a" (print_typ env) ty_a argno (print_typ env) ty_p end else - err + error "passing %a to parameter %d of incompatible type %a" (print_typ env) ty_a argno (print_typ env) ty_p end; @@ -2102,16 +2328,16 @@ let elab_expr vararg loc env a = in elab env a (* Filling in forward declaration *) -let _ = elab_expr_f := (elab_expr false) +let _ = elab_expr_f := (elab_expr ctx_constexp) -let elab_opt_expr vararg loc env = function +let elab_opt_expr ctx loc env = function | None -> None,env - | Some a -> let a,env = (elab_expr vararg loc env a) in + | Some a -> let a,env = (elab_expr ctx loc env a) in Some a,env -let elab_for_expr vararg loc env = function +let elab_for_expr ctx loc env = function | None -> { sdesc = Sskip; sloc = elab_loc loc },env - | Some a -> let a,env = elab_expr vararg loc env a in + | Some a -> let a,env = elab_expr ctx loc env a in { sdesc = Sdo a; sloc = elab_loc loc },env (* Handling of __func__ (section 6.4.2.2) *) @@ -2125,49 +2351,69 @@ let __func__type_and_init s = let enter_typedefs loc env sto dl = if sto <> Storage_default then - error loc "non-default storage-class on 'typedef' definition"; + error loc "non-default storage class on 'typedef' definition"; + if dl = [] then + warning loc Missing_declarations "typedef requires a name"; List.fold_left (fun env (s, ty, init) -> if init <> NO_INIT then error loc "initializer in typedef"; + if has_std_alignas env ty then + error loc "alignment specified for typedef '%s'" s; match previous_def Env.lookup_typedef env s with - | Some (s',ty') -> + | Some (s',ty') when Env.in_current_scope env s' -> if equal_types env ty ty' then begin - warning loc Celeven_extension "redefinition of typedef '%s' is C11 extension" s; + warning loc Celeven_extension "redefinition of typedef '%s' is a C11 extension" s; env end else begin 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 '%s' as different kind of symbol" s; let (id, env') = Env.enter_typedef env s ty in + check_reduced_alignment loc env' ty; emit_elab env loc (Gtypedef(id, ty)); env') env dl -let enter_decdefs local loc env sto dl = +let enter_decdefs local nonstatic_inline loc env sto dl = (* Sanity checks on storage class *) - if sto = Storage_register && not local then - fatal_error loc "'register' storage-class on file-scoped variable"; + if (sto = Storage_auto || sto = Storage_register) && not local then + fatal_error loc "illegal storage class %s on file-scoped variable" + (name_of_storage_class sto); if sto <> Storage_default && 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_register && has_std_alignas env ty then + error loc "alignment specified for 'register' object '%s'" s; if sto = Storage_extern && init <> NO_INIT then - error loc "'extern' declaration variable has an initializer"; + 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"; + | Storage_static -> + error loc "function declared in block scope cannot have 'static' storage class" + | Storage_auto | Storage_register -> + error loc "illegal storage class %s on function" + (name_of_storage_class sto) | _ -> () end; - (* Local function declarations are always treated as extern *) - let sto1 = if local && isfun then Storage_extern else sto in + if is_qualified_array ty then + error loc "type qualifier used in array declarator outside of function prototype"; + (* Local variable declarations with default storage are treated as 'auto'. + Local function declarations with default storage remain with + default storage. *) + let sto1 = + if local && sto = Storage_default && not isfun + then Storage_auto + else sto in (* enter ident in environment with declared type, because initializer can refer to the ident *) let (id, sto', env1, ty, linkage) = enter_or_refine_ident local loc env s sto1 ty in + if init <> NO_INIT && not local then + add_global_define loc s; if not isfun && is_void_type env ty then fatal_error loc "'%s' has incomplete type" s; (* process the initializer *) @@ -2175,16 +2421,30 @@ let enter_decdefs local loc env sto dl = (* update environment with refined type *) let env2 = Env.add_ident env1 id sto' ty' in (* check for incomplete type *) - if local && sto' <> Storage_extern - && not isfun - && wrap incomplete_type loc env ty' then - error loc "variable has incomplete type %a" (print_typ env) ty'; + if not isfun && wrap incomplete_type loc env ty' then + if not local && sto' = Storage_static then begin + warning loc Tentative_incomplete_static "tentative static definition with incomplete type"; + end else if local && sto' <> Storage_extern then + error loc "variable has incomplete type %a" (print_typ env) ty'; + (* check if alignment is reduced *) + check_reduced_alignment loc env ty'; + (* check for static variables in nonstatic inline functions *) + if local && nonstatic_inline + && sto' = Storage_static + && not (List.mem AConst (attributes_of_type env ty')) then + warning loc Static_in_inline "non-constant static local variable '%s' in inline function may be different in different files" s; if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then (* Local definition *) ((sto', id, ty', init') :: decls, env2) else begin (* Global definition *) emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init')); + (* Make sure the initializer is constant. *) + begin match init' with + | Some i when not (Ceval.is_constant_init env2 i) -> + error loc "initializer is not a compile-time constant" + | _ -> () + end; (decls, env2) end in let (decls, env') = List.fold_left enter_decdef ([], env) dl in @@ -2216,7 +2476,7 @@ let elab_KR_function_parameters env params defs loc = (* 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; + error loc' "declaration of '%s' which is not a function parameter" s; if ie <> NO_INIT then error loc' "illegal initialization of parameter '%s'" s; name @@ -2225,18 +2485,17 @@ let elab_KR_function_parameters env params defs loc = let elab_param_def env = function | DECDEF((spec', name_init_list), loc') -> let name_list = List.map extract_name name_init_list in - let (paramsenv, sto) = elab_name_group 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; + if name_list = [] then + error loc' "declaration does not declare a parameter"; + let (paramsenv, sto) = elab_name_group loc' env (spec', name_list) in + if sto <> Storage_default && sto <> Storage_register then + error loc' (* NB: 'auto' not allowed *) + "invalid storage class %s for function parameter" + (name_of_storage_class sto); paramsenv | d -> (* Should never be produced by the parser *) fatal_error (Cabshelper.get_definitionloc d) - "Illegal declaration of function parameter" in + "illegal declaration of function parameter" in let kr_params_defs,paramsenv = let params,paramsenv = mmap elab_param_def env defs in List.concat params,paramsenv in @@ -2296,11 +2555,22 @@ let inherit_vararg env s sto ty = (* Function definitions *) -let elab_fundef env spec name defs body loc = - let (s, sto, inline, noret, ty, kr_params, env1) = - elab_fundef_name true env spec name in - if sto = Storage_register then - fatal_error loc "invalid 'register' storage-class on function"; +let elab_fundef genv spec name defs body loc = + (* We maintain two environments: + - genv is the "global", file-scope environment. It is enriched + with the declaration of the function, and also with + structs and unions defined as part of its return type. + - lenv is the "local" environment used to elaborate the function body. + It contains everything that genv contains, including + a declaration for the function, so as to support recursive calls. + In addition, it contains declarations for function parameters + and structs and unions defined in the parameter list. *) + let (fun_id, sto, inline, noret, ty, kr_params, genv, lenv) = + elab_fundef_name genv spec name in + let s = fun_id.C.name in + if sto = Storage_auto || sto = Storage_register then + fatal_error loc "invalid storage class %s on function" + (name_of_storage_class sto); begin match kr_params, defs with | None, d::_ -> error (Cabshelper.get_definitionloc d) @@ -2310,54 +2580,77 @@ let elab_fundef env spec name defs body loc = (* 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,env1) = + beginning of the function + - [lenv]: a first cut at the local environment, containing in particular + the structs and unions defined in the parameter list. *) + let (ty, extra_decls, lenv) = match ty, kr_params with | TFun(ty_ret, None, vararg, attr), None -> - (TFun(ty_ret, Some [], vararg, attr), [],env1) + (TFun(ty_ret, Some [], vararg, attr), [], lenv) | ty, None -> - (ty, [],env1) + (ty, [], lenv) | TFun(ty_ret, None, false, attr), Some params -> 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) + let (params', extra_decls, lenv) = + elab_KR_function_parameters lenv params defs loc in + (TFun(ty_ret, Some params', inherit_vararg genv s sto ty, attr), extra_decls, lenv) | _, Some params -> assert false in - (* Extract infos from the type of the function *) + (* Extract infos from the type of the function. + Checks on the return type must be done in the global environment. *) 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 + if has_std_alignas genv ty then + error loc "alignment specified for function '%s'" s; + if wrap incomplete_type loc genv ty_ret && not (is_void_type genv ty_ret) then fatal_error loc "incomplete result type %a in function definition" - (print_typ env) ty_ret; + (print_typ genv) 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 = + (* Enter function in the global environment *) + let (fun_id, sto1, genv, new_ty, _) = + enter_or_refine_function loc genv fun_id sto ty in + add_global_define loc s; + (* Also enter it in the local environment, for recursive references *) + let lenv = Env.add_ident lenv fun_id sto new_ty in + (* Take into account attributes from previous declarations of the function *) + let attr = attributes_of_type genv new_ty in + (* Additional checks on function parameters. They should have a complete type + and additionally they should have an identifier. In both cases a fatal + error is raised in order to avoid problems at later places. *) + let add_param env (id, 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) -> incomplete_param e ty; - Env.add_ident e id Storage_default ty) - (Env.new_scope env1) params in - let env2 = + fatal_error loc "parameter has incomplete type"; + if id.C.name = "" then + fatal_error loc "parameter name omitted"; + Env.add_ident env id Storage_default ty + in + (* Enter parameters and extra declarations in the local environment. + For K&R functions this hasn't been done yet. + For prototyped functions this has been done by [elab_fundef_name] + already, but some parameter may have been shadowed by the + function name, while it should be the other way around, e.g. + [int f(int f) { return f+1; }], with [f] refering to the + parameter [f] and not to the function [f] within the body of the + function. *) + let lenv = + List.fold_left add_param lenv params in + let lenv = List.fold_left (fun e (sto, id, ty, init) -> Env.add_ident e id sto ty) - env2 extra_decls in - (* Define "__func__" and enter it in the environment *) + lenv extra_decls in + (* Define "__func__" and enter it in the local environment *) let (func_ty, func_init) = __func__type_and_init s in - let (func_id, _, env3, func_ty, _) = - enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in - emit_elab ~debuginfo:false env3 loc + let (func_id, _, lenv, func_ty, _) = + enter_or_refine_ident true loc lenv "__func__" Storage_static func_ty in + emit_elab ~debuginfo:false lenv loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) - let body1 = !elab_funbody_f ty_ret vararg env3 body in + let body1 = !elab_funbody_f ty_ret vararg (inline && sto <> Storage_static) + lenv body in (* Analyse it for returns *) - let (can_return, can_fallthrough) = Cflow.function_returns env3 body1 in + let (can_return, can_fallthrough) = Cflow.function_returns lenv body1 in (* Special treatment of the "main" function. *) let body2 = if s = "main" then begin @@ -2365,7 +2658,7 @@ let elab_fundef env spec name defs body loc = error loc "'main' is not allowed to be declared inline"; if noret then warning loc Unnamed "'main' is not allowed to be declared _Noreturn"; - match unroll env ty_ret with + match unroll genv ty_ret with | TInt(IInt, []) -> (* Add implicit "return 0;" at end of function body. If we trusted the return analysis, we would do this only if @@ -2378,7 +2671,7 @@ let elab_fundef env spec name defs body loc = end else begin (* For non-"main" functions, warn if the body can fall through and the return type is not "void". *) - if can_fallthrough && not (is_void_type env ty_ret) then + if can_fallthrough && not (is_void_type genv ty_ret) then warning loc Return_type "control reaches end of non-void function"; body1 end in @@ -2407,12 +2700,13 @@ let elab_fundef env spec name defs body loc = fd_vararg = vararg; fd_locals = []; fd_body = body3 } in - emit_elab ~linkage:true env1 loc (Gfundef fn); - env1 + emit_elab ~linkage:true genv loc (Gfundef fn); + genv (* Definitions *) -let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) +let elab_definition (for_loop: bool) (local: bool) (nonstatic_inline: bool) + (env: Env.t) (def: Cabs.definition) : decl list * Env.t = match def with (* "int f(int x) { ... }" *) @@ -2425,44 +2719,32 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) (* "int x = 12, y[10], *z" *) | DECDEF(init_name_group, loc) -> let ((dl, env1), sto, tydef) = - elab_init_name_group false loc env init_name_group in + elab_init_name_group loc env init_name_group in + if for_loop then begin + let fun_declaration = List.exists (fun (_, ty, _) -> is_function_type env ty) dl in + if fun_declaration || sto = Storage_extern || sto = Storage_static || tydef then + error loc "declaration of non-local variable in 'for' loop" ; + end; if tydef then let env2 = enter_typedefs loc env1 sto dl in ([], env2) else - enter_decdefs local loc env1 sto dl + enter_decdefs local nonstatic_inline loc env1 sto dl (* pragma *) | PRAGMA(s, loc) -> emit_elab env loc (Gpragma s); ([], env) -and elab_definitions local env = function - | [] -> ([], env) - | d1 :: dl -> - let (decl1, env1) = elab_definition local env d1 in - let (decl2, env2) = elab_definitions local env1 dl in - (decl1 @ decl2, env2) - (* Extended asm *) -let elab_asm_operand vararg loc env (ASMOPERAND(label, wide, chars, e)) = +let elab_asm_operand ctx loc env (ASMOPERAND(label, wide, chars, e)) = let s = elab_simple_string loc wide chars in - let e',env = elab_expr vararg loc env e in + let e',env = elab_expr ctx loc env e in (label, s, e'),env -(* Contexts for elaborating statements *) - -module StringSet = Set.Make(String) - -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_vararg: bool; (**r is this a vararg function? *) -} +(* Operations over contexts *) let stmt_labels stmt = let lbls = ref StringSet.empty in @@ -2487,7 +2769,48 @@ let stmt_labels stmt = let ctx_loop ctx = { ctx with ctx_break = true; ctx_continue = true } -let ctx_switch ctx = { ctx with ctx_break = true } +let ctx_switch ctx = { ctx with ctx_break = true; ctx_in_switch = true } + +(* Check the uniqueness of 'case' and 'default' in a 'switch' *) + +module Int64Set = Set.Make(Int64) + +let check_switch_cases switch_body = + let cases = ref Int64Set.empty + and default = ref false in + let rec check s = + match s.sdesc with + | Sskip -> () + | Sdo _ -> () + | Sseq(s1, s2) -> check s1; check s2 + | Sif(_, s1, s2) -> check s1; check s2 + | Swhile(_, s1) -> check s1 + | Sdowhile(s1, _) -> check s1 + | Sfor(s1, _, s2, s3) -> check s1; check s2; check s3 + | Sbreak -> () + | Scontinue -> () + | Sswitch(_, _) -> () (* already checked during elaboration of this switch *) + | Slabeled(lbl, s1) -> + begin match lbl with + | Slabel _ -> () + | Scase(_, n) -> + if Int64Set.mem n !cases then + Diagnostics.error s.sloc "duplicate case value '%Ld'" n + else + cases := Int64Set.add n !cases + | Sdefault -> + if !default then + Diagnostics.error s.sloc "multiple default labels in one switch" + else + default := true + end; + check s1 + | Sgoto _ -> () + | Sreturn _ -> () + | Sblock sl -> List.iter check sl + | Sdecl _ -> () + | Sasm _ -> () + in check switch_body (* Elaboration of statements *) @@ -2498,7 +2821,7 @@ let rec elab_stmt env ctx s = (* 6.8.3 Expression statements *) | COMPUTATION(a, loc) -> - let a,env = (elab_expr ctx.ctx_vararg loc env a) in + let a,env = elab_expr ctx loc env a in { sdesc = Sdo a; sloc = elab_loc loc },env (* 6.8.1 Labeled statements *) @@ -2508,16 +2831,20 @@ 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 ctx.ctx_vararg loc env a in - begin match Ceval.integer_expr env a' with + if not ctx.ctx_in_switch then + error loc "'case' statement not in switch statement"; + let a',env = elab_expr ctx loc env a in + let n = + match Ceval.integer_expr env a' with | None -> - error loc "expression of 'case' label is not an integer constant expression" - | Some n -> () - end; + error loc "expression of 'case' label is not an integer constant expression"; 0L + | Some n -> n in let s1,env = elab_stmt env ctx s1 in - { sdesc = Slabeled(Scase a', s1); sloc = elab_loc loc },env + { sdesc = Slabeled(Scase(a', n), s1); sloc = elab_loc loc },env | DEFAULT(s1, loc) -> + if not ctx.ctx_in_switch then + error loc "'case' statement not in switch statement"; let s1,env = elab_stmt env ctx s1 in { sdesc = Slabeled(Sdefault, s1); sloc = elab_loc loc },env @@ -2529,7 +2856,7 @@ let rec elab_stmt env ctx s = (* 6.8.4 Conditional statements *) | If(a, s1, s2, loc) -> - let a',env = elab_expr ctx.ctx_vararg loc env a in + let a',env = elab_expr ctx loc env a in if not (is_scalar_type env a'.etyp) then error loc "controlling expression of 'if' does not have scalar type (%a invalid)" (print_typ env) a'.etyp; @@ -2544,7 +2871,7 @@ let rec elab_stmt env ctx s = (* 6.8.5 Iterative statements *) | WHILE(a, s1, loc) -> - let a',env = elab_expr ctx.ctx_vararg loc env a in + let a',env = elab_expr ctx loc env a in if not (is_scalar_type env a'.etyp) then error loc "controlling expression of 'while' does not have scalar type (%a invalid)" (print_typ env) a'.etyp; @@ -2553,7 +2880,7 @@ let rec elab_stmt env ctx s = | DOWHILE(a, s1, loc) -> let s1',env = elab_stmt env (ctx_loop ctx) s1 in - let a',env = elab_expr ctx.ctx_vararg loc env a in + let a',env = elab_expr ctx loc env a in if not (is_scalar_type env a'.etyp) then error loc "controlling expression of 'while' does not have scalar type (%a invalid)" (print_typ env) a'.etyp; @@ -2563,24 +2890,25 @@ let rec elab_stmt env ctx s = let (a1', env_decls, decls') = match fc with | Some (FC_EXP a1) -> - let a1,env = elab_for_expr ctx.ctx_vararg loc env (Some a1) in + let a1,env = elab_for_expr ctx loc env (Some a1) in (a1, env, None) | None -> - let a1,env = elab_for_expr ctx.ctx_vararg loc env None in + let a1,env = elab_for_expr ctx loc env None in (a1, env, None) | Some (FC_DECL def) -> - let (dcl, env') = elab_definition true (Env.new_scope env) def in + let (dcl, env') = elab_definition true true ctx.ctx_nonstatic_inline + (Env.new_scope env) 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_test = match a2 with | None -> intconst 1L IInt,env_decls - | Some a2 -> elab_expr ctx.ctx_vararg loc env_decls a2 + | Some a2 -> elab_expr ctx loc env_decls a2 in if not (is_scalar_type env_test a2'.etyp) then error loc "controlling expression of 'for' does not have scalar type (%a invalid)" (print_typ env) a2'.etyp; - let a3',env_for = elab_for_expr ctx.ctx_vararg loc env_test a3 in + let a3',env_for = elab_for_expr ctx loc env_test a3 in let s1',env_body = elab_stmt env_for (ctx_loop ctx) s1 in let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in begin match decls' with @@ -2590,11 +2918,12 @@ let rec elab_stmt env ctx s = (* 6.8.4 Switch statement *) | SWITCH(a, s1, loc) -> - let a',env = elab_expr ctx.ctx_vararg loc env a in + let a',env = elab_expr ctx loc env a in if not (is_integer_type env a'.etyp) then 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 + check_switch_cases s1'; { sdesc = Sswitch(a', s1'); sloc = elab_loc loc },env (* 6.8.6 Break and continue statements *) @@ -2609,7 +2938,7 @@ let rec elab_stmt env ctx s = (* 6.8.6 Return statements *) | RETURN(a, loc) -> - let a',env = elab_opt_expr ctx.ctx_vararg loc env a in + let a',env = elab_opt_expr ctx loc env a in begin match (unroll env ctx.ctx_return_typ, a') with | TVoid _, None -> () | TVoid _, Some _ -> @@ -2628,7 +2957,7 @@ let rec elab_stmt env ctx s = (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" + "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 @@ -2652,8 +2981,13 @@ 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 ctx.ctx_vararg loc) env outputs in - let inputs ,env= mmap (elab_asm_operand ctx.ctx_vararg loc) env inputs in + let outputs,env = mmap (elab_asm_operand ctx loc) env outputs in + List.iter + (fun (lbl, cst, e) -> + if not (is_modifiable_lvalue env e) then + error loc "asm output is not a modifiable l-value";) + outputs; + let inputs ,env= mmap (elab_asm_operand ctx 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 @@ -2672,7 +3006,8 @@ and elab_block_body env ctx sl = | [] -> [],env | DEFINITION def :: sl1 -> - let (dcl, env') = elab_definition true env def in + let (dcl, env') = + elab_definition false true ctx.ctx_nonstatic_inline env 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; @@ -2686,14 +3021,24 @@ and elab_block_body env ctx sl = (* Elaboration of a function body. Return the corresponding C statement. *) -let elab_funbody return_typ vararg env b = +let elab_funbody return_typ vararg nonstatic_inline env b = let ctx = { ctx_return_typ = return_typ; ctx_labels = stmt_labels b; ctx_break = false; ctx_continue = false; - ctx_vararg = vararg;} in - fst(elab_stmt env ctx b) + ctx_in_switch = false; + ctx_vararg = vararg; + ctx_nonstatic_inline = nonstatic_inline } in + (* The function body appears as a block in the AST but should not create + a new scope. Instead, the scope used for function parameters must be + used for the body. *) + match b with + | BLOCK (b,loc) -> + let b',_ = elab_block_body env ctx b in + { sdesc = Sblock b'; sloc = elab_loc loc } + | _ -> + assert false (* Filling in forward declaration *) let _ = elab_funbody_f := elab_funbody @@ -2703,7 +3048,9 @@ let _ = elab_funbody_f := elab_funbody let elab_file prog = reset(); - ignore (elab_definitions false (Builtins.environment()) prog); + let env = Builtins.environment () in + let elab_def env d = snd (elab_definition false false false env d) in + ignore (List.fold_left elab_def env prog); let p = elaborated_program () in Checks.unused_variables p; Checks.unknown_attrs_program p; |