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.

8 files changed, 38 insertions, 22 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 97bfd6d7..b7fe5fb0 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1098,7 +1098,7 @@ let convertFundef loc env fd =
   Hashtbl.add decl_atom id'
     { a_storage = fd.fd_storage;
       a_alignment = None;
-      a_sections = Sections.for_function env id' fd.fd_ret;
+      a_sections = Sections.for_function env id' fd.fd_attrib;
       a_access = Sections.Access_default;
       a_inline = fd.fd_inline && not fd.fd_vararg;  (* PR#15 *)
       a_loc = loc };
diff --git a/common/Sections.ml b/common/Sections.ml
index b792581f..1c2e8291 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -189,8 +189,7 @@ let for_variable env id ty init =
 
 (* Determine sections for a function definition *)
 
-let for_function env id ty_res =
-  let attr = Cutil.attributes_of_type env ty_res in
+let for_function env id attr =
   let si_code =
     try
       (* 1- Section explicitly associated with #use_section *)
diff --git a/common/Sections.mli b/common/Sections.mli
index 8a13fb8a..b83b0bb4 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -47,5 +47,5 @@ val use_section_for: AST.ident -> string -> bool
 
 val for_variable: Env.t -> AST.ident -> C.typ -> bool ->
                                           section_name * access_mode
-val for_function: Env.t -> AST.ident -> C.typ -> section_name list
+val for_function: Env.t -> AST.ident -> C.attributes -> section_name list
 val for_stringlit: unit -> section_name
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 2a110104..470c22e5 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -156,10 +156,8 @@ let rec dcl ?(pp_indication=true) pp ty n =
         dcl pp ty
           (fun pp -> fprintf pp " %a" ident id) in
       let n' pp =
-        begin match a with
-        | [] -> n pp
-        | _  -> fprintf pp " (%a%t)" attributes a n
-        end;
+        attributes pp a;
+        n pp;
         fprintf pp "(";
         if pp_indication then fprintf pp "@[<hov 0>";
         begin match args with
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index f5d5c425..21e6f71e 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -92,6 +92,12 @@ let attr_is_standard = function
 (* Is an attribute type-related (true) or variable-related (false)? *)
 
 let attr_is_type_related = function
+  | AConst | AVolatile | ARestrict | AAlignas _ -> true
+  | Attr(_, _) -> false
+
+(* Is an attribute related to structs, unions and enum (true) or not (false)? *)
+
+let attr_is_struct_related = function
   | Attr(("packed" | "__packed__"), _) -> true
   | _ -> false
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index edff9ee1..4906a8a8 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -54,6 +54,8 @@ val change_attributes_type : Env.t -> (attributes -> attributes) -> typ -> typ
   (* Apply the given function to the top-level attributes of the given type *)
 val attr_is_type_related: attribute -> bool
   (* Is an attribute type-related (true) or variable-related (false)? *)
+val attr_is_struct_related: attribute -> bool
+  (* Is an attribute related to structs, unions and enum (true) or not (false)? *)
 val attr_inherited_by_members: attribute -> bool
   (* Is an attribute of a composite inherited by members of the composite? *)
 val strip_attributes_type: typ -> attribute list -> typ
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 *)
 
diff --git a/test/regression/attribs1.c b/test/regression/attribs1.c
index 808610b7..0650b189 100644
--- a/test/regression/attribs1.c
+++ b/test/regression/attribs1.c
@@ -24,7 +24,7 @@ __attribute((__section__("myconst"))) const int e = 12;
 const char filler4 = 1;
 __attribute((__section__("myconst"))) const int f = 34;
 
-__attribute((__section__("mycode"))) int myfunc(int x) { return x + 1; }
+__attribute((__section__("mycode"))) int * myfunc(int * x) { return x + 1; }
 
 /* Alignment with typedefs and structs */