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, 36 insertions, 6 deletions

diff --git a/test/regression/packedstruct1.c b/test/regression/packedstruct1.c
index 8b138dd4..5d3e7124 100644
--- a/test/regression/packedstruct1.c
+++ b/test/regression/packedstruct1.c
@@ -2,8 +2,18 @@
 
 #include <stdio.h>
 
+/* offsetof is the offset computed by the verified front-end (cfrontend/) */
 #define offsetof(s,f) (int)&(((struct s *)0)->f)
 
+/* boffsetof is the offset computed by the elaborator (cparser/) */
+#define boffsetof(s,f) (int)__builtin_offsetof(struct s, f)
+
+/* szof is the size computed by the verified front-end (cfrontend/) */
+#define szof(s) (int) sizeof(struct s)
+
+/* bszof is the size computed by the elaborator (cparser/) */
+#define bszof(s) (int) sizeof(char [sizeof(struct s)])
+
 /* Simple packing */
 
 struct __packed__(1) s1 { unsigned short x; int y; double z; };
@@ -11,9 +21,12 @@ struct __packed__(1) s1 { unsigned short x; int y; double z; };
 void test1(void)
 {
   struct s1 s1;
-  printf("sizeof(struct s1) = %d\n", sizeof(struct s1));
+  printf("sizeof(struct s1) = %d\n", szof(s1));
+  printf("precomputed sizeof(struct s1) = %d\n", bszof(s1));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s1,x), offsetof(s1,y), offsetof(s1,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s1,x), boffsetof(s1,y), boffsetof(s1,z));
   s1.x = 123; s1.y = -456; s1.z = 3.14159;
   printf("s1 = {x = %d, y = %d, z = %.5f}\n\n", s1.x, s1.y, s1.z);
 }
@@ -28,10 +41,13 @@ struct s2 s2;
 
 void test2(void)
 {
-  printf("sizeof(struct s2) = %d\n", sizeof(struct s2));
+  printf("sizeof(struct s2) = %d\n", szof(s2));
+  printf("precomputed sizeof(struct s2) = %d\n", bszof(s2));
   printf("&s2 mod 16 = %d\n", ((int) &s2) & 0xF);
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s2,x), offsetof(s2,y), offsetof(s2,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s2,x), boffsetof(s2,y), boffsetof(s2,z));
   s2.x = 12345; s2.y = -456; s2.z = 3.14159;
   printf("s2 = {x = %d, y = %d, z = %.5f}\n\n", s2.x, s2.y, s2.z);
 }
@@ -55,8 +71,10 @@ void test3(void)
 {
   char xx;
 
-  printf("sizeof(struct s3) = %d\n", sizeof(struct s3));
+  printf("sizeof(struct s3) = %d\n", szof(s3));
+  printf("precomputed sizeof(struct s3) = %d\n", bszof(s3));
   printf("offsetof(s) = %d\n", offsetof(s3,s));
+  printf("precomputed offsetof(s) = %d\n", boffsetof(s3,s));
   s3.x = 123;
   s3.y = 45678;
   s3.z = 0x80000001U;
@@ -82,9 +100,13 @@ struct s4 { unsigned short x; int y; double z; };
 void test4(void)
 {
   struct s4 s4;
-  printf("sizeof(struct s4) = %d\n", sizeof(struct s4));
+
+  printf("sizeof(struct s4) = %d\n", szof(s4));
+  printf("precomputed sizeof(struct s4) = %d\n", bszof(s4));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s4,x), offsetof(s4,y), offsetof(s4,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s4,x), boffsetof(s4,y), boffsetof(s4,z));
   s4.x = 123; s4.y = -456; s4.z = 3.14159;
   printf("s4 = {x = %d, y = %d, z = %.5f}\n\n", s4.x, s4.y, s4.z);
 }
@@ -96,9 +118,13 @@ struct __attribute((packed)) s5 { unsigned short x; int y; double z; };
 void test5(void)
 {
   struct s5 s5;
-  printf("sizeof(struct s5) = %d\n", sizeof(struct s5));
+
+  printf("sizeof(struct s5) = %d\n", szof(s5));
+  printf("precomputed sizeof(struct s5) = %d\n", bszof(s5));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s5,x), offsetof(s5,y), offsetof(s5,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s5,x), boffsetof(s5,y), boffsetof(s5,z));
   s5.x = 123; s5.y = -456; s5.z = 3.14159;
   printf("s5 = {x = %d, y = %d, z = %.5f}\n\n", s5.x, s5.y, s5.z);
 }
@@ -110,9 +136,13 @@ struct s6 { unsigned short x; int y; double z; }  __attribute((packed)) const s6
 void test6(void)
 {
   struct s6 s62;
-  printf("sizeof(struct s6) = %d\n", sizeof(struct s6));
+
+  printf("sizeof(struct s6) = %d\n", szof(s6));
+  printf("precomputed sizeof(struct s6) = %d\n", bszof(s6));
   printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
          offsetof(s6,x), offsetof(s6,y), offsetof(s6,z));
+  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+         boffsetof(s6,x), boffsetof(s6,y), boffsetof(s6,z));
   s62.x = 123; s62.y = -456; s62.z = 3.14159;
   printf("s62 = {x = %d, y = %d, z = %.5f}\n\n", s62.x, s62.y, s62.z);
 }