Native support for bit fields (#400)

This big PR adds support for bit fields in structs and unions to
the verified part of CompCert, namely the CompCert C and Clight
languages.

The compilation of bit field accesses to normal integer accesses +
shifts and masks is done and proved correct as part of the Cshmgen
pass.

The layout of bit fields in memory is done by the functions in module
Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic
soundness properties of the layout are shown, such as "two different
bit fields do not overlap" or "a bit field and a regular field do not
overlap".

All this replaces the previous emulation of bit fields by
source-to-source rewriting in the unverified front-end of CompCert
(module cparse/Bitfield.ml). This emulation was prone to errors (see
nonstandard layout instead.

The core idea for the PR is that expressions in l-value position
denote not just a block, a byte offset and a type, but also a bitfield
designator saying whether all the bits of the type are accessed
(designator Full) or only some of its bits (designator
Bits). Designators of the Bits kind appear when the l-value is a bit
field access; the bit width and bit offset in Bits are computed by the
functions in Ctypes that implement the layout algorithm.

Consequently, both in the semantics of CompCert C and Clight and in
the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a
type and a bitfield designator are used in a number of places where a
single type was used before.

The introduction of bit fields has a big impact on static
initialization (module cfrontend/Initializers.v), which had to be
rewritten in large part, along with its soundness proof
(cfrontend/Initializersproof.v).

Both static initialization and run-time manipulation of bit fields are
tested in test/abi using differential testing against GCC and
randomly-generated structs.

This work exposed subtle interactions between bit fields and the
volatile modifier. Currently, the volatile modifier is ignored when
accessing a bit field (and a warning is printed at compile-time), just
like it is ignored when accessing a struct or union as a r-value.

Currently, the natural alignment of bit fields and their storage units
cannot be modified with the aligned attribute. _Alignas on bit fields
is rejected as per C11, and the packed modifier cannot be applied to a
struct containing bit fields.

7 files changed, 96 insertions, 31 deletions

diff --git a/test/regression/Makefile b/test/regression/Makefile
index 698c1392..33a9f993 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -21,7 +21,7 @@ TESTS=int32 int64 floats floats-basics floats-lit \
 # Can run, but only in compiled mode, and have reference output in Results
 
 TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
-  bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t \
+  bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t bitfields10 \
   builtins-common builtins-$(ARCH) packedstruct1 packedstruct2 alignas \
   varargs1 varargs2 varargs3 sections alias aligned
 
diff --git a/test/regression/Results/bitfields10 b/test/regression/Results/bitfields10
new file mode 100644
index 00000000..9dc00daf
--- /dev/null
+++ b/test/regression/Results/bitfields10
@@ -0,0 +1,14 @@
+loc_s = { a = 11, b = 2 }
+loc_t = { c = 11, d = 1, e = 2 }
+loc_u_u = { u = -5 }
+loc_u_v = { v = 3 }
+compound_s = { a = 2, b = 3 }
+compound_t = { c = 2, d = 1, e = -11 }
+compound_u = { u = 2 }
+loc_s = { a = 7, b = 2 }
+loc_t = { c = 7, d = 1, e = 50 }
+loc_u_u = { u = 7 }
+loc_u_v = { v = 2 }
+compound_s = { a = -14, b = 3 }
+compound_t = { c = 50, d = 1, e = -7 }
+compound_u = { u = 2 }
diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9
index e35c2414..ec35fc08 100644
--- a/test/regression/Results/bitfields9
+++ b/test/regression/Results/bitfields9
@@ -2,17 +2,7 @@ glob_s = { a = -12, b = 1 }
 glob_t = { c = 123, d = 1, e = -45 }
 glob_u_u = { u = -3 }
 glob_u_v = { v = 6 }
-loc_s = { a = 11, b = 2 }
-loc_t = { c = 11, d = 1, e = 2 }
-loc_u_u = { u = -5 }
-loc_u_v = { v = 3 }
-compound_s = { a = 2, b = 3 }
-compound_t = { c = 2, d = 1, e = -11 }
-compound_u = { u = 2 }
-loc_s = { a = 7, b = 2 }
-loc_t = { c = 7, d = 1, e = 50 }
-loc_u_u = { u = 7 }
-loc_u_v = { v = 2 }
-compound_s = { a = -14, b = 3 }
-compound_t = { c = 50, d = 1, e = -7 }
-compound_u = { u = 2 }
+loc_s = { a = -12, b = 1 }
+loc_t = { c = 123, d = 1, e = -45 }
+loc_u_u = { u = -3 }
+loc_u_v = { v = 6 }
diff --git a/test/regression/Runtest b/test/regression/Runtest
index f693219a..600ae045 100755
--- a/test/regression/Runtest
+++ b/test/regression/Runtest
@@ -51,7 +51,7 @@ then
       exit 0
     else
       echo "$name: WRONG OUTPUT (diff follows)"
-      diff -u "$ref" "$out"
+      diff -a -u "$ref" "$out"
       exit 2
     fi
   else
diff --git a/test/regression/bitfields10.c b/test/regression/bitfields10.c
new file mode 100644
index 00000000..0f022664
--- /dev/null
+++ b/test/regression/bitfields10.c
@@ -0,0 +1,66 @@
+#include <stdio.h>
+
+/* Dynamic initialization of bit-fields */
+/* Known not to work with the reference interpreter */
+
+struct s {
+  signed char a: 6;
+  unsigned int b: 2;
+};
+
+struct t {
+  unsigned int c: 16;
+  _Bool d: 1;
+  short e: 8;
+  int : 10;
+};
+
+union u {
+  int u: 4;
+  unsigned int v: 3;
+};
+
+void print_s(char * msg, struct s p)
+{
+  printf("%s = { a = %d, b = %d }\n", msg, p.a, p.b);
+}
+
+void print_t(char * msg, struct t p)
+{
+  printf("%s = { c = %d, d = %d, e = %d }\n", msg, p.c, p.d, p.e);
+}
+
+void print_u_u(char * msg, union u p)
+{
+  printf("%s = { u = %d }\n", msg, p.u);
+}
+
+void print_u_v(char * msg, union u p)
+{
+  printf("%s = { v = %u }\n", msg, p.v);
+}
+
+/* Local, non-static initialization */
+void f(int x, int y, int z)
+{
+  struct s loc_s = { x, y };
+  struct t loc_t = { x, z, y };
+  union u loc_u_u = { .u = x };
+  union u loc_u_v = { .v = z };
+  print_s("loc_s", loc_s);
+  print_t("loc_t", loc_t);
+  print_u_u("loc_u_u", loc_u_u);
+  print_u_v("loc_u_v", loc_u_v);
+  print_s("compound_s", (struct s) { y, x });
+  print_t("compound_t", (struct t) { y, ~z, -x });
+  print_u_u("compound_u", (union u) { y });
+}
+
+int main()
+{
+  f(11, 2, 3);
+  f(7, 50, 2);
+  return 0;
+}
+
+
diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c
index eef20168..025216fa 100644
--- a/test/regression/bitfields9.c
+++ b/test/regression/bitfields9.c
@@ -1,6 +1,6 @@
 #include <stdio.h>
 
-/* Initialization of bit-fields */
+/* Static initialization of bit-fields */
 
 struct s {
   signed char a: 6;
@@ -39,27 +39,23 @@ void print_u_v(char * msg, union u p)
   printf("%s = { v = %u }\n", msg, p.v);
 }
 
-
 /* Global initialization */
 struct s glob_s = { -12, 1 };
 struct t glob_t = { 123, 2, -45 };
 union u glob_u_u = { -3 };
 union u glob_u_v = { .v = 6 };
 
-/* Local initialization */
-void f(int x, int y, int z)
+/* Local, static initialization */
+void f(void)
 {
-  struct s loc_s = { x, y };
-  struct t loc_t = { x, z, y };
-  union u loc_u_u = { .u = x };
-  union u loc_u_v = { .v = z };
+  static struct s loc_s = { -12, 1 };
+  static struct t loc_t = { 123, 2, -45 };
+  static union u loc_u_u = { -3 };
+  static union u loc_u_v = { .v = 6 };
   print_s("loc_s", loc_s);
   print_t("loc_t", loc_t);
   print_u_u("loc_u_u", loc_u_u);
   print_u_v("loc_u_v", loc_u_v);
-  print_s("compound_s", (struct s) { y, x });
-  print_t("compound_t", (struct t) { y, ~z, -x });
-  print_u_u("compound_u", (union u) { y });
 }
 
 int main()
@@ -68,8 +64,7 @@ int main()
   print_t("glob_t", glob_t);
   print_u_u("glob_u_u", glob_u_u);
   print_u_v("glob_u_v", glob_u_v);
-  f(11, 2, 3);
-  f(7, 50, 2);
+  f();
   return 0;
 }
 
diff --git a/test/regression/sizeof1.c b/test/regression/sizeof1.c
index ca494622..5bd4d739 100644
--- a/test/regression/sizeof1.c
+++ b/test/regression/sizeof1.c
@@ -17,8 +17,8 @@ char tbl[sizeof(struct s)];
 */
 
 struct bits1 {
-  unsigned a: 1;
-  unsigned b: 6;
+  unsigned char a: 1;
+  unsigned char b: 6;
 };
 
 char b1[sizeof(struct bits1)];  /* should be 1 */