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, 38 insertions, 22 deletions

diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 988988a1..e4b759c4 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -391,7 +391,7 @@ Lemma match_envs_assign_lifted:
   e!id = Some(b, ty) ->
   val_casted v ty ->
   Val.inject f v tv ->
-  assign_loc ge ty m b Ptrofs.zero v m' ->
+  assign_loc ge ty m b Ptrofs.zero Full v m' ->
   VSet.mem id cenv = true ->
   match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi.
 Proof.
@@ -1004,13 +1004,13 @@ Proof.
 Qed.
 
 Lemma assign_loc_inject:
-  forall f ty m loc ofs v m' tm loc' ofs' v',
-  assign_loc ge ty m loc ofs v m' ->
+  forall f ty m loc ofs bf v m' tm loc' ofs' v',
+  assign_loc ge ty m loc ofs bf v m' ->
   Val.inject f (Vptr loc ofs) (Vptr loc' ofs') ->
   Val.inject f v v' ->
   Mem.inject f m tm ->
   exists tm',
-     assign_loc tge ty tm loc' ofs' v' tm'
+     assign_loc tge ty tm loc' ofs' bf v' tm'
   /\ Mem.inject f m' tm'
   /\ (forall b chunk v,
       f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v).
@@ -1078,15 +1078,25 @@ Proof.
   split. auto.
   intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto.
   left. congruence.
+- (* bitfield *)
+  inv H3.
+  exploit Mem.loadv_inject; eauto. intros (vc' & LD' & INJ). inv INJ.
+  exploit Mem.storev_mapped_inject; eauto. intros [tm' [A B]].
+  inv H1.
+  exists tm'; split. eapply assign_loc_bitfield; eauto. econstructor; eauto.
+  split. auto.
+  intros. rewrite <- H3. eapply Mem.load_store_other; eauto.
+  left. inv H0. congruence.
 Qed.
 
 Lemma assign_loc_nextblock:
-  forall ge ty m b ofs v m',
-  assign_loc ge ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m.
+  forall ge ty m b ofs bf v m',
+  assign_loc ge ty m b ofs bf v m' -> Mem.nextblock m' = Mem.nextblock m.
 Proof.
   induction 1.
   simpl in H0. eapply Mem.nextblock_store; eauto.
   eapply Mem.nextblock_storebytes; eauto.
+  inv H. eapply Mem.nextblock_store; eauto.
 Qed.
 
 Theorem store_params_correct:
@@ -1168,7 +1178,7 @@ Local Opaque Conventions1.parameter_needs_normalization.
   reflexivity. reflexivity.
   eexact U.
   traceEq.
-  rewrite (assign_loc_nextblock _ _ _ _ _ _ _ A) in Z. auto.
+  rewrite (assign_loc_nextblock _ _ _ _ _ _ _ _ A) in Z. auto.
 Qed.
 
 Lemma bind_parameters_nextblock:
@@ -1400,19 +1410,22 @@ Proof.
 Qed.
 
 Lemma deref_loc_inject:
-  forall ty loc ofs v loc' ofs',
-  deref_loc ty m loc ofs v ->
+  forall ty loc ofs bf v loc' ofs',
+  deref_loc ty m loc ofs bf v ->
   Val.inject f (Vptr loc ofs) (Vptr loc' ofs') ->
-  exists tv, deref_loc ty tm loc' ofs' tv /\ Val.inject f v tv.
+  exists tv, deref_loc ty tm loc' ofs' bf tv /\ Val.inject f v tv.
 Proof.
   intros. inv H.
-  (* by value *)
+- (* by value *)
   exploit Mem.loadv_inject; eauto. intros [tv [A B]].
   exists tv; split; auto. eapply deref_loc_value; eauto.
-  (* by reference *)
+- (* by reference *)
   exists (Vptr loc' ofs'); split; auto. eapply deref_loc_reference; eauto.
-  (* by copy *)
+- (* by copy *)
   exists (Vptr loc' ofs'); split; auto. eapply deref_loc_copy; eauto.
+- (* bitfield *)
+  inv H1.   exploit Mem.loadv_inject; eauto. intros [tc [A B]]. inv B. 
+  econstructor; split. eapply deref_loc_bitfield. econstructor; eauto. constructor.
 Qed.
 
 Lemma eval_simpl_expr:
@@ -1422,11 +1435,11 @@ Lemma eval_simpl_expr:
   exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv
 
 with eval_simpl_lvalue:
-  forall a b ofs,
-  eval_lvalue ge e le m a b ofs ->
+  forall a b ofs bf,
+  eval_lvalue ge e le m a b ofs bf ->
   compat_cenv (addr_taken_expr a) cenv ->
   match a with Evar id ty => VSet.mem id cenv = false | _ => True end ->
-  exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ Val.inject f (Vptr b ofs) (Vptr b' ofs').
+  exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' bf /\ Val.inject f (Vptr b ofs) (Vptr b' ofs').
 
 Proof.
   destruct 1; simpl; intros.
@@ -1472,7 +1485,7 @@ Proof.
   subst a. simpl. rewrite OPT.
   exploit me_vars; eauto. instantiate (1 := id). intros MV.
   inv H; inv MV; try congruence.
-  rewrite ENV in H6; inv H6.
+  rewrite ENV in H7; inv H7.
   inv H0; try congruence.
   assert (chunk0 = chunk). simpl in H. congruence. subst chunk0.
   assert (v0 = v). unfold Mem.loadv in H2. rewrite Ptrofs.unsigned_zero in H2. congruence. subst v0.
@@ -1516,7 +1529,8 @@ Proof.
   exploit eval_simpl_expr; eauto. intros [tv [A B]].
   inversion B. subst.
   econstructor; econstructor; split.
-  eapply eval_Efield_union; eauto. rewrite typeof_simpl_expr; eauto. auto.
+  eapply eval_Efield_union; eauto. rewrite typeof_simpl_expr; eauto.
+  econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
 Qed.
 
 Lemma eval_simpl_exprlist:
@@ -1607,18 +1621,20 @@ Qed.
 (** Invariance by assignment to location "above" *)
 
 Lemma match_cont_assign_loc:
-  forall f cenv k tk m bound tbound ty loc ofs v m',
+  forall f cenv k tk m bound tbound ty loc ofs bf v m',
   match_cont f cenv k tk m bound tbound ->
-  assign_loc ge ty m loc ofs v m' ->
+  assign_loc ge ty m loc ofs bf v m' ->
   Ple bound loc ->
   match_cont f cenv k tk m' bound tbound.
 Proof.
   intros. eapply match_cont_invariant; eauto.
   intros. rewrite <- H4. inv H0.
-  (* scalar *)
+- (* scalar *)
   simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; extlia.
-  (* block copy *)
+- (* block copy *)
   eapply Mem.load_storebytes_other; eauto. left. unfold block; extlia.
+- (* bitfield *)
+  inv H5. eapply Mem.load_store_other; eauto. left. unfold block; extlia.
 Qed.
 
 (** Invariance by external calls *)