Do not expand type names when floating attributes "up" a declaration

During elaboration of type declarators, non-type-related attributes such as "aligned" or "section" are "floated up" so that they apply to the thing being declared.  For example, consider:
```
   __attribute((aligned(16))) int * p;
```
The attribute is first attached to type `int`, then floated up to type `int *`, so that it finally applies to `p`, giving a 16-aligned pointer to int, and not a naturally-aligned pointer to 16-aligned int.

What happens when the non-type-related attribute comes from a typedef?
```
   typedef __attribute((aligned(16))) int i16;
   i16 * p;
```
CompCert used to expand the typedef then float up the attribute, resulting in `p` being a 16-aligned pointer to int.

GCC and Clang produce a naturally-aligned pointer, so they do not expand the typedef before floating.

The old CompCert behavior is somewhat surprising, and potentially less useful than the GCC/Clang behavior.

This commit changes the floating up of non-type-related attributes so that typedefs and struct/union/enum definitions are not expanded when determining which attributes to float up.  This is a first step towards mimicking the GCC/Clang behavior.

3 files changed, 24 insertions, 2 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index ea9713d5..b926e84a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -163,7 +163,10 @@ let rec unroll env t =
       unroll env (add_attributes_type attr ty)
   | _ -> t
 
-(* Extracting the attributes of a type *)
+(* Extracting the attributes of a type, including the attributes
+   attached to typedefs, structs and unions.  In other words,
+   typedefs are unrolled and composite definitions expanded
+   before extracting the attributes.  *)
 
 let rec attributes_of_type env t =
   match t with
@@ -190,6 +193,23 @@ let rec attributes_of_type env t =
       | exception Env.Error(Env.Unbound_tag _) -> a
       end
 
+(* Extracting the attributes of a type, excluding the attributes
+   attached to typedefs, structs and unions.  In other words,
+   typedefs are not unrolled and composite definitions are not expanded. *)
+
+let rec attributes_of_type_no_expand t =
+  match t with
+  | TVoid a -> a
+  | TInt(ik, a) -> a
+  | TFloat(fk, a) -> a
+  | TPtr(ty, a) -> a
+  | TArray(ty, sz, a) -> add_attributes a (attributes_of_type_no_expand ty)
+  | TFun(ty, params, vararg, a) -> a
+  | TNamed(s, a) -> a
+  | TStruct(s, a) -> a
+  | TUnion(s, a) -> a
+  | TEnum(s, a) -> a
+
 (* Changing the attributes of a type (at top-level) *)
 (* Same hack as above for array types. *)
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index dc9dc0cc..a99bf3af 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -50,6 +50,8 @@ val remove_custom_attributes : string list -> attributes -> attributes
      in the given list of names. *)
 val attributes_of_type : Env.t -> typ -> attributes
   (* Return the attributes of the given type, expanding typedefs if needed. *)
+val attributes_of_type_no_expand : typ -> attributes
+  (* Return the attributes of the given type, without expanding typedefs. *)
 val add_attributes_type : attributes -> typ -> typ
   (* Add the given set of attributes to those of the given type. *)
 val remove_attributes_type : Env.t -> attributes -> typ -> typ
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 8f27b2a0..8f42fe0a 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -598,7 +598,7 @@ let get_nontype_attrs env ty =
     | 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
+  let nta = List.filter to_be_removed (attributes_of_type_no_expand ty) in
   (remove_attributes_type env nta ty, nta)
 
 (* Elaboration of a type specifier.  Returns 6-tuple: