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, 12 insertions, 0 deletions

diff --git a/test/regression/Results/packedstruct1-32 b/test/regression/Results/packedstruct1-32
index e4bca769..e7d1c296 100644
--- a/test/regression/Results/packedstruct1-32
+++ b/test/regression/Results/packedstruct1-32
@@ -1,25 +1,37 @@
 sizeof(struct s1) = 14
+precomputed sizeof(struct s1) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s1 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s2) = 16
+precomputed sizeof(struct s2) = 16
 &s2 mod 16 = 0
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s2 = {x = 57, y = -456, z = 3.14159}
 
 sizeof(struct s3) = 31
+precomputed sizeof(struct s3) = 31
 offsetof(s) = 29
+precomputed offsetof(s) = 29
 s3 = {x = 123, y = 45678, z = 2147483649, v = -456, w = -1234567, p is ok, t = {111,222,333}, s = {'o','k'}}
 
 sizeof(struct s4) = 16
+precomputed sizeof(struct s4) = 16
 offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8
+precomputed offsetof(x) = 0, offsetof(y) = 4, offsetof(z) = 8
 s4 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s5) = 14
+precomputed sizeof(struct s5) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s5 = {x = 123, y = -456, z = 3.14159}
 
 sizeof(struct s6) = 14
+precomputed sizeof(struct s6) = 14
 offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
+precomputed offsetof(x) = 0, offsetof(y) = 2, offsetof(z) = 6
 s62 = {x = 123, y = -456, z = 3.14159}