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, 1188 insertions, 969 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 4bce535..b3c3f6b 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -13,6 +13,7 @@
 (** Animating the CompCert C semantics *)
 
 Require Import Axioms.
+Require Import Classical.
 Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
@@ -28,28 +29,20 @@ Require Import Csyntax.
 Require Import Csem.
 Require Cstrategy.
 
-Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
-with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}
-with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}.
-Proof.
-  assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality.
-  assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality.
-  assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality.
-  generalize ident_eq zeq. intros E1 E2. 
-  decide equality.
-  decide equality.
-  generalize ident_eq. intros E1.
-  decide equality.
-Defined.
-
-Opaque type_eq.
-
 (** Error monad with options or lists *)
 
 Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
   (at level 200, X ident, A at level 100, B at level 200)
   : option_monad_scope.
 
+Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => None end)
+  (at level 200, X ident, Y ident, A at level 100, B at level 200)
+  : option_monad_scope.
+
+Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => None end)
+  (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
+  : option_monad_scope.
+
 Notation " 'check' A ; B" := (if A then B else None)
   (at level 200, A at level 100, B at level 200)
   : option_monad_scope.
@@ -99,20 +92,558 @@ Proof.
   destruct s; (left; congruence) || (right; congruence).
 Qed.
 
-(** * Reduction of expressions *)
+(** * Events, volatile memory accesses, and external functions. *)
 
 Section EXEC.
 
 Variable ge: genv.
 
+Definition eventval_of_val (v: val) (t: typ) : option eventval :=
+  match v, t with
+  | Vint i, AST.Tint => Some (EVint i)
+  | Vfloat f, AST.Tfloat => Some (EVfloat f)
+  | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs)
+  | _, _ => None
+  end.
+
+Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) :=
+  match vl, tl with
+  | nil, nil => Some nil
+  | v1::vl, t1::tl =>
+      do ev1 <- eventval_of_val v1 t1;
+      do evl <- list_eventval_of_val vl tl;
+      Some (ev1 :: evl)
+  | _, _ => None
+  end.
+
+Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
+  match ev, t with
+  | EVint i, AST.Tint => Some (Vint i)
+  | EVfloat f, AST.Tfloat => Some (Vfloat f)
+  | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs)
+  | _, _ => None
+  end.
+
+Lemma eventval_of_val_sound:
+  forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v.
+Proof.
+  intros. destruct v; destruct t; simpl in H; inv H.
+  constructor.
+  constructor.
+  destruct (Genv.invert_symbol ge b) as [id|]_eqn; inv H1. 
+  constructor. apply Genv.invert_find_symbol; auto.
+Qed.
+
+Lemma eventval_of_val_complete:
+  forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
+Proof.
+  induction 1; simpl; auto.
+  rewrite (Genv.find_invert_symbol _ _ H). auto. 
+Qed.
+
+Lemma list_eventval_of_val_sound:
+  forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match ge evl tl vl.
+Proof with try discriminate.
+  induction vl; destruct tl; simpl; intros; inv H.
+  constructor.
+  destruct (eventval_of_val a t) as [ev1|]_eqn...
+  destruct (list_eventval_of_val vl tl) as [evl'|]_eqn...
+  inv H1. constructor. apply eventval_of_val_sound; auto. eauto.
+Qed.
+
+Lemma list_eventval_of_val_complete:
+  forall evl tl vl, eventval_list_match ge evl tl vl -> list_eventval_of_val vl tl = Some evl.
+Proof.
+  induction 1; simpl. auto. 
+  rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto.
+Qed.
+
+Lemma val_of_eventval_sound:
+  forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v.
+Proof.
+  intros. destruct ev; destruct t; simpl in H; inv H.
+  constructor.
+  constructor.
+  destruct (Genv.find_symbol ge i) as [b|]_eqn; inv H1.
+  constructor. auto.
+Qed.
+
+Lemma val_of_eventval_complete:
+  forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.
+Proof.
+  induction 1; simpl; auto. rewrite H; auto.
+Qed.
+
+(** Volatile memory accesses. *)
+
+Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) 
+                             : option (world * trace * val) :=
+  if block_is_volatile ge b then
+    do id <- Genv.invert_symbol ge b;
+    match nextworld_vload w chunk id ofs with
+    | None => None
+    | Some(res, w') =>
+        do vres <- val_of_eventval res (type_of_chunk chunk);
+        Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres)
+    end
+  else
+    do v <- Mem.load chunk m b (Int.unsigned ofs);
+    Some(w, E0, v).
+
+Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block) (ofs: int) (v: val)
+                             : option (world * trace * mem) :=
+  if block_is_volatile ge b then
+    do id <- Genv.invert_symbol ge b;
+    do ev <- eventval_of_val v (type_of_chunk chunk);
+    do w' <- nextworld_vstore w chunk id ofs ev;
+    Some(w', Event_vstore chunk id ofs ev :: nil, m)
+  else
+    do m' <- Mem.store chunk m b (Int.unsigned ofs) v;
+    Some(w, E0, m').
+
+Ltac mydestr :=
+  match goal with
+  | [ |- None = Some _ -> _ ] => intro X; discriminate
+  | [ |- Some _ = Some _ -> _ ] => intro X; inv X
+  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
+  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
+  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
+  | _ => idtac
+  end.
+
+Lemma do_volatile_load_sound:
+  forall w chunk m b ofs w' t v,
+  do_volatile_load w chunk m b ofs = Some(w', t, v) ->
+  volatile_load ge chunk m b ofs t v /\ possible_trace w t w'.
+Proof.
+  intros until v. unfold do_volatile_load. mydestr. 
+  destruct p as [ev w'']. mydestr. 
+  split. constructor; auto. apply Genv.invert_find_symbol; auto. 
+  apply val_of_eventval_sound; auto. 
+  econstructor. constructor; eauto. constructor. 
+  split. constructor; auto. constructor.
+Qed.
+
+Lemma do_volatile_load_complete:
+  forall w chunk m b ofs w' t v,
+  volatile_load ge chunk m b ofs t v -> possible_trace w t w' ->
+  do_volatile_load w chunk m b ofs = Some(w', t, v).
+Proof.
+  unfold do_volatile_load; intros. inv H. 
+  rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2). inv H0. inv H8. inv H6. rewrite H9.
+  rewrite (val_of_eventval_complete _ _ _ H3). auto.
+  rewrite H1. rewrite H2. inv H0. auto.
+Qed.
+
+Lemma do_volatile_store_sound:
+  forall w chunk m b ofs v w' t m',
+  do_volatile_store w chunk m b ofs v = Some(w', t, m') ->
+  volatile_store ge chunk m b ofs v t m' /\ possible_trace w t w'.
+Proof.
+  intros until m'. unfold do_volatile_store. mydestr. 
+  split. constructor; auto. apply Genv.invert_find_symbol; auto. 
+  apply eventval_of_val_sound; auto. 
+  econstructor. constructor; eauto. constructor. 
+  split. constructor; auto. constructor.
+Qed.
+
+Lemma do_volatile_store_complete:
+  forall w chunk m b ofs v w' t m',
+  volatile_store ge chunk m b ofs v t m' -> possible_trace w t w' ->
+  do_volatile_store w chunk m b ofs v = Some(w', t, m').
+Proof.
+  unfold do_volatile_store; intros. inv H. 
+  rewrite H1. rewrite (Genv.find_invert_symbol _ _ H2).
+  rewrite (eventval_of_val_complete _ _ _ H3).
+  inv H0. inv H8. inv H6. rewrite H9. auto.
+  rewrite H1. rewrite H2. inv H0. auto.
+Qed.
+
+(** Accessing locations *)
+
+Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : option (world * trace * val) :=
+  match access_mode ty with
+  | By_value chunk =>
+      match type_is_volatile ty with
+      | false => do v <- Mem.loadv chunk m (Vptr b ofs); Some(w, E0, v)
+      | true => do_volatile_load w chunk m b ofs
+      end
+  | By_reference => Some(w, E0, Vptr b ofs)
+  | By_copy => Some(w, E0, Vptr b ofs)
+  | _ => None
+  end.
+
+Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop :=
+  (alignof ty | Int.unsigned ofs') /\ (alignof ty | Int.unsigned ofs) /\
+  (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
+           \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
+           \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs').
+
+Remark check_assign_copy:
+  forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int),
+  { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
+Proof with try (right; intuition omega).
+  intros. unfold assign_copy_ok. 
+  assert (alignof ty > 0). apply alignof_pos; auto.
+  destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs')); auto...
+  destruct (Zdivide_dec (alignof ty) (Int.unsigned ofs)); auto...
+  assert (Y: {b' <> b \/
+              Int.unsigned ofs' = Int.unsigned ofs \/
+              Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/
+              Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'} +
+           {~(b' <> b \/
+              Int.unsigned ofs' = Int.unsigned ofs \/
+              Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/
+              Int.unsigned ofs + sizeof ty <= Int.unsigned ofs')}).
+  destruct (eq_block b' b); auto.
+  destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto.
+  destruct (zle (Int.unsigned ofs' + sizeof ty) (Int.unsigned ofs)); auto.
+  destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto.
+  right; intuition omega.
+  destruct Y... left; intuition omega. 
+Qed.
+
+Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) :=
+  match access_mode ty with
+  | By_value chunk =>
+      match type_is_volatile ty with
+      | false => do m' <- Mem.storev chunk m (Vptr b ofs) v; Some(w, E0, m')
+      | true => do_volatile_store w chunk m b ofs v
+      end
+  | By_copy =>
+      match v with
+      | Vptr b' ofs' =>
+          if check_assign_copy ty b ofs b' ofs' then
+            do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty);
+            do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes;
+            Some(w, E0, m')
+          else None
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Lemma do_deref_loc_sound:
+  forall w ty m b ofs w' t v,
+  do_deref_loc w ty m b ofs = Some(w', t, v) ->
+  deref_loc ge ty m b ofs t v /\ possible_trace w t w'.
+Proof.
+  unfold do_deref_loc; intros until v.
+  destruct (access_mode ty) as []_eqn; mydestr. 
+  intros. exploit do_volatile_load_sound; eauto. intuition. eapply deref_loc_volatile; eauto. 
+  split. eapply deref_loc_value; eauto. constructor.
+  split. eapply deref_loc_reference; eauto. constructor.
+  split. eapply deref_loc_copy; eauto. constructor.
+Qed.
+
+Lemma do_deref_loc_complete:
+  forall w ty m b ofs w' t v,
+  deref_loc ge ty m b ofs t v -> possible_trace w t w' ->
+  do_deref_loc w ty m b ofs = Some(w', t, v).
+Proof.
+  unfold do_deref_loc; intros. inv H.
+  inv H0. rewrite H1; rewrite H2; rewrite H3; auto.
+  rewrite H1; rewrite H2. apply do_volatile_load_complete; auto.
+  inv H0. rewrite H1. auto.
+  inv H0. rewrite H1. auto.
+Qed.
+
+Lemma do_assign_loc_sound:
+  forall w ty m b ofs v w' t m',
+  do_assign_loc w ty m b ofs v = Some(w', t, m') ->
+  assign_loc ge ty m b ofs v t m' /\ possible_trace w t w'.
+Proof.
+  unfold do_assign_loc; intros until m'.
+  destruct (access_mode ty) as []_eqn; mydestr. 
+  intros. exploit do_volatile_store_sound; eauto. intuition. eapply assign_loc_volatile; eauto. 
+  split. eapply assign_loc_value; eauto. constructor.
+  destruct v; mydestr. destruct a as [P [Q R]]. 
+  split. eapply assign_loc_copy; eauto. constructor.
+Qed.
+
+Lemma do_assign_loc_complete:
+  forall w ty m b ofs v w' t m',
+  assign_loc ge ty m b ofs v t m' -> possible_trace w t w' ->
+  do_assign_loc w ty m b ofs v = Some(w', t, m').
+Proof.
+  unfold do_assign_loc; intros. inv H.
+  inv H0. rewrite H1; rewrite H2; rewrite H3; auto.
+  rewrite H1; rewrite H2. apply do_volatile_store_complete; auto.
+  rewrite H1. destruct (check_assign_copy ty b ofs b' ofs').
+  inv H0. rewrite H5; rewrite H6; auto.
+  elim n. red; tauto. 
+Qed.
+
+(** System calls and library functions *)
+
+Definition do_ef_external (name: ident) (sg: signature)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  do args <- list_eventval_of_val vargs (sig_args sg);
+  match nextworld_io w name args with
+  | None => None
+  | Some(res, w') =>
+      do vres <- val_of_eventval res (proj_sig_res sg);
+      Some(w', Event_syscall name args res :: E0, vres, m)
+  end.
+
+Definition do_ef_volatile_load (chunk: memory_chunk)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr b ofs :: nil => do w',t,v <- do_volatile_load w chunk m b ofs; Some(w',t,v,m)
+  | _ => None
+  end.
+
+Definition do_ef_volatile_store (chunk: memory_chunk)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr b ofs :: v :: nil => do w',t,m' <- do_volatile_store w chunk m b ofs v; Some(w',t,Vundef,m')
+  | _ => None
+  end.
+
+Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  do b <- Genv.find_symbol ge id; do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m.
+
+Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  do b <- Genv.find_symbol ge id; do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m.
+
+Definition do_ef_malloc
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vint n :: nil =>
+      let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in
+      do m'' <- Mem.store Mint32 m' b (-4) (Vint n);
+      Some(w, E0, Vptr b Int.zero, m'')
+  | _ => None
+  end.
+
+Definition do_ef_free
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr b lo :: nil =>
+      do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4);
+      match vsz with
+      | Vint sz =>
+          check (zlt 0 (Int.unsigned sz));
+          do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz);
+          Some(w, E0, Vundef, m')
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Definition memcpy_args_ok
+  (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
+      (al = 1 \/ al = 2 \/ al = 4)
+   /\ sz > 0
+   /\ (al | sz) /\ (al | osrc) /\ (al | odst)
+   /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).
+
+Remark memcpy_check_args:
+  forall sz al bdst odst bsrc osrc,
+  {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.
+Proof with try (right; intuition omega).
+  intros. 
+  assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}).
+    destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto...
+  unfold memcpy_args_ok. destruct X...
+  assert (al > 0) by (intuition omega).
+  destruct (zlt 0 sz)...
+  destruct (Zdivide_dec al sz); auto...
+  destruct (Zdivide_dec al osrc); auto...
+  destruct (Zdivide_dec al odst); auto...
+  assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc}
+           +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}).
+    destruct (eq_block bsrc bdst); auto.
+    destruct (zeq osrc odst); auto.
+    destruct (zle (osrc + sz) odst); auto.
+    destruct (zle (odst + sz) osrc); auto.
+    right; intuition omega.
+  destruct Y... left; intuition omega.
+Qed.
+
+Definition do_ef_memcpy (sz al: Z)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr bdst odst :: Vptr bsrc osrc :: nil =>
+      if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then
+        do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz;
+        do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes;
+        Some(w, E0, Vundef, m')
+      else None
+  | _ => None
+  end.
+
+Definition do_ef_annot (text: ident) (targs: list typ)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  do args <- list_eventval_of_val vargs targs;
+  Some(w, Event_annot text args :: E0, Vundef, m).
+
+Definition do_ef_annot_val (text: ident) (targ: typ)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | varg :: nil =>
+      do arg <- eventval_of_val varg targ;
+      Some(w, Event_annot text (arg :: nil) :: E0, varg, m)
+  | _ => None
+  end.
+
+Definition do_external (ef: external_function):
+       world -> list val -> mem -> option (world * trace * val * mem) :=
+  match ef with
+  | EF_external name sg => do_ef_external name sg
+  | EF_builtin name sg => do_ef_external name sg
+  | EF_vload chunk => do_ef_volatile_load chunk
+  | EF_vstore chunk => do_ef_volatile_store chunk
+  | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs
+  | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs
+  | EF_malloc => do_ef_malloc
+  | EF_free => do_ef_free
+  | EF_memcpy sz al => do_ef_memcpy sz al
+  | EF_annot text targs => do_ef_annot text targs
+  | EF_annot_val text targ => do_ef_annot_val text targ
+  end.
+
+Lemma do_ef_external_sound:
+  forall ef w vargs m w' t vres m',
+  do_external ef w vargs m = Some(w', t, vres, m') ->
+  external_call ef ge vargs m t vres m' /\ possible_trace w t w'.
+Proof with try congruence.
+  intros until m'.
+  assert (IO: forall name sg,
+             do_ef_external name sg w vargs m = Some(w', t, vres, m') ->
+             extcall_io_sem name sg ge vargs m t vres m' /\ possible_trace w t w').
+    intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr.
+    split. econstructor. apply list_eventval_of_val_sound; auto. 
+    apply val_of_eventval_sound; auto. 
+    econstructor. constructor; eauto. constructor.
+
+  assert (VLOAD: forall chunk vargs,
+    do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') ->
+    volatile_load_sem chunk ge vargs m t vres m' /\ possible_trace w t w').
+  intros chunk vargs'.
+  unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... 
+  mydestr. destruct p as [[w'' t''] v]; mydestr.
+  exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. 
+
+  assert (VSTORE: forall chunk vargs,
+    do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') ->
+    volatile_store_sem chunk ge vargs m t vres m' /\ possible_trace w t w').
+  intros chunk vargs'.
+  unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... 
+  mydestr. destruct p as [[w'' t''] m'']. mydestr. 
+  exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto.
+
+  destruct ef; simpl.
+(* EF_external *)
+  auto. 
+(* EF_builtin *)
+  auto.
+(* EF_vload *)
+  auto.
+(* EF_vstore *)
+  auto.
+(* EF_vload_global *)
+  rewrite volatile_load_global_charact.
+  unfold do_ef_volatile_load_global. destruct (Genv.find_symbol ge)...
+  intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto.
+(* EF_vstore_global *)
+  rewrite volatile_store_global_charact.
+  unfold do_ef_volatile_store_global. destruct (Genv.find_symbol ge)...
+  intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto.
+(* EF_malloc *)
+  unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs...
+  destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr.
+  split. econstructor; eauto. constructor.
+(* EF_free *)
+  unfold do_ef_free. destruct vargs... destruct v... destruct vargs... 
+  mydestr. destruct v... mydestr. 
+  split. econstructor; eauto. omega. constructor.
+(* EF_memcpy *)
+  unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... 
+  destruct v... destruct vargs... mydestr. red in m0. 
+  split. econstructor; eauto; tauto. constructor.
+(* EF_annot *)
+  unfold do_ef_annot. mydestr. 
+  split. constructor. apply list_eventval_of_val_sound; auto.
+  econstructor. constructor; eauto. constructor.
+(* EF_annot_val *)
+  unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. 
+  split. constructor. apply eventval_of_val_sound; auto.
+  econstructor. constructor; eauto. constructor.
+Qed.
+
+Lemma do_ef_external_complete:
+  forall ef w vargs m w' t vres m',
+  external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
+  do_external ef w vargs m = Some(w', t, vres, m').
+Proof.
+  intros.
+  assert (IO: forall name sg,
+             extcall_io_sem name sg ge vargs m t vres m' ->
+             do_ef_external name sg w vargs m = Some (w', t, vres, m')).
+    intros. inv H1. inv H0. inv H8. inv H6. 
+    unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. 
+    rewrite (val_of_eventval_complete _ _ _ H3). auto.
+ 
+  assert (VLOAD: forall chunk vargs,
+             volatile_load_sem chunk ge vargs m t vres m' ->
+             do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')).
+  intros. inv H1; unfold do_ef_volatile_load.
+  exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
+
+  assert (VSTORE: forall chunk vargs,
+             volatile_store_sem chunk ge vargs m t vres m' ->
+             do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')).
+  intros. inv H1; unfold do_ef_volatile_store.
+  exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto.
+
+  destruct ef; simpl in *.
+(* EF_external *)
+  auto.
+(* EF_builtin *)
+  auto.
+(* EF_vload *)
+  auto.
+(* EF_vstore *)
+  auto.
+(* EF_vload_global *)
+  rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. 
+  unfold do_ef_volatile_load_global. rewrite P. auto. 
+(* EF_vstore *)
+  rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. 
+  unfold do_ef_volatile_store_global. rewrite P. auto. 
+(* EF_malloc *)
+  inv H; unfold do_ef_malloc. 
+  inv H0. rewrite H1. rewrite H2. auto.
+(* EF_free *)
+  inv H; unfold do_ef_free.
+  inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega.
+(* EF_memcpy *)
+  inv H; unfold do_ef_memcpy.
+  inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto.
+  red. tauto. 
+(* EF_annot *)
+  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. 
+  rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
+(* EF_annot_val *)
+  inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. 
+  rewrite (eventval_of_val_complete _ _ _ H1). auto.
+Qed.
+
+(** * Reduction of expressions *)
+
 Inductive reduction: Type :=
   | Lred (l': expr) (m': mem)
-  | Rred (r': expr) (m': mem)
-  | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem).
+  | Rred (r': expr) (m': mem) (t: trace)
+  | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem)
+  | Stuckred.
 
 Section EXPRS.
 
 Variable e: env.
+Variable w: world.
 
 Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) :=
   match vtl, tl with
@@ -122,41 +653,51 @@ Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (li
   | _, _ => None
   end.
 
-(** The result of stepping an expression can be
-- [None] denoting that the expression is stuck;
-- [Some nil] meaning that the expression is fully reduced
-   (it's [Eval] for a r-value and [Eloc] for a l-value);
-- [Some ll] meaning that the expression can reduce to any of
-   the elements of [ll].  Each element is a pair of a context
-   and a reduction inside this context (see type [reduction] above).
+(** The result of stepping an expression is a list [ll] of possible reducts.
+  Each element of [ll] is a pair of a context and the result of reducing
+  inside this context (see type [reduction] above).
+  The list [ll] is empty if the expression is fully reduced
+   (it's [Eval] for a r-value and [Eloc] for a l-value).
 *)
 
-Definition reducts (A: Type): Type := option (list ((expr -> A) * reduction)).
+Definition reducts (A: Type): Type := list ((expr -> A) * reduction).
 
 Definition topred (r: reduction) : reducts expr :=
-  Some (((fun (x: expr) => x), r) :: nil).
+  ((fun (x: expr) => x), r) :: nil.
 
-Definition incontext {A B: Type} (ctx: A -> B) (r: reducts A) : reducts B :=
-  match r with
-  | None => None
-  | Some l => Some (map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) l)
-  end.
+Definition stuck : reducts expr :=
+  ((fun (x: expr) => x), Stuckred) :: nil.
+
+Definition incontext {A B: Type} (ctx: A -> B) (ll: reducts A) : reducts B :=
+  map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) ll.
 
 Definition incontext2 {A1 A2 B: Type}
-                     (ctx1: A1 -> B) (r1: reducts A1)
-                     (ctx2: A2 -> B) (r2: reducts A2) : reducts B :=
-  match r1, r2 with
-  | None, _ => None
-  | _, None => None
-  | Some l1, Some l2 =>
-      Some (map (fun z => ((fun (x: expr) => ctx1(fst z x)), snd z)) l1
-            ++ map (fun z => ((fun (x: expr) => ctx2(fst z x)), snd z)) l2)
-  end.
+                     (ctx1: A1 -> B) (ll1: reducts A1)
+                     (ctx2: A2 -> B) (ll2: reducts A2) : reducts B :=
+  incontext ctx1 ll1 ++ incontext ctx2 ll2.
+
+Notation "'do' X <- A ; B" := (match A with Some X => B | None => stuck end)
+  (at level 200, X ident, A at level 100, B at level 200)
+  : reducts_monad_scope.
+
+Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => stuck end)
+  (at level 200, X ident, Y ident, A at level 100, B at level 200)
+  : reducts_monad_scope.
+
+Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => stuck end)
+  (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
+  : reducts_monad_scope.
+
+Notation " 'check' A ; B" := (if A then B else stuck)
+  (at level 200, A at level 100, B at level 200)
+  : reducts_monad_scope.
+
+Local Open Scope reducts_monad_scope.
 
 Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
   match k, a with
   | LV, Eloc b ofs ty =>
-      Some nil
+      nil
   | LV, Evar x ty =>
       match e!x with
       | Some(b, ty') =>
@@ -173,47 +714,49 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       | Some(Vptr b ofs, ty') =>
           topred (Lred (Eloc b ofs ty) m)
       | Some _ =>
-          None
+          stuck
       | None =>
           incontext (fun x => Ederef x ty) (step_expr RV r m)
       end
-  | LV, Efield l f ty =>
-      match is_loc l with
-      | Some(b, ofs, ty') =>
+  | LV, Efield r f ty =>
+      match is_val r with
+      | Some(Vptr b ofs, ty') =>
           match ty' with
-          | Tstruct id fList =>
+          | Tstruct id fList _ =>
               match field_offset f fList with
-              | Error _ => None
+              | Error _ => stuck
               | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m)
               end
-          | Tunion id fList =>
+          | Tunion id fList _ =>
               topred (Lred (Eloc b ofs ty) m)
-          | _ => None
+          | _ => stuck
           end
+      | Some _ =>
+          stuck
       | None =>
-          incontext (fun x => Efield x f ty) (step_expr LV l m)
+          incontext (fun x => Efield x f ty) (step_expr RV r m)
       end
   | RV, Eval v ty =>
-      Some nil
+      nil
   | RV, Evalof l ty =>
       match is_loc l with
       | Some(b, ofs, ty') =>
           check type_eq ty ty';
-          do v <- load_value_of_type ty m b ofs;
-          topred (Rred (Eval v ty) m)
+          do w',t,v <- do_deref_loc w ty m b ofs;
+          topred (Rred (Eval v ty) m t)
       | None =>
           incontext (fun x => Evalof x ty) (step_expr LV l m)
       end
   | RV, Eaddrof l ty =>
       match is_loc l with
-      | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m)
+      | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m E0)
       | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m)
       end
   | RV, Eunop op r1 ty =>
       match is_val r1 with
       | Some(v1, ty1) =>
           do v <- sem_unary_operation op v1 ty1;
-          topred (Rred (Eval v ty) m)
+          topred (Rred (Eval v ty) m E0)
       | None =>
           incontext (fun x => Eunop op x ty) (step_expr RV r1 m)
       end
@@ -221,7 +764,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1, is_val r2 with
       | Some(v1, ty1), Some(v2, ty2) =>
           do v <- sem_binary_operation op v1 ty1 v2 ty2 m;
-          topred (Rred (Eval v ty) m)
+          topred (Rred (Eval v ty) m E0)
       | _, _ =>
          incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m)
                     (fun x => Ebinop op r1 x ty) (step_expr RV r2 m)
@@ -230,7 +773,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do v <- sem_cast v1 ty1 ty;
-          topred (Rred (Eval v ty) m)
+          topred (Rred (Eval v ty) m E0)
       | None =>
           incontext (fun x => Ecast x ty) (step_expr RV r1 m)
       end
@@ -238,19 +781,19 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some(v1, ty1) =>
           do b <- bool_val v1 ty1;
-          topred (Rred (Eparen (if b then r2 else r3) ty) m)
+          topred (Rred (Eparen (if b then r2 else r3) ty) m E0)
       | None =>
           incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
       end
   | RV, Esizeof ty' ty =>
-      topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m)
+      topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0)
   | RV, Eassign l1 r2 ty =>
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
           check type_eq ty1 ty;
           do v <- sem_cast v2 ty2 ty1;
-          do m' <- store_value_of_type ty1 m b ofs v;
-          topred (Rred (Eval v ty) m')
+          do w',t,m' <- do_assign_loc w ty1 m b ofs v;
+          topred (Rred (Eval v ty) m' t)
       | _, _ =>
          incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m)
                     (fun x => Eassign l1 x ty) (step_expr RV r2 m)
@@ -259,11 +802,10 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_loc l1, is_val r2 with
       | Some(b, ofs, ty1), Some(v2, ty2) =>
           check type_eq ty1 ty;
-          do v1 <- load_value_of_type ty1 m b ofs;
-          do v <- sem_binary_operation op v1 ty1 v2 ty2 m;
-          do v' <- sem_cast v tyres ty1;
-          do m' <- store_value_of_type ty1 m b ofs v';
-          topred (Rred (Eval v' ty) m')
+          do w',t,v1 <- do_deref_loc w ty1 m b ofs;
+          let r' := Eassign (Eloc b ofs ty1)
+                           (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1 in
+          topred (Rred r' m t)
       | _, _ =>
          incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m)
                     (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m)
@@ -272,11 +814,14 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_loc l with
       | Some(b, ofs, ty1) =>
           check type_eq ty1 ty;
-          do v1 <- load_value_of_type ty m b ofs;
-          do v2 <- sem_incrdecr id v1 ty;
-          do v3 <- sem_cast v2 (typeconv ty) ty;
-          do m' <- store_value_of_type ty m b ofs v3;
-          topred (Rred (Eval v1 ty) m')
+          do w',t, v1 <- do_deref_loc w ty m b ofs;
+          let op := match id with Incr => Oadd | Decr => Osub end in
+          let r' :=
+            Ecomma (Eassign (Eloc b ofs ty) 
+                           (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (typeconv ty))
+                           ty)
+                   (Eval v1 ty) ty in
+          topred (Rred r' m t)
       | None =>
           incontext (fun x => Epostincr id x ty) (step_expr LV l m)
       end
@@ -284,7 +829,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some _ =>
           check type_eq (typeof r2) ty;
-          topred (Rred r2 m)
+          topred (Rred r2 m E0)
       | None =>
           incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m)
       end
@@ -292,7 +837,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
       match is_val r1 with
       | Some (v1, ty1) =>
           do v <- sem_cast v1 ty1 ty;
-          topred (Rred (Eval v ty) m)
+          topred (Rred (Eval v ty) m E0)
       | None =>
           incontext (fun x => Eparen x ty) (step_expr RV r1 m)
       end
@@ -305,24 +850,224 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
               do vargs <- sem_cast_arguments vtl tyargs;
               check type_eq (type_of_fundef fd) (Tfunction tyargs tyres);
               topred (Callred fd vargs ty m)
-          | _ => None
+          | _ => stuck
           end
       | _, _ =>
           incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m)
                      (fun x => Ecall r1 x ty) (step_exprlist rargs m)
       end
-  | _, _ => None
+  | _, _ => stuck
   end
 
 with step_exprlist (rl: exprlist) (m: mem): reducts exprlist :=
   match rl with
   | Enil =>
-      Some nil
+      nil
   | Econs r1 rs =>
       incontext2 (fun x => Econs x rs) (step_expr RV r1 m)
                  (fun x => Econs r1 x) (step_exprlist rs m)
   end.
 
+(** Technical properties on safe expressions. *)
+
+Inductive imm_safe_t: kind -> expr -> mem -> Prop :=
+  | imm_safe_t_val: forall v ty m,
+      imm_safe_t RV (Eval v ty) m
+  | imm_safe_t_loc: forall b ofs ty m,
+      imm_safe_t LV (Eloc b ofs ty) m
+  | imm_safe_t_lred: forall to C l m l' m',
+      lred ge e l m l' m' ->
+      context LV to C ->
+      imm_safe_t to (C l) m
+  | imm_safe_t_rred: forall to C r m t r' m' w',
+      rred ge r m t r' m' -> possible_trace w t w' ->
+      context RV to C ->
+      imm_safe_t to (C r) m
+  | imm_safe_t_callred: forall to C r m fd args ty,
+      callred ge r fd args ty ->
+      context RV to C ->
+      imm_safe_t to (C r) m.
+
+Remark imm_safe_t_imm_safe:
+  forall k a m, imm_safe_t k a m -> imm_safe ge e k a m.
+Proof.
+  induction 1. 
+  constructor.
+  constructor.
+  eapply imm_safe_lred; eauto.
+  eapply imm_safe_rred; eauto.
+  eapply imm_safe_callred; eauto.
+Qed.
+
+(*
+Definition not_stuck (a: expr) (m: mem) :=
+  forall a' k C, context k RV C -> a = C a' -> imm_safe_t k a' m.
+
+Lemma safe_expr_kind:
+  forall k C a m,
+  context k RV C ->
+  not_stuck (C a) m ->
+  k = Cstrategy.expr_kind a.
+Proof.
+  intros.
+  symmetry. eapply Cstrategy.imm_safe_kind. eapply imm_safe_t_imm_safe. eauto.
+Qed.
+*)
+
+Fixpoint exprlist_all_values (rl: exprlist) : Prop :=
+  match rl with
+  | Enil => True
+  | Econs (Eval v ty) rl' => exprlist_all_values rl'
+  | Econs _ _ => False
+  end.
+
+Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
+  match a with
+  | Eloc b ofs ty => False
+  | Evar x ty =>
+      exists b,
+      e!x = Some(b, ty)
+      \/ (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 (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
+      | _ => False
+      end
+  | Eval v ty => False
+  | Evalof (Eloc b ofs ty') ty =>
+      ty' = ty /\ exists t, exists v, exists w', deref_loc ge ty m b ofs t v /\ possible_trace w t w'
+  | 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 =>
+      exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v
+  | Ecast (Eval v1 ty1) ty =>
+      exists v, sem_cast v1 ty1 ty = Some v
+  | 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', exists t, exists w',
+      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w'
+  | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
+      exists t, exists v1, exists w',
+      ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w'
+  | Epostincr id (Eloc b ofs ty1) ty =>
+      exists t, exists v1, exists w', 
+      ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w'
+  | Ecomma (Eval v ty1) r2 ty =>
+      typeof r2 = ty
+  | Eparen (Eval v1 ty1) ty =>
+      exists v, sem_cast v1 ty1 ty = Some v
+  | Ecall (Eval vf tyf) rargs ty =>
+      exprlist_all_values rargs ->
+      exists tyargs, exists tyres, exists fd, exists vl,
+         classify_fun tyf = fun_case_f tyargs tyres
+      /\ Genv.find_funct ge vf = Some fd
+      /\ cast_arguments rargs tyargs vl
+      /\ type_of_fundef fd = Tfunction tyargs tyres
+  | _ => True
+  end.
+
+Lemma lred_invert:
+  forall l m l' m', lred ge e l m l' m' -> invert_expr_prop l m.
+Proof.
+  induction 1; red; auto.
+  exists b; auto.
+  exists b; auto.
+  exists b; exists ofs; auto.
+  exists b; exists ofs; split; auto. exists delta; auto.
+  exists b; exists ofs; auto.
+Qed.
+
+Lemma rred_invert:
+  forall w' r m t r' m', rred ge r m t r' m' -> possible_trace w t w' -> invert_expr_prop r m.
+Proof.
+  induction 1; intros; red; auto.
+  split; auto; exists t; exists v; exists w'; auto.
+  exists v; auto.
+  exists v; auto.
+  exists v; auto.
+  exists b; auto.
+  exists v; exists m'; exists t; exists w'; auto.
+  exists t; exists v1; exists w'; auto.
+  exists t; exists v1; exists w'; auto.
+  exists v; auto.
+Qed.
+
+Lemma callred_invert:
+  forall r fd args ty m,
+  callred ge r fd args ty ->
+  invert_expr_prop r m.
+Proof.
+  intros. inv H. simpl.
+  intros. exists tyargs; exists tyres; exists fd; exists args; auto.
+Qed.
+
+Scheme context_ind2 := Minimality for context Sort Prop
+  with contextlist_ind2 := Minimality for contextlist Sort Prop.
+Combined Scheme context_contextlist_ind from context_ind2, contextlist_ind2.
+
+Lemma invert_expr_context:
+  (forall from to C, context from to C ->
+   forall a m,
+   invert_expr_prop a m ->
+   invert_expr_prop (C a) m)
+/\(forall from C, contextlist from C ->
+  forall a m,
+  invert_expr_prop a m ->
+  ~exprlist_all_values (C a)).
+Proof.
+  apply context_contextlist_ind; intros; try (exploit H0; [eauto|intros]); simpl.
+  auto.
+  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 e1; auto; destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  destruct e1; auto; destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  destruct e1; auto; destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  destruct e1; auto. intros. elim (H0 a m); auto.
+  destruct (C a); auto; contradiction.
+  destruct (C a); auto; contradiction.
+  red; intros. destruct (C a); auto. 
+  red; intros. destruct e1; auto. elim (H0 a m); auto. 
+Qed.
+
+Lemma imm_safe_t_inv:
+  forall k a m,
+  imm_safe_t k a m ->
+  match a with
+  | Eloc _ _ _ => True
+  | Eval _ _ => True
+  | _ => invert_expr_prop a m
+  end.
+Proof.
+  destruct invert_expr_context as [A B].
+  intros. inv H. 
+  auto.
+  auto.
+  assert (invert_expr_prop (C l) m).
+    eapply A; eauto. eapply lred_invert; eauto.
+  red in H. destruct (C l); auto; contradiction.
+  assert (invert_expr_prop (C r) m).
+    eapply A; eauto. eapply rred_invert; eauto.
+  red in H. destruct (C r); auto; contradiction.
+  assert (invert_expr_prop (C r) m).
+    eapply A; eauto. eapply callred_invert; eauto.
+  red in H. destruct (C r); auto; contradiction.
+Qed.
+
 (** Soundness: if [step_expr] returns [Some ll], then every element
   of [ll] is a reduct. *)
 
@@ -343,19 +1088,27 @@ Qed.
 Hint Constructors context contextlist.
 Hint Resolve context_compose contextlist_compose.
 
-Definition reduction_ok (a: expr) (m: mem) (rd: reduction) : Prop :=
-  match rd with
-  | Lred l' m' => lred ge e a m l' m'
-  | Rred r' m' => rred a m r' m'
-  | Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m
+Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop :=
+  match k, rd with
+  | LV, Lred l' m' => lred ge e a m l' m'
+  | RV, Rred r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
+  | RV, Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m
+  | LV, Stuckred => ~imm_safe_t k a m
+  | RV, Stuckred => ~imm_safe_t k a m
+  | _, _ => False
   end.
 
-Definition reduction_kind (rd: reduction): kind :=
-  match rd with
-  | Lred l' m' => LV
-  | Rred r' m' => RV
-  | Callred fd args tyres m' => RV
-  end.
+Definition reducts_ok (k: kind) (a: expr) (m: mem) (ll: reducts expr) : Prop :=
+  (forall C rd,
+      In (C, rd) ll ->
+      exists a', exists k', context k' k C /\ a = C a' /\ reduction_ok k' a' m rd)
+  /\ (ll = nil -> match k with LV => is_loc a <> None | RV => is_val a <> None end).
+
+Definition list_reducts_ok (al: exprlist) (m: mem) (ll: reducts exprlist) : Prop :=
+  (forall C rd,
+      In (C, rd) ll ->
+      exists a', exists k', contextlist k' C /\ al = C a' /\ reduction_ok k' a' m rd)
+  /\ (ll = nil -> is_val_list al <> None).
 
 Ltac monadInv :=
   match goal with
@@ -378,36 +1131,59 @@ Proof.
   inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. 
 Qed.
 
-Definition reducts_ok (k: kind) (a: expr) (m: mem) (res: reducts expr) : Prop :=
-  match res with
-  | None => True
-  | Some nil => match k with LV => is_loc a <> None | RV => is_val a <> None end
-  | Some ll =>
-      forall C rd,
-      In (C, rd) ll ->
-      context (reduction_kind rd) k C /\ exists a', a = C a' /\ reduction_ok a' m rd
-  end.
-
-Definition list_reducts_ok (al: exprlist) (m: mem) (res: reducts exprlist) : Prop :=
-  match res with
-  | None => True
-  | Some nil => is_val_list al <> None
-  | Some ll =>
-      forall C rd,
-      In (C, rd) ll ->
-      contextlist (reduction_kind rd) C /\ exists a', al = C a' /\ reduction_ok a' m rd
-  end.
+Lemma sem_cast_arguments_complete:
+  forall al tyl vl,
+  cast_arguments al tyl vl ->
+  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl.
+Proof.
+  induction 1.
+  exists (@nil (val * type)); auto.
+  destruct IHcast_arguments as [vtl [A B]]. 
+  exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto.
+Qed.
 
 Lemma topred_ok:
   forall k a m rd,
-  reduction_ok a m rd ->
-  k = reduction_kind rd ->
+  reduction_ok k a m rd ->
   reducts_ok k a m (topred rd).
 Proof.
-  intros. unfold topred; red. simpl; intros. destruct H1; try contradiction.
-  inv H1. split. auto. exists a; auto.
+  intros. unfold topred; split; simpl; intros. 
+  destruct H0; try contradiction. inv H0. exists a; exists k; auto.
+  congruence.
+Qed.
+
+Lemma stuck_ok:
+  forall k a m,
+  ~imm_safe_t k a m ->
+  reducts_ok k a m stuck.
+Proof.
+  intros. unfold stuck; split; simpl; intros.
+  destruct H0; try contradiction. inv H0. exists a; exists k; intuition. red. destruct k; auto.
+  congruence.
 Qed.
 
+Lemma wrong_kind_ok:
+  forall k a m,
+  k <> Cstrategy.expr_kind a ->
+  reducts_ok k a m stuck.
+Proof.
+  intros. apply stuck_ok. red; intros. exploit Cstrategy.imm_safe_kind; eauto. 
+  eapply imm_safe_t_imm_safe; eauto.
+Qed.
+
+Lemma not_invert_ok:
+  forall k a m,
+  match a with
+  | Eloc _ _ _ => False
+  | Eval _ _ => False
+  | _ => invert_expr_prop a m -> False
+  end ->
+  reducts_ok k a m stuck.
+Proof.
+  intros. apply stuck_ok. red; intros. 
+  exploit imm_safe_t_inv; eauto. destruct a; auto. 
+Qed. 
+
 Lemma incontext_ok:
   forall k a m C res k' a',
   reducts_ok k' a' m res ->
@@ -416,48 +1192,11 @@ Lemma incontext_ok:
   match k' with LV => is_loc a' = None | RV => is_val a' = None end ->
   reducts_ok k a m (incontext C res).
 Proof.
-  unfold reducts_ok; intros. destruct res; simpl. destruct l.
-(* res = Some nil *)
-  destruct k'; congruence.
-(* res = Some nonempty-list *)
-  simpl map at 1. hnf. intros. 
+  unfold reducts_ok, incontext; intros. destruct H. split; intros.
   exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P.
-  exploit H; eauto. intros [U [a'' [V W]]].
-  split. eapply context_compose; eauto. exists a''; split; auto. congruence. 
-(* res = None *)
-  auto.
-Qed.
-
-Remark incontext2_inv:
-  forall {A1 A2 B: Type} (C1: A1 -> B) res1 (C2: A2 -> B) res2,
-  match incontext2 C1 res1 C2 res2 with
-  | None => res1 = None \/ res2 = None
-  | Some nil => res1 = Some nil /\ res2 = Some nil
-  | Some ll => 
-      exists ll1, exists ll2,
-      res1 = Some ll1 /\ res2 = Some ll2 /\
-      forall C rd, In (C, rd) ll ->
-      (exists C', C = (fun x => C1(C' x)) /\ In (C', rd) ll1)
-      \/ (exists C', C = (fun x => C2(C' x)) /\ In (C', rd) ll2)
-  end.
-Proof.
-  intros. unfold incontext2. destruct res1 as [ll1|]; auto. destruct res2 as [ll2|]; auto.
-  set (ll := map
-    (fun z : (expr -> A1) * reduction =>
-     (fun x : expr => C1 (fst z x), snd z)) ll1 ++
-  map
-    (fun z : (expr -> A2) * reduction =>
-     (fun x : expr => C2 (fst z x), snd z)) ll2).
-  destruct ll as []_eqn.
-  destruct (app_eq_nil _ _ Heql). 
-  split. destruct ll1; auto || discriminate. destruct ll2; auto || discriminate.
-  rewrite <- Heql. exists ll1; exists ll2. split. auto. split. auto.
-  unfold ll; intros.
-  rewrite in_app in H. destruct H.
-  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
-  left; exists C'; auto. 
-  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
-  right; exists C'; auto.
+  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eapply context_compose; eauto. rewrite V; auto.
+  destruct res; simpl in H4; try congruence. destruct k'; intuition congruence.
 Qed.
 
 Lemma incontext2_ok:
@@ -470,17 +1209,16 @@ Lemma incontext2_ok:
   \/ match k2 with LV => is_loc a2 = None | RV => is_val a2 = None end ->
   reducts_ok k a m (incontext2 C1 res1 C2 res2).
 Proof.
-  unfold reducts_ok; intros.
-  generalize (incontext2_inv C1 res1 C2 res2). 
-  destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto.
-  destruct ll. 
-  intros [EQ1 EQ2]. subst. destruct H5. destruct k1; congruence. destruct k2; congruence.
-  intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. 
-  exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst.
-  destruct ll1; try contradiction. exploit H; eauto.
-  intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto. 
-  destruct ll2; try contradiction. exploit H0; eauto.
-  intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto.
+  unfold reducts_ok, incontext2, incontext; intros. destruct H; destruct H0; split; intros.
+  destruct (in_app_or _ _ _ H8).
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eapply context_compose; eauto. rewrite V; auto.
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eapply context_compose; eauto. rewrite H2; rewrite V; auto.
+  destruct res1; simpl in H8; try congruence. destruct res2; simpl in H8; try congruence.
+  destruct H5. destruct k1; intuition congruence. destruct k2; intuition congruence.
 Qed.
 
 Lemma incontext2_list_ok:
@@ -492,18 +1230,16 @@ Lemma incontext2_list_ok:
                (incontext2 (fun x => Ecall x a2 ty) res1
                            (fun x => Ecall a1 x ty) res2).
 Proof.
-  unfold reducts_ok, list_reducts_ok; intros.
-  set (C1 := fun x => Ecall x a2 ty). set (C2 := fun x => Ecall a1 x ty). 
-  generalize (incontext2_inv C1 res1 C2 res2). 
-  destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto.
-  destruct ll. 
-  intros [EQ1 EQ2]. subst. intuition congruence.
-  intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. 
-  exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst.
-  destruct ll1; try contradiction. exploit H; eauto.
-  intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. 
-  destruct ll2; try contradiction. exploit H0; eauto.
-  intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto.
+  unfold reducts_ok, incontext2, incontext; intros. destruct H; destruct H0; split; intros.
+  destruct (in_app_or _ _ _ H4).
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eauto. rewrite V; auto. 
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eauto. rewrite V; auto.
+  destruct res1; simpl in H4; try congruence. destruct res2; simpl in H4; try congruence.
+  tauto.
 Qed.
 
 Lemma incontext2_list_ok':
@@ -514,165 +1250,201 @@ Lemma incontext2_list_ok':
                (incontext2 (fun x => Econs x a2) res1
                            (fun x => Econs a1 x) res2).
 Proof.
-  unfold reducts_ok, list_reducts_ok; intros.
-  set (C1 := fun x => Econs x a2). set (C2 := fun x => Econs a1 x). 
-  generalize (incontext2_inv C1 res1 C2 res2). 
-  destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto.
-  destruct ll. 
-  intros [EQ1 EQ2]. subst.
-  simpl. destruct (is_val a1); try congruence. destruct (is_val_list a2); congruence.
-  intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. 
-  exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst.
-  destruct ll1; try contradiction. exploit H; eauto.
-  intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. 
-  destruct ll2; try contradiction. exploit H0; eauto.
-  intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto.
-Qed.
-
-Ltac mysimpl :=
+  unfold reducts_ok, list_reducts_ok, incontext2, incontext; intros.
+  destruct H; destruct H0. split; intros.
+  destruct (in_app_or _ _ _ H3).
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  exploit H; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eauto. rewrite V; auto. 
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  exploit H0; eauto. intros [a'' [k'' [U [V W]]]].
+  exists a''; exists k''. split. eauto. rewrite V; auto.
+  destruct res1; simpl in H3; try congruence. destruct res2; simpl in H3; try congruence.
+  simpl. destruct (is_val a1). destruct (is_val_list a2). congruence. intuition congruence. intuition congruence.
+Qed.
+
+Lemma is_val_list_all_values:
+  forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al.
+Proof.
+  induction al; simpl; intros. auto. 
+  destruct (is_val r1) as [[v ty]|]_eqn; try discriminate.
+  destruct (is_val_list al) as [vtl'|]_eqn; try discriminate.
+  rewrite (is_val_inv _ _ _ Heqo). eauto.
+Qed.
+
+Ltac myinv :=
   match goal with
-  | [ |- reducts_ok _ _ _ (match ?x with Some _ => _ | None => None end) ] =>
-      destruct x as []_eqn; [mysimpl|exact I]
-  | [ |- reducts_ok _ _ _ (match ?x with left _ => _ | right _ => None end) ] =>
-      destruct x as []_eqn; [subst;mysimpl|exact I]
-  | _ =>
-      idtac
+  | [ H: False |- _ ] => destruct H
+  | [ H: _ /\ _ |- _ ] => destruct H; myinv
+  | [ H: exists _, _ |- _ ] => destruct H; myinv
+  | _ => idtac
   end.
 
 Theorem step_expr_sound:
   forall a k m, reducts_ok k a m (step_expr k a m)
 with step_exprlist_sound:
   forall al m, list_reducts_ok al m (step_exprlist al m).
-Proof with try (exact I).
-  induction a; destruct k; intros; simpl...
+Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; fail)).
+  induction a; intros; simpl; destruct k; try (apply wrong_kind_ok; simpl; congruence).
 (* Eval *)
-  congruence.
+  split; intros. tauto. simpl; congruence.
 (* Evar *)
-  destruct (e!x) as [[b ty'] | ]_eqn; mysimpl.
-  apply topred_ok; auto. apply red_var_local; auto.
-  apply topred_ok; auto. apply red_var_global; auto.
+  destruct (e!x) as [[b ty']|]_eqn.
+  destruct (type_eq ty ty')...
+  subst. apply topred_ok; auto. apply red_var_local; auto.
+  destruct (Genv.find_symbol ge x) as [b|]_eqn...
+  destruct (type_of_global ge b) as [ty'|]_eqn...
+  destruct (type_eq ty ty')...
+  subst. apply topred_ok; auto. apply red_var_global; auto.
 (* Efield *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  destruct (is_val a) as [[v ty'] | ]_eqn.
+  rewrite (is_val_inv _ _ _ Heqo).
+  destruct v...
   destruct ty'... 
   (* top struct *)
   destruct (field_offset f f0) as [delta|]_eqn...
-  rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_struct; auto.
+  apply topred_ok; auto. apply red_field_struct; auto.
   (* top union *)
-  rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_union; auto.
+  apply topred_ok; auto. apply red_field_union; auto.
   (* in depth *)
   eapply incontext_ok; eauto. 
 (* Evalof *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo).
   (* top *)
-  mysimpl. apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_rvalof; auto. 
+  destruct (type_eq ty ty')... subst ty'.
+  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn.
+  exploit do_deref_loc_sound; eauto. intros [A B].
+  apply topred_ok; auto. red. split. apply red_rvalof; auto. exists w'; auto.
+  apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
   (* depth *)
   eapply incontext_ok; eauto.
 (* Ederef *)
-  destruct (is_val a) as [[v ty'] | ]_eqn.
+  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo).
   (* top *)
-  destruct v... mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_deref; auto. 
+  destruct v... apply topred_ok; auto. apply red_deref; auto. 
   (* depth *)
   eapply incontext_ok; eauto.
 (* Eaddrof *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo).
   (* top *)
-  apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_addrof; auto. 
+  apply topred_ok; auto. split. apply red_addrof; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* unop *)
-  destruct (is_val a) as [[v ty'] | ]_eqn.
+  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_unop; auto. 
+  destruct (sem_unary_operation op v ty') as [v'|]_eqn...
+  apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
 (* binop *)
-  destruct (is_val a1) as [[v1 ty1] | ]_eqn.
+  destruct (is_val a1) as [[v1 ty1] | ]_eqn. 
   destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
   (* top *)
-  mysimpl. apply topred_ok; auto. 
-  rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_binop; auto.
+  destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|]_eqn...
+  apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor.
   (* depth *)
   eapply incontext2_ok; eauto. 
   eapply incontext2_ok; eauto. 
 (* cast *)
-  destruct (is_val a) as [[v ty'] | ]_eqn.
+  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  mysimpl. apply topred_ok; auto. 
-  rewrite (is_val_inv _ _ _ Heqo). apply red_cast; auto. 
+  destruct (sem_cast v ty' ty) as [v'|]_eqn...
+  apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
 (* condition *)
-  destruct (is_val a1) as [[v ty'] | ]_eqn.
+  destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_val_inv _ _ _ Heqo). eapply red_condition; eauto.
+  destruct (bool_val v ty') as [v'|]_eqn...
+  apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* sizeof *)
-  apply topred_ok; auto. apply red_sizeof.
+  apply topred_ok; auto. split. apply red_sizeof. exists w; constructor.
 (* assign *)
-  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn.
-  destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. 
+  destruct (is_val a2) as [[v2 ty2] | ]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0).
   (* top *)
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_assign; auto.
+  destruct (type_eq ty1 ty)... subst ty1.
+  destruct (sem_cast v2 ty2 ty) as [v|]_eqn...
+  destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|]_eqn.
+  exploit do_assign_loc_sound; eauto. intros [P Q].
+  apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto.
+  apply not_invert_ok; simpl; intros; myinv. exploit do_assign_loc_complete; eauto. congruence.
   (* depth *)
   eapply incontext2_ok; eauto.
   eapply incontext2_ok; eauto.
 (* assignop *)
-  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn.
-  destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. 
+  destruct (is_val a2) as [[v2 ty2] | ]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). 
   (* top *)
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). eapply red_assignop; eauto.
+  destruct (type_eq ty1 ty)... subst ty1.
+  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn.
+  exploit do_deref_loc_sound; eauto. intros [A B].
+  apply topred_ok; auto. red. split. apply red_assignop; auto. exists w'; auto.
+  apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
   (* depth *)
   eapply incontext2_ok; eauto.
   eapply incontext2_ok; eauto.
 (* postincr *)
-  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. rewrite (is_loc_inv _ _ _ _ Heqo). 
   (* top *)
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_loc_inv _ _ _ _ Heqo). eapply red_postincr; eauto. 
+  destruct (type_eq ty' ty)... subst ty'.
+  destruct (do_deref_loc w ty m b ofs) as [[[w' t] v] | ]_eqn.
+  exploit do_deref_loc_sound; eauto. intros [A B].
+  apply topred_ok; auto. red. split. apply red_postincr; auto. exists w'; auto.
+  apply not_invert_ok; simpl; intros; myinv. exploit do_deref_loc_complete; eauto. congruence.
   (* depth *)
   eapply incontext_ok; eauto.
 (* comma *)
-  destruct (is_val a1) as [[v ty'] | ]_eqn.
+  destruct (is_val a1) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_val_inv _ _ _ Heqo). apply red_comma; auto. 
+  destruct (type_eq (typeof a2) ty)... subst ty.
+  apply topred_ok; auto. split. apply red_comma; auto. exists w; constructor.
   (* depth *)
   eapply incontext_ok; eauto.
 (* call *)
-  destruct (is_val a) as [[vf tyf] | ]_eqn.
-  destruct (is_val_list rargs) as [vtl | ]_eqn.
+  destruct (is_val a) as [[vf tyf] | ]_eqn.  
+  destruct (is_val_list rargs) as [vtl | ]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo). exploit is_val_list_all_values; eauto. intros ALLVAL.
   (* top *)
   destruct (classify_fun tyf) as [tyargs tyres|]_eqn...
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_val_inv _ _ _ Heqo). red. split; auto. eapply red_Ecall; eauto. 
-  eapply sem_cast_arguments_sound; eauto. 
+  destruct (Genv.find_funct ge vf) as [fd|]_eqn...
+  destruct (sem_cast_arguments vtl tyargs) as [vargs|]_eqn... 
+  destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres))...
+  apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. 
+  eapply sem_cast_arguments_sound; eauto.
+  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
+  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv.
+  exploit sem_cast_arguments_complete; eauto. intros [vtl' [P Q]]. congruence.
+  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
+  apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence.
   (* depth *)
   eapply incontext2_list_ok; eauto.
   eapply incontext2_list_ok; eauto. 
 (* loc *)
-  congruence.
+  split; intros. tauto. simpl; congruence.
 (* paren *)
-  destruct (is_val a) as [[v ty'] | ]_eqn.
+  destruct (is_val a) as [[v ty'] | ]_eqn. rewrite (is_val_inv _ _ _ Heqo). 
   (* top *)
-  mysimpl. apply topred_ok; auto.
-  rewrite (is_val_inv _ _ _ Heqo). apply red_paren; auto. 
+  destruct (sem_cast v ty' ty) as [v'|]_eqn...
+  apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. 
   (* depth *)
   eapply incontext_ok; eauto.
 
   induction al; simpl; intros.
 (* nil *)
-  congruence.
+  split; intros. tauto. simpl; congruence.
 (* cons *)
   eapply incontext2_list_ok'; eauto.
 Qed.
 
-
 Lemma step_exprlist_val_list:
-  forall m al, is_val_list al <> None -> step_exprlist al m = Some nil.
+  forall m al, is_val_list al <> None -> step_exprlist al m = nil.
 Proof.
   induction al; simpl; intros. 
   auto.
@@ -682,8 +1454,7 @@ Proof.
   rewrite IHal. auto. congruence.
 Qed.
 
-(** Completeness, part 1: if [step_expr] returns [Some ll],
-  then [ll] contains all possible reducts. *)
+(** Completeness part 1: [step_expr] contains all possible non-error reducts. *)
 
 Lemma lred_topred:
   forall l1 m1 l2 m2,
@@ -704,46 +1475,35 @@ Proof.
 Qed.
 
 Lemma rred_topred:
-  forall r1 m1 r2 m2,
-  rred r1 m1 r2 m2 ->
-  step_expr RV r1 m1 = topred (Rred r2 m2).
+  forall w' r1 m1 t r2 m2,
+  rred ge r1 m1 t r2 m2 -> possible_trace w t w' ->
+  step_expr RV r1 m1 = topred (Rred r2 m2 t).
 Proof.
-  induction 1; simpl.
+  induction 1; simpl; intros.
 (* valof *)
-  rewrite dec_eq_true; auto. rewrite H; auto.
+  rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. 
 (* addrof *)
-  auto.
+  inv H. auto.
 (* unop *)
-  rewrite H; auto.
+  inv H0. rewrite H; auto.
 (* binop *)
-  rewrite H; auto.
+  inv H0. rewrite H; auto.
 (* cast *)
-  rewrite H; auto.
+  inv H0. rewrite H; auto.
 (* condition *)
-  rewrite H; auto.
+  inv H0. rewrite H; auto.
 (* sizeof *)
-  auto.
+  inv H. auto.
 (* assign *)
-  rewrite dec_eq_true; auto. rewrite H; rewrite H0; auto.
+  rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto.
 (* assignop *)
-  rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto.
+  rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. 
 (* postincr *)
-  rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto.
+  rewrite dec_eq_true; auto. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). auto.
 (* comma *)
-  rewrite H; rewrite dec_eq_true; auto.
+  inv H0. rewrite dec_eq_true; auto.
 (* paren *)
-  rewrite H; auto.
-Qed.
-
-Lemma sem_cast_arguments_complete:
-  forall al tyl vl,
-  cast_arguments al tyl vl ->
-  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl.
-Proof.
-  induction 1.
-  exists (@nil (val * type)); auto.
-  destruct IHcast_arguments as [vtl [A B]]. 
-  exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto.
+  inv H0. rewrite H; auto.
 Qed.
 
 Lemma callred_topred:
@@ -757,12 +1517,7 @@ Proof.
 Qed.
 
 Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop :=
-  match res1, res2 with
-  | Some ll1, Some ll2 =>
-      forall C1 rd, In (C1, rd) ll1 -> In ((fun x => C(C1 x)), rd) ll2
-  | None, Some ll2 => False
-  | _, None => True
-  end.
+  forall C1 rd, In (C1, rd) res1 -> In ((fun x => C(C1 x)), rd) res2.
 
 Lemma reducts_incl_trans:
   forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 ->
@@ -770,14 +1525,14 @@ Lemma reducts_incl_trans:
   reducts_incl C' res2 res3 ->
   reducts_incl (fun x => C'(C x)) res1 res3.
 Proof.
-  unfold reducts_incl; intros. destruct res1; destruct res2; destruct res3; auto. contradiction.
+  unfold reducts_incl; intros. auto. 
 Qed.
 
 Lemma reducts_incl_nil:
   forall (A B: Type) (C: A -> B) res,
-  reducts_incl C (Some nil) res.
+  reducts_incl C nil res.
 Proof.
-  intros; red. destruct res; auto. intros; contradiction.
+  intros; red. intros; contradiction.
 Qed.
 
 Lemma reducts_incl_val:
@@ -805,29 +1560,29 @@ Lemma reducts_incl_incontext:
   forall (A B: Type) (C: A -> B) res,
   reducts_incl C res (incontext C res).
 Proof.
-  intros; unfold reducts_incl. destruct res; simpl; auto.
-  intros. set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)).
-  change (In (f (C1, rd)) (map f l)). apply in_map. auto.
+  unfold reducts_incl, incontext. intros.
+  set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)).
+  change (In (f (C1, rd)) (map f res)). apply in_map. auto.
 Qed.
 
 Lemma reducts_incl_incontext2_left:
   forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
   reducts_incl C1 res1 (incontext2 C1 res1 C2 res2).
 Proof.
-  intros. destruct res1; simpl; auto. destruct res2; auto. 
-  intros. rewrite in_app_iff. left.
+  unfold reducts_incl, incontext2, incontext. intros.
+  rewrite in_app_iff. left.
   set (f := fun z : (expr -> A1) * reduction => (fun x : expr => C1 (fst z x), snd z)).
-  change (In (f (C0, rd)) (map f l)). apply in_map; auto.
+  change (In (f (C0, rd)) (map f res1)). apply in_map; auto.
 Qed.
 
 Lemma reducts_incl_incontext2_right:
   forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
   reducts_incl C2 res2 (incontext2 C1 res1 C2 res2).
 Proof.
-  intros. destruct res1; destruct res2; simpl; auto.
-  intros. rewrite in_app_iff. right.
+  unfold reducts_incl, incontext2, incontext. intros.
+  rewrite in_app_iff. right.
   set (f := fun z : (expr -> A2) * reduction => (fun x : expr => C2 (fst z x), snd z)).
-  change (In (f (C0, rd)) (map f l0)). apply in_map; auto.
+  change (In (f (C0, rd)) (map f res2)). apply in_map; auto.
 Qed.
 
 Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval
@@ -849,7 +1604,7 @@ Proof.
   destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
 (* field *)
   eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto.
-  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
 (* valof *)
   eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto.
   destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
@@ -912,625 +1667,83 @@ Proof.
   apply step_exprlist_context; eauto. eauto.
 Qed.
 
-(** Completeness, part 2: given a safe expression, [step_expr] does not return [None]. *)
+(** Completeness part 2: if we can reduce to [Stuckstate], [step_expr]
+    contains at least one [Stuckred] reduction. *)
 
-Lemma topred_none:
-  forall rd, topred rd <> None.
+Lemma not_stuckred_imm_safe:
+  forall m a k,
+  (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m.
 Proof.
-  intros; unfold topred; congruence.
+  intros. generalize (step_expr_sound a k m). intros [A B]. 
+  destruct (step_expr k a m) as [|[C rd] res]_eqn.
+  specialize (B (refl_equal _)). destruct k.
+  destruct a; simpl in B; try congruence. constructor.
+  destruct a; simpl in B; try congruence. constructor.
+  assert (NOTSTUCK: rd <> Stuckred).
+    red; intros. elim (H C); subst rd; auto with coqlib.
+  exploit A. eauto with coqlib. intros [a' [k' [P [Q R]]]]. 
+  destruct k'; destruct rd; simpl in R; intuition.
+  subst a. eapply imm_safe_t_lred; eauto.
+  subst a. destruct H1 as [w' PT]. eapply imm_safe_t_rred; eauto. 
+  subst. eapply imm_safe_t_callred; eauto. 
 Qed.
 
-Lemma incontext_none:
-  forall (A B: Type) (C: A -> B) rds,
-  rds <> None -> incontext C rds <> None.
-Proof.
-  unfold incontext; intros. destruct rds; congruence.
-Qed.
-
-Lemma incontext2_none:
-  forall (A1 A2 B: Type) (C1: A1 -> B) rds1 (C2: A2 -> B) rds2,
-  rds1 <> None -> rds2 <> None -> incontext2 C1 rds1 C2 rds2 <> None.
-Proof.
-  unfold incontext2; intros. destruct rds1; destruct rds2; congruence.
-Qed.
-
-Lemma safe_expr_kind:
-  forall k C a m,
-  context k RV C ->
-  not_stuck ge e (C a) m ->
-  k = Cstrategy.expr_kind a.
-Proof.
-  intros.
-  symmetry. eapply Cstrategy.not_imm_stuck_kind; eauto.
-Qed.
-
-Lemma safe_inversion:
-  forall k C a m,
+Lemma not_imm_safe_stuck_red:
+  forall m a k C,
   context k RV C ->
-  not_stuck ge e (C a) m ->
-  match a with
-  | Eloc _ _ _ => True
-  | Eval _ _ => True
-  | _ => Cstrategy.invert_expr_prop ge e a m
-  end.
+  ~imm_safe_t k a m ->
+  exists C', In (C', Stuckred) (step_expr RV (C a) m).
 Proof.
-  intros. eapply Cstrategy.not_imm_stuck_inv; eauto.
-Qed. 
-
-Lemma is_val_list_all_values:
-  forall al vtl, is_val_list al = Some vtl -> Cstrategy.exprlist_all_values al.
-Proof.
-  induction al; simpl; intros. auto. 
-  destruct (is_val r1) as [[v ty]|]_eqn; try discriminate.
-  destruct (is_val_list al) as [vtl'|]_eqn; try discriminate.
-  rewrite (is_val_inv _ _ _ Heqo). eauto.
-Qed.
-
-Theorem step_expr_defined:
-  forall a k m C,
-  context k RV C ->
-  not_stuck ge e (C a) m ->
-  step_expr k a m <> None
-with step_exprlist_defined:
-  forall al m C,
-  Cstrategy.contextlist' C ->
-  not_stuck ge e (C al) m ->
-  step_exprlist al m <> None.
-Proof.
-  induction a; intros k m C CTX NS; 
-  rewrite (safe_expr_kind _ _ _ _ CTX NS);
-  rewrite (safe_expr_kind _ _ _ _ CTX NS) in CTX;
-  simpl in *;
-  generalize (safe_inversion _ _ _ _ CTX NS); intro INV.
-(* val *)
-  congruence.
-(* var *)
-  red in INV. destruct INV as [b [P | [P [Q R]]]].
-  rewrite P; rewrite dec_eq_true. apply topred_none.
-  rewrite P; rewrite Q; rewrite R; rewrite dec_eq_true. apply topred_none.
-(* field *)
-  destruct (is_loc a) as [[[b ofs] ty']|]_eqn. 
-  rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. 
-  destruct ty'; try contradiction. destruct INV as [delta EQ]. rewrite EQ. apply topred_none.
-  apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Efield x f ty)); eauto.
-(* valof *)
-  destruct (is_loc a) as [[[b ofs] ty']|]_eqn. 
-  rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. destruct INV as [EQ [v LD]]. subst.
-  rewrite dec_eq_true; rewrite LD; apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Evalof x ty)); eauto.
-(* deref *)
-  destruct (is_val a) as [[v ty']|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [b [ofs EQ]]. subst. 
-  apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Ederef x ty)); eauto.
-(* addrof *) 
-  destruct (is_loc a) as [[[b ofs] ty']|]_eqn. 
-  apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Eaddrof x ty)); eauto.
-(* unop *)
-  destruct (is_val a) as [[v1 ty1]|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
-  rewrite EQ; apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Eunop op x ty)); eauto.
-(* binop *)
-  destruct (is_val a1) as [[v1 ty1]|]_eqn. 
-  destruct (is_val a2) as [[v2 ty2]|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV.
-  rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. destruct INV as [v EQ].
-  rewrite EQ; apply topred_none.
-  apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto.
-  apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto.
-(* cast *)
-  destruct (is_val a) as [[v1 ty1]|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
-  rewrite EQ; apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Ecast x ty)); eauto.
-(* condition *)
-  destruct (is_val a1) as [[v1 ty1]|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
-  rewrite EQ; apply topred_none.
-  apply incontext_none. apply IHa1 with (C := fun x => C(Econdition x a2 a3 ty)); eauto.
-(* sizeof *)
-  apply topred_none.
-(* assign *)
-  destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. 
-  destruct (is_val a2) as [[v2 ty2]|]_eqn. 
-  rewrite (is_loc_inv _ _ _ _ Heqo) in INV.
-  rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. 
-  destruct INV as [v [m' [P [Q R]]]]. 
-  subst. rewrite dec_eq_true; rewrite Q; rewrite R; apply topred_none.
-  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto.
-  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto.
-(* assignop *)
-  destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. 
-  destruct (is_val a2) as [[v2 ty2]|]_eqn. 
-  rewrite (is_loc_inv _ _ _ _ Heqo) in INV.
-  rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. 
-  destruct INV as [v1 [v [v' [m' [P [Q [R [S T]]]]]]]]. 
-  subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none.
-  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto.
-  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto.
-(* postincr *)
-  destruct (is_loc a) as [[[b ofs] ty1]|]_eqn. 
-  rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. 
-  destruct INV as [v1 [v2 [v3 [m' [P [Q [R [S T]]]]]]]]. 
-  subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Epostincr id x ty)); eauto.
-(* comma *)
-  destruct (is_val a1) as [[v1 ty1]|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. rewrite INV.
-  rewrite dec_eq_true; apply topred_none.
-  apply incontext_none. apply IHa1 with (C := fun x => C(Ecomma x a2 ty)); eauto.
-(* call *)
-  destruct (is_val a) as [[vf tyf]|]_eqn. 
-  destruct (is_val_list rargs) as [vtl|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. 
-  destruct INV as [tyargs [tyres [fd [vl [P [Q [R S]]]]]]].
-  eapply is_val_list_all_values; eauto.
-  rewrite P; rewrite Q. 
-  exploit sem_cast_arguments_complete; eauto. intros [vtl' [U V]]. 
-  assert (vtl' = vtl) by congruence. subst. rewrite V. rewrite S. rewrite dec_eq_true. 
-  apply topred_none.
-  apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto.
-  apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto.
-  apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto.
-  apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto.
-  apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto.
-  apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto.
-(* loc *)
-  congruence.
-(* paren *)
-  destruct (is_val a) as [[v1 ty1]|]_eqn. 
-  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
-  rewrite EQ; apply topred_none.
-  apply incontext_none. apply IHa with (C := fun x => C(Eparen x ty)); eauto.
-
-  induction al; intros; simpl.
-(* nil *)
-  congruence.
-(* cons *)
-  apply incontext2_none.
-  apply step_expr_defined with (C := fun x => C(Econs x al)); eauto. 
-  apply Cstrategy.contextlist'_head; auto.
-  apply IHal with (C := fun x => C(Econs r1 x)); auto.
-  apply Cstrategy.contextlist'_tail; auto.
+  intros. 
+  assert (exists C', In (C', Stuckred) (step_expr k a m)).
+    destruct (classic (exists C', In (C', Stuckred) (step_expr k a m))); auto.
+    elim H0. apply not_stuckred_imm_safe. apply not_ex_all_not. auto. 
+  destruct H1 as [C' IN].
+  specialize (step_expr_context _ _ _ H a m). unfold reducts_incl. 
+  intro.
+  exists (fun x => (C (C' x))). apply H1; auto. 
 Qed.
 
-(** Connections between [not_stuck] and [step_expr]. *)
+(** Connections between [imm_safe_t] and [imm_safe] *)
 
-Lemma step_expr_not_imm_stuck:
+Lemma imm_safe_imm_safe_t:
   forall k a m,
-  step_expr k a m <> None ->
-  not_imm_stuck ge e k a m.
-Proof.
-  intros. generalize (step_expr_sound a k m). unfold reducts_ok. 
-  destruct (step_expr k a m) as [ll|]. destruct ll.
-(* value or location *)
-  destruct k; destruct a; simpl; intros; try congruence. 
-  apply not_stuck_loc.
-  apply Csem.not_stuck_val.
-(* reducible *)
-  intros R. destruct p as [C1 rd1]. destruct (R C1 rd1) as [P [a' [U V]]]; auto with coqlib.
-  subst a. red in V. destruct rd1. 
-  eapply not_stuck_lred; eauto. 
-  eapply not_stuck_rred; eauto.
-  destruct V. subst m'. eapply not_stuck_callred; eauto.
-(* stuck *)
-  congruence.
-Qed.
-
-Lemma step_expr_not_stuck:
-  forall a m,
-  step_expr RV a m <> None ->
-  not_stuck ge e a m.
-Proof.
-  intros; red; intros. subst a. 
-  apply step_expr_not_imm_stuck.
-  generalize (step_expr_context _ _ C H0 e' m). unfold reducts_incl. 
-  destruct (step_expr k e' m). congruence.
-  destruct (step_expr RV (C e') m). tauto. congruence.
-Qed.
-
-Lemma not_stuck_step_expr:
-  forall a m,
-  not_stuck ge e a m ->
-  step_expr RV a m <> None.
-Proof.
-  intros. apply step_expr_defined with (C := fun x => x); auto. 
-Qed.
-
-End EXPRS.
-
-(** * External functions and events. *)
-
-Section EVENTS.
-
-Variable F V: Type.
-Variable genv: Genv.t F V.
-
-Definition eventval_of_val (v: val) (t: typ) : option eventval :=
-  match v, t with
-  | Vint i, AST.Tint => Some (EVint i)
-  | Vfloat f, AST.Tfloat => Some (EVfloat f)
-  | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol genv b; Some (EVptr_global id ofs)
-  | _, _ => None
-  end.
-
-Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) :=
-  match vl, tl with
-  | nil, nil => Some nil
-  | v1::vl, t1::tl =>
-      do ev1 <- eventval_of_val v1 t1;
-      do evl <- list_eventval_of_val vl tl;
-      Some (ev1 :: evl)
-  | _, _ => None
-  end.
-
-Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
-  match ev, t with
-  | EVint i, AST.Tint => Some (Vint i)
-  | EVfloat f, AST.Tfloat => Some (Vfloat f)
-  | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol genv id; Some (Vptr b ofs)
-  | _, _ => None
-  end.
-
-Lemma eventval_of_val_sound:
-  forall v t ev, eventval_of_val v t = Some ev -> eventval_match genv ev t v.
-Proof.
-  intros. destruct v; destruct t; simpl in H; inv H.
-  constructor.
-  constructor.
-  destruct (Genv.invert_symbol genv b) as [id|]_eqn; inv H1. 
-  constructor. apply Genv.invert_find_symbol; auto.
-Qed.
-
-Lemma eventval_of_val_complete:
-  forall ev t v, eventval_match genv ev t v -> eventval_of_val v t = Some ev.
+  imm_safe ge e k a m ->
+  imm_safe_t k a m \/
+  exists C, exists a1, exists t, exists a1', exists m',
+    context RV k C /\ a = C a1 /\ rred ge a1 m t a1' m' /\ forall w', ~possible_trace w t w'.
 Proof.
-  induction 1; simpl; auto.
-  rewrite (Genv.find_invert_symbol _ _ H). auto. 
-Qed.
-
-Lemma list_eventval_of_val_sound:
-  forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match genv evl tl vl.
-Proof with try discriminate.
-  induction vl; destruct tl; simpl; intros; inv H.
-  constructor.
-  destruct (eventval_of_val a t) as [ev1|]_eqn...
-  destruct (list_eventval_of_val vl tl) as [evl'|]_eqn...
-  inv H1. constructor. apply eventval_of_val_sound; auto. eauto.
-Qed.
-
-Lemma list_eventval_of_val_complete:
-  forall evl tl vl, eventval_list_match genv evl tl vl -> list_eventval_of_val vl tl = Some evl.
-Proof.
-  induction 1; simpl. auto. 
-  rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto.
-Qed.
-
-Lemma val_of_eventval_sound:
-  forall ev t v, val_of_eventval ev t = Some v -> eventval_match genv ev t v.
-Proof.
-  intros. destruct ev; destruct t; simpl in H; inv H.
-  constructor.
-  constructor.
-  destruct (Genv.find_symbol genv i) as [b|]_eqn; inv H1.
-  constructor. auto.
-Qed.
-
-Lemma val_of_eventval_complete:
-  forall ev t v, eventval_match genv ev t v -> val_of_eventval ev t = Some v.
-Proof.
-  induction 1; simpl; auto. rewrite H; auto.
-Qed.
-
-(** System calls and library functions *)
-
-Definition do_ef_external (name: ident) (sg: signature)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  do args <- list_eventval_of_val vargs (sig_args sg);
-  match nextworld_io w name args with
-  | None => None
-  | Some(res, w') =>
-      do vres <- val_of_eventval res (proj_sig_res sg);
-      Some(w', Event_syscall name args res :: E0, vres, m)
-  end.
-
-Definition do_ef_volatile_load (chunk: memory_chunk)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match vargs with
-  | Vptr b ofs :: nil =>
-      if block_is_volatile genv b then
-        do id <- Genv.invert_symbol genv b;
-        match nextworld_vload w chunk id ofs with
-        | None => None
-        | Some(res, w') =>
-            do vres <- val_of_eventval res (type_of_chunk chunk);
-            Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres, m)
-        end
-      else
-        do v <- Mem.load chunk m b (Int.unsigned ofs);
-        Some(w, E0, v, m)
-  | _ => None
-  end.
-
-Definition do_ef_volatile_store (chunk: memory_chunk)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match vargs with
-  | Vptr b ofs :: v :: nil =>
-      if block_is_volatile genv b then
-        do id <- Genv.invert_symbol genv b;
-        do ev <- eventval_of_val v (type_of_chunk chunk);
-        do w' <- nextworld_vstore w chunk id ofs ev;
-        Some(w', Event_vstore chunk id ofs ev :: nil, Vundef, m)
-      else
-        do m' <- Mem.store chunk m b (Int.unsigned ofs) v;
-        Some(w, E0, Vundef, m')
-  | _ => None
-  end.
-
-Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match Genv.find_symbol genv id with
-  | Some b => do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m
-  | None => None
-  end.
-
-Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match Genv.find_symbol genv id with
-  | Some b => do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m
-  | None => None
-  end.
-
-Definition do_ef_malloc
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match vargs with
-  | Vint n :: nil =>
-      let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in
-      do m'' <- Mem.store Mint32 m' b (-4) (Vint n);
-      Some(w, E0, Vptr b Int.zero, m'')
-  | _ => None
-  end.
-
-Definition do_ef_free
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match vargs with
-  | Vptr b lo :: nil =>
-      do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4);
-      match vsz with
-      | Vint sz =>
-          check (zlt 0 (Int.unsigned sz));
-          do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz);
-          Some(w, E0, Vundef, m')
-      | _ => None
-      end
-  | _ => None
-  end.
-
-Definition memcpy_args_ok
-  (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
-      (al = 1 \/ al = 2 \/ al = 4)
-   /\ sz > 0
-   /\ (al | sz) /\ (al | osrc) /\ (al | odst)
-   /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).
-
-Remark memcpy_check_args:
-  forall sz al bdst odst bsrc osrc,
-  {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.
-Proof with try (right; intuition omega).
-  intros. 
-  assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}).
-    destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto...
-  unfold memcpy_args_ok. destruct X...
-  assert (al > 0) by (intuition omega).
-  destruct (zlt 0 sz)...
-  destruct (Zdivide_dec al sz); auto...
-  destruct (Zdivide_dec al osrc); auto...
-  destruct (Zdivide_dec al odst); auto...
-  assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc}
-           +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}).
-    destruct (eq_block bsrc bdst); auto.
-    destruct (zeq osrc odst); auto.
-    destruct (zle (osrc + sz) odst); auto.
-    destruct (zle (odst + sz) osrc); auto.
-    right; intuition omega.
-  destruct Y... left; intuition omega.
+  intros. inv H. 
+  left. apply imm_safe_t_val.
+  left. apply imm_safe_t_loc.
+  left. eapply imm_safe_t_lred; eauto.
+  destruct (classic (exists w', possible_trace w t w')) as [[w' A] | A].
+  left. eapply imm_safe_t_rred; eauto. 
+  right. exists C; exists e0; exists t; exists e'; exists m'; intuition. apply A; exists w'; auto.
+  left. eapply imm_safe_t_callred; eauto.
 Qed.
 
-Definition do_ef_memcpy (sz al: Z)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match vargs with
-  | Vptr bdst odst :: Vptr bsrc osrc :: nil =>
-      if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then
-        do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz;
-        do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes;
-        Some(w, E0, Vundef, m')
-      else None
-  | _ => None
-  end.
-
-Definition do_ef_annot (text: ident) (targs: list typ)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  do args <- list_eventval_of_val vargs targs;
-  Some(w, Event_annot text args :: E0, Vundef, m).
-
-Definition do_ef_annot_val (text: ident) (targ: typ)
-       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  match vargs with
-  | varg :: nil =>
-      do arg <- eventval_of_val varg targ;
-      Some(w, Event_annot text (arg :: nil) :: E0, varg, m)
-  | _ => None
-  end.
-
-Definition do_external (ef: external_function):
-       world -> list val -> mem -> option (world * trace * val * mem) :=
-  match ef with
-  | EF_external name sg => do_ef_external name sg
-  | EF_builtin name sg => do_ef_external name sg
-  | EF_vload chunk => do_ef_volatile_load chunk
-  | EF_vstore chunk => do_ef_volatile_store chunk
-  | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs
-  | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs
-  | EF_malloc => do_ef_malloc
-  | EF_free => do_ef_free
-  | EF_memcpy sz al => do_ef_memcpy sz al
-  | EF_annot text targs => do_ef_annot text targs
-  | EF_annot_val text targ => do_ef_annot_val text targ
-  end.
-
-Ltac mydestr :=
-  match goal with
-  | [ |- None = Some _ -> _ ] => intro X; discriminate
-  | [ |- Some _ = Some _ -> _ ] => intro X; inv X
-  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
-  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
-  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
-  | _ => idtac
-  end.
-
-Lemma do_ef_external_sound:
-  forall ef w vargs m w' t vres m',
-  do_external ef w vargs m = Some(w', t, vres, m') ->
-  external_call ef genv vargs m t vres m' /\ possible_trace w t w'.
-Proof with try congruence.
-  intros until m'.
-  assert (IO: forall name sg,
-             do_ef_external name sg w vargs m = Some(w', t, vres, m') ->
-             extcall_io_sem name sg genv vargs m t vres m' /\ possible_trace w t w').
-    intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr.
-    split. econstructor. apply list_eventval_of_val_sound; auto. 
-    apply val_of_eventval_sound; auto. 
-    econstructor. constructor; eauto. constructor.
-
-  assert (VLOAD: forall chunk vargs,
-    do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') ->
-    volatile_load_sem chunk genv vargs m t vres m' /\ possible_trace w t w').
-  intros chunk vargs'.
-  unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... 
-  mydestr. destruct p as [res w'']; mydestr.
-  split. constructor. apply Genv.invert_find_symbol; auto. auto. 
-  apply val_of_eventval_sound; auto. 
-  econstructor. constructor; eauto. constructor.
-  split. constructor; auto. constructor.
+(** A state can "crash the world" if it can make an observable transition
+  whose trace is not accepted by the external world. *)
 
-  assert (VSTORE: forall chunk vargs,
-    do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') ->
-    volatile_store_sem chunk genv vargs m t vres m' /\ possible_trace w t w').
-  intros chunk vargs'.
-  unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... 
-  mydestr.
-  split. constructor. apply Genv.invert_find_symbol; auto. auto. 
-  apply eventval_of_val_sound; auto. 
-  econstructor. constructor; eauto. constructor.
-  split. constructor; auto. constructor.
+Definition can_crash_world (w: world) (S: state) : Prop :=
+  exists t, exists S', Csem.step ge S t S' /\ forall w', ~possible_trace w t w'.
 
-  destruct ef; simpl.
-(* EF_external *)
-  auto. 
-(* EF_builtin *)
-  auto.
-(* EF_vload *)
-  auto.
-(* EF_vstore *)
-  auto.
-(* EF_vload_global *)
-  rewrite volatile_load_global_charact.
-  unfold do_ef_volatile_load_global. destruct (Genv.find_symbol genv)...
-  intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto.
-(* EF_vstore_global *)
-  rewrite volatile_store_global_charact.
-  unfold do_ef_volatile_store_global. destruct (Genv.find_symbol genv)...
-  intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto.
-(* EF_malloc *)
-  unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs...
-  destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr.
-  split. econstructor; eauto. constructor.
-(* EF_free *)
-  unfold do_ef_free. destruct vargs... destruct v... destruct vargs... 
-  mydestr. destruct v... mydestr. 
-  split. econstructor; eauto. omega. constructor.
-(* EF_memcpy *)
-  unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... 
-  destruct v... destruct vargs... mydestr. red in m0. 
-  split. econstructor; eauto; tauto. constructor.
-(* EF_annot *)
-  unfold do_ef_annot. mydestr. 
-  split. constructor. apply list_eventval_of_val_sound; auto.
-  econstructor. constructor; eauto. constructor.
-(* EF_annot_val *)
-  unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. 
-  split. constructor. apply eventval_of_val_sound; auto.
-  econstructor. constructor; eauto. constructor.
-Qed.
-
-Lemma do_ef_external_complete:
-  forall ef w vargs m w' t vres m',
-  external_call ef genv vargs m t vres m' -> possible_trace w t w' ->
-  do_external ef w vargs m = Some(w', t, vres, m').
+Theorem not_imm_safe_t:
+  forall K C a m f k,
+  context K RV C ->
+  ~imm_safe_t K a m ->
+  Csem.step ge (ExprState f (C a) k e m) E0 Stuckstate \/ can_crash_world w (ExprState f (C a) k e m).
 Proof.
-  intros.
-  assert (IO: forall name sg,
-             extcall_io_sem name sg genv vargs m t vres m' ->
-             do_ef_external name sg w vargs m = Some (w', t, vres, m')).
-    intros. inv H1. inv H0. inv H8. inv H6. 
-    unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. 
-    rewrite (val_of_eventval_complete _ _ _ H3). auto.
- 
-  assert (VLOAD: forall chunk vargs,
-             volatile_load_sem chunk genv vargs m t vres m' ->
-             do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')).
-  intros. inv H1; unfold do_ef_volatile_load.
-  inv H0. inv H9. inv H7. 
-  rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). rewrite H10. 
-  rewrite (val_of_eventval_complete _ _ _ H4). auto.
-  inv H0. rewrite H2. rewrite H3. auto.
-
-  assert (VSTORE: forall chunk vargs,
-             volatile_store_sem chunk genv vargs m t vres m' ->
-             do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')).
-  intros. inv H1; unfold do_ef_volatile_store.
-  inv H0. inv H9. inv H7. 
-  rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2).
-  rewrite (eventval_of_val_complete _ _ _ H4). rewrite H10. auto.
-  inv H0. rewrite H2. rewrite H3. auto.
-
-  destruct ef; simpl in *.
-(* EF_external *)
-  auto.
-(* EF_builtin *)
-  auto.
-(* EF_vload *)
-  auto.
-(* EF_vstore *)
-  auto.
-(* EF_vload_global *)
-  rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. 
-  unfold do_ef_volatile_load_global. rewrite P. auto. 
-(* EF_vstore *)
-  rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. 
-  unfold do_ef_volatile_store_global. rewrite P. auto. 
-(* EF_malloc *)
-  inv H; unfold do_ef_malloc. 
-  inv H0. rewrite H1. rewrite H2. auto.
-(* EF_free *)
-  inv H; unfold do_ef_free.
-  inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega.
-(* EF_memcpy *)
-  inv H; unfold do_ef_memcpy.
-  inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto.
-  red. tauto. 
-(* EF_annot *)
-  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. 
-  rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
-(* EF_annot_val *)
-  inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. 
-  rewrite (eventval_of_val_complete _ _ _ H1). auto.
+  intros. destruct (classic (imm_safe ge e K a m)).
+  exploit imm_safe_imm_safe_t; eauto. 
+  intros [A | [C1 [a1 [t [a1' [m' [A [B [D E]]]]]]]]]. contradiction.
+  right. red. exists t; econstructor; split; auto. 
+  left. rewrite B. eapply step_rred with (C := fun x => C(C1 x)). eauto. eauto. 
+  left. left. eapply step_stuck; eauto.
 Qed.
 
-End EVENTS.
+End EXPRS.
 
 (** * Transitions over states. *)
 
@@ -1560,7 +1773,7 @@ Proof.
   rewrite H; rewrite IHalloc_variables; auto. 
 Qed.
 
-Function sem_bind_parameters (e: env) (m: mem) (l: list (ident * type)) (lv: list val) 
+Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list val) 
                           {struct l} : option mem :=
   match l, lv  with
   | nil, nil => Some m
@@ -1568,37 +1781,39 @@ Function sem_bind_parameters (e: env) (m: mem) (l: list (ident * type)) (lv: lis
       match PTree.get id e with
          | Some (b, ty') =>
              check (type_eq ty ty');
-             do m1 <- store_value_of_type ty m b Int.zero v1;
-             sem_bind_parameters e m1 params lv
+             do w', t, m1 <- do_assign_loc w ty m b Int.zero v1;
+             match t with nil => sem_bind_parameters w e m1 params lv | _ => None end
         | None => None
       end
    | _, _ => None
 end.
 
-Lemma sem_bind_parameters_sound : forall e m l lv m',
-  sem_bind_parameters e m l lv = Some m' -> 
-  bind_parameters e m l lv m'.
+Lemma sem_bind_parameters_sound : forall w e m l lv m',
+  sem_bind_parameters w e m l lv = Some m' -> 
+  bind_parameters ge e m l lv m'.
 Proof.
-   intros; functional induction (sem_bind_parameters e m l lv); try discriminate.
-   inversion H; constructor; auto.  
-   econstructor; eauto.
+   intros; functional induction (sem_bind_parameters w e m l lv); try discriminate.
+   inversion H; constructor; auto.
+   exploit do_assign_loc_sound; eauto. intros [A B]. econstructor; eauto.
 Qed.
 
-Lemma sem_bind_parameters_complete : forall e m l lv m',
-  bind_parameters e m l lv m' ->
-  sem_bind_parameters e m l lv = Some m'.
+Lemma sem_bind_parameters_complete : forall w e m l lv m',
+  bind_parameters ge e m l lv m' ->
+  sem_bind_parameters w e m l lv = Some m'.
 Proof.
    induction 1; simpl; auto.
-   rewrite H. rewrite dec_eq_true. 
-   destruct (store_value_of_type ty m b Int.zero v1); try discriminate.
-   inv H0; auto.
+   rewrite H. rewrite dec_eq_true.
+   assert (possible_trace w E0 w) by constructor.
+   rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H2).
+   simpl. auto. 
 Qed.
 
 Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) :=
   match snd C_rd with
   | Lred a m => (E0, ExprState f (fst C_rd a) k e m)
-  | Rred a m => (E0, ExprState f (fst C_rd a) k e m)
+  | Rred a m t => (t, ExprState f (fst C_rd a) k e m)
   | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m)
+  | Stuck => (E0, Stuckstate)
   end.
 
 Local Open Scope list_monad_scope.
@@ -1637,10 +1852,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
         end
 
       | None =>
-          match step_expr e RV a m with
-          | None => nil
-          | Some ll => map (expr_final_state f k e) ll
-          end
+          map (expr_final_state f k e) (step_expr e w RV a m)
       end
 
   | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m)
@@ -1674,9 +1886,9 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
       ret (Returnstate Vundef (call_cont k) m')
   | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m)
   | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => 
-     check (type_eq f.(fn_return) Tvoid);
-     do m' <- Mem.free_list m (blocks_of_env e);
-     ret (Returnstate Vundef k m')
+      check type_eq (f.(fn_return)) Tvoid;
+      do m' <- Mem.free_list m (blocks_of_env e);
+      ret (Returnstate Vundef k m')
 
   | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m)
   | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m)
@@ -1692,10 +1904,10 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
   | Callstate (Internal f) vargs k m =>
       check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f)));
       let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in
-      do m2 <- sem_bind_parameters e m1 f.(fn_params) vargs;
+      do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs;
       ret (State f f.(fn_body) k e m2)
   | Callstate (External ef _ _) vargs k m =>
-      match do_external _ _ ge ef w vargs m with
+      match do_external ef w vargs m with
       | None => nil
       | Some(w',t,v,m') => (t, Returnstate v k m') :: nil
       end
@@ -1721,9 +1933,11 @@ Ltac myinv :=
 
 Hint Extern 3 => exact I.
 
-Lemma do_step_sound:
-  forall w S t S', In (t, S') (do_step w S) -> Csem.step ge S t S'.
-Proof with try (right; econstructor; eauto; fail).
+Theorem do_step_sound:
+  forall w S t S',
+  In (t, S') (do_step w S) ->
+  Csem.step ge S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S).
+Proof with try (left; right; econstructor; eauto; fail).
   intros until S'. destruct S; simpl.
 (* State *)
   destruct s; myinv...
@@ -1742,82 +1956,87 @@ Proof with try (right; econstructor; eauto; fail).
   destruct k; myinv...
   destruct v; myinv...
   (* expression reduces *)
-  destruct (step_expr e RV r m) as [ll|]_eqn; try contradiction. intros.
-  exploit list_in_map_inv; eauto. intros [[C rd] [A B]].
-  generalize (step_expr_sound e r RV m). unfold reducts_ok. rewrite Heqr0. 
-  destruct ll; try contradiction. intros SOUND. 
-  exploit SOUND; eauto. intros [CTX [a [EQ RD]]]. subst r. 
-  unfold expr_final_state in A. simpl in A. left.
-  destruct rd; inv A; simpl in RD. 
-  apply step_lred. auto. apply step_expr_not_stuck; congruence. auto. 
-  apply step_rred. auto. apply step_expr_not_stuck; congruence. auto.
-  destruct RD; subst m'. apply Csem.step_call. auto.  apply step_expr_not_stuck; congruence. auto.
+  intros. exploit list_in_map_inv; eauto. intros [[C rd] [A B]].
+  generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q].
+  exploit P; eauto. intros [a' [k' [CTX [EQ RD]]]].
+  unfold expr_final_state in A. simpl in A.
+  destruct k'; destruct rd; inv A; simpl in RD; try contradiction. 
+  (* lred *)
+  left; left; apply step_lred; auto.
+  (* stuck lred *)
+  exploit not_imm_safe_t; eauto. intros [R | R]; eauto.
+  (* rred *)
+  destruct RD. left; left; apply step_rred; auto.
+  (* callred *)
+  destruct RD; subst m'. left; left; apply step_call; eauto.
+  (* stuck rred *)
+  exploit not_imm_safe_t; eauto. intros [R | R]; eauto.
 (* callstate *)
   destruct fd; myinv.
   (* internal *)
   destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1]_eqn.
-  myinv. right; apply step_internal_function with m1. auto. 
+  myinv. left; right; apply step_internal_function with m1. auto. 
   change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. 
-  apply do_alloc_variables_sound. apply sem_bind_parameters_sound; auto.
+  apply do_alloc_variables_sound. eapply sem_bind_parameters_sound; eauto.
   (* external *)
-  destruct p as [[[w' tr] v] m']. myinv. right; constructor. 
+  destruct p as [[[w' tr] v] m']. myinv. left; right; constructor. 
   eapply do_ef_external_sound; eauto.
 (* returnstate *)
   destruct k; myinv...
+(* stuckstate *)
+  contradiction.
 Qed.
 
 Remark estep_not_val:
   forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None.
 Proof.
   intros. 
-  assert (forall b from to C, context from to C -> (C = fun x => x) \/ is_val (C b) = None).
+  assert (forall b from to C, context from to C -> (from = to /\ C = fun x => x) \/ is_val (C b) = None).
     induction 1; simpl; auto. 
   inv H. 
-  destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto.
-  destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto.
-  destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto.
+  destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
+  destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
+  destruct (H0 a0 _ _ _ H9) as [[A B] | A]. subst. inv H8; auto. auto.
+  destruct (H0 a0 _ _ _ H8) as [[A B] | A]. subst. destruct a0; auto. elim H9. constructor. auto.
 Qed.
 
-Lemma do_step_complete:
+Theorem do_step_complete:
   forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S).
 Proof with (unfold ret; auto with coqlib).
-  intros until w'; intro PT; intros. 
+  intros until w'; intros PT H.
   destruct H. 
   (* Expression step *)
   inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL.
 (* lred *)
   unfold do_step; rewrite NOTVAL.
-  destruct (step_expr e RV (C a) m) as [ll|]_eqn.
   change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')).
   apply in_map.
-  generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl.
-  rewrite Heqr. destruct (step_expr e LV a m) as [ll'|]_eqn; try tauto.
-  intro. replace C with (fun x => C x). apply H3. 
-  rewrite (lred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib.
+  generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
+  intro. replace C with (fun x => C x). apply H2. 
+  rewrite (lred_topred _ _ _ _ _ _ H0). unfold topred; auto with coqlib.
   apply extensionality; auto.
-  exploit not_stuck_step_expr; eauto.
 (* rred *)
   unfold do_step; rewrite NOTVAL.
-  destruct (step_expr e RV (C a) m) as [ll|]_eqn.
-  change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m')).
+  change (t, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m' t)).
   apply in_map.
-  generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl.
-  rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto.
-  intro. replace C with (fun x => C x). apply H3. 
-  rewrite (rred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib.
+  generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
+  intro. replace C with (fun x => C x). apply H2. 
+  rewrite (rred_topred _ _ _ _ _ _ _ _ H0 PT). unfold topred; auto with coqlib.
   apply extensionality; auto.
-  exploit not_stuck_step_expr; eauto.
 (* callred *)
   unfold do_step; rewrite NOTVAL.
-  destruct (step_expr e RV (C a) m) as [ll|]_eqn.
   change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)).
   apply in_map.
-  generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl.
-  rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto.
-  intro. replace C with (fun x => C x). apply H3. 
-  rewrite (callred_topred _ _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib.
+  generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl.
+  intro. replace C with (fun x => C x). apply H2. 
+  rewrite (callred_topred _ _ _ _ _ _ _ H0). unfold topred; auto with coqlib.
   apply extensionality; auto.
-  exploit not_stuck_step_expr; eauto.
+(* stuck *)
+  exploit not_imm_safe_stuck_red. eauto. red; intros; elim H1. eapply imm_safe_t_imm_safe. eauto.
+  instantiate (1 := w). intros [C' IN].
+  simpl do_step. rewrite NOTVAL. 
+  change (E0, Stuckstate) with (expr_final_state f k e (C', Stuckred)).
+  apply in_map. auto. 
 
   (* Statement step *)
   inv H; simpl...
@@ -1835,13 +2054,13 @@ Proof with (unfold ret; auto with coqlib).
   destruct H0; subst x...
   rewrite H0...
   rewrite H0; rewrite H1...
-  rewrite pred_dec_true; auto. rewrite H2. red in H0. destruct k; try contradiction...
+  rewrite H1. rewrite dec_eq_true. rewrite H2. red in H0. destruct k; try contradiction...
   destruct H0; subst x...
   rewrite H0...
 
   (* Call step *)
   rewrite pred_dec_true; auto. rewrite (do_alloc_variables_complete _ _ _ _ _ H1).
-  rewrite (sem_bind_parameters_complete _ _ _ _ _ H2)...
+  rewrite (sem_bind_parameters_complete _ _ _ _ _ _ H2)...
   exploit do_ef_external_complete; eauto. intro EQ; rewrite EQ. auto with coqlib.
 Qed.
 
@@ -1854,7 +2073,7 @@ Definition do_initial_state (p: program): option (genv * state) :=
   do m0 <- Genv.init_mem p;
   do b <- Genv.find_symbol ge p.(prog_main);
   do f <- Genv.find_funct_ptr ge b;
-  check (type_eq (type_of_fundef f) (Tfunction Tnil (Tint I32 Signed)));
+  check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s));
   Some (ge, Callstate f nil Kstop m0).
 
 Definition at_final_state (S: state): option int :=