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

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 3b21be28..d15bc90a 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -197,36 +197,42 @@ Definition empty_env: env := (PTree.empty (block * type)).
 
 Definition temp_env := PTree.t val.
 
-(** [deref_loc ty m b ofs v] computes the value of a datum
-  of type [ty] residing in memory [m] at block [b], offset [ofs].
+(** [deref_loc ty m b ofs bf v] computes the value of a datum
+  of type [ty] residing in memory [m] at block [b], offset [ofs],
+  and bitfield designation [bf].
   If the type [ty] indicates an access by value, the corresponding
   memory load is performed.  If the type [ty] indicates an access by
   reference or by copy, the pointer [Vptr b ofs] is returned. *)
 
-Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : val -> Prop :=
+Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : 
+                                             bitfield -> val -> Prop :=
   | deref_loc_value: forall chunk v,
       access_mode ty = By_value chunk ->
       Mem.loadv chunk m (Vptr b ofs) = Some v ->
-      deref_loc ty m b ofs v
+      deref_loc ty m b ofs Full v
   | deref_loc_reference:
       access_mode ty = By_reference ->
-      deref_loc ty m b ofs (Vptr b ofs)
+      deref_loc ty m b ofs Full (Vptr b ofs)
   | deref_loc_copy:
       access_mode ty = By_copy ->
-      deref_loc ty m b ofs (Vptr b ofs).
+      deref_loc ty m b ofs Full (Vptr b ofs)
+  | deref_loc_bitfield: forall sz sg pos width v,
+      load_bitfield ty sz sg pos width m (Vptr b ofs) v ->
+      deref_loc ty m b ofs (Bits sz sg pos width) v.
 
-(** Symmetrically, [assign_loc ty m b ofs v m'] returns the
+(** Symmetrically, [assign_loc ty m b ofs bf v m'] returns the
   memory state after storing the value [v] in the datum
-  of type [ty] residing in memory [m] at block [b], offset [ofs].
+  of type [ty] residing in memory [m] at block [b], offset [ofs],
+  bitfield designation [bf].
   This is allowed only if [ty] indicates an access by value or by copy.
   [m'] is the updated memory state. *)
 
 Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: ptrofs):
-                                            val -> mem -> Prop :=
+                                            bitfield -> val -> mem -> Prop :=
   | assign_loc_value: forall v chunk m',
       access_mode ty = By_value chunk ->
       Mem.storev chunk m (Vptr b ofs) v = Some m' ->
-      assign_loc ce ty m b ofs v m'
+      assign_loc ce ty m b ofs Full v m'
   | assign_loc_copy: forall b' ofs' bytes m',
       access_mode ty = By_copy ->
       (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs')) ->
@@ -236,7 +242,10 @@ Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: pt
               \/ Ptrofs.unsigned ofs + sizeof ce ty <= Ptrofs.unsigned ofs' ->
       Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ce ty) = Some bytes ->
       Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
-      assign_loc ce ty m b ofs (Vptr b' ofs') m'.
+      assign_loc ce ty m b ofs Full (Vptr b' ofs') m'
+  | assign_loc_bitfield: forall sz sg pos width v m' v',
+      store_bitfield ty sz sg pos width m (Vptr b ofs) v m' v' ->
+      assign_loc ce ty m b ofs (Bits sz sg pos width) v m'.
 
 Section SEMANTICS.
 
@@ -275,7 +284,7 @@ Inductive bind_parameters (e: env):
   | bind_parameters_cons:
       forall m id ty params v1 vl b m1 m2,
       PTree.get id e = Some(b, ty) ->
-      assign_loc ge ty m b Ptrofs.zero v1 m1 ->
+      assign_loc ge ty m b Ptrofs.zero Full v1 m1 ->
       bind_parameters e m1 params vl m2 ->
       bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
 
@@ -369,7 +378,7 @@ Inductive eval_expr: expr -> val -> Prop :=
       le!id = Some v ->
       eval_expr (Etempvar id ty) v
   | eval_Eaddrof: forall a ty loc ofs,
-      eval_lvalue a loc ofs ->
+      eval_lvalue a loc ofs Full ->
       eval_expr (Eaddrof a ty) (Vptr loc ofs)
   | eval_Eunop:  forall op a ty v1 v,
       eval_expr a v1 ->
@@ -388,37 +397,39 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1)))
   | eval_Ealignof: forall ty1 ty,
       eval_expr (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1)))
-  | eval_Elvalue: forall a loc ofs v,
-      eval_lvalue a loc ofs ->
-      deref_loc (typeof a) m loc ofs v ->
+  | eval_Elvalue: forall a loc ofs bf v,
+      eval_lvalue a loc ofs bf ->
+      deref_loc (typeof a) m loc ofs bf v ->
       eval_expr a v
 
 (** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
   in l-value position.  The result is the memory location [b, ofs]
-  that contains the value of the expression [a]. *)
+  that contains the value of the expression [a], and the bitfield [bf]
+  designation. *)
 
-with eval_lvalue: expr -> block -> ptrofs -> Prop :=
+with eval_lvalue: expr -> block -> ptrofs -> bitfield -> Prop :=
   | eval_Evar_local:   forall id l ty,
       e!id = Some(l, ty) ->
-      eval_lvalue (Evar id ty) l Ptrofs.zero
+      eval_lvalue (Evar id ty) l Ptrofs.zero Full
   | eval_Evar_global: forall id l ty,
       e!id = None ->
       Genv.find_symbol ge id = Some l ->
-      eval_lvalue (Evar id ty) l Ptrofs.zero
+      eval_lvalue (Evar id ty) l Ptrofs.zero Full
   | eval_Ederef: forall a ty l ofs,
       eval_expr a (Vptr l ofs) ->
-      eval_lvalue (Ederef a ty) l ofs
- | eval_Efield_struct:   forall a i ty l ofs id co att delta,
+      eval_lvalue (Ederef a ty) l ofs Full
+ | eval_Efield_struct:   forall a i ty l ofs id co att delta bf,
       eval_expr a (Vptr l ofs) ->
       typeof a = Tstruct id att ->
       ge.(genv_cenv)!id = Some co ->
-      field_offset ge i (co_members co) = OK delta ->
-      eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta))
- | eval_Efield_union:   forall a i ty l ofs id co att,
+      field_offset ge i (co_members co) = OK (delta, bf) ->
+      eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) bf
+ | eval_Efield_union:   forall a i ty l ofs id co att delta bf,
       eval_expr a (Vptr l ofs) ->
       typeof a = Tunion id att ->
       ge.(genv_cenv)!id = Some co ->
-      eval_lvalue (Efield a i ty) l ofs.
+      union_field_offset ge i (co_members co) = OK (delta, bf) ->
+      eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) bf.
 
 Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
   with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
@@ -547,11 +558,11 @@ Variable function_entry: function -> list val -> mem -> env -> temp_env -> mem -
 
 Inductive step: state -> trace -> state -> Prop :=
 
-  | step_assign:   forall f a1 a2 k e le m loc ofs v2 v m',
-      eval_lvalue e le m a1 loc ofs ->
+  | step_assign:   forall f a1 a2 k e le m loc ofs bf v2 v m',
+      eval_lvalue e le m a1 loc ofs bf ->
       eval_expr e le m a2 v2 ->
       sem_cast v2 (typeof a2) (typeof a1) m = Some v ->
-      assign_loc ge (typeof a1) m loc ofs v m' ->
+      assign_loc ge (typeof a1) m loc ofs bf v m' ->
       step (State f (Sassign a1 a2) k e le m)
         E0 (State f Sskip k e le m')