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, 110 insertions, 40 deletions

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index c7e57a54..bb1dbe38 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -13,17 +13,8 @@
 (** Translation from Compcert C to Clight.
     Side effects are pulled out of Compcert C expressions. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Clight.
+Require Import Coqlib Maps Integers Floats Values AST Memory Errors.
+Require Import Ctypes Cop Csyntax Clight.
 
 Local Open Scope string_scope.
 Local Open Scope list_scope.
@@ -71,8 +62,6 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
    (at level 200, X ident, Y ident, A at level 100, B at level 200)
    : gensym_monad_scope.
 
-Local Open Scope gensym_monad_scope.
-
 Parameter first_unused_ident: unit -> ident.
 
 Definition initial_generator (x: unit) : generator :=
@@ -96,6 +85,12 @@ Fixpoint makeseq_rec (s: statement) (l: list statement) : statement :=
 Definition makeseq (l: list statement) : statement :=
   makeseq_rec Sskip l.
 
+Section SIMPL_EXPR.
+
+Local Open Scope gensym_monad_scope.
+
+Variable ce: composite_env.
+
 (** Smart constructor for [if ... then ... else]. *)
 
 Fixpoint eval_simpl_expr (a: expr) : option val :=
@@ -144,16 +139,64 @@ Definition transl_incrdecr (id: incr_or_decr) (a: expr) (ty: type) : expr :=
   | Decr => Ebinop Osub a (Econst_int Int.one type_int32s) (incrdecr_type ty)
   end.
 
-(** Generate a [Sset] or [Sbuiltin] operation as appropriate
-  to dereference a l-value [l] and store its result in temporary variable [id]. *)
+(** Given a simple l-value expression [l], determine whether it
+    designates a bitfield.  *)
+
+Definition is_bitfield_access_aux
+              (fn: composite_env -> ident -> members -> res (Z * bitfield))
+              (id: ident) (fld: ident) : mon bitfield :=
+  match ce!id with
+  | None => error (MSG "unknown composite " :: CTX id :: nil)
+  | Some co =>
+      match fn ce fld (co_members co) with
+      | OK (_, bf) => ret bf
+      | Error _ => error (MSG "unknown field " :: CTX fld :: nil)
+      end
+  end.
 
-Definition chunk_for_volatile_type (ty: type) : option memory_chunk :=
-  if type_is_volatile ty
-  then match access_mode ty with By_value chunk => Some chunk | _ => None end
+Definition is_bitfield_access (l: expr) : mon bitfield :=
+  match l with
+  | Efield r f _ =>
+      match typeof r with
+      | Tstruct id _ => is_bitfield_access_aux field_offset id f
+      | Tunion id _  => is_bitfield_access_aux union_field_offset id f
+      | _ => error (msg "is_bitfield_access")
+      end
+  | _ => ret Full
+  end.
+
+(** According to the CompCert C semantics, an access to a l-value of
+    volatile-qualified type can either
+  - produce an event in the trace of observable events, or
+  - produce no event and behave as if no volatile qualifier was there.
+
+    The latter case, where the volatile qualifier is ignored, happens if
+  - the l-value is a struct or union
+  - the l-value is an access to a bit field.
+
+    The [chunk_for_volatile_type] function distinguishes between the two
+    cases.  It returns [Some chunk] if the semantics is to produce
+    an observable event of the [Event_vload chunk] or [Event_vstore chunk]
+    kind.  It returns [None] if the semantics is that of a non-volatile
+    access. *)
+
+Definition chunk_for_volatile_type (ty: type) (bf: bitfield) : option memory_chunk :=
+  if type_is_volatile ty then
+    match access_mode ty with
+    | By_value chunk =>
+        match bf with
+        | Full => Some chunk
+        | Bits _ _ _ _ => None
+        end
+    | _ => None
+    end
   else None.
 
-Definition make_set (id: ident) (l: expr) : statement :=
-  match chunk_for_volatile_type (typeof l) with
+(** Generate a [Sset] or [Sbuiltin] operation as appropriate
+  to dereference a l-value [l] and store its result in temporary variable [id]. *)
+
+Definition make_set (bf: bitfield) (id: ident) (l: expr) : statement :=
+  match chunk_for_volatile_type (typeof l) bf with
   | None => Sset id l
   | Some chunk =>
       let typtr := Tpointer (typeof l) noattr in
@@ -165,13 +208,15 @@ Definition make_set (id: ident) (l: expr) : statement :=
 
 Definition transl_valof (ty: type) (l: expr) : mon (list statement * expr) :=
   if type_is_volatile ty
-  then do t <- gensym ty; ret (make_set t l :: nil, Etempvar t ty)
+  then do t <- gensym ty;
+       do bf <- is_bitfield_access l;
+       ret (make_set bf t l :: nil, Etempvar t ty)
   else ret (nil, l).
 
 (** Translation of an assignment. *)
 
-Definition make_assign (l r: expr) : statement :=
-  match chunk_for_volatile_type (typeof l) with
+Definition make_assign (bf: bitfield) (l r: expr) : statement :=
+  match chunk_for_volatile_type (typeof l) bf with
   | None =>
       Sassign l r
   | Some chunk =>
@@ -181,6 +226,30 @@ Definition make_assign (l r: expr) : statement :=
                     (Eaddrof l typtr :: r :: nil)
   end.
 
+(** Translation of the value of an assignment expression.
+    For non-bitfield assignments, it's the value of the right-hand side
+    converted to the type of the left-hand side.
+    For assignments to bitfields, an additional normalization to
+    the width and signedness of the bitfield is required. *)
+
+Definition make_normalize (sz: intsize) (sg: signedness) (width: Z) (r: expr) :=
+  let intconst (n: Z) := Econst_int (Int.repr n) type_int32s in
+  if intsize_eq sz IBool || signedness_eq sg Unsigned then
+    let mask := two_p width - 1 in
+    Ebinop Oand r (intconst mask) (typeof r)
+  else
+    let amount := Int.zwordsize - width in
+    Ebinop Oshr
+           (Ebinop Oshl r (intconst amount) type_int32s)
+           (intconst amount)
+           (typeof r).
+
+Definition make_assign_value (bf: bitfield) (r: expr): expr :=
+  match bf with
+  | Full => r
+  | Bits sz sg pos width => make_normalize sz sg width r
+  end.
+
 (** Translation of expressions.  Return a pair [(sl, a)] of
     a list of statements [sl] and a pure expression [a].
 - If the [dst] argument is [For_val], the statements [sl]
@@ -229,7 +298,7 @@ Definition sd_seqbool_set (ty: type) (sd: set_destination) :=
 
 Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
   match a with
-  | Csyntax.Eloc b ofs ty =>
+  | Csyntax.Eloc b ofs bf ty =>
       error (msg "SimplExpr.transl_expr: Eloc")
   | Csyntax.Evar x ty =>
       ret (finish dst nil (Evar x ty))
@@ -335,16 +404,17 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
   | Csyntax.Eassign l1 r2 ty =>
       do (sl1, a1) <- transl_expr For_val l1;
       do (sl2, a2) <- transl_expr For_val r2;
+      do bf <- is_bitfield_access a1;
       let ty1 := Csyntax.typeof l1 in
       let ty2 := Csyntax.typeof r2 in
       match dst with
       | For_val | For_set _ =>
           do t <- gensym ty1;
           ret (finish dst
-                 (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil)
-                 (Etempvar t ty1))
+                 (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign bf a1 (Etempvar t ty1) :: nil)
+                 (make_assign_value bf (Etempvar t ty1)))
       | For_effects =>
-          ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil,
+          ret (sl1 ++ sl2 ++ make_assign bf a1 a2 :: nil,
                dummy_expr)
       end
   | Csyntax.Eassignop op l1 r2 tyres ty =>
@@ -352,31 +422,33 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       do (sl1, a1) <- transl_expr For_val l1;
       do (sl2, a2) <- transl_expr For_val r2;
       do (sl3, a3) <- transl_valof ty1 a1;
+      do bf <- is_bitfield_access a1;
       match dst with
       | For_val | For_set _ =>
           do t <- gensym ty1;
           ret (finish dst
                  (sl1 ++ sl2 ++ sl3 ++
                   Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
-                  make_assign a1 (Etempvar t ty1) :: nil)
-                 (Etempvar t ty1))
+                  make_assign bf a1 (Etempvar t ty1) :: nil)
+                 (make_assign_value bf (Etempvar t ty1)))
       | For_effects =>
-          ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil,
+          ret (sl1 ++ sl2 ++ sl3 ++ make_assign bf a1 (Ebinop op a3 a2 tyres) :: nil,
                dummy_expr)
       end
   | Csyntax.Epostincr id l1 ty =>
       let ty1 := Csyntax.typeof l1 in
       do (sl1, a1) <- transl_expr For_val l1;
+      do bf <- is_bitfield_access a1;
       match dst with
       | For_val | For_set _ =>
           do t <- gensym ty1;
           ret (finish dst
-                 (sl1 ++ make_set t a1 ::
-                  make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: nil)
+                 (sl1 ++ make_set bf t a1 ::
+                  make_assign bf a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: nil)
                  (Etempvar t ty1))
       | For_effects =>
           do (sl2, a2) <- transl_valof ty1 a1;
-          ret (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil,
+          ret (sl1 ++ sl2 ++ make_assign bf a1 (transl_incrdecr id a2 ty1) :: nil,
                dummy_expr)
       end
   | Csyntax.Ecomma r1 r2 ty =>
@@ -424,12 +496,6 @@ Definition transl_expression (r: Csyntax.expr) : mon (statement * expr) :=
 Definition transl_expr_stmt (r: Csyntax.expr) : mon statement :=
   do (sl, a) <- transl_expr For_effects r; ret (makeseq sl).
 
-(*
-Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement :=
-  do (sl, a) <- transl_expr For_val r;
-  ret (makeseq (sl ++ makeif a s1 s2 :: nil)).
-*)
-
 Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement :=
   do (sl, a) <- transl_expr For_val r;
   ret (makeseq (sl ++ makeif a s1 s2 :: nil)).
@@ -533,8 +599,12 @@ Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
       OK (External ef targs tres cc)
   end.
 
+End SIMPL_EXPR.
+
+Local Open Scope error_monad_scope.
+
 Definition transl_program (p: Csyntax.program) : res program :=
-  do p1 <- AST.transform_partial_program transl_fundef p;
+  do p1 <- AST.transform_partial_program (transl_fundef p.(prog_comp_env)) p;
   OK {| prog_defs := AST.prog_defs p1;
         prog_public := AST.prog_public p1;
         prog_main := AST.prog_main p1;