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, 162 insertions, 158 deletions

diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 6365f85c..ce965672 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -49,7 +49,7 @@ Variable ge: genv.
 
 Fixpoint simple (a: expr) : bool :=
   match a with
-  | Eloc _ _ _ => true
+  | Eloc _ _ _ _ => true
   | Evar _ _ => true
   | Ederef r _ => simple r
   | Efield r _ _ => simple r
@@ -86,41 +86,42 @@ Section SIMPLE_EXPRS.
 Variable e: env.
 Variable m: mem.
 
-Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop :=
-  | esl_loc: forall b ofs ty,
-      eval_simple_lvalue (Eloc b ofs ty) b ofs
+Inductive eval_simple_lvalue: expr -> block -> ptrofs -> bitfield -> Prop :=
+  | esl_loc: forall b ofs ty bf,
+      eval_simple_lvalue (Eloc b ofs bf ty) b ofs bf
   | esl_var_local: forall x ty b,
       e!x = Some(b, ty) ->
-      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero Full
   | esl_var_global: forall x ty b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero Full
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
-      eval_simple_lvalue (Ederef r ty) b ofs
-  | esl_field_struct: forall r f ty b ofs id co a delta,
+      eval_simple_lvalue (Ederef r ty) b ofs Full
+  | esl_field_struct: forall r f ty b ofs id co a delta bf,
       eval_simple_rvalue r (Vptr b ofs) ->
       typeof r = Tstruct id a ->
       ge.(genv_cenv)!id = Some co ->
-      field_offset ge f (co_members co) = OK delta ->
-      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta))
-  | esl_field_union: forall r f ty b ofs id co a,
+      field_offset ge f (co_members co) = OK (delta, bf) ->
+      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) bf
+  | esl_field_union: forall r f ty b ofs id co a delta bf,
       eval_simple_rvalue r (Vptr b ofs) ->
       typeof r = Tunion id a ->
+      union_field_offset ge f (co_members co) = OK (delta, bf) ->
       ge.(genv_cenv)!id = Some co ->
-      eval_simple_lvalue (Efield r f ty) b ofs
+      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) bf
 
 with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_val: forall v ty,
       eval_simple_rvalue (Eval v ty) v
-  | esr_rvalof: forall b ofs l ty v,
-      eval_simple_lvalue l b ofs ->
+  | esr_rvalof: forall b ofs bf l ty v,
+      eval_simple_lvalue l b ofs bf ->
       ty = typeof l -> type_is_volatile ty = false ->
-      deref_loc ge ty m b ofs E0 v ->
+      deref_loc ge ty m b ofs bf E0 v ->
       eval_simple_rvalue (Evalof l ty) v
   | esr_addrof: forall b ofs l ty,
-      eval_simple_lvalue l b ofs ->
+      eval_simple_lvalue l b ofs Full ->
       eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs)
   | esr_unop: forall op r1 ty v1 v,
       eval_simple_rvalue r1 v1 ->
@@ -240,10 +241,10 @@ Inductive estep: state -> trace -> state -> Prop :=
       estep (ExprState f r k e m)
          E0 (ExprState f (Eval v ty) k e m)
 
-  | step_rvalof_volatile: forall f C l ty k e m b ofs t v,
+  | step_rvalof_volatile: forall f C l ty k e m b ofs bf t v,
       leftcontext RV RV C ->
-      eval_simple_lvalue e m l b ofs ->
-      deref_loc ge ty m b ofs t v ->
+      eval_simple_lvalue e m l b ofs bf ->
+      deref_loc ge ty m b ofs bf t v ->
       ty = typeof l -> type_is_volatile ty = true ->
       estep (ExprState f (C (Evalof l ty)) k e m)
           t (ExprState f (C (Eval v ty)) k e m)
@@ -281,68 +282,68 @@ Inductive estep: state -> trace -> state -> Prop :=
       estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m)
          E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m)
 
-  | step_assign: forall f C l r ty k e m b ofs v v' t m',
+  | step_assign: forall f C l r ty k e m b ofs bf v v1 t m' v',
       leftcontext RV RV C ->
-      eval_simple_lvalue e m l b ofs ->
+      eval_simple_lvalue e m l b ofs bf ->
       eval_simple_rvalue e m r v ->
-      sem_cast v (typeof r) (typeof l) m = Some v' ->
-      assign_loc ge (typeof l) m b ofs v' t m' ->
+      sem_cast v (typeof r) (typeof l) m = Some v1 ->
+      assign_loc ge (typeof l) m b ofs bf v1 t m' v' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassign l r ty)) k e m)
           t (ExprState f (C (Eval v' ty)) k e m')
 
-  | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 t1 t2 m' t,
+  | step_assignop: forall f C op l r tyres ty k e m b ofs bf v1 v2 v3 v4 t1 t2 m' v' t,
       leftcontext RV RV C ->
-      eval_simple_lvalue e m l b ofs ->
-      deref_loc ge (typeof l) m b ofs t1 v1 ->
+      eval_simple_lvalue e m l b ofs bf ->
+      deref_loc ge (typeof l) m b ofs bf t1 v1 ->
       eval_simple_rvalue e m r v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 ->
       sem_cast v3 tyres (typeof l) m = Some v4 ->
-      assign_loc ge (typeof l) m b ofs v4 t2 m' ->
+      assign_loc ge (typeof l) m b ofs bf v4 t2 m' v' ->
       ty = typeof l ->
       t = t1 ** t2 ->
       estep (ExprState f (C (Eassignop op l r tyres ty)) k e m)
-          t (ExprState f (C (Eval v4 ty)) k e m')
+          t (ExprState f (C (Eval v' ty)) k e m')
 
-  | step_assignop_stuck: forall f C op l r tyres ty k e m b ofs v1 v2 t,
+  | step_assignop_stuck: forall f C op l r tyres ty k e m b ofs bf v1 v2 t,
       leftcontext RV RV C ->
-      eval_simple_lvalue e m l b ofs ->
-      deref_loc ge (typeof l) m b ofs t v1 ->
+      eval_simple_lvalue e m l b ofs bf ->
+      deref_loc ge (typeof l) m b ofs bf t v1 ->
       eval_simple_rvalue e m r v2 ->
       match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with
       | None => True
       | Some v3 =>
           match sem_cast v3 tyres (typeof l) m with
           | None => True
-          | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m')
+          | Some v4 => forall t2 m' v', ~(assign_loc ge (typeof l) m b ofs bf v4 t2 m' v')
           end
       end ->
       ty = typeof l ->
       estep (ExprState f (C (Eassignop op l r tyres ty)) k e m)
           t Stuckstate
 
-  | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 t1 t2 m' t,
+  | step_postincr: forall f C id l ty k e m b ofs bf v1 v2 v3 t1 t2 m' v' t,
       leftcontext RV RV C ->
-      eval_simple_lvalue e m l b ofs ->
-      deref_loc ge ty m b ofs t1 v1 ->
+      eval_simple_lvalue e m l b ofs bf ->
+      deref_loc ge ty m b ofs bf t1 v1 ->
       sem_incrdecr ge id v1 ty m = Some v2 ->
       sem_cast v2 (incrdecr_type ty) ty m = Some v3 ->
-      assign_loc ge ty m b ofs v3 t2 m' ->
+      assign_loc ge ty m b ofs bf v3 t2 m' v' ->
       ty = typeof l ->
       t = t1 ** t2 ->
       estep (ExprState f (C (Epostincr id l ty)) k e m)
           t (ExprState f (C (Eval v1 ty)) k e m')
 
-  | step_postincr_stuck: forall f C id l ty k e m b ofs v1 t,
+  | step_postincr_stuck: forall f C id l ty k e m b ofs bf v1 t,
       leftcontext RV RV C ->
-      eval_simple_lvalue e m l b ofs ->
-      deref_loc ge ty m b ofs t v1 ->
+      eval_simple_lvalue e m l b ofs bf ->
+      deref_loc ge ty m b ofs bf t v1 ->
       match sem_incrdecr ge id v1 ty m with
       | None => True
       | Some v2 =>
           match sem_cast v2 (incrdecr_type ty) ty m with
           | None => True
-          | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m')
+          | Some v3 => forall t2 m' v', ~(assign_loc ge (typeof l) m b ofs bf v3 t2 m' v')
           end
       end ->
       ty = typeof l ->
@@ -452,7 +453,7 @@ Qed.
 
 Definition expr_kind (a: expr) : kind :=
   match a with
-  | Eloc _ _ _ => LV
+  | Eloc _ _ _ _ => LV
   | Evar _ _ => LV
   | Ederef _ _ => LV
   | Efield _ _ _ => LV
@@ -518,23 +519,25 @@ Fixpoint exprlist_all_values (rl: exprlist) : Prop :=
 
 Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   match a with
-  | Eloc b ofs ty => False
+  | Eloc b ofs bf ty => False
   | Evar x ty =>
       exists b,
       e!x = Some(b, ty)
       \/ (e!x = None /\ Genv.find_symbol ge x = Some b)
   | Ederef (Eval v ty1) ty =>
       exists b, exists ofs, v = Vptr b ofs
+  | Eaddrof (Eloc b ofs bf ty) ty' =>
+      bf = Full
   | Efield (Eval v ty1) f ty =>
       exists b, exists ofs, v = Vptr b ofs /\
       match ty1 with
-      | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = Errors.OK delta
-      | Tunion id _ => exists co, ge.(genv_cenv)!id = Some co
+      | Tstruct id _ => exists co delta bf, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = Errors.OK (delta, bf)
+      | Tunion id _ => exists co delta bf, ge.(genv_cenv)!id = Some co /\ union_field_offset ge f (co_members co) = Errors.OK (delta, bf)
       | _ => False
       end
   | Eval v ty => False
-  | Evalof (Eloc b ofs ty') ty =>
-      ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v
+  | Evalof (Eloc b ofs bf ty') ty =>
+      ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs bf t v
   | Eunop op (Eval v1 ty1) ty =>
       exists v, sem_unary_operation op v1 ty1 m = Some v
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
@@ -547,17 +550,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       exists b, bool_val v1 ty1 m = Some b
   | Econdition (Eval v1 ty1) r1 r2 ty =>
       exists b, bool_val v1 ty1 m = Some b
-  | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
-      exists v, exists m', exists t,
-      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m'
-  | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
-      exists t, exists v1,
+  | Eassign (Eloc b ofs bf ty1) (Eval v2 ty2) ty =>
+      exists v m' v' t,
+      ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs bf v t m' v'
+  | Eassignop op (Eloc b ofs bf ty1) (Eval v2 ty2) tyres ty =>
+      exists t v1,
       ty = ty1
-      /\ deref_loc ge ty1 m b ofs t v1
-  | Epostincr id (Eloc b ofs ty1) ty =>
-      exists t, exists v1,
+      /\ deref_loc ge ty1 m b ofs bf t v1
+  | Epostincr id (Eloc b ofs bf ty1) ty =>
+      exists t v1,
       ty = ty1
-      /\ deref_loc ge ty m b ofs t v1
+      /\ deref_loc ge ty m b ofs bf t v1
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) ty2 ty =>
@@ -584,8 +587,8 @@ Proof.
   exists b; auto.
   exists b; auto.
   exists b; exists ofs; auto.
-  exists b; exists ofs; split; auto. exists co, delta; auto.
-  exists b; exists ofs; split; auto. exists co; auto.
+  exists b; exists ofs; split; auto. exists co, delta, bf; auto.
+  exists b; exists ofs; split; auto. exists co, delta, bf; auto.
 Qed.
 
 Lemma rred_invert:
@@ -599,7 +602,7 @@ Proof.
   exists true; auto. exists false; auto.
   exists true; auto. exists false; auto.
   exists b; auto.
-  exists v; exists m'; exists t; auto.
+  exists v; exists m'; exists v'; exists t; auto.
   exists t; exists v1; auto.
   exists t; exists v1; auto.
   exists v; auto.
@@ -634,7 +637,7 @@ Proof.
   destruct (C a); auto; contradiction.
   destruct (C a); auto; contradiction.
   destruct (C a); auto; contradiction.
-  auto.
+  destruct (C a); auto; contradiction.
   destruct (C a); auto; contradiction.
   destruct (C a); auto; contradiction.
   destruct e1; auto; destruct (C a); auto; contradiction.
@@ -660,7 +663,7 @@ Lemma imm_safe_inv:
   forall k a m,
   imm_safe ge e k a m ->
   match a with
-  | Eloc _ _ _ => True
+  | Eloc _ _ _ _ => True
   | Eval _ _ => True
   | _ => invert_expr_prop a m
   end.
@@ -685,7 +688,7 @@ Lemma safe_inv:
   safe (ExprState f (C a) K e m) ->
   context k RV C ->
   match a with
-  | Eloc _ _ _ => True
+  | Eloc _ _ _ _ => True
   | Eval _ _ => True
   | _ => invert_expr_prop a m
   end.
@@ -709,10 +712,10 @@ Lemma eval_simple_steps:
     forall C, context RV RV C ->
     star Csem.step ge (ExprState f (C a) k e m)
                    E0 (ExprState f (C (Eval v (typeof a))) k e m))
-/\ (forall a b ofs, eval_simple_lvalue e m a b ofs ->
+/\ (forall a b ofs bf, eval_simple_lvalue e m a b ofs bf ->
     forall C, context LV RV C ->
     star Csem.step ge (ExprState f (C a) k e m)
-                   E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)).
+                   E0 (ExprState f (C (Eloc b ofs bf (typeof a))) k e m)).
 Proof.
 
 Ltac Steps REC C' := eapply star_trans; [apply (REC C'); eauto | idtac | simpl; reflexivity].
@@ -760,10 +763,10 @@ Lemma eval_simple_rvalue_steps:
 Proof (proj1 eval_simple_steps).
 
 Lemma eval_simple_lvalue_steps:
-  forall a b ofs, eval_simple_lvalue e m a b ofs ->
+  forall a b ofs bf, eval_simple_lvalue e m a b ofs bf ->
   forall C, context LV RV C ->
   star Csem.step ge (ExprState f (C a) k e m)
-                E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m).
+                E0 (ExprState f (C (Eloc b ofs bf (typeof a))) k e m).
 Proof (proj2 eval_simple_steps).
 
 Corollary eval_simple_rvalue_safe:
@@ -776,10 +779,10 @@ Proof.
 Qed.
 
 Corollary eval_simple_lvalue_safe:
-  forall C a b ofs,
-  eval_simple_lvalue e m a b ofs ->
+  forall C a b ofs bf,
+  eval_simple_lvalue e m a b ofs bf ->
   context LV RV C -> safe (ExprState f (C a) k e m) ->
-  safe (ExprState f (C (Eloc b ofs (typeof a))) k e m).
+  safe (ExprState f (C (Eloc b ofs bf (typeof a))) k e m).
 Proof.
   intros. eapply safe_steps; eauto. eapply eval_simple_lvalue_steps; eauto.
 Qed.
@@ -788,15 +791,15 @@ Lemma simple_can_eval:
   forall a from C,
   simple a = true -> context from RV C -> safe (ExprState f (C a) k e m) ->
   match from with
-  | LV => exists b, exists ofs, eval_simple_lvalue e m a b ofs
+  | LV => exists b ofs bf, eval_simple_lvalue e m a b ofs bf
   | RV => exists v, eval_simple_rvalue e m a v
   end.
 Proof.
 Ltac StepL REC C' a :=
-  let b := fresh "b" in let ofs := fresh "ofs" in
+  let b := fresh "b" in let ofs := fresh "ofs" in let bf := fresh "bf" in
   let E := fresh "E" in let S := fresh "SAFE" in
-  exploit (REC LV C'); eauto; intros [b [ofs E]];
-  assert (S: safe (ExprState f (C' (Eloc b ofs (typeof a))) k e m)) by
+  exploit (REC LV C'); eauto; intros (b & ofs & bf & E);
+  assert (S: safe (ExprState f (C' (Eloc b ofs bf (typeof a))) k e m)) by
     (eapply (eval_simple_lvalue_safe C'); eauto);
   simpl in S.
 Ltac StepR REC C' a :=
@@ -809,51 +812,52 @@ Ltac StepR REC C' a :=
   induction a; intros from C S CTX SAFE;
   generalize (safe_expr_kind _ _ _ _ _ _ _ CTX SAFE); intro K; subst;
   simpl in S; try discriminate; simpl.
-(* val *)
+- (* val *)
   exists v; constructor.
-(* var *)
+- (* var *)
   exploit safe_inv; eauto; simpl. intros [b A].
-  exists b; exists Ptrofs.zero.
+  exists b, Ptrofs.zero, Full.
   intuition. apply esl_var_local; auto. apply esl_var_global; auto.
-(* field *)
+- (* field *)
   StepR IHa (fun x => C(Efield x f0 ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl.
   intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction.
-  destruct TY as (co & delta & CE & OFS). exists b; exists (Ptrofs.add ofs (Ptrofs.repr delta)); econstructor; eauto.
-  destruct TY as (co & CE).  exists b; exists ofs; econstructor; eauto.
-(* valof *)
+  destruct TY as (co & delta & bf & CE & OFS). exists b, (Ptrofs.add ofs (Ptrofs.repr delta)), bf; eapply esl_field_struct; eauto.
+  destruct TY as (co & delta & bf & CE & OFS). exists b, (Ptrofs.add ofs (Ptrofs.repr delta)), bf; eapply esl_field_union; eauto.
+- (* valof *)
   destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2.
   StepL IHa (fun x => C(Evalof x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [t [v LOAD]]].
   assert (t = E0). inv LOAD; auto. congruence. subst t.
   exists v; econstructor; eauto. congruence.
-(* deref *)
+- (* deref *)
   StepR IHa (fun x => C(Ederef x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b [ofs EQ]].
-  subst v. exists b; exists ofs; econstructor; eauto.
-(* addrof *)
+  subst v. exists b, ofs, Full; econstructor; eauto.
+- (* addrof *)
   StepL IHa (fun x => C(Eaddrof x ty)) a.
+  exploit safe_inv. eexact SAFE0. eauto. simpl. intros EQ; subst bf.
   exists (Vptr b ofs); econstructor; eauto.
-(* unop *)
+- (* unop *)
   StepR IHa (fun x => C(Eunop op x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' EQ].
   exists v'; econstructor; eauto.
-(* binop *)
+- (* binop *)
   destruct (andb_prop _ _ S) as [S1 S2]; clear S.
   StepR IHa1 (fun x => C(Ebinop op x a2 ty)) a1.
   StepR IHa2 (fun x => C(Ebinop op (Eval v (typeof a1)) x ty)) a2.
   exploit safe_inv. eexact SAFE1. eauto. simpl. intros [v' EQ].
   exists v'; econstructor; eauto.
-(* cast *)
+- (* cast *)
   StepR IHa (fun x => C(Ecast x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [v' CAST].
   exists v'; econstructor; eauto.
-(* sizeof *)
+- (* sizeof *)
   econstructor; econstructor.
-(* alignof *)
+- (* alignof *)
   econstructor; econstructor.
-(* loc *)
-  exists b; exists ofs; constructor.
+- (* loc *)
+  exists b, ofs, bf; constructor.
 Qed.
 
 Lemma simple_can_eval_rval:
@@ -869,11 +873,11 @@ Qed.
 Lemma simple_can_eval_lval:
   forall l C,
   simple l = true -> context LV RV C -> safe (ExprState f (C l) k e m) ->
-  exists b, exists ofs, eval_simple_lvalue e m l b ofs
-         /\ safe (ExprState f (C (Eloc b ofs (typeof l))) k e m).
+  exists b ofs bf, eval_simple_lvalue e m l b ofs bf
+         /\ safe (ExprState f (C (Eloc b ofs bf (typeof l))) k e m).
 Proof.
-  intros. exploit (simple_can_eval l LV); eauto. intros [b [ofs A]].
-  exists b; exists ofs; split; auto. eapply eval_simple_lvalue_safe; eauto.
+  intros. exploit (simple_can_eval l LV); eauto. intros (b & ofs & bf & A).
+  exists b, ofs, bf; split; auto. eapply eval_simple_lvalue_safe; eauto.
 Qed.
 
 Fixpoint rval_list (vl: list val) (rl: exprlist) : exprlist :=
@@ -1178,18 +1182,18 @@ Proof.
   eapply star_plus_trans.
   eapply eval_simple_lvalue_steps with (C := fun x => C(Eassign x r (typeof l))); eauto.
   eapply plus_right.
-  eapply eval_simple_rvalue_steps with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto.
+  eapply eval_simple_rvalue_steps with (C := fun x => C(Eassign (Eloc b ofs bf (typeof l)) x (typeof l))); eauto.
   left; apply step_rred; eauto. econstructor; eauto.
   reflexivity. auto.
 (* assignop *)
   eapply star_plus_trans.
   eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto.
   eapply star_plus_trans.
-  eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto.
+  eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs bf (typeof l)) x tyres (typeof l))); eauto.
   eapply plus_left.
   left; apply step_rred; auto. econstructor; eauto.
   eapply star_left.
-  left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto.
+  left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs bf (typeof l)) x (typeof l))); eauto. econstructor; eauto.
   apply star_one.
   left; apply step_rred; auto. econstructor; eauto.
   reflexivity. reflexivity. reflexivity. traceEq.
@@ -1197,19 +1201,19 @@ Proof.
   eapply star_plus_trans.
   eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto.
   eapply star_plus_trans.
-  eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto.
+  eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs bf (typeof l)) x tyres (typeof l))); eauto.
   eapply plus_left.
   left; apply step_rred; auto. econstructor; eauto.
   destruct (sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?.
   eapply star_left.
-  left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto.
+  left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs bf (typeof l)) x (typeof l))); eauto. econstructor; eauto.
   apply star_one.
   left; eapply step_stuck; eauto.
-  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v4' [m' [t' [A [B D]]]]].
+  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v4' [m' [v' [t' [A [B D]]]]]].
   rewrite B in H4. eelim H4; eauto.
   reflexivity.
   apply star_one.
-  left; eapply step_stuck with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto.
+  left; eapply step_stuck with (C := fun x => C(Eassign (Eloc b ofs bf (typeof l)) x (typeof l))); eauto.
   red; intros. exploit imm_safe_inv; eauto. simpl. intros [v3 A]. congruence.
   reflexivity.
   reflexivity. traceEq.
@@ -1219,7 +1223,7 @@ Proof.
   eapply plus_left.
   left; apply step_rred; auto. econstructor; eauto.
   eapply star_left.
-  left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
+  left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs bf (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
   econstructor. instantiate (1 := v2). destruct id; assumption.
   eapply star_left.
   left; apply step_rred with (C := fun x => C (Ecomma x (Eval v1 (typeof l)) (typeof l))); eauto.
@@ -1238,15 +1242,15 @@ Proof.
     destruct id; auto.
   destruct (sem_incrdecr ge id v1 (typeof l) m) as [v2|].
   eapply star_left.
-  left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
+  left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs bf (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
   econstructor; eauto.
   apply star_one.
   left; eapply step_stuck with (C := fun x => C (Ecomma x (Eval v1 (typeof l)) (typeof l))); eauto.
-  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v3 [m' [t' [A [B D]]]]].
+  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v3 [m' [v' [t' [A [B D]]]]]].
   rewrite B in H3. eelim H3; eauto.
   reflexivity.
   apply star_one.
-  left; eapply step_stuck with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
+  left; eapply step_stuck with (C := fun x => C (Ecomma (Eassign (Eloc b ofs bf (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto.
   red; intros. exploit imm_safe_inv; eauto. simpl. intros [v2 A]. congruence.
   reflexivity.
   traceEq.
@@ -1291,7 +1295,7 @@ Proof.
 (* valof volatile *)
   destruct Q.
   exploit (simple_can_eval_lval f k e m b (fun x => C(Evalof x ty))); eauto.
-  intros [b1 [ofs [E1 S1]]].
+  intros (b1 & ofs & bf & E1 & S1).
   exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]].
   econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence.
 (* seqand *)
@@ -1316,40 +1320,40 @@ Proof.
 (* assign *)
   destruct Q.
   exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassign x b2 ty))); eauto.
-  intros [b [ofs [E1 S1]]].
-  exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassign (Eloc b ofs (typeof b1)) x ty))); eauto.
+  intros (b & ofs & bf & E1 & S1).
+  exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassign (Eloc b ofs bf (typeof b1)) x ty))); eauto.
   intros [v [E2 S2]].
-  exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [t [A [B D]]]]].
+  exploit safe_inv. eexact S2. eauto. simpl. intros [v1 [m' [v' [t [A [B D]]]]]].
   econstructor; econstructor; eapply step_assign; eauto.
 (* assignop *)
   destruct Q.
   exploit (simple_can_eval_lval f k e m b1 (fun x => C(Eassignop op x b2 tyres ty))); eauto.
-  intros [b [ofs [E1 S1]]].
-  exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto.
+  intros (b & ofs & bf & E1 & S1).
+  exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs bf (typeof b1)) x tyres ty))); eauto.
   intros [v [E2 S2]].
   exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
   destruct (sem_binary_operation ge op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?.
   destruct (sem_cast v3 tyres (typeof b1) m) as [v4|] eqn:?.
-  destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')).
-  destruct H2 as [t2 [m' D]].
+  destruct (classic (exists t2 m' v', assign_loc ge (typeof b1) m b ofs bf v4 t2 m' v')).
+  destruct H2 as [t2 [m' [v' D]]].
   econstructor; econstructor; eapply step_assignop; eauto.
   econstructor; econstructor; eapply step_assignop_stuck; eauto.
-  rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H2. exists t2; exists m'; auto.
+  rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H2. exists t2, m', v'; auto.
   econstructor; econstructor; eapply step_assignop_stuck; eauto.
   rewrite Heqo. rewrite Heqo0. auto.
   econstructor; econstructor; eapply step_assignop_stuck; eauto.
   rewrite Heqo. auto.
 (* postincr *)
   exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto.
-  intros [b1 [ofs [E1 S1]]].
+  intros (b1 & ofs & bf & E1 & S1).
   exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]].
   destruct (sem_incrdecr ge id v1 ty m) as [v2|] eqn:?.
   destruct (sem_cast v2 (incrdecr_type ty) ty m) as [v3|] eqn:?.
-  destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')).
-  destruct H0 as [t2 [m' D]].
+  destruct (classic (exists t2 m' v', assign_loc ge ty m b1 ofs bf v3 t2 m' v')).
+  destruct H0 as [t2 [m' [v' D]]].
   econstructor; econstructor; eapply step_postincr; eauto.
   econstructor; econstructor; eapply step_postincr_stuck; eauto.
-  rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H0. exists t2; exists m'; congruence.
+  rewrite Heqo. rewrite Heqo0. intros; red; intros. elim H0. exists t2, m', v'; congruence.
   econstructor; econstructor; eapply step_postincr_stuck; eauto.
   rewrite Heqo. rewrite Heqo0. auto.
   econstructor; econstructor; eapply step_postincr_stuck; eauto.
@@ -1440,18 +1444,18 @@ Definition semantics (p: program) :=
 (** This semantics is receptive to changes in events. *)
 
 Remark deref_loc_trace:
-  forall ge ty m b ofs t v,
-  deref_loc ge ty m b ofs t v ->
+  forall ge ty m b ofs bf t v,
+  deref_loc ge ty m b ofs bf t v ->
   match t with nil => True | ev :: nil => True | _ => False end.
 Proof.
   intros. inv H; simpl; auto. inv H2; simpl; auto.
 Qed.
 
 Remark deref_loc_receptive:
-  forall ge ty m b ofs ev1 t1 v ev2,
-  deref_loc ge ty m b ofs (ev1 :: t1) v ->
+  forall ge ty m b ofs bf ev1 t1 v ev2,
+  deref_loc ge ty m b ofs bf (ev1 :: t1) v ->
   match_traces ge (ev1 :: nil) (ev2 :: nil) ->
-  t1 = nil /\ exists v', deref_loc ge ty m b ofs (ev2 :: nil) v'.
+  t1 = nil /\ exists v', deref_loc ge ty m b ofs bf (ev2 :: nil) v'.
 Proof.
   intros.
   assert (t1 = nil). exploit deref_loc_trace; eauto. destruct t1; simpl; tauto.
@@ -1460,16 +1464,16 @@ Proof.
 Qed.
 
 Remark assign_loc_trace:
-  forall ge ty m b ofs t v m',
-  assign_loc ge ty m b ofs v t m' ->
+  forall ge ty m b ofs bf t v m' v',
+  assign_loc ge ty m b ofs bf v t m' v' ->
   match t with nil => True | ev :: nil => output_event ev | _ => False end.
 Proof.
   intros. inv H; simpl; auto. inv H2; simpl; auto.
 Qed.
 
 Remark assign_loc_receptive:
-  forall ge ty m b ofs ev1 t1 v m' ev2,
-  assign_loc ge ty m b ofs v (ev1 :: t1) m' ->
+  forall ge ty m b ofs bf ev1 t1 v m' v' ev2,
+  assign_loc ge ty m b ofs bf v (ev1 :: t1) m' v' ->
   match_traces ge (ev1 :: nil) (ev2 :: nil) ->
   ev1 :: t1 = ev2 :: nil.
 Proof.
@@ -1499,11 +1503,11 @@ Proof.
   inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
   destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
-  destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
-  destruct H1 as [t2' [m'' P]].
+  destruct (classic (exists t2' m'' v'', assign_loc ge (typeof l) m b ofs bf v4' t2' m'' v'')).
+  destruct H1 as [t2' [m'' [v'' P]]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
-  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto.
+  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0, m'0, v'0; auto.
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
   rewrite Heqo; rewrite Heqo0; auto.
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
@@ -1512,11 +1516,11 @@ Proof.
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
   destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?.
   destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?.
-  destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')).
-  destruct H1 as [t2' [m'' P]].
+  destruct (classic (exists t2' m'' v'', assign_loc ge (typeof l) m b ofs bf v4' t2' m'' v'')).
+  destruct H1 as [t2' [m'' [v'' P]]].
   econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity.
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
-  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto.
+  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2, m', v'; auto.
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
   rewrite Heqo; rewrite Heqo0; auto.
   econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto.
@@ -1528,11 +1532,11 @@ Proof.
   inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
   destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
   destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
-  destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
-  destruct H1 as [t2' [m'' P]].
+  destruct (classic (exists t2' m'' v'', assign_loc ge (typeof l) m b ofs bf v3' t2' m'' v'')).
+  destruct H1 as [t2' [m'' [v'' P]]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
-  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0; exists m'0; auto.
+  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t0, m'0, v'0; auto.
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
   rewrite Heqo; rewrite Heqo0; auto.
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
@@ -1541,11 +1545,11 @@ Proof.
   exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
   destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?.
   destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?.
-  destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')).
-  destruct H1 as [t2' [m'' P]].
+  destruct (classic (exists t2' m'' v'', assign_loc ge (typeof l) m b ofs bf v3' t2' m'' v'')).
+  destruct H1 as [t2' [m'' [v'' P]]].
   econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity.
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
-  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2; exists m'; auto.
+  rewrite Heqo; rewrite Heqo0. intros; red; intros; elim H1. exists t2, m', v'; auto.
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
   rewrite Heqo; rewrite Heqo0; auto.
   econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto.
@@ -1671,11 +1675,11 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       type_is_volatile (typeof a) = false ->
       eval_expr e m LV a t m' a' ->
       eval_expr e m RV (Evalof a ty) t m' (Evalof a' ty)
-  | eval_valof_volatile: forall e m a t1 m' a' ty b ofs t2 v,
+  | eval_valof_volatile: forall e m a t1 m' a' ty b ofs bf t2 v,
       type_is_volatile (typeof a) = true ->
       eval_expr e m LV a t1 m' a' ->
-      eval_simple_lvalue ge e m' a' b ofs ->
-      deref_loc ge (typeof a) m' b ofs t2 v ->
+      eval_simple_lvalue ge e m' a' b ofs bf ->
+      deref_loc ge (typeof a) m' b ofs bf t2 v ->
       ty = typeof a ->
       eval_expr e m RV (Evalof a ty) (t1 ** t2) m' (Eval v ty)
   | eval_deref: forall e m a t m' a' ty,
@@ -1723,32 +1727,32 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty)
   | eval_alignof: forall e m ty' ty,
       eval_expr e m RV (Ealignof ty' ty) E0 m (Ealignof ty' ty)
-  | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v v' t3 m3,
+  | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs bf v v1 v' t3 m3,
       eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' ->
-      eval_simple_lvalue ge e m2 l' b ofs ->
+      eval_simple_lvalue ge e m2 l' b ofs bf ->
       eval_simple_rvalue ge e m2 r' v ->
-      sem_cast v (typeof r) (typeof l) m2 = Some v' ->
-      assign_loc ge (typeof l) m2 b ofs v' t3 m3 ->
+      sem_cast v (typeof r) (typeof l) m2 = Some v1 ->
+      assign_loc ge (typeof l) m2 b ofs bf v1 t3 m3 v' ->
       ty = typeof l ->
       eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty)
-  | eval_assignop: forall e m op l r tyres ty t1 m1 l' t2 m2 r' b ofs
-                          v1 v2 v3 v4 t3 t4 m3,
+  | eval_assignop: forall e m op l r tyres ty t1 m1 l' t2 m2 r' b ofs bf
+                          v1 v2 v3 v4 v' t3 t4 m3,
       eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' ->
-      eval_simple_lvalue ge e m2 l' b ofs ->
-      deref_loc ge (typeof l) m2 b ofs t3 v1 ->
+      eval_simple_lvalue ge e m2 l' b ofs bf ->
+      deref_loc ge (typeof l) m2 b ofs bf t3 v1 ->
       eval_simple_rvalue ge e m2 r' v2 ->
       sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
       sem_cast v3 tyres (typeof l) m2 = Some v4 ->
-      assign_loc ge (typeof l) m2 b ofs v4 t4 m3 ->
+      assign_loc ge (typeof l) m2 b ofs bf v4 t4 m3 v' ->
       ty = typeof l ->
-      eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty)
-  | eval_postincr: forall e m id l ty t1 m1 l' b ofs v1 v2 v3 m2 t2 t3,
+      eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v' ty)
+  | eval_postincr: forall e m id l ty t1 m1 l' b ofs bf v1 v2 v3 v' m2 t2 t3,
       eval_expr e m LV l t1 m1 l' ->
-      eval_simple_lvalue ge e m1 l' b ofs ->
-      deref_loc ge ty m1 b ofs t2 v1 ->
+      eval_simple_lvalue ge e m1 l' b ofs bf ->
+      deref_loc ge ty m1 b ofs bf t2 v1 ->
       sem_incrdecr ge id v1 ty m1 = Some v2 ->
       sem_cast v2 (incrdecr_type ty) ty m1 = Some v3 ->
-      assign_loc ge ty m1 b ofs v3 t3 m2 ->
+      assign_loc ge ty m1 b ofs bf v3 t3 m2 v' ->
       ty = typeof l ->
       eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty)
   | eval_comma: forall e m r1 r2 ty t1 m1 r1' v1 t2 m2 r2',
@@ -2311,7 +2315,7 @@ Proof.
   simpl; intuition.
   eapply star_trans. eexact D.
   eapply star_right. eexact G.
-  left. eapply step_assign; eauto. congruence. rewrite B; eauto. congruence.
+  left. eapply step_assign with (v1 := v1); eauto. congruence. rewrite B; eauto. congruence.
   reflexivity. traceEq.
 (* assignop *)
   exploit (H0 (fun x => C(Eassignop op x r tyres ty))).
@@ -2322,7 +2326,7 @@ Proof.
   eapply star_trans. eexact D.
   eapply star_right. eexact G.
   left. eapply step_assignop; eauto.
-  rewrite B; eauto. rewrite B; rewrite F; eauto. congruence. rewrite B; eauto. congruence.
+  rewrite B; eauto. rewrite B; rewrite F; eauto. rewrite B; eauto. rewrite B; eauto. congruence.
   reflexivity. traceEq.
 (* postincr *)
   exploit (H0 (fun x => C(Epostincr id x ty))).
@@ -2656,7 +2660,7 @@ Proof (proj2 (proj2 (proj2 (proj2 bigstep_to_steps)))).
 
 Fixpoint esize (a: expr) : nat :=
   match a with
-  | Eloc _ _ _ => 1%nat
+  | Eloc _ _ _ _ => 1%nat
   | Evar _ _ => 1%nat
   | Ederef r1 _ => S(esize r1)
   | Efield l1 _ _ => S(esize l1)