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.

1 files changed, 42 insertions, 52 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 2dcf193d..d3a830ce 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -449,34 +449,6 @@ let rec equal_types env t1 t2 =
 let compatible_types mode env t1 t2 =
   match combine_types mode env t1 t2 with Some _ -> true | None -> false
 
-(* Naive placement algorithm for bit fields, might not match that
-   of the compiler. *)
-
-let pack_bitfields ml =
-  let rec pack nbits = function
-  | [] ->
-      (nbits, [])
-  | m :: ms as ml ->
-      match m.fld_bitfield with
-      | None -> (nbits, ml)
-      | Some n ->
-          if n = 0 then
-            (nbits, ms) (* bit width 0 means end of pack *)
-          else if nbits + n > 8 * !config.sizeof_int then
-            (nbits, ml) (* doesn't fit in current word *)
-          else
-            pack (nbits + n) ms (* add to current word *)
-  in
-  let (nbits, ml') = pack 0 ml in
-  let (sz, al) =
-    (* A lone bitfield of width 0 consumes no space and aligns to 1 *)
-    if nbits = 0 then (0, 1) else
-    if nbits <= 8 then (1, 1) else
-    if nbits <= 16 then (2, 2) else
-    if nbits <= 32 then (4, 4) else
-    if nbits <= 64 then (8, 8) else assert false in
-  (sz, al, ml')
-
 (* Natural alignment, in bytes *)
 
 let alignof_ikind = function
@@ -520,15 +492,13 @@ let rec alignof env t =
 let alignof_struct_union env members =
   let rec align_rec al = function
   | [] -> Some al
-  | m :: rem as ml ->
-      if m.fld_bitfield = None then begin
+  | m :: rem ->
+      if m.fld_name = "" then
+        align_rec al rem
+      else
         match alignof env m.fld_typ with
         | None -> None
         | Some a -> align_rec (max a al) rem
-      end else begin
-        let (s, a, ml') = pack_bitfields ml in
-        align_rec (max a al) ml'
-      end
   in align_rec 1 members
 
 let align x boundary =
@@ -605,43 +575,63 @@ let sizeof_union env members =
    Bitfields are taken into account for the size and offset computations
    but not given an offset.
    Not done here but in composite_info_def: rounding size to alignment. *)
+
 let sizeof_layout_struct env members ma =
-  let align_offset ofs a =
-    align ofs (if ma > 0 && a > ma then ma else a) in
-  let rec sizeof_rec ofs accu = function
+
+  let align_bit_offset pos a =
+    align pos (8 * (if ma > 0 && a > ma then ma else a)) in
+
+  let record_field name pos =
+    assert (pos mod 8 = 0);
+    (name, pos / 8) in
+
+  (* pos is the current position in bits *)
+  let rec sizeof_rec pos accu = function
   | [] ->
-      Some (ofs, accu)
+      Some (pos, accu)
   | [ { fld_typ = TArray(_, None, _) } as m ] ->
       (* C99: ty[] allowed as last field *)
       begin match alignof env m.fld_typ with
       | Some a ->
-          let ofs = align_offset ofs a in
-          Some (ofs, (m.fld_name, ofs) :: accu)
+          let pos = align_bit_offset pos a in
+          Some (pos, record_field m.fld_name pos :: accu)
       | None -> None
       end
-  | m :: rem as ml ->
-      if m.fld_bitfield = None then begin
-        match alignof env m.fld_typ, sizeof env m.fld_typ with
-        | Some a, Some s ->
-            let ofs = align_offset ofs a in
-            sizeof_rec (ofs + s) ((m.fld_name, ofs) :: accu) rem
-        | _, _ -> None
-      end else begin
-        let (s, a, ml') = pack_bitfields ml in
-        sizeof_rec (align_offset ofs a + s) accu ml'
+  | m :: rem ->
+      begin match alignof env m.fld_typ, sizeof env m.fld_typ with
+      | Some a, Some s ->
+          begin match m.fld_bitfield with
+          | None ->
+              let pos = align_bit_offset pos a in
+              sizeof_rec (pos + s * 8)
+                         (record_field m.fld_name pos :: accu)
+                         rem
+          | Some width ->
+              (* curr = beginning of storage unit, in bits
+                 next = one past end of storage unit, in bits *)
+              let curr = pos / (a * 8) * (a * 8) in
+              let next = curr + s * 8 in
+              let pos' =
+                if width <= 0 then align pos (a * 8)
+                else if pos + width <= next then pos + width
+                else next + width in
+              sizeof_rec pos' accu rem
+          end
+      | _, _ ->
+          None
       end
   in sizeof_rec 0 [] members
 
 let sizeof_struct env members ma =
   match sizeof_layout_struct env members ma with
   | None -> None
-  | Some(sz, offsets) -> Some sz
+  | Some(bitsize, offsets) -> Some ((bitsize + 7) / 8)
 
 (* Compute the offsets of all non-bitfield members of a struct. *)
 let struct_layout env attrs members =
   let (ma, _, _) = packing_parameters attrs in
   match sizeof_layout_struct env members ma with
-  | Some(sz, offsets) -> offsets
+  | Some(bitsize, offsets) -> offsets
   | None -> []
 
 (* Compute the offset of a struct member *)