Merge of the "volatile" branch:

- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 441 insertions, 184 deletions

diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 8b66ef9..e088c26 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -49,9 +49,9 @@ Fixpoint simple (a: expr) : Prop :=
   | Eloc _ _ _ => True
   | Evar _ _ => True
   | Ederef r _ => simple r
-  | Efield l1 _ _ => simple l1
+  | Efield r _ _ => simple r
   | Eval _ _ => True
-  | Evalof l _ => simple l
+  | Evalof l _ => simple l /\ type_is_volatile (typeof l) = false
   | Eaddrof l _ => simple l
   | Eunop _ r1 _ => simple r1
   | Ebinop _ r1 r2 _ => simple r1 /\ simple r2
@@ -93,22 +93,22 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
   | 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 l f ty b ofs id fList delta,
-      eval_simple_lvalue l b ofs ->
-      typeof l = Tstruct id fList -> field_offset f fList = OK delta ->
-      eval_simple_lvalue (Efield l f ty) b (Int.add ofs (Int.repr delta))
-  | esl_field_union: forall l f ty b ofs id fList,
-      eval_simple_lvalue l b ofs ->
-      typeof l = Tunion id fList ->
-      eval_simple_lvalue (Efield l f ty) b ofs
+  | esl_field_struct: forall r f ty b ofs id fList a delta,
+      eval_simple_rvalue r (Vptr b ofs) ->
+      typeof r = Tstruct id fList a -> field_offset f fList = OK delta ->
+      eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
+  | esl_field_union: forall r f ty b ofs id fList a,
+      eval_simple_rvalue r (Vptr b ofs) ->
+      typeof r = Tunion id fList a ->
+      eval_simple_lvalue (Efield r f ty) b ofs
 
 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 ->
-      ty = typeof l ->
-      load_value_of_type ty m b ofs = Some v ->
+      ty = typeof l -> type_is_volatile ty = false ->
+      deref_loc ge ty m b ofs E0 v ->
       eval_simple_rvalue (Evalof l ty) v
   | esr_addrof: forall b ofs l ty,
       eval_simple_lvalue l b ofs ->
@@ -151,7 +151,7 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop :=
   | lctx_deref: forall k C ty,
       leftcontext k RV C -> leftcontext k LV (fun x => Ederef (C x) ty)
   | lctx_field: forall k C f ty,
-      leftcontext k LV C -> leftcontext k LV (fun x => Efield (C x) f ty)
+      leftcontext k RV C -> leftcontext k LV (fun x => Efield (C x) f ty)
   | lctx_rvalof: forall k C ty,
       leftcontext k LV C -> leftcontext k RV (fun x => Evalof (C x) ty)
   | lctx_addrof: forall k C ty,
@@ -222,6 +222,14 @@ 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,
+      leftcontext RV RV C ->
+      eval_simple_lvalue e m l b ofs ->
+      deref_loc ge ty m b ofs 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)
+
   | step_condition: forall f C r1 r2 r3 ty k e m v b,
       leftcontext RV RV C ->
       eval_simple_rvalue e m r1 v ->
@@ -229,38 +237,73 @@ 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)) k e m)
 
-  | step_assign: forall f C l r ty k e m b ofs v v' m',
+  | step_assign: forall f C l r ty k e m b ofs v v' t m',
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
       eval_simple_rvalue e m r v ->
       sem_cast v (typeof r) (typeof l) = Some v' ->
-      store_value_of_type (typeof l) m b ofs v' = Some m' ->
+      assign_loc ge (typeof l) m b ofs v' t m' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassign l r ty)) k e m)
-         E0 (ExprState f (C (Eval v' 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 m',
+  | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 t1 t2 m' t,
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
-      load_value_of_type (typeof l) m b ofs = Some v1 ->
+      deref_loc ge (typeof l) m b ofs t1 v1 ->
       eval_simple_rvalue e m r v2 ->
       sem_binary_operation op v1 (typeof l) v2 (typeof r) m = Some v3 ->
       sem_cast v3 tyres (typeof l) = Some v4 ->
-      store_value_of_type (typeof l) m b ofs v4 = Some m' ->
+      assign_loc ge (typeof l) m b ofs v4 t2 m' ->
       ty = typeof l ->
+      t = t1 ** t2 ->
       estep (ExprState f (C (Eassignop op l r tyres ty)) k e m)
-         E0 (ExprState f (C (Eval v4 ty)) k e m')
+          t (ExprState f (C (Eval v4 ty)) k e m')
 
-  | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 m',
+  | step_assignop_stuck: forall f C op l r tyres ty k e m b ofs v1 v2 t,
       leftcontext RV RV C ->
       eval_simple_lvalue e m l b ofs ->
-      load_value_of_type ty m b ofs = Some v1 ->
+      deref_loc ge (typeof l) m b ofs t v1 ->
+      eval_simple_rvalue e m r v2 ->
+      match sem_binary_operation op v1 (typeof l) v2 (typeof r) m with
+      | None => True
+      | Some v3 =>
+          match sem_cast v3 tyres (typeof l) with
+          | None => True
+          | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m')
+          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,
+      leftcontext RV RV C ->
+      eval_simple_lvalue e m l b ofs ->
+      deref_loc ge ty m b ofs t1 v1 ->
       sem_incrdecr id v1 ty = Some v2 ->
       sem_cast v2 (typeconv ty) ty = Some v3 ->
-      store_value_of_type ty m b ofs v3 = Some m' ->
+      assign_loc ge ty m b ofs v3 t2 m' ->
+      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,
+      leftcontext RV RV C ->
+      eval_simple_lvalue e m l b ofs ->
+      deref_loc ge ty m b ofs t v1 ->
+      match sem_incrdecr id v1 ty with
+      | None => True
+      | Some v2 =>
+          match sem_cast v2 (typeconv ty) ty with
+          | None => True
+          | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m')
+          end
+      end ->
       ty = typeof l ->
       estep (ExprState f (C (Epostincr id l ty)) k e m)
-         E0 (ExprState f (C (Eval v1 ty)) k e m')
+          t Stuckstate
 
   | step_comma: forall f C r1 r2 ty k e m v,
       leftcontext RV RV C ->
@@ -326,53 +369,37 @@ Proof.
 Qed.
 
 Lemma star_safe:
-  forall s1 s2 s3,
-  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 E0 s3) ->
-  star Csem.step ge s1 E0 s3.
+  forall s1 s2 t s3,
+  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 t s3) ->
+  star Csem.step ge s1 t s3.
 Proof.
   intros. eapply star_trans; eauto. apply H1. eapply safe_steps; eauto. auto.
 Qed.
 
 Lemma plus_safe:
-  forall s1 s2 s3,
-  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 E0 s3) ->
-  plus Csem.step ge s1 E0 s3.
+  forall s1 s2 t s3,
+  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 t s3) ->
+  plus Csem.step ge s1 t s3.
 Proof.
   intros. eapply star_plus_trans; eauto. apply H1. eapply safe_steps; eauto. auto.
 Qed.
 
-Remark not_stuck_val:
-  forall e v ty m,
-  not_stuck ge e (Eval v ty) m.
-Proof.
-  intros; red; intros. inv H; try congruence. subst e'. constructor.
-Qed.
-
-Lemma safe_not_stuck:
-  forall f a k e m,
-  safe (ExprState f a k e m) ->
-  not_stuck ge e a m.
-Proof.
-  intros. exploit H. apply star_refl. intros [[r FIN] | [t [s' STEP]]].
-  inv FIN.
-  inv STEP. 
-    inv H0; auto; apply not_stuck_val.
-    inv H0; apply not_stuck_val.
-Qed.
-
-Hint Resolve safe_not_stuck.
+Require Import Classical. 
 
-Lemma safe_not_imm_stuck:
-  forall k C f a K e m,
-  safe (ExprState f (C a) K e m) ->
-  context k RV C ->
-  not_imm_stuck ge e k a m.
+Lemma safe_imm_safe:
+  forall f C a k e m K,
+  safe (ExprState f (C a) k e m) ->
+  context K RV C ->
+  imm_safe ge e K a m.
 Proof.
-  intros. exploit safe_not_stuck; eauto.
+  intros. destruct (classic (imm_safe ge e K a m)); auto.
+  destruct (H Stuckstate). 
+  apply star_one. left. econstructor; eauto.
+  destruct H2 as [r F]. inv F. 
+  destruct H2 as [t [s' S]]. inv S. inv H2. inv H2. 
 Qed.
 
-(** Simple, non-stuck expressions are well-formed with respect to
-    l-values and r-values. *)
+(** Safe expressions are well-formed with respect to l-values and r-values. *)
 
 Definition expr_kind (a: expr) : kind :=
   match a with
@@ -390,7 +417,7 @@ Proof.
 Qed.
 
 Lemma rred_kind:
-  forall a m a' m', rred a m a' m' -> expr_kind a = RV.
+  forall a m t a' m', rred ge a m t a' m' -> expr_kind a = RV.
 Proof.
   induction 1; auto.
 Qed.
@@ -407,8 +434,8 @@ Proof.
   induction 1; intros; simpl; auto.
 Qed.
 
-Lemma not_imm_stuck_kind:
-  forall e k a m, not_imm_stuck ge e k a m -> expr_kind a = k.
+Lemma imm_safe_kind:
+  forall e k a m, imm_safe ge e k a m -> expr_kind a = k.
 Proof.
   induction 1.
   auto.
@@ -424,10 +451,10 @@ Lemma safe_expr_kind:
   safe (ExprState f (C a) k e m) ->
   expr_kind a = from.
 Proof.
-  intros. eapply not_imm_stuck_kind. eapply safe_not_imm_stuck; eauto.
+  intros. eapply imm_safe_kind. eapply safe_imm_safe; eauto.
 Qed.
 
-(** Painful inversion lemmas on particular states that are not stuck. *)
+(** Painful inversion lemmas on particular states that are safe. *)
 
 Section INVERSION_LEMMAS.
 
@@ -449,15 +476,16 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
       \/ (e!x = None /\ Genv.find_symbol ge x = Some b /\ type_of_global ge b = Some ty)
   | Ederef (Eval v ty1) ty =>
       exists b, exists ofs, v = Vptr b ofs
-  | Efield (Eloc b ofs ty1) f ty =>
+  | Efield (Eval v ty1) f ty =>
+      exists b, exists ofs, v = Vptr b ofs /\
       match ty1 with
-      | Tstruct _ fList => exists delta, field_offset f fList = Errors.OK delta
-      | Tunion _ _ => True
+      | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta
+      | Tunion _ _ _ => True
       | _ => False
       end
   | Eval v ty => False
   | Evalof (Eloc b ofs ty') ty =>
-      ty' = ty /\ exists v, load_value_of_type ty m b ofs = Some v
+      ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v
   | Eunop op (Eval v1 ty1) ty =>
       exists v, sem_unary_operation op v1 ty1 = Some v
   | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
@@ -467,22 +495,16 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Econdition (Eval v1 ty1) r1 r2 ty =>
       exists b, bool_val v1 ty1 = Some b
   | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
-      exists v, exists m',
-      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ store_value_of_type ty1 m b ofs v = Some m'
+      exists v, exists m', exists t,
+      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m'
   | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
-      exists v1, exists v, exists v', exists m',
-      ty = ty1 
-      /\ load_value_of_type ty1 m b ofs = Some v1
-      /\ sem_binary_operation op v1 ty1 v2 ty2 m = Some v
-      /\ sem_cast v tyres ty1 = Some v'
-      /\ store_value_of_type ty1 m b ofs v' = Some m'
+      exists t, exists v1,
+      ty = ty1
+      /\ deref_loc ge ty1 m b ofs t v1
   | Epostincr id (Eloc b ofs ty1) ty =>
-      exists v1, exists v2, exists v3, exists m',
+      exists t, exists v1,
       ty = ty1
-      /\ load_value_of_type ty m b ofs = Some v1
-      /\ sem_incrdecr id v1 ty = Some v2
-      /\ sem_cast v2 (typeconv ty) ty = Some v3
-      /\ store_value_of_type ty m b ofs v3 = Some m'
+      /\ deref_loc ge ty m b ofs t v1
   | Ecomma (Eval v ty1) r2 ty =>
       typeof r2 = ty
   | Eparen (Eval v1 ty1) ty =>
@@ -504,21 +526,22 @@ Proof.
   exists b; auto.
   exists b; auto.
   exists b; exists ofs; auto.
-  exists delta; auto.
+  exists b; exists ofs; split; auto. exists delta; auto.
+  exists b; exists ofs; auto.
 Qed.
 
 Lemma rred_invert:
-  forall r m r' m', rred r m r' m' -> invert_expr_prop r m.
+  forall r m t r' m', rred ge r m t r' m' -> invert_expr_prop r m.
 Proof.
   induction 1; red; auto.
-  split; auto; exists v; auto.
+  split; auto; exists t; exists v; auto.
   exists v; auto.
   exists v; auto.
   exists v; auto.
   exists b; auto.
-  exists v; exists m'; auto.
-  exists v1; exists v; exists v'; exists m'; auto.
-  exists v1; exists v2; exists v3; exists m'; auto.
+  exists v; exists m'; exists t; auto.
+  exists t; exists v1; auto.
+  exists t; exists v1; auto.
   exists v; auto.
 Qed.
 
@@ -569,9 +592,9 @@ Proof.
   red; intros. destruct e1; auto. elim (H0 a m); auto. 
 Qed.
 
-Lemma not_imm_stuck_inv:
+Lemma imm_safe_inv:
   forall k a m,
-  not_imm_stuck ge e k a m ->
+  imm_safe ge e k a m ->
   match a with
   | Eloc _ _ _ => True
   | Eval _ _ => True
@@ -603,7 +626,7 @@ Lemma safe_inv:
   | _ => invert_expr_prop a m
   end.
 Proof.
-  intros. eapply not_imm_stuck_inv; eauto. eapply safe_not_imm_stuck; eauto.
+  intros. eapply imm_safe_inv; eauto. eapply safe_imm_safe; eauto.
 Qed.
 
 End INVERSION_LEMMAS.
@@ -619,16 +642,16 @@ Variable m: mem.
 
 Lemma eval_simple_steps:
    (forall a v, eval_simple_rvalue e m a v ->
-    forall C, context RV RV C -> safe (ExprState f (C a) k e m) ->
+    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 C, context LV RV C -> safe (ExprState f (C a) k e m) ->
+    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)).
 Proof.
 
-Ltac Steps REC C' := eapply star_safe; eauto; [apply (REC C'); eauto | intros].
+Ltac Steps REC C' := eapply star_trans; [apply (REC C'); eauto | idtac | simpl; reflexivity].
 Ltac FinishR := apply star_one; left; apply step_rred; eauto; simpl; try (econstructor; eauto; fail).
 Ltac FinishL := apply star_one; left; apply step_lred; eauto; simpl; try (econstructor; eauto; fail).
 
@@ -665,14 +688,14 @@ Qed.
 
 Lemma eval_simple_rvalue_steps:
   forall a v, eval_simple_rvalue e m a v ->
-  forall C, context RV RV C -> safe (ExprState f (C a) k e m) ->
+  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).
 Proof (proj1 eval_simple_steps).
 
 Lemma eval_simple_lvalue_steps:
   forall a b ofs, eval_simple_lvalue e m a b ofs ->
-  forall C, context LV RV C -> safe (ExprState f (C a) k e m) ->
+  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).
 Proof (proj2 eval_simple_steps).
@@ -727,14 +750,16 @@ Ltac StepR REC C' a :=
   exists b; exists Int.zero.
   intuition. apply esl_var_local; auto. apply esl_var_global; auto.
 (* field *)
-  StepL IHa (fun x => C(Efield x f0 ty)) a.
-  exploit safe_inv. eexact SAFE0. eauto. simpl. case_eq (typeof a); intros; try contradiction.
-  destruct H0 as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
+  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) as []_eqn; try contradiction.
+  destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto.
   exists b; exists ofs; econstructor; eauto.
 (* valof *)
-  StepL IHa (fun x => C(Evalof x ty)) a.
-  exploit safe_inv. eexact SAFE0. eauto. simpl. intros [TY [v LOAD]]. 
-  exists v; econstructor; eauto.
+  destruct S. 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 *)
   StepR IHa (fun x => C(Ederef x ty)) a.
   exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b [ofs EQ]].
@@ -875,7 +900,7 @@ Hint Resolve contextlist'_head contextlist'_tail.
 
 Lemma eval_simple_list_steps:
   forall rl vl, eval_simple_list' rl vl ->
-  forall C, contextlist' C -> safe (ExprState f (C rl) k e m) ->
+  forall C, contextlist' C ->
   star Csem.step ge (ExprState f (C rl) k e m)
                 E0 (ExprState f (C (rval_list vl rl)) k e m).
 Proof.
@@ -883,9 +908,10 @@ Proof.
 (* nil *)
   apply star_refl.
 (* cons *)
-  eapply star_safe. eauto. 
+  eapply star_trans.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Econs x rl)); eauto.
-  intros. apply IHeval_simple_list' with (C := fun x => C(Econs (Eval v (typeof r)) x)); auto.
+  apply IHeval_simple_list' with (C := fun x => C(Econs (Eval v (typeof r)) x)); auto.
+  auto.
 Qed.
 
 Lemma simple_list_can_eval:
@@ -926,7 +952,8 @@ Variable m: mem.
 
 Definition simple_side_effect (r: expr) : Prop :=
   match r with
-  | Econdition r1 r2 r3 ty => simple r1
+  | Evalof l _ => simple l /\ type_is_volatile (typeof l) = true
+  | Econdition r1 r2 r3 _ => simple r1
   | Eassign l1 r2 _ => simple l1 /\ simple r2
   | Eassignop _ l1 r2 _ _ => simple l1 /\ simple r2
   | Epostincr _ l1 _ => simple l1
@@ -964,9 +991,11 @@ Ltac Base :=
   right; exists (fun x => x); econstructor; split; [eauto | simpl; auto].
 
 (* field *)
-  Kind. Rec H LV C (fun x => Efield x f0 ty).
+  Kind. Rec H RV C (fun x => Efield x f0 ty).
 (* rvalof *)
   Kind. Rec H LV C (fun x => Evalof x ty).
+  destruct (type_is_volatile (typeof l)) as []_eqn.
+  Base. auto.
 (* deref *)
   Kind. Rec H RV C (fun x => Ederef x ty).
 (* addrof *)
@@ -1020,95 +1049,185 @@ End DECOMPOSITION.
 
 Lemma estep_simulation:
   forall S t S',
-  estep S t S' -> safe S -> plus Csem.step ge S t S'.
+  estep S t S' -> plus Csem.step ge S t S'.
 Proof.
   intros. inv H. 
 (* simple *)
   exploit eval_simple_rvalue_steps; eauto. simpl; intros STEPS.
-  exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; auto. 
-  inversion EQ1. rewrite <- H3 in H2; contradiction.
+  exploit star_inv; eauto. intros [[EQ1 EQ2] | A]; eauto. 
+  inversion EQ1. rewrite <- H2 in H1; contradiction.
+(* valof volatile *)
+  eapply plus_right. 
+  eapply eval_simple_lvalue_steps with (C := fun x => C(Evalof x (typeof l))); eauto.
+  left. apply step_rred; eauto. econstructor; eauto. auto.
 (* condition *)
-  eapply plus_safe; eauto.
+  eapply plus_right.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Econdition x r2 r3 ty)); eauto.
-  intros. apply plus_one. left; apply step_rred; eauto. constructor; auto. 
+  left; apply step_rred; eauto. constructor; auto. auto. 
 (* assign *)
-  eapply plus_safe; eauto.
+  eapply star_plus_trans.
   eapply eval_simple_lvalue_steps with (C := fun x => C(Eassign x r (typeof l))); eauto.
-  intros. eapply plus_safe; eauto.
+  eapply plus_right.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto.
-  intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto.
+  left; apply step_rred; eauto. econstructor; eauto.
+  reflexivity. auto. 
 (* assignop *) 
-  eapply plus_safe; eauto.
+  eapply star_plus_trans.
   eapply eval_simple_lvalue_steps with (C := fun x => C(Eassignop op x r tyres (typeof l))); eauto.
-  intros. eapply plus_safe; 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.
-  intros. apply plus_one; left; apply step_rred; eauto. econstructor; 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.  
+  apply star_one. 
+  left; apply step_rred; auto. econstructor; eauto. 
+  reflexivity. reflexivity. reflexivity. traceEq.
+(* assignop stuck *)
+  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 plus_left.
+  left; apply step_rred; auto. econstructor; eauto.
+  destruct (sem_binary_operation 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.  
+  apply star_one. 
+  left; eapply step_stuck; eauto.
+  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v4' [m' [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.
+  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v3 A]. congruence.
+  reflexivity.
+  reflexivity. traceEq.
 (* postincr *)
-  eapply plus_safe; eauto.
+  eapply star_plus_trans.
+  eapply eval_simple_lvalue_steps with (C := fun x => C(Epostincr id x (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 (Ecomma (Eassign (Eloc b ofs (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.
+  econstructor; eauto.
+  apply star_one.
+  left; apply step_rred; auto. econstructor; eauto. 
+  reflexivity. reflexivity. reflexivity. traceEq.
+(* postincr stuck *)
+  eapply star_plus_trans.
   eapply eval_simple_lvalue_steps with (C := fun x => C(Epostincr id x (typeof l))); eauto.
-  intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto.
+  eapply plus_left.
+  left; apply step_rred; auto. econstructor; eauto.
+  set (op := match id with Incr => Oadd | Decr => Osub end).
+  assert (SEM: sem_binary_operation op v1 (typeof l) (Vint Int.one) type_int32s m =
+              sem_incrdecr id v1 (typeof l)).
+    destruct id; auto.
+  destruct (sem_incrdecr id v1 (typeof l)) 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.
+  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]]]]].
+  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.
+  red; intros. exploit imm_safe_inv; eauto. simpl. intros [v2 A]. congruence.
+  reflexivity. 
+  traceEq.
 (* comma *)
-  eapply plus_safe; eauto.
+  eapply plus_right.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Ecomma x r2 (typeof r2))); eauto.
-  intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto.
+  left; apply step_rred; eauto. econstructor; eauto. auto.
 (* paren *)
-  eapply plus_safe; eauto.
+  eapply plus_right; eauto.
   eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x ty)); eauto.
-  intros. apply plus_one; left; apply step_rred; eauto. econstructor; eauto.
+  left; apply step_rred; eauto. econstructor; eauto. auto.
 (* call *)
   exploit eval_simple_list_implies; eauto. intros [vl' [A B]].
-  eapply plus_safe; eauto.
+  eapply star_plus_trans. 
   eapply eval_simple_rvalue_steps with (C := fun x => C(Ecall x rargs ty)); eauto.
-  intros. eapply plus_safe; eauto. 
+  eapply plus_right.
   eapply eval_simple_list_steps with (C := fun x => C(Ecall (Eval vf (typeof rf)) x ty)); eauto.
   eapply contextlist'_intro with (rl0 := Enil); auto.
-  intros. apply plus_one; left; apply Csem.step_call; eauto.
-  econstructor; eauto.
+  left; apply Csem.step_call; eauto. econstructor; eauto.
+  traceEq. auto.
 Qed.
 
 Lemma can_estep:
   forall f a k e m,
   safe (ExprState f a k e m) ->
   match a with Eval _ _ => False | _ => True end ->
-  exists S, estep (ExprState f a k e m) E0 S.
+  exists t, exists S, estep (ExprState f a k e m) t S.
 Proof.
   intros. destruct (decompose_topexpr f k e m a H) as [A | [C [b [P [Q R]]]]].
 (* simple expr *)
   exploit (simple_can_eval f k e m a RV (fun x => x)); auto. intros [v P].
-  econstructor; eapply step_expr; eauto. 
+  econstructor; econstructor; eapply step_expr; eauto. 
 (* side effect *)
   clear H0. subst a. red in Q. destruct b; try contradiction. 
+(* 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]]].
+  exploit safe_inv. eexact S1. eauto. simpl. intros [A [t [v B]]].
+  econstructor; econstructor; eapply step_rvalof_volatile; eauto. congruence. 
 (* condition *)
   exploit (simple_can_eval_rval f k e m b1 (fun x => C(Econdition x b2 b3 ty))); eauto.
   intros [v1 [E1 S1]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [b BV].
-  econstructor. eapply step_condition; eauto. 
+  econstructor; econstructor. eapply step_condition; eauto. 
 (* 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 [v [E2 S2]].
-  exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [A [B D]]]].
-  econstructor; eapply step_assign; eauto. 
+  exploit safe_inv. eexact S2. eauto. simpl. intros [v' [m' [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 [v [E2 S2]].
-  exploit safe_inv. eexact S2. eauto. simpl. intros [v1 [v2 [v3 [m' [A [B [D [E F]]]]]]]].
-  econstructor; eapply step_assignop; eauto.
+  exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]].
+  destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|]_eqn.
+  destruct (sem_cast v3 tyres (typeof b1)) 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]].
+  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.
+  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]]].
-  exploit safe_inv. eexact S1. eauto. simpl. intros [v1 [v2 [v3 [m' [A [B [D [E F]]]]]]]].
-  econstructor; eapply step_postincr; eauto.
+  exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]].
+  destruct (sem_incrdecr id v1 ty) as [v2|]_eqn.
+  destruct (sem_cast v2 (typeconv ty) ty) 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]].
+  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.
+  econstructor; econstructor; eapply step_postincr_stuck; eauto. 
+  rewrite Heqo. rewrite Heqo0. auto.
+  econstructor; econstructor; eapply step_postincr_stuck; eauto. 
+  rewrite Heqo. auto.
 (* comma *)
   exploit (simple_can_eval_rval f k e m b1 (fun x => C(Ecomma x b2 ty))); eauto.
   intros [v1 [E1 S1]].
   exploit safe_inv. eexact S1. eauto. simpl. intros EQ.
-  econstructor; eapply step_comma; eauto.
+  econstructor; econstructor; eapply step_comma; eauto.
 (* call *)
   destruct Q.
   exploit (simple_can_eval_rval f k e m b (fun x => C(Ecall x rargs ty))); eauto.
@@ -1122,19 +1241,19 @@ Proof.
   apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto.
   simpl. intros X. exploit X. eapply rval_list_all_values. 
   intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]].
-  econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. 
+  econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. 
 (* paren *)
   exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto.
   intros [v1 [E1 S1]].
   exploit safe_inv. eexact S1. eauto. simpl. intros [v CAST].
-  econstructor; eapply step_paren; eauto.
+  econstructor; econstructor; eapply step_paren; eauto.
 Qed.
 
 (** Simulation for all states *)
 
 Theorem step_simulation:
   forall S1 t S2,
-  step S1 t S2 -> safe S1 -> plus Csem.step ge S1 t S2.
+  step S1 t S2 -> plus Csem.step ge S1 t S2.
 Proof.
   intros. inv H.
   apply estep_simulation; auto.
@@ -1150,16 +1269,19 @@ Proof.
   auto.
   right. destruct STEP.
   (* 2. Expression step. *)
-  assert (exists S', estep S E0 S').
+  assert (exists t, exists S', estep S t S').
     inv H0.
     (* lred *)
-    eapply can_estep; eauto. inv H3; auto. 
+    eapply can_estep; eauto. inv H2; auto. 
     (* rred *)
-    eapply can_estep; eauto. inv H3; auto. inv H1; auto. 
+    eapply can_estep; eauto. inv H2; auto. inv H1; auto. 
     (* callred *)
-    eapply can_estep; eauto. inv H3; auto. inv H1; auto.
-  destruct H1 as [S'' ESTEP].
-  exists E0; exists S''; left; auto.
+    eapply can_estep; eauto. inv H2; auto. inv H1; auto.
+    (* stuck *)
+    exploit (H Stuckstate). apply star_one. left. econstructor; eauto.
+    intros [[r F] | [t [S' R]]]. inv F. inv R. inv H0. inv H0.
+  destruct H1 as [t' [S'' ESTEP]].
+  exists t'; exists S''; left; auto.
   (* 3. Other step. *)
   exists t; exists S'; right; auto.
 Qed.
@@ -1173,22 +1295,145 @@ Definition semantics (p: program) :=
 
 (** This semantics is receptive to changes in events. *)
 
-Lemma semantics_receptive: 
-  forall p, receptive (semantics p).
+Remark deref_loc_trace:
+  forall F V (ge: Genv.t F V) ty m b ofs t v,
+  deref_loc ge ty m b ofs 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 F V (ge: Genv.t F V) ty m b ofs ev1 t1 v ev2,
+  deref_loc ge ty m b ofs (ev1 :: t1) v ->
+  match_traces ge (ev1 :: nil) (ev2 :: nil) ->
+  t1 = nil /\ exists v', deref_loc ge ty m b ofs (ev2 :: nil) v'.
+Proof.
+  intros.
+  assert (t1 = nil). exploit deref_loc_trace; eauto. destruct t1; simpl; tauto.
+  inv H. exploit volatile_load_receptive; eauto. intros [v' A]. 
+  split; auto; exists v'; econstructor; eauto.
+Qed.
+
+Remark assign_loc_trace:
+  forall F V (ge: Genv.t F V) ty m b ofs t v m',
+  assign_loc ge ty m b ofs v t m' ->
+  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 F V (ge: Genv.t F V) ty m b ofs ev1 t1 v m' ev2,
+  assign_loc ge ty m b ofs v (ev1 :: t1) m' ->
+  match_traces ge (ev1 :: nil) (ev2 :: nil) ->
+  ev1 :: t1 = ev2 :: nil.
+Proof.
+  intros.
+  assert (t1 = nil). exploit assign_loc_trace; eauto. destruct t1; simpl; tauto.
+  inv H. eapply volatile_store_receptive; eauto. 
+Qed.
+
+Lemma semantics_strongly_receptive: 
+  forall p, strongly_receptive (semantics p).
 Proof.
   intros. constructor; simpl; intros.
 (* receptiveness *)
-  assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2).
-    intros. subst. inv H0. exists s1; auto.
   inversion H; subst.
-  inv H2; auto.
-  inv H2; auto. 
+  inv H1.
+  (* valof volatile *)
+  exploit deref_loc_receptive; eauto. intros [A [v' B]]. 
+  econstructor; econstructor. left; eapply step_rvalof_volatile; eauto. 
+  (* assign *)
+  exploit assign_loc_receptive; eauto. intro EQ; rewrite EQ in H.
+  econstructor; econstructor; eauto.
+  (* assignop *)
+  destruct t0 as [ | ev0 t0]; simpl in H10. 
+  subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
+  econstructor; econstructor; eauto.
+  inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
+  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn.
+  destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn.
+  destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')).
+  destruct H1 as [t2' [m'' 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.
+  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. 
+  rewrite Heqo; auto.
+  (* assignop stuck *)
+  exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
+  destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|]_eqn.
+  destruct (sem_cast v3' tyres (typeof l)) as [v4'|]_eqn.
+  destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')).
+  destruct H1 as [t2' [m'' 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.
+  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. 
+  rewrite Heqo; auto.
+  (* postincr *)
+  destruct t0 as [ | ev0 t0]; simpl in H9. 
+  subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H.
+  econstructor; econstructor; eauto.
+  inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0.
+  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn.
+  destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn.
+  destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')).
+  destruct H1 as [t2' [m'' 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.
+  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. 
+  rewrite Heqo; auto.
+  (* postincr stuck *)
+  exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1.
+  destruct (sem_incrdecr id v1' (typeof l)) as [v2'|]_eqn.
+  destruct (sem_cast v2' (typeconv (typeof l)) (typeof l)) as [v3'|]_eqn.
+  destruct (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')).
+  destruct H1 as [t2' [m'' 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.
+  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. 
+  rewrite Heqo; auto.
+  (* external calls *)
+  inv H1.
+  exploit external_call_trace_length; eauto. destruct t1; simpl; intros. 
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
-  exists (Returnstate vres2 k m2). right; econstructor; eauto.
-(* trace length *)
-  inv H. 
-  inv H0; simpl; omega.
-  inv H0; simpl; try omega. eapply external_call_trace_length; eauto.
+  exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto.
+  omegaContradiction.
+(* well-behaved traces *)
+  red; intros. inv H; inv H0; simpl; auto.
+  (* valof volatile *)
+  exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
+  (* assign *)
+  exploit assign_loc_trace; eauto. destruct t; auto. destruct t; simpl; tauto.
+  (* assignop *)
+  exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto.
+  destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. 
+  destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. 
+  tauto.
+  (* assignop stuck *)
+  exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
+  (* postincr *)
+  exploit deref_loc_trace; eauto. exploit assign_loc_trace; eauto.
+  destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. 
+  destruct t1. destruct t2. simpl; auto. destruct t2; simpl; tauto. 
+  tauto.
+  (* postincr stuck *)
+  exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
+  (* external calls *)
+  exploit external_call_trace_length; eauto.
+  destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
 Qed.
 
 (** The main simulation result. *)
@@ -1200,8 +1445,6 @@ Proof.
   apply backward_simulation_plus with (match_states := fun (S1 S2: state) => S1 = S2); simpl.
 (* symbols *)
   auto.
-(* trace length *)
-  intros. eapply sr_traces. apply semantics_receptive. simpl. eauto.
 (* initial states exist *)
   intros. exists s1; auto.
 (* initial states match *)
@@ -1269,11 +1512,19 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
   | eval_var: forall e m x ty,
       eval_expr e m LV (Evar x ty) E0 m (Evar x ty)
   | eval_field: forall e m a t m' a' f ty,
-      eval_expr e m LV a t m' a' ->
+      eval_expr e m RV a t m' a' ->
       eval_expr e m LV (Efield a f ty) t m' (Efield a' f ty)
   | eval_valof: forall e m a t m' a' ty,
+      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,
+      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 ->
+      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,
       eval_expr e m RV a t m' a' ->
       eval_expr e m LV (Ederef a ty) t m' (Ederef a' ty)
@@ -1297,34 +1548,34 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty)
   | eval_sizeof: forall e m ty' ty,
       eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty)
-  | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v v' m3,
+  | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v 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_rvalue ge e m2 r' v ->
       sem_cast v (typeof r) (typeof l) = Some v' ->
-      store_value_of_type (typeof l) m2 b ofs v' = Some m3 ->
+      assign_loc ge (typeof l) m2 b ofs v' t3 m3 ->
       ty = typeof l ->
-      eval_expr e m RV (Eassign l r ty) (t1**t2) m3 (Eval v' ty)
+      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 m3,
+                          v1 v2 v3 v4 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 ->
-      load_value_of_type (typeof l) m2 b ofs = Some v1 ->
+      deref_loc ge (typeof l) m2 b ofs t3 v1 ->
       eval_simple_rvalue ge e m2 r' v2 ->
       sem_binary_operation op v1 (typeof l) v2 (typeof r) m2 = Some v3 ->
       sem_cast v3 tyres (typeof l) = Some v4 ->
-      store_value_of_type (typeof l) m2 b ofs v4 = Some m3 ->
+      assign_loc ge (typeof l) m2 b ofs v4 t4 m3 ->
       ty = typeof l ->
-      eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2) m3 (Eval v4 ty)
-  | eval_postincr: forall e m id l ty t m1 l' b ofs v1 v2 v3 m2,
-      eval_expr e m LV l t m1 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 LV l t1 m1 l' ->
       eval_simple_lvalue ge e m1 l' b ofs ->
-      load_value_of_type ty m1 b ofs = Some v1 ->
+      deref_loc ge ty m1 b ofs t2 v1 ->
       sem_incrdecr id v1 ty = Some v2 ->
       sem_cast v2 (typeconv ty) ty = Some v3 ->
-      store_value_of_type ty m1 b ofs v3 = Some m2 ->
+      assign_loc ge ty m1 b ofs v3 t3 m2 ->
       ty = typeof l ->
-      eval_expr e m RV (Epostincr id l ty) t m2 (Eval v1 ty)
+      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',
       eval_expr e m RV r1 t1 m1 r1' ->
       eval_simple_rvalue ge e m1 r1' v1 ->
@@ -1472,7 +1723,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
   | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4,
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       exec_stmt e m2 f.(fn_body) t m3 out ->
       outcome_result_value out f.(fn_return) vres ->
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
@@ -1497,7 +1748,7 @@ Combined Scheme bigstep_induction from
 
 CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop :=
   | evalinf_field: forall e m a t f ty,
-      evalinf_expr e m LV a t ->
+      evalinf_expr e m RV a t ->
       evalinf_expr e m LV (Efield a f ty) t
   | evalinf_valof: forall e m a t ty,
       evalinf_expr e m LV a t ->
@@ -1677,7 +1928,7 @@ with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
   | evalinf_funcall_internal: forall m f vargs t e m1 m2,
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
       execinf_stmt e m2 f.(fn_body) t ->
       evalinf_funcall m (Internal f) vargs t.
 
@@ -1780,9 +2031,16 @@ Proof.
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
   simpl; intuition; eauto. 
 (* valof *)
-  exploit (H0 (fun x => C(Evalof x ty))).
+  exploit (H1 (fun x => C(Evalof x ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
-  simpl; intuition; eauto. 
+  simpl; intuition; eauto. congruence.
+(* valof volatile *)
+  exploit (H1 (fun x => C(Evalof x ty))).
+    eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
+  simpl; intuition.
+  eapply star_right. eexact D. 
+  left. eapply step_rvalof_volatile; eauto. rewrite H4; eauto. congruence. congruence. 
+  traceEq.
 (* deref *)
   exploit (H0 (fun x => C(Ederef x ty))).
     eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]].
@@ -1825,7 +2083,7 @@ Proof.
   simpl; intuition.
   eapply star_trans. eexact D. 
   eapply star_right. eexact G.
-  left. eapply step_assign; eauto. congruence. congruence. congruence. 
+  left. eapply step_assign; eauto. congruence. rewrite B; eauto. congruence.
   reflexivity. traceEq.
 (* assignop *)
   exploit (H0 (fun x => C(Eassignop op x r tyres ty))).
@@ -1836,7 +2094,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. congruence. congruence.
+  rewrite B; eauto. rewrite B; rewrite F; eauto. congruence. rewrite B; eauto. congruence.
   reflexivity. traceEq.
 (* postincr *)
   exploit (H0 (fun x => C(Epostincr id x ty))).
@@ -2113,16 +2371,15 @@ Proof.
   (* Out_normal *)
   assert (fn_return f = Tvoid /\ vres = Vundef).
     destruct (fn_return f); auto || contradiction.
-  destruct H7. subst vres. right; apply step_skip_call; auto.
+  destruct H7 as [P Q]. subst vres. right; eapply step_skip_call; eauto.
   (* Out_return None *)
   assert (fn_return f = Tvoid /\ vres = Vundef).
     destruct (fn_return f); auto || contradiction.
-  destruct H8. subst vres.
+  destruct H8 as [P Q]. subst vres.
   rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7.
   right; apply step_return_0; auto.
   (* Out_return Some *)
-  destruct H4.
-  rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7.
+  destruct H4. rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7.
   right; eapply step_return_2; eauto.
   reflexivity. traceEq.
 
@@ -2510,7 +2767,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil (Tint I32 Signed) ->
+      type_of_fundef f = Tfunction Tnil type_int32s ->
       eval_funcall ge m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
@@ -2520,7 +2777,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       Genv.init_mem p = Some m0 ->
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil (Tint I32 Signed) ->
+      type_of_fundef f = Tfunction Tnil type_int32s ->
       evalinf_funcall ge m0 f nil t ->
       bigstep_program_diverges p t.