Issue with packed structs and sizeof, alignof, offsetof in cparser/

CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field):
- the reference implementation, in Coq, from cfrontend/Ctypes.v
- the implementation used during elaboration, in OCaml, from cparser/Cutil.ml

The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used.

This causes issues with packed structs.  Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs.  Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml.  For example:
```
struct __packed__(1) s { char c; short s; int i; };
assert (__builtin_offsetof(struct s, i) == 3);
assert (sizeof(struct s) = sizeof(char[sizeof(struct s)]));
```
The two assertions fail.  In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration.  In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs.

This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout.

Related changes:
* cparser/Cutil: add `packing_parameters` function to extract packing info from attributes
* cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout
* cparser/Elab: check the alignment parameters given in packed attributes.  (The check was previously done in cparser/PackedStruct.ml but now it would come too late.)
* cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)).
* cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab
* cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given.  Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/.
* test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.

1 files changed, 35 insertions, 17 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 173d3e03..5f785c04 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -495,36 +495,54 @@ 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 || n = 0L  -> 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 [AAlignas (Int64.to_int n)] 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
-  | _ -> a
+  | 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] ->
+          if check_alignment loc n && check_alignment loc p then [a] else []
+      | _ -> error loc "ill-formed 'packed' attribute"; []
+      end
+  | _ -> [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 || n = 0L 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