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, 95 insertions, 44 deletions

diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5bd12d00..9e804176 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -372,19 +372,56 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type
         e1 ty1 e2 ty2
   end.
 
+(** Auxiliary for translating bitfield accesses *)
+
+Definition make_extract_bitfield (sz: intsize) (sg: signedness) (pos width: Z)
+                                 (addr: expr) : res expr :=
+  if zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz) then
+    let amount1 := Int.repr (Int.zwordsize - first_bit sz pos width - width) in
+    let amount2 := Int.repr (Int.zwordsize - width) in
+    let e1 := Eload (chunk_for_carrier sz) addr in
+    let e2 := Ebinop Oshl e1 (make_intconst amount1) in
+    let e3 := Ebinop (if intsize_eq sz IBool
+                      || signedness_eq sg Unsigned then Oshru else Oshr)
+                     e2 (make_intconst amount2) in
+    OK e3
+  else
+    Error(msg "Cshmgen.extract_bitfield").
+
 (** [make_load addr ty_res] loads a value of type [ty_res] from
-   the memory location denoted by the Csharpminor expression [addr].
+   the memory location denoted by the Csharpminor expression [addr]
+   and the bitfield designator [bf].
    If [ty_res] is an array or function type, returns [addr] instead,
    as consistent with C semantics.
 *)
 
-Definition make_load (addr: expr) (ty_res: type) :=
-  match (access_mode ty_res) with
-  | By_value chunk => OK (Eload chunk addr)
-  | By_reference => OK addr
-  | By_copy => OK addr
-  | By_nothing => Error (msg "Cshmgen.make_load")
-  end.
+Definition make_load (addr: expr) (ty_res: type) (bf: bitfield) :=
+  match bf with
+  | Full =>
+      match access_mode ty_res with
+      | By_value chunk => OK (Eload chunk addr)
+      | By_reference => OK addr
+      | By_copy => OK addr
+      | By_nothing => Error (msg "Cshmgen.make_load")
+      end
+  | Bits sz sg pos width =>
+      make_extract_bitfield sz sg pos width addr
+  end.
+
+(** Auxiliary for translating bitfield updates *)
+
+Definition make_store_bitfield (sz: intsize) (sg: signedness) (pos width: Z)
+                               (addr val: expr) : res stmt :=
+  if zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz) then
+    let amount := first_bit sz pos width in
+    let mask := Int.shl (Int.repr (two_p width - 1)) (Int.repr amount) in
+    let e1 := Eload (chunk_for_carrier sz) addr in
+    let e2 := Ebinop Oshl val (make_intconst (Int.repr amount)) in
+    let e3 := Ebinop Oor (Ebinop Oand e2 (make_intconst mask))
+                         (Ebinop Oand e1 (make_intconst (Int.not mask))) in
+    OK (Sstore (chunk_for_carrier sz) addr e3)
+  else
+    Error(msg "Cshmgen.make_store_bitfield").
 
 (** [make_memcpy dst src ty] returns a [memcpy] builtin appropriate for
   by-copy assignment of a value of Clight type [ty]. *)
@@ -394,16 +431,21 @@ Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) :=
   OK (Sbuiltin None (EF_memcpy sz (Ctypes.alignof_blockcopy ce ty))
                     (dst :: src :: nil)).
 
-(** [make_store addr ty rhs] stores the value of the
+(** [make_store addr ty bf rhs] stores the value of the
    Csharpminor expression [rhs] into the memory location denoted by the
    Csharpminor expression [addr].
-   [ty] is the type of the memory location. *)
-
-Definition make_store (ce: composite_env) (addr: expr) (ty: type) (rhs: expr) :=
-  match access_mode ty with
-  | By_value chunk => OK (Sstore chunk addr rhs)
-  | By_copy => make_memcpy ce addr rhs ty
-  | _ => Error (msg "Cshmgen.make_store")
+   [ty] is the type of the memory location and [bf] a bitfield designator. *)
+
+Definition make_store (ce: composite_env) (addr: expr) (ty: type) (bf: bitfield) (rhs: expr) :=
+  match bf with
+  | Full =>
+      match access_mode ty with
+      | By_value chunk => OK (Sstore chunk addr rhs)
+      | By_copy => make_memcpy ce addr rhs ty
+      | _ => Error (msg "Cshmgen.make_store")
+      end
+  | Bits sz sg pos width =>
+      make_store_bitfield sz sg pos width addr rhs
   end.
 
 (** ** Translation of operators *)
@@ -441,23 +483,27 @@ Definition transl_binop (ce: composite_env)
 
 (** ** Translation of field accesses *)
 
-Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr) : res expr :=
-  match ty with
-  | Tstruct id _ =>
-      match ce!id with
-      | None =>
-          Error (MSG "Undefined struct " :: CTX id :: nil)
-      | Some co =>
-          do ofs <- field_offset ce f (co_members co);
-          OK (if Archi.ptr64
-              then Ebinop Oaddl a (make_longconst (Int64.repr ofs))
-              else Ebinop Oadd a (make_intconst (Int.repr ofs)))
-      end
-  | Tunion id _ =>
-      OK a
-  | _ =>
-      Error(msg "Cshmgen.make_field_access")
-  end.
+Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr) : res (expr * bitfield) :=
+  do (ofs, bf) <-
+    match ty with
+    | Tstruct id _ =>
+        match ce!id with
+        | None => Error (MSG "Undefined struct " :: CTX id :: nil)
+        | Some co => field_offset ce f (co_members co)
+        end
+    | Tunion id _ =>
+        match ce!id with
+        | None => Error (MSG "Undefined union " :: CTX id :: nil)
+        | Some co => union_field_offset ce f (co_members co)
+        end
+    | _ =>
+        Error(msg "Cshmgen.make_field_access")
+    end;
+  let a' :=
+    if Archi.ptr64
+    then Ebinop Oaddl a (make_longconst (Int64.repr ofs))
+    else Ebinop Oadd a (make_intconst (Int.repr ofs)) in
+  OK (a', bf).
 
 (** * Translation of expressions *)
 
@@ -476,14 +522,18 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
   | Clight.Econst_long n _ =>
       OK(make_longconst n)
   | Clight.Evar id ty =>
-      make_load (Eaddrof id) ty
+      make_load (Eaddrof id) ty Full
   | Clight.Etempvar id ty =>
       OK(Evar id)
   | Clight.Ederef b ty =>
       do tb <- transl_expr ce b;
-      make_load tb ty
+      make_load tb ty Full
   | Clight.Eaddrof b _ =>
-      transl_lvalue ce b
+      do (tb, bf) <- transl_lvalue ce b;
+      match bf with
+      | Full => OK tb
+      | Bits _ _ _ _ => Error (msg "Cshmgen.transl_expr: addrof bitfield")
+      end
   | Clight.Eunop op b _ =>
       do tb <- transl_expr ce b;
       transl_unop op tb (typeof b)
@@ -496,8 +546,8 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
       make_cast (typeof b) ty tb
   | Clight.Efield b i ty =>
       do tb <- transl_expr ce b;
-      do addr <- make_field_access ce (typeof b) i tb;
-      make_load addr ty
+      do (addr, bf) <- make_field_access ce (typeof b) i tb;
+      make_load addr ty bf
   | Clight.Esizeof ty' ty =>
       do sz <- sizeof ce ty'; OK(make_ptrofsconst sz)
   | Clight.Ealignof ty' ty =>
@@ -506,15 +556,16 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
 
 (** [transl_lvalue a] returns the Csharpminor code that evaluates
    [a] as a lvalue, that is, code that returns the memory address
-   where the value of [a] is stored.
+   where the value of [a] is stored.  It also returns the bitfield to be
+   accessed at this address, if appropriate.
 *)
 
-with transl_lvalue (ce: composite_env) (a: Clight.expr) {struct a} : res expr :=
+with transl_lvalue (ce: composite_env) (a: Clight.expr) {struct a} : res (expr * bitfield) :=
   match a with
   | Clight.Evar id _ =>
-      OK (Eaddrof id)
+      OK (Eaddrof id, Full)
   | Clight.Ederef b _ =>
-      transl_expr ce b
+      do tb <- transl_expr ce b; OK (tb, Full)
   | Clight.Efield b i ty =>
       do tb <- transl_expr ce b;
       make_field_access ce (typeof b) i tb
@@ -618,10 +669,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
   | Clight.Sskip =>
       OK Sskip
   | Clight.Sassign b c =>
-      do tb <- transl_lvalue ce b;
+      do (tb, bf) <- transl_lvalue ce b;
       do tc <- transl_expr ce c;
       do tc' <- make_cast (typeof c) (typeof b) tc;
-      make_store ce tb (typeof b) tc'
+      make_store ce tb (typeof b) bf tc'
   | Clight.Sset x b =>
       do tb <- transl_expr ce b;
       OK(Sset x tb)