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, 102 insertions, 59 deletions

diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 98425311..b689bdeb 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -18,6 +18,8 @@ Require Import Ctypes Cop Csyntax Clight SimplExpr.
 
 Section SPEC.
 
+Variable ce: composite_env.
+
 Local Open Scope gensym_monad_scope.
 
 (** * Relational specification of the translation. *)
@@ -40,13 +42,28 @@ Definition final (dst: destination) (a: expr) : list statement :=
   | For_set sd => do_set sd a
   end.
 
+Definition tr_is_bitfield_access (l: expr) (bf: bitfield) : Prop :=
+  match l with
+  | Efield r f _ =>
+      exists co ofs,
+      match typeof r with
+      | Tstruct id _ =>
+          ce!id = Some co /\ field_offset ce f (co_members co) = OK (ofs, bf)
+      | Tunion id _ =>
+          ce!id = Some co /\ union_field_offset ce f (co_members co) = OK (ofs, bf)
+      | _ => False
+      end
+  | _ => bf = Full
+  end.
+
 Inductive tr_rvalof: type -> expr -> list statement -> expr -> list ident -> Prop :=
   | tr_rvalof_nonvol: forall ty a tmp,
       type_is_volatile ty = false ->
       tr_rvalof ty a nil a tmp
-  | tr_rvalof_vol: forall ty a t tmp,
+  | tr_rvalof_vol: forall ty a t bf tmp,
       type_is_volatile ty = true -> In t tmp ->
-      tr_rvalof ty a (make_set t a :: nil) (Etempvar t ty) tmp.
+      tr_is_bitfield_access a bf ->
+      tr_rvalof ty a (make_set bf t a :: nil) (Etempvar t ty) tmp.
 
 Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop :=
   | tr_var: forall le dst id ty tmp,
@@ -200,15 +217,16 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       tr_expr le (For_set sd) (Csyntax.Econdition e1 e2 e3 ty)
                        (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil)
                        any tmp
-  | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
+  | tr_assign_effects: forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 bf any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       list_disjoint tmp1 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
+      tr_is_bitfield_access a1 bf ->
       tr_expr le For_effects (Csyntax.Eassign e1 e2 ty)
-                      (sl1 ++ sl2 ++ make_assign a1 a2 :: nil)
+                      (sl1 ++ sl2 ++ make_assign bf a1 a2 :: nil)
                       any tmp
-  | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2,
+  | tr_assign_val: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2 bf,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
@@ -216,23 +234,25 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       In t tmp -> ~In t tmp1 -> ~In t tmp2 ->
       ty1 = Csyntax.typeof e1 ->
       ty2 = Csyntax.typeof e2 ->
+      tr_is_bitfield_access a1 bf ->
       tr_expr le dst (Csyntax.Eassign e1 e2 ty)
                    (sl1 ++ sl2 ++
                     Sset t (Ecast a2 ty1) ::
-                    make_assign a1 (Etempvar t ty1) ::
-                    final dst (Etempvar t ty1))
-                   (Etempvar t ty1) tmp
-  | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
+                    make_assign bf a1 (Etempvar t ty1) ::
+                    final dst (make_assign_value bf (Etempvar t ty1)))
+                   (make_assign_value bf (Etempvar t ty1)) tmp
+  | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 bf sl3 a3 tmp3 any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       ty1 = Csyntax.typeof e1 ->
       tr_rvalof ty1 a1 sl3 a3 tmp3 ->
       list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
+      tr_is_bitfield_access a1 bf ->
       tr_expr le For_effects (Csyntax.Eassignop op e1 e2 tyres ty)
-                      (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil)
+                      (sl1 ++ sl2 ++ sl3 ++ make_assign bf a1 (Ebinop op a3 a2 tyres) :: nil)
                       any tmp
-  | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp ty1,
+  | tr_assignop_val: forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t bf tmp ty1,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_expr le For_val e2 sl2 a2 tmp2 ->
       tr_rvalof ty1 a1 sl3 a3 tmp3 ->
@@ -240,28 +260,31 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement ->
       incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
       In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 ->
       ty1 = Csyntax.typeof e1 ->
+      tr_is_bitfield_access a1 bf ->
       tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty)
                    (sl1 ++ sl2 ++ sl3 ++
                     Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
-                    make_assign a1 (Etempvar t ty1) ::
-                    final dst (Etempvar t ty1))
-                   (Etempvar t ty1) tmp
-  | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
+                    make_assign bf a1 (Etempvar t ty1) ::
+                    final dst (make_assign_value bf (Etempvar t ty1)))
+                   (make_assign_value bf (Etempvar t ty1)) tmp
+  | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 bf any tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       tr_rvalof ty1 a1 sl2 a2 tmp2 ->
       ty1 = Csyntax.typeof e1 ->
       incl tmp1 tmp -> incl tmp2 tmp ->
       list_disjoint tmp1 tmp2 ->
+      tr_is_bitfield_access a1 bf ->
       tr_expr le For_effects (Csyntax.Epostincr id e1 ty)
-                      (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil)
+                      (sl1 ++ sl2 ++ make_assign bf a1 (transl_incrdecr id a2 ty1) :: nil)
                       any tmp
-  | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 t ty1 tmp,
+  | tr_postincr_val: forall le dst id e1 ty sl1 a1 tmp1 bf t ty1 tmp,
       tr_expr le For_val e1 sl1 a1 tmp1 ->
       incl tmp1 tmp -> In t tmp -> ~In t tmp1 ->
       ty1 = Csyntax.typeof e1 ->
+      tr_is_bitfield_access a1 bf ->
       tr_expr le dst (Csyntax.Epostincr id e1 ty)
-                   (sl1 ++ make_set t a1 ::
-                    make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) ::
+                   (sl1 ++ make_set bf t a1 ::
+                    make_assign bf a1 (transl_incrdecr id (Etempvar t ty1) ty1) ::
                     final dst (Etempvar t ty1))
                    (Etempvar t ty1) tmp
   | tr_comma: forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp,
@@ -746,14 +769,31 @@ Proof.
   intros. apply tr_expr_monotone with tmps; auto. apply add_dest_incl.
 Qed.
 
+Lemma is_bitfield_access_meets_spec: forall l g bf g' I,
+  is_bitfield_access ce l g = Res bf g' I ->
+  tr_is_bitfield_access l bf.
+Proof.
+  unfold is_bitfield_access; intros; red. destruct l; try (monadInv H; auto).
+  assert (AUX: forall fn id,
+               is_bitfield_access_aux ce fn id i g = Res bf g' I ->
+               exists co ofs,
+               ce!id = Some co /\ fn ce i (co_members co) = OK (ofs, bf)).
+  { unfold is_bitfield_access_aux; intros.
+    destruct ce!id as [co|]; try discriminate.
+    destruct (fn ce i (co_members co)) as [[ofs1 bf1]|] eqn:FN; inv H0.
+    exists co, ofs1; auto. }
+  destruct (typeof l); try discriminate; apply AUX; auto.
+Qed.
+
 Lemma transl_valof_meets_spec:
   forall ty a g sl b g' I,
-  transl_valof ty a g = Res (sl, b) g' I ->
+  transl_valof ce ty a g = Res (sl, b) g' I ->
   exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'.
 Proof.
   unfold transl_valof; intros.
   destruct (type_is_volatile ty) eqn:?; monadInv H.
-  exists (x :: nil); split; eauto with gensym. econstructor; eauto with coqlib.
+  exists (x :: nil); split; eauto with gensym.
+  econstructor; eauto using is_bitfield_access_meets_spec with coqlib.
   exists (@nil ident); split; eauto with gensym. constructor; auto.
 Qed.
 
@@ -763,12 +803,12 @@ Combined Scheme expr_exprlist_ind from expr_ind2, exprlist_ind2.
 
 Lemma transl_meets_spec:
    (forall r dst g sl a g' I,
-    transl_expr dst r g = Res (sl, a) g' I ->
+    transl_expr ce dst r g = Res (sl, a) g' I ->
     dest_below dst g ->
     exists tmps, (forall le, tr_expr le dst r sl a (add_dest dst tmps)) /\ contained tmps g g')
   /\
    (forall rl g sl al g' I,
-    transl_exprlist rl g = Res (sl, al) g' I ->
+    transl_exprlist ce rl g = Res (sl, al) g' I ->
     exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g').
 Proof.
   apply expr_exprlist_ind; simpl add_dest; intros.
@@ -920,9 +960,10 @@ Opaque makeif.
 - (* assign *)
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
-  destruct dst; monadInv EQ2; simpl add_dest in *.
+  apply is_bitfield_access_meets_spec in EQ0.
+  destruct dst; monadInv EQ3; simpl add_dest in *.
 + (* for value *)
-  exists (x1 :: tmp1 ++ tmp2); split.
+  exists (x2 :: tmp1 ++ tmp2); split.
   intros. eapply tr_assign_val with (dst := For_val); eauto with gensym.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
@@ -931,7 +972,7 @@ Opaque makeif.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
 + (* for set *)
-  exists (x1 :: tmp1 ++ tmp2); split.
+  exists (x2 :: tmp1 ++ tmp2); split.
   repeat rewrite app_ass. simpl.
   intros. eapply tr_assign_val with (dst := For_set sd); eauto with gensym.
   apply contained_cons. eauto with gensym.
@@ -940,37 +981,39 @@ Opaque makeif.
   monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]].
-  destruct dst; monadInv EQ3; simpl add_dest in *.
+  apply is_bitfield_access_meets_spec in EQ2.
+  destruct dst; monadInv EQ4; simpl add_dest in *.
 + (* for value *)
-  exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
-  intros. eapply tr_assignop_val with (dst := For_val); eauto with gensym.
-  apply contained_cons. eauto with gensym.
-  apply contained_app; eauto with gensym.
+  exists (x3 :: tmp1 ++ tmp2 ++ tmp3); split.
+  intros. eapply tr_assignop_val with (dst := For_val); eauto 6 with gensym.
+  apply contained_cons. eauto 6 with gensym.
+  apply contained_app; eauto 6 with gensym.
 + (* for effects *)
   exists (tmp1 ++ tmp2 ++ tmp3); split.
   econstructor; eauto with gensym.
   apply contained_app; eauto with gensym.
 + (* for set *)
-  exists (x2 :: tmp1 ++ tmp2 ++ tmp3); split.
+  exists (x3 :: tmp1 ++ tmp2 ++ tmp3); split.
   repeat rewrite app_ass. simpl.
-  intros. eapply tr_assignop_val with (dst := For_set sd); eauto with gensym.
-  apply contained_cons. eauto with gensym.
-  apply contained_app; eauto with gensym.
+  intros. eapply tr_assignop_val with (dst := For_set sd); eauto 6 with gensym.
+  apply contained_cons. eauto 6 with gensym.
+  apply contained_app; eauto 6 with gensym.
 - (* postincr *)
   monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
-  destruct dst; monadInv EQ0; simpl add_dest in *.
+  apply is_bitfield_access_meets_spec in EQ1.
+  destruct dst; monadInv EQ2; simpl add_dest in *.
 + (* for value *)
-  exists (x0 :: tmp1); split.
+  exists (x1 :: tmp1); split.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
 + (* for effects *)
-  exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]].
+  exploit transl_valof_meets_spec; eauto. intros [tmp2 [C D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
   eauto with gensym.
 + (* for set *)
   repeat rewrite app_ass; simpl.
-  exists (x0 :: tmp1); split.
+  exists (x1 :: tmp1); split.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
 - (* comma *)
@@ -1032,7 +1075,7 @@ Qed.
 
 Lemma transl_expr_meets_spec:
    forall r dst g sl a g' I,
-   transl_expr dst r g = Res (sl, a) g' I ->
+   transl_expr ce dst r g = Res (sl, a) g' I ->
    dest_below dst g ->
    exists tmps, forall ge e le m, tr_top ge e le m dst r sl a tmps.
 Proof.
@@ -1042,7 +1085,7 @@ Qed.
 
 Lemma transl_expression_meets_spec:
   forall r g s a g' I,
-  transl_expression r g = Res (s, a) g' I ->
+  transl_expression ce r g = Res (s, a) g' I ->
   tr_expression r s a.
 Proof.
   intros. monadInv H. exploit transl_expr_meets_spec; eauto.
@@ -1051,7 +1094,7 @@ Qed.
 
 Lemma transl_expr_stmt_meets_spec:
   forall r g s g' I,
-  transl_expr_stmt r g = Res s g' I ->
+  transl_expr_stmt ce r g = Res s g' I ->
   tr_expr_stmt r s.
 Proof.
   intros. monadInv H. exploit transl_expr_meets_spec; eauto.
@@ -1060,7 +1103,7 @@ Qed.
 
 Lemma transl_if_meets_spec:
   forall r s1 s2 g s g' I,
-  transl_if r s1 s2 g = Res s g' I ->
+  transl_if ce r s1 s2 g = Res s g' I ->
   tr_if r s1 s2 s.
 Proof.
   intros. monadInv H. exploit transl_expr_meets_spec; eauto.
@@ -1068,9 +1111,9 @@ Proof.
 Qed.
 
 Lemma transl_stmt_meets_spec:
-  forall s g ts g' I, transl_stmt s g = Res ts g' I -> tr_stmt s ts
+  forall s g ts g' I, transl_stmt ce s g = Res ts g' I -> tr_stmt s ts
 with transl_lblstmt_meets_spec:
-  forall s g ts g' I, transl_lblstmt s g = Res ts g' I -> tr_lblstmts s ts.
+  forall s g ts g' I, transl_lblstmt ce s g = Res ts g' I -> tr_lblstmts s ts.
 Proof.
   generalize transl_expression_meets_spec transl_expr_stmt_meets_spec transl_if_meets_spec; intros T1 T2 T3.
 Opaque transl_expression transl_expr_stmt.
@@ -1099,32 +1142,32 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
       fn_vars tf = Csyntax.fn_vars f ->
       tr_function f tf.
 
-Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
-  | tr_internal: forall f tf,
-      tr_function f tf ->
-      tr_fundef (Internal f) (Internal tf)
-  | tr_external: forall ef targs tres cconv,
-      tr_fundef (External ef targs tres cconv) (External ef targs tres cconv).
-
 Lemma transl_function_spec:
   forall f tf,
-  transl_function f = OK tf ->
+  transl_function ce f = OK tf ->
   tr_function f tf.
 Proof.
   unfold transl_function; intros.
-  destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)) eqn:T; inv H.
+  destruct (transl_stmt ce (Csyntax.fn_body f) (initial_generator tt)) eqn:T; inv H.
   constructor; auto. simpl. eapply transl_stmt_meets_spec; eauto.
 Qed.
 
+End SPEC.
+
+Inductive tr_fundef (p: Csyntax.program): Csyntax.fundef -> Clight.fundef -> Prop :=
+  | tr_internal: forall f tf,
+      tr_function p.(prog_comp_env) f tf ->
+      tr_fundef p (Internal f) (Internal tf)
+  | tr_external: forall ef targs tres cconv,
+      tr_fundef p (External ef targs tres cconv) (External ef targs tres cconv).
+
 Lemma transl_fundef_spec:
-  forall fd tfd,
-  transl_fundef fd = OK tfd ->
-  tr_fundef fd tfd.
+  forall p fd tfd,
+  transl_fundef p.(prog_comp_env) fd = OK tfd ->
+  tr_fundef p fd tfd.
 Proof.
   unfold transl_fundef; intros.
   destruct fd; Errors.monadInv H.
 + constructor. eapply transl_function_spec; eauto.
 + constructor.
 Qed.
-
-End SPEC.