From 8b178cf0b7e9dcc823ad164a6856032627b3bc6f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 31 Jan 2017 16:13:03 +0100 Subject: Revised elaboration of attributes The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that. --- cparser/Elab.ml | 37 ++++++++++++++++++++++++------------- 1 file changed, 24 insertions(+), 13 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1bfc2d11..951ae5b3 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -477,6 +477,13 @@ let typespec_rank = function (* Don't change this *) let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) +(* Auxiliary for type declarator elaboration. Remove the non-type-related + attributes from the given type and return those attributes separately. *) + +let get_nontype_attrs env ty = + let (ta, nta) = List.partition attr_is_type_related (attributes_of_type env ty) in + (change_attributes_type env (fun _ -> ta) ty, nta) + (* Is a specifier an anonymous struct/union in the sense of ISO C2011? *) let is_anonymous_composite spec = @@ -528,14 +535,14 @@ 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 attr_is_struct_related !attr in attr := nta; ta in @@ -594,21 +601,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 +648,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 +667,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 *) -- cgit From be2192f295290c72d56e01263bc354f6844229ec Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 1 Feb 2017 15:38:30 +0100 Subject: Regression: type attributes and array modifiers Owing to the peculiarities of array types in Cutil.change_attributes_type, type-related attributes of the array element type were duplicated on the array type. E.g. elaborating 'const int a[10][5]' produced "a is an array of 5 const arrays of 10 const ints" instead of "a is an array of 5 arrays of 10 const ints" --- cparser/Elab.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 951ae5b3..cc66f04b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -481,8 +481,10 @@ let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) attributes from the given type and return those attributes separately. *) let get_nontype_attrs env ty = - let (ta, nta) = List.partition attr_is_type_related (attributes_of_type env ty) in - (change_attributes_type env (fun _ -> ta) ty, nta) + let nta = + List.filter (fun a -> not (attr_is_type_related a)) + (attributes_of_type env ty) in + (remove_attributes_type env nta ty, nta) (* Is a specifier an anonymous struct/union in the sense of ISO C2011? *) -- cgit From 3babd253e1d194549294c282e1b0c60097b26b07 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 3 Feb 2017 14:12:32 +0100 Subject: Refactor the classification of attributes Introduce Cutil.class_of_attribute to return the class of the given attribute: one among Attr_type attribute related to types (e.g. "aligned") Attr_struct attribute related to struct/union/enum types (e.g. "packed") Attr_function attribute related to function types (e.g. "noreturn") Attr_name attribute related to variable and function declarations (e.g. "section") Attr_unknown attribute was not declared Cutil.declare_attribute is used to associate a class to a custom attribute. Standard attributes (const, volatile, _Alignas, etc) are Attr_type. cfronted/C2C.ml: declare the few attributes that CompCert honors currently. cparser/GCC.ml: a bigger list of attributes taken from GCC, for reference only. --- cparser/Elab.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index cc66f04b..5d2a5cfe 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -478,12 +478,17 @@ let typespec_rank = function (* Don't change this *) let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) (* Auxiliary for type declarator elaboration. Remove the non-type-related - attributes from the given type and return those attributes separately. *) + 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 get_nontype_attrs env ty = - let nta = - List.filter (fun a -> not (attr_is_type_related a)) - (attributes_of_type env ty) in + 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) (* Is a specifier an anonymous struct/union in the sense of ISO C2011? *) @@ -544,7 +549,8 @@ let rec elab_specifier keep_ty ?(only = false) loc env specifier = The leftover non-struct-related attributes will be applied to the variable being defined. *) let get_struct_attrs () = - let (ta, nta) = List.partition attr_is_struct_related !attr in + let (ta, nta) = + List.partition (fun a -> class_of_attribute a = Attr_struct) !attr in attr := nta; ta in -- cgit From 4afaf8c23274752c8a6067bd785e114578068702 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 6 Feb 2017 16:03:45 +0100 Subject: Preliminary support for the "noreturn" attribute - Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type. - Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later. --- cparser/Elab.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 5d2a5cfe..9cffd934 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -767,12 +767,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 *) @@ -2323,17 +2325,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; -- cgit