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.

3 files changed, 4 insertions, 6 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 80883372..25c3e1dd 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,7 +17,6 @@ let linker_options = ref ([]: string list)
 let assembler_options = ref ([]: string list)
 let option_flongdouble = ref false
 let option_fstruct_passing = ref false
-let option_fbitfields = ref false
 let option_fvararg_calls = ref true
 let option_funprototyped = ref true
 let option_fpacked_structs = ref false
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index a816dd41..9da1e533 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -32,7 +32,7 @@ let version_options tool_name =
 (* Language support options *)
 
 let all_language_support_options = [
-  option_fbitfields; option_flongdouble;
+  option_flongdouble;
   option_fstruct_passing; option_fvararg_calls; option_funprototyped;
   option_fpacked_structs; option_finline_asm
 ]
@@ -44,11 +44,11 @@ let unset_all opts () = List.iter (fun r -> r := false) opts
 
 let language_support_options =
   [ Exact "-fall", Unit (set_all all_language_support_options);
-    Exact "-fnone", Unit (unset_all all_language_support_options);]
+    Exact "-fnone", Unit (unset_all all_language_support_options);
+    Exact "-fbitfields", Unit (fun () -> ()); ]
   @ f_opt "longdouble" option_flongdouble
   @ f_opt "struct-return" option_fstruct_passing
   @ f_opt "struct-passing" option_fstruct_passing
-  @ f_opt "bitfields" option_fbitfields
   @ f_opt "vararg-calls" option_fvararg_calls
   @ f_opt "unprototyped" option_funprototyped
   @ f_opt "packed-structs" option_fpacked_structs
@@ -56,7 +56,6 @@ let language_support_options =
 
 let language_support_help =
   {|Language support options (use -fno-<opt> to turn off -f<opt>) :
-  -fbitfields    Emulate bit fields in structs [off]
   -flongdouble   Treat 'long double' as 'double' [off]
   -fstruct-passing  Support passing structs and unions by value as function
                     results or function arguments [off]
@@ -67,6 +66,7 @@ let language_support_help =
   -finline-asm   Support inline 'asm' statements [off]
   -fall          Activate all language support options above
   -fnone         Turn off all language support options above
+  -fbitfields    Ignored (bit fields are now implemented natively)
 |}
 
 (* General options *)
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 6590e793..6133291e 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -80,7 +80,6 @@ let parse_c_file sourcename ifile =
   let simplifs =
     "b" (* blocks: mandatory *)
   ^ (if !option_fstruct_passing then "s" else "")
-  ^ (if !option_fbitfields then "f" else "")
   ^ (if !option_fpacked_structs then "p" else "")
   in
   (* Parsing and production of a simplified C AST *)