Merge of branch seq-and-or. See Changelog for details.

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

1 files changed, 291 insertions, 471 deletions

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index e4c451b..a8624e9 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -56,7 +56,6 @@ Inductive expr : Type :=
   | Eunop: unary_operation -> expr -> type -> expr  (**r unary operation *)
   | Ebinop: binary_operation -> expr -> expr -> type -> expr (**r binary operation *)
   | Ecast: expr -> type -> expr   (**r type cast ([(ty) e]) *)
-  | Econdition: expr -> expr -> expr -> type -> expr (**r conditional ([e1 ? e2 : e3]) *)
   | Efield: expr -> ident -> type -> expr. (**r access to a member of a struct or union *)
 
 (** [sizeof] and [alignof] are derived forms. *)
@@ -77,7 +76,6 @@ Definition typeof (e: expr) : type :=
   | Eunop _ _ ty => ty
   | Ebinop _ _ _ ty => ty
   | Ecast _ ty => ty
-  | Econdition _ _ _ ty => ty
   | Efield _ _ ty => ty
   end.
 
@@ -86,7 +84,8 @@ Definition typeof (e: expr) : type :=
 (** Clight statements are similar to those of Compcert C, with the addition
   of assigment (of a rvalue to a lvalue), assignment to a temporary,
   and function call (with assignment of the result to a temporary).
-  The [for] loop is slightly simplified: there is no initial statement. *)
+  The three C loops are replaced by a single infinite loop [Sloop s1 s2]
+  that executes [s1] then [s2] repeatedly.  A [continue] in [s1] branches to [s2]. *)
 
 Definition label := ident.
 
@@ -94,13 +93,11 @@ Inductive statement : Type :=
   | Sskip : statement                   (**r do nothing *)
   | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
   | Sset : ident -> expr -> statement   (**r assignment [tempvar = rvalue] *)
-  | Svolread : ident -> expr -> statement (**r volatile read [tempvar = volatile lvalue] *)
   | Scall: option ident -> expr -> list expr -> statement (**r function call *)
+  | Sbuiltin: option ident -> external_function -> typelist -> list expr -> statement (**r builtin invocation *)
   | Ssequence : statement -> statement -> statement  (**r sequence *)
   | Sifthenelse : expr  -> statement -> statement -> statement (**r conditional *)
-  | Swhile : expr -> statement -> statement   (**r [while] loop *)
-  | Sdowhile : expr -> statement -> statement (**r [do] loop *)
-  | Sfor': expr -> statement -> statement -> statement (**r [for] loop *)
+  | Sloop: statement -> statement -> statement (**r infinite loop *)
   | Sbreak : statement                      (**r [break] statement *)
   | Scontinue : statement                   (**r [continue] statement *)
   | Sreturn : option expr -> statement      (**r [return] statement *)
@@ -112,10 +109,16 @@ with labeled_statements : Type :=            (**r cases of a [switch] *)
   | LSdefault: statement -> labeled_statements
   | LScase: int -> statement -> labeled_statements -> labeled_statements.
 
-(** The full [for] loop is a derived form. *)
+(** The C loops are derived forms. *)
 
-Definition Sfor (s1: statement) (e2: expr) (s3 s4: statement) :=
-  Ssequence s1 (Sfor' e2 s3 s4).
+Definition Swhile (e: expr) (s: statement) :=
+  Sloop (Ssequence (Sifthenelse e Sskip Sbreak) s) Sskip.
+
+Definition Sdowhile (s: statement) (e: expr) :=
+  Sloop s (Sifthenelse e Sskip Sbreak).
+
+Definition Sfor (s1: statement) (e2: expr) (s3: statement) (s4: statement) :=
+  Ssequence s1 (Sloop (Ssequence (Sifthenelse e2 Sskip Sbreak) s3) s4).
 
 (** ** Functions *)
 
@@ -183,6 +186,80 @@ Definition empty_env: env := (PTree.empty (block * type)).
 
 Definition temp_env := PTree.t val.
 
+(** [deref_loc ty m b ofs v] computes the value of a datum
+  of type [ty] residing in memory [m] at block [b], offset [ofs].
+  If the type [ty] indicates an access by value, the corresponding
+  memory load is performed.  If the type [ty] indicates an access by
+  reference or by copy, the pointer [Vptr b ofs] is returned. *)
+
+Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop :=
+  | deref_loc_value: forall chunk v,
+      access_mode ty = By_value chunk ->
+      Mem.loadv chunk m (Vptr b ofs) = Some v ->
+      deref_loc ty m b ofs v
+  | deref_loc_reference:
+      access_mode ty = By_reference ->
+      deref_loc ty m b ofs (Vptr b ofs)
+  | deref_loc_copy:
+      access_mode ty = By_copy ->
+      deref_loc ty m b ofs (Vptr b ofs).
+
+(** Symmetrically, [assign_loc ty m b ofs v m'] returns the
+  memory state after storing the value [v] in the datum
+  of type [ty] residing in memory [m] at block [b], offset [ofs].
+  This is allowed only if [ty] indicates an access by value or by copy.
+  [m'] is the updated memory state. *)
+
+Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int):
+                                            val -> mem -> Prop :=
+  | assign_loc_value: forall v chunk m',
+      access_mode ty = By_value chunk ->
+      Mem.storev chunk m (Vptr b ofs) v = Some m' ->
+      assign_loc ty m b ofs v m'
+  | assign_loc_copy: forall b' ofs' bytes m',
+      access_mode ty = By_copy ->
+      (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' ->
+      Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty) = Some bytes ->
+      Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' ->
+      assign_loc ty m b ofs (Vptr b' ofs') m'.
+
+(** Initialization of local variables that are parameters to a function.
+  [bind_parameters e m1 params args m2] stores the values [args]
+  in the memory blocks corresponding to the variables [params].
+  [m1] is the initial memory state and [m2] the final memory state. *)
+
+Inductive bind_parameters (e: env):
+                           mem -> list (ident * type) -> list val ->
+                           mem -> Prop :=
+  | bind_parameters_nil:
+      forall m,
+      bind_parameters e m nil nil m
+  | bind_parameters_cons:
+      forall m id ty params v1 vl b m1 m2,
+      PTree.get id e = Some(b, ty) ->
+      assign_loc ty m b Int.zero v1 m1 ->
+      bind_parameters e m1 params vl m2 ->
+      bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2.
+
+(** Initialization of temporary variables *)
+
+Fixpoint create_undef_temps (temps: list (ident * type)) : temp_env :=
+  match temps with
+  | nil => PTree.empty val
+  | (id, t) :: temps' => PTree.set id Vundef (create_undef_temps temps')
+ end.
+
+(** Optional assignment to a temporary *)
+
+Definition set_opttemp (optid: option ident) (v: val) (le: temp_env) :=
+  match optid with
+  | None => le
+  | Some id => PTree.set id v le
+  end.
+
 (** Selection of the appropriate case of a [switch], given the value [n]
   of the selector expression. *)
 
@@ -250,19 +327,13 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr a2 v2 ->
       sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
       eval_expr (Ebinop op a1 a2 ty) v
-  | eval_Econdition: forall a1 a2 a3 ty v1 b v' v,
-      eval_expr a1 v1 ->
-      bool_val v1 (typeof a1) = Some b ->
-      eval_expr (if b then a2 else a3) v' ->
-      sem_cast v' (typeof (if b then a2 else a3)) ty = Some v ->
-      eval_expr (Econdition a1 a2 a3 ty) v
   | eval_Ecast:   forall a ty v1 v,
       eval_expr a v1 ->
       sem_cast v1 (typeof a) ty = Some v ->
       eval_expr (Ecast a ty) v
   | eval_Elvalue: forall a loc ofs v,
-      eval_lvalue a loc ofs -> type_is_volatile (typeof a) = false ->
-      deref_loc ge (typeof a) m loc ofs E0 v ->
+      eval_lvalue a loc ofs -> 
+      deref_loc (typeof a) m loc ofs v ->
       eval_expr a v
 
 (** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
@@ -318,10 +389,8 @@ End EXPR.
 Inductive cont: Type :=
   | Kstop: cont
   | Kseq: statement -> cont -> cont       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
-  | Kwhile: expr -> statement -> cont -> cont       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
-  | Kdowhile: expr -> statement -> cont -> cont       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
-  | Kfor2: expr -> statement -> statement -> cont -> cont       (**r [Kfor2 e2 e3 s k] = after [s] in [for'(e2;e3) s] *)
-  | Kfor3: expr -> statement -> statement -> cont -> cont       (**r [Kfor3 e2 e3 s k] = after [e3] in [for'(e2;e3) s] *)
+  | Kloop1: statement -> statement -> cont -> cont (**r [Kloop1 s1 s2 k] = after [s1] in [Sloop s1 s2] *)
+  | Kloop2: statement -> statement -> cont -> cont (**r [Kloop1 s1 s2 k] = after [s2] in [Sloop s1 s2] *)
   | Kswitch: cont -> cont       (**r catches [break] statements arising out of [switch] *)
   | Kcall: option ident ->                  (**r where to store result *)
            function ->                      (**r calling function *)
@@ -334,10 +403,8 @@ Inductive cont: Type :=
 Fixpoint call_cont (k: cont) : cont :=
   match k with
   | Kseq s k => call_cont k
-  | Kwhile e s k => call_cont k
-  | Kdowhile e s k => call_cont k
-  | Kfor2 e2 e3 s k => call_cont k
-  | Kfor3 e2 e3 s k => call_cont k
+  | Kloop1 s1 s2 k => call_cont k
+  | Kloop2 s1 s2 k => call_cont k
   | Kswitch k => call_cont k
   | _ => k
   end.
@@ -385,14 +452,10 @@ Fixpoint find_label (lbl: label) (s: statement) (k: cont)
       | Some sk => Some sk
       | None => find_label lbl s2 k
       end
-  | Swhile a s1 =>
-      find_label lbl s1 (Kwhile a s1 k)
-  | Sdowhile a s1 =>
-      find_label lbl s1 (Kdowhile a s1 k)
-  | Sfor' a2 a3 s1 =>
-      match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
+  | Sloop s1 s2 =>
+      match find_label lbl s1 (Kloop1 s1 s2 k) with
       | Some sk => Some sk
-      | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
+      | None => find_label lbl s2 (Kloop2 s1 s2 k)
       end
   | Sswitch e sl =>
       find_label_ls lbl sl (Kswitch k)
@@ -416,26 +479,19 @@ with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont)
 
 Inductive step: state -> trace -> state -> Prop :=
 
-  | step_assign:   forall f a1 a2 k e le m loc ofs v2 v t m',
+  | step_assign:   forall f a1 a2 k e le m loc ofs v2 v m',
       eval_lvalue e le m a1 loc ofs ->
       eval_expr e le m a2 v2 ->
       sem_cast v2 (typeof a2) (typeof a1) = Some v ->
-      assign_loc ge (typeof a1) m loc ofs v t m' ->
+      assign_loc (typeof a1) m loc ofs v m' ->
       step (State f (Sassign a1 a2) k e le m)
-         t (State f Sskip k e le m')
+        E0 (State f Sskip k e le m')
 
   | step_set:   forall f id a k e le m v,
       eval_expr e le m a v ->
       step (State f (Sset id a) k e le m)
         E0 (State f Sskip k e (PTree.set id v le) m)
 
-  | step_vol_read:   forall f id a k e le m loc ofs t v,
-      eval_lvalue e le m a loc ofs ->
-      deref_loc ge (typeof a) m loc ofs t v ->
-      type_is_volatile (typeof a) = true ->
-      step (State f (Svolread id a) k e le m)
-         t (State f Sskip k e (PTree.set id v le) m)
-
   | step_call:   forall f optid a al k e le m tyargs tyres vf vargs fd,
       classify_fun (typeof a) = fun_case_f tyargs tyres ->
       eval_expr e le m a vf ->
@@ -445,6 +501,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid a al) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
+  | step_builtin:   forall f optid ef tyargs al k e le m vargs t vres m',
+      eval_exprlist e le m al tyargs vargs ->
+      external_call ef ge vargs m t vres m' ->
+      step (State f (Sbuiltin optid ef tyargs al) k e le m)
+         t (State f Sskip k e (set_opttemp optid vres le) m')
+
   | step_seq:  forall f s1 s2 k e le m,
       step (State f (Ssequence s1 s2) k e le m)
         E0 (State f s1 (Kseq s2 k) e le m)
@@ -464,65 +526,21 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sifthenelse a s1 s2) k e le m)
         E0 (State f (if b then s1 else s2) k e le m)
 
-  | step_while_false: forall f a s k e le m v,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some false ->
-      step (State f (Swhile a s) k e le m)
-        E0 (State f Sskip k e le m)
-  | step_while_true: forall f a s k e le m v,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some true ->
-      step (State f (Swhile a s) k e le m)
-        E0 (State f s (Kwhile a s k) e le m)
-  | step_skip_or_continue_while: forall f x a s k e le m,
-      x = Sskip \/ x = Scontinue ->
-      step (State f x (Kwhile a s k) e le m)
-        E0 (State f (Swhile a s) k e le m)
-  | step_break_while: forall f a s k e le m,
-      step (State f Sbreak (Kwhile a s k) e le m)
-        E0 (State f Sskip k e le m)
-
-  | step_dowhile: forall f a s k e le m,
-      step (State f (Sdowhile a s) k e le m)
-        E0 (State f s (Kdowhile a s k) e le m)
-  | step_skip_or_continue_dowhile_false: forall f x a s k e le m v,
+  | step_loop: forall f s1 s2 k e le m,
+      step (State f (Sloop s1 s2) k e le m)
+        E0 (State f s1 (Kloop1 s1 s2 k) e le m)
+  | step_skip_or_continue_loop1:  forall f s1 s2 k e le m x,
       x = Sskip \/ x = Scontinue ->
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some false ->
-      step (State f x (Kdowhile a s k) e le m)
-        E0 (State f Sskip k e le m)
-  | step_skip_or_continue_dowhile_true: forall f x a s k e le m v,
-      x = Sskip \/ x = Scontinue ->
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some true ->
-      step (State f x (Kdowhile a s k) e le m)
-        E0 (State f (Sdowhile a s) k e le m)
-  | step_break_dowhile: forall f a s k e le m,
-      step (State f Sbreak (Kdowhile a s k) e le m)
-        E0 (State f Sskip k e le m)
-
-  | step_for_false: forall f a2 a3 s k e le m v,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some false ->
-      step (State f (Sfor' a2 a3 s) k e le m)
-        E0 (State f Sskip k e le m)
-  | step_for_true: forall f a2 a3 s k e le m v,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some true ->
-      step (State f (Sfor' a2 a3 s) k e le m)
-        E0 (State f s (Kfor2 a2 a3 s k) e le m)
-  | step_skip_or_continue_for2: forall f x a2 a3 s k e le m,
-      x = Sskip \/ x = Scontinue ->
-      step (State f x (Kfor2 a2 a3 s k) e le m)
-        E0 (State f a3 (Kfor3 a2 a3 s k) e le m)
-  | step_break_for2: forall f a2 a3 s k e le m,
-      step (State f Sbreak (Kfor2 a2 a3 s k) e le m)
+      step (State f x (Kloop1 s1 s2 k) e le m)
+        E0 (State f s2 (Kloop2 s1 s2 k) e le m)
+  | step_break_loop1:  forall f s1 s2 k e le m,
+      step (State f Sbreak (Kloop1 s1 s2 k) e le m)
         E0 (State f Sskip k e le m)
-  | step_skip_for3: forall f a2 a3 s k e le m,
-      step (State f Sskip (Kfor3 a2 a3 s k) e le m)
-        E0 (State f (Sfor' a2 a3 s) k e le m)
-  | step_break_for3: forall f a2 a3 s k e le m,
-      step (State f Sbreak (Kfor3 a2 a3 s k) e le m)
+  | step_skip_loop2: forall f s1 s2 k e le m,
+      step (State f Sskip (Kloop2 s1 s2 k) e le m)
+        E0 (State f (Sloop s1 s2) k e le m)
+  | step_break_loop2: forall f s1 s2 k e le m,
+      step (State f Sbreak (Kloop2 s1 s2 k) e le m)
         E0 (State f Sskip k e le m)
 
   | step_return_0: forall f k e le m m',
@@ -566,25 +584,76 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_internal_function: forall f vargs k m e m1 m2,
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
       step (Callstate (Internal f) vargs k m)
-        E0 (State f f.(fn_body) k e (PTree.empty val) m2)
+        E0 (State f f.(fn_body) k e (create_undef_temps f.(fn_temps)) m2)
 
   | step_external_function: forall ef targs tres vargs k m vres t m',
-      external_call ef  ge vargs m t vres m' ->
+      external_call ef ge vargs m t vres m' ->
       step (Callstate (External ef targs tres) vargs k m)
          t (Returnstate vres k m')
 
-  | step_returnstate_none: forall v f e le k m,
-      step (Returnstate v (Kcall None f e le k) m)
-        E0 (State f Sskip k e le m)
-  | step_returnstate_some: forall v id f e le k m,
-      step (Returnstate v (Kcall (Some id) f e le k) m)
-        E0 (State f Sskip k e (PTree.set id v le) m).
+  | step_returnstate: forall v optid f e le k m,
+      step (Returnstate v (Kcall optid f e le k) m)
+        E0 (State f Sskip k e (set_opttemp optid v le) m).
 
+(** ** Whole-program semantics *)
+
+(** Execution of whole programs are described as sequences of transitions
+  from an initial state to a final state.  An initial state is a [Callstate]
+  corresponding to the invocation of the ``main'' function of the program
+  without arguments and with an empty continuation. *)
+
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b f m0,
+      let ge := Genv.globalenv p in
+      Genv.init_mem p = Some m0 ->
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      type_of_fundef f = Tfunction Tnil type_int32s ->
+      initial_state p (Callstate f nil Kstop m0).
+
+(** A final state is a [Returnstate] with an empty continuation. *)
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall r m,
+      final_state (Returnstate (Vint r) Kstop m) r.
+
+End SEMANTICS.
+
+(** Wrapping up these definitions in a small-step semantics. *)
+
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).
+
+(** This semantics is receptive to changes in events. *)
+
+Lemma semantics_receptive:
+  forall (p: program), receptive (semantics p).
+Proof.
+  intros. constructor; simpl; intros.
+(* receptiveness *)
+  assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2).
+    intros. subst. inv H0. exists s1; auto.
+  inversion H; subst; auto.
+  (* builtin *)
+  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
+  econstructor; econstructor; eauto.
+  (* external *)
+  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
+  exists (Returnstate vres2 k m2). econstructor; eauto.
+(* trace length *)
+  red; intros. inv H; simpl; try omega.
+  eapply external_call_trace_length; eauto.
+  eapply external_call_trace_length; eauto.
+Qed.
 
 (** * Alternate big-step semantics *)
 
+Section BIGSTEP.
+
+Variable ge: genv.
+
 (** ** Big-step semantics for terminating statements and functions *)
 
 (** The execution of a statement produces an ``outcome'', indicating
@@ -630,41 +699,31 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
   | exec_Sskip:   forall e le m,
       exec_stmt e le m Sskip
                E0 le m Out_normal
-  | exec_Sassign:   forall e le m a1 a2 loc ofs v2 v t m',
-      eval_lvalue e le m a1 loc ofs ->
-      eval_expr e le m a2 v2 ->
+  | exec_Sassign:   forall e le m a1 a2 loc ofs v2 v m',
+      eval_lvalue ge e le m a1 loc ofs ->
+      eval_expr ge e le m a2 v2 ->
       sem_cast v2 (typeof a2) (typeof a1) = Some v ->
-      assign_loc ge (typeof a1) m loc ofs v t m' ->
+      assign_loc (typeof a1) m loc ofs v m' ->
       exec_stmt e le m (Sassign a1 a2)
-               t le m' Out_normal
+               E0 le m' Out_normal
   | exec_Sset:     forall e le m id a v,
-      eval_expr e le m a v ->
+      eval_expr ge e le m a v ->
       exec_stmt e le m (Sset id a)
                E0 (PTree.set id v le) m Out_normal 
-  | exec_Svol_read:   forall e le m id a loc ofs t v,
-      eval_lvalue e le m a loc ofs ->
-      type_is_volatile (typeof a) = true ->
-      deref_loc ge (typeof a) m loc ofs t v ->
-      exec_stmt e le m (Svolread id a)
-               t (PTree.set id v le) m Out_normal 
-  | exec_Scall_none:   forall e le m a al tyargs tyres vf vargs f t m' vres,
-      classify_fun (typeof a) = fun_case_f tyargs tyres ->
-      eval_expr e le m a vf ->
-      eval_exprlist e le m al tyargs vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = Tfunction tyargs tyres ->
-      eval_funcall m f vargs t m' vres ->
-      exec_stmt e le m (Scall None a al)
-                t le m' Out_normal
-  | exec_Scall_some:   forall e le m id a al tyargs tyres vf vargs f t m' vres,
+  | exec_Scall:   forall e le m optid a al tyargs tyres vf vargs f t m' vres,
       classify_fun (typeof a) = fun_case_f tyargs tyres ->
-      eval_expr e le m a vf ->
-      eval_exprlist e le m al tyargs vargs ->
+      eval_expr ge e le m a vf ->
+      eval_exprlist ge e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
       type_of_fundef f = Tfunction tyargs tyres ->
       eval_funcall m f vargs t m' vres ->
-      exec_stmt e le m (Scall (Some id) a al)
-                t (PTree.set id vres le) m' Out_normal
+      exec_stmt e le m (Scall optid a al)
+                t (set_opttemp optid vres le) m' Out_normal
+  | exec_Sbuiltin:   forall e le m optid ef al tyargs vargs t m' vres,
+      eval_exprlist ge e le m al tyargs vargs ->
+      external_call ef ge vargs m t vres m' ->
+      exec_stmt e le m (Sbuiltin optid ef tyargs al)
+                t (set_opttemp optid vres le) m' Out_normal
   | exec_Sseq_1:   forall e le m s1 s2 t1 le1 m1 t2 le2 m2 out,
       exec_stmt e le m s1 t1 le1 m1 Out_normal ->
       exec_stmt e le1 m1 s2 t2 le2 m2 out ->
@@ -676,7 +735,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
       exec_stmt e le m (Ssequence s1 s2)
                 t1 le1 m1 out
   | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out,
-      eval_expr e le m a v1 ->
+      eval_expr ge e le m a v1 ->
       bool_val v1 (typeof a) = Some b ->
       exec_stmt e le m (if b then s1 else s2) t le' m' out ->
       exec_stmt e le m (Sifthenelse a s1 s2)
@@ -685,7 +744,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
       exec_stmt e le m (Sreturn None)
                E0 le m (Out_return None)
   | exec_Sreturn_some: forall e le m a v,
-      eval_expr e le m a v ->
+      eval_expr ge e le m a v ->
       exec_stmt e le m (Sreturn (Some a))
                 E0 le m (Out_return (Some (v, typeof a)))
   | exec_Sbreak:   forall e le m,
@@ -694,70 +753,27 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
   | exec_Scontinue:   forall e le m,
       exec_stmt e le m Scontinue
                E0 le m Out_continue
-  | exec_Swhile_false: forall e le m a s v,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some false ->
-      exec_stmt e le m (Swhile a s)
-               E0 le m Out_normal
-  | exec_Swhile_stop: forall e le m a v s t le' m' out' out,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some true ->
-      exec_stmt e le m s t le' m' out' ->
+  | exec_Sloop_stop1: forall e le m s1 s2 t le' m' out' out,
+      exec_stmt e le m s1 t le' m' out' ->
       out_break_or_return out' out ->
-      exec_stmt e le m (Swhile a s)
+      exec_stmt e le m (Sloop s1 s2)
                 t le' m' out
-  | exec_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2 le2 m2 out,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some true ->
-      exec_stmt e le m s t1 le1 m1 out1 ->
+  | exec_Sloop_stop2: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 out2 out,
+      exec_stmt e le m s1 t1 le1 m1 out1 ->
       out_normal_or_continue out1 ->
-      exec_stmt e le1 m1 (Swhile a s) t2 le2 m2 out ->
-      exec_stmt e le m (Swhile a s)
-                (t1 ** t2) le2 m2 out
-  | exec_Sdowhile_false: forall e le m s a t le1 m1 out1 v,
-      exec_stmt e le m s t le1 m1 out1 ->
+      exec_stmt e le1 m1 s2 t2 le2 m2 out2 ->
+      out_break_or_return out2 out ->
+      exec_stmt e le m (Sloop s1 s2)
+                (t1**t2) le2 m2 out
+  | exec_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3 le3 m3 out,
+      exec_stmt e le m s1 t1 le1 m1 out1 ->
       out_normal_or_continue out1 ->
-      eval_expr e le1 m1 a v ->
-      bool_val v (typeof a) = Some false ->
-      exec_stmt e le m (Sdowhile a s)
-                t le1 m1 Out_normal
-  | exec_Sdowhile_stop: forall e le m s a t le1 m1 out1 out,
-      exec_stmt e le m s t le1 m1 out1 ->
-      out_break_or_return out1 out ->
-      exec_stmt e le m (Sdowhile a s)
-                t le1 m1 out
-  | exec_Sdowhile_loop: forall e le m s a le1 m1 le2 m2 t1 t2 out out1 v,
-      exec_stmt e le m s t1 le1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      eval_expr e le1 m1 a v ->
-      bool_val v (typeof a) = Some true ->
-      exec_stmt e le1 m1 (Sdowhile a s) t2 le2 m2 out ->
-      exec_stmt e le m (Sdowhile a s) 
-                (t1 ** t2) le2 m2 out
-
-  | exec_Sfor_false: forall e le m s a2 a3 v,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some false ->
-      exec_stmt e le m (Sfor' a2 a3 s)
-               E0 le m Out_normal
-  | exec_Sfor_stop: forall e le m s a2 a3 v le1 m1 t out1 out,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some true ->
-      exec_stmt e le m s t le1 m1 out1 ->
-      out_break_or_return out1 out ->
-      exec_stmt e le m (Sfor' a2 a3 s)
-                t le1 m1 out
-  | exec_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 le3 m3 t1 t2 t3 out1 out,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some true ->
-      exec_stmt e le m s t1 le1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal ->
-      exec_stmt e le2 m2 (Sfor' a2 a3 s) t3 le3 m3 out ->
-      exec_stmt e le m (Sfor' a2 a3 s)
-                (t1 ** t2 ** t3) le3 m3 out
+      exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal ->
+      exec_stmt e le2 m2 (Sloop s1 s2) t3 le3 m3 out ->
+      exec_stmt e le m (Sloop s1 s2)
+                (t1**t2**t3) le3 m3 out
   | exec_Sswitch:   forall e le m a t n sl le1 m1 out,
-      eval_expr e le m a (Vint n) ->
+      eval_expr ge e le m a (Vint n) ->
       exec_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t le1 m1 out ->
       exec_stmt e le m (Sswitch a sl)
                 t le1 m1 (outcome_switch out)
@@ -770,8 +786,8 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
   | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4,
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
-      exec_stmt e (PTree.empty val) m2 f.(fn_body) t le m3 out ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out ->
       outcome_result_value out f.(fn_return) vres ->
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
@@ -781,6 +797,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
 
 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
   with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
+Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2.
 
 (** ** Big-step semantics for diverging statements and functions *)
 
@@ -790,22 +807,14 @@ Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
   trace of observable events performed during the execution. *)
 
 CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop :=
-  | execinf_Scall_none:   forall e le m a al vf tyargs tyres vargs f t,
+  | execinf_Scall:   forall e le m optid a al vf tyargs tyres vargs f t,
       classify_fun (typeof a) = fun_case_f tyargs tyres ->
-      eval_expr e le m a vf ->
-      eval_exprlist e le m al tyargs vargs ->
-      Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = Tfunction tyargs tyres ->
-      evalinf_funcall m f vargs t ->
-      execinf_stmt e le m (Scall None a al) t
-  | execinf_Scall_some:   forall e le m id a al vf tyargs tyres vargs f t,
-      classify_fun (typeof a) = fun_case_f tyargs tyres ->
-      eval_expr e le m a vf ->
-      eval_exprlist e le m al tyargs vargs ->
+      eval_expr ge e le m a vf ->
+      eval_exprlist ge e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
       type_of_fundef f = Tfunction tyargs tyres ->
       evalinf_funcall m f vargs t ->
-      execinf_stmt e le m (Scall (Some id) a al) t
+      execinf_stmt e le m (Scall optid a al) t
   | execinf_Sseq_1:   forall e le m s1 s2 t,
       execinf_stmt e le m s1 t ->
       execinf_stmt e le m (Ssequence s1 s2) t
@@ -814,54 +823,26 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro
       execinf_stmt e le1 m1 s2 t2 ->
       execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2)
   | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t,
-      eval_expr e le m a v1 ->
+      eval_expr ge e le m a v1 ->
       bool_val v1 (typeof a) = Some b ->
       execinf_stmt e le m (if b then s1 else s2) t ->
       execinf_stmt e le m (Sifthenelse a s1 s2) t
-  | execinf_Swhile_body: forall e le m a v s t,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some true ->
-      execinf_stmt e le m s t ->
-      execinf_stmt e le m (Swhile a s) t
-  | execinf_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2,
-      eval_expr e le m a v ->
-      bool_val v (typeof a) = Some true ->
-      exec_stmt e le m s t1 le1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      execinf_stmt e le1 m1 (Swhile a s) t2 ->
-      execinf_stmt e le m (Swhile a s) (t1 *** t2)
-  | execinf_Sdowhile_body: forall e le m s a t,
-      execinf_stmt e le m s t ->
-      execinf_stmt e le m (Sdowhile a s) t
-  | execinf_Sdowhile_loop: forall e le m s a le1 m1 t1 t2 out1 v,
-      exec_stmt e le m s t1 le1 m1 out1 ->
-      out_normal_or_continue out1 ->
-      eval_expr e le1 m1 a v ->
-      bool_val v (typeof a) = Some true ->
-      execinf_stmt e le1 m1 (Sdowhile a s) t2 ->
-      execinf_stmt e le m (Sdowhile a s) (t1 *** t2)
-  | execinf_Sfor_body: forall e le m s a2 a3 v t,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some true ->
-      execinf_stmt e le m s t ->
-      execinf_stmt e le m (Sfor' a2 a3 s) t
-  | execinf_Sfor_next: forall e le m s a2 a3 v le1 m1 t1 t2 out1,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some true ->
-      exec_stmt e le m s t1 le1 m1 out1 ->
+  | execinf_Sloop_body1: forall e le m s1 s2 t,
+      execinf_stmt e le m s1 t ->
+      execinf_stmt e le m (Sloop s1 s2) t
+  | execinf_Sloop_body2: forall e le m s1 s2 t1 le1 m1 out1 t2,
+      exec_stmt e le m s1 t1 le1 m1 out1 ->
       out_normal_or_continue out1 ->
-      execinf_stmt e le1 m1 a3 t2 ->
-      execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2)
-  | execinf_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 t1 t2 t3 out1,
-      eval_expr e le m a2 v ->
-      bool_val v (typeof a2) = Some true ->
-      exec_stmt e le m s t1 le1 m1 out1 ->
+      execinf_stmt e le1 m1 s2 t2 ->
+      execinf_stmt e le m (Sloop s1 s2) (t1***t2)
+  | execinf_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3,
+      exec_stmt e le m s1 t1 le1 m1 out1 ->
       out_normal_or_continue out1 ->
-      exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal ->
-      execinf_stmt e le2 m2 (Sfor' a2 a3 s) t3 ->
-      execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2 *** t3)
+      exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal ->
+      execinf_stmt e le2 m2 (Sloop s1 s2) t3 ->
+      execinf_stmt e le m (Sloop s1 s2) (t1***t2***t3)
   | execinf_Sswitch:   forall e le m a t n sl,
-      eval_expr e le m a (Vint n) ->
+      eval_expr ge e le m a (Vint n) ->
       execinf_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t ->
       execinf_stmt e le m (Sswitch a sl) t
 
@@ -872,63 +853,11 @@ with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
   | evalinf_funcall_internal: forall m f vargs t e m1 m2,
       alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
       list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
-      execinf_stmt e (PTree.empty val) m2 f.(fn_body) t ->
+      bind_parameters e m1 f.(fn_params) vargs m2 ->
+      execinf_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t ->
       evalinf_funcall m (Internal f) vargs t.
 
-End SEMANTICS.
-
-(** * Whole-program semantics *)
-
-(** Execution of whole programs are described as sequences of transitions
-  from an initial state to a final state.  An initial state is a [Callstate]
-  corresponding to the invocation of the ``main'' function of the program
-  without arguments and with an empty continuation. *)
-
-Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f m0,
-      let ge := Genv.globalenv p in
-      Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      type_of_fundef f = Tfunction Tnil type_int32s ->
-      initial_state p (Callstate f nil Kstop m0).
-
-(** A final state is a [Returnstate] with an empty continuation. *)
-
-Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall r m,
-      final_state (Returnstate (Vint r) Kstop m) r.
-
-(** Wrapping up these definitions in a small-step semantics. *)
-
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-(** This semantics is receptive to changes in events. *)
-
-Lemma semantics_receptive:
-  forall (p: program), receptive (semantics p).
-Proof.
-  intros. constructor; simpl; intros.
-(* receptiveness *)
-  assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2).
-    intros. subst. inv H0. exists s1; auto.
-  inversion H; subst; auto.
-  (* assign *)
-  inv H5; auto. exploit volatile_store_receptive; eauto. intros EQ. subst t2; econstructor; eauto.
-  (* volatile read *)
-  inv H3; auto. exploit volatile_load_receptive; eauto. intros [v2 LD]. 
-  econstructor. eapply step_vol_read; eauto. eapply deref_loc_volatile; eauto. 
-  (* external *)
-  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
-  exists (Returnstate vres2 k m2). econstructor; eauto.
-(* trace length *)
-  red; intros. inv H; simpl; try omega.
-  inv H3; simpl; try omega. inv H5; simpl; omega.
-  inv H1; simpl; try omega. inv H4; simpl; omega.
-  eapply external_call_trace_length; eauto.
-Qed.
+End BIGSTEP.
 
 (** Big-step execution of a whole program.  *)
 
@@ -962,13 +891,6 @@ Section BIGSTEP_TO_TRANSITIONS.
 Variable prog: program.
 Let ge : genv := Genv.globalenv prog.
 
-Definition exec_stmt_eval_funcall_ind
-  (PS: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop)
-  (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) :=
-  fun a b c d e f g h i j k l m n o p q r s t u v w x y =>
-  conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y)
-       (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y).
-
 Inductive outcome_state_match
        (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
   | osm_normal:
@@ -1006,7 +928,7 @@ Lemma exec_stmt_eval_funcall_steps:
    is_call_cont k ->
    star step ge (Callstate fd args k m) t (Returnstate res k m')).
 Proof.
-  apply exec_stmt_eval_funcall_ind; intros.
+  apply exec_stmt_funcall_ind; intros.
 
 (* skip *)
   econstructor; split. apply star_refl. constructor.
@@ -1017,20 +939,14 @@ Proof.
 (* set *)
   econstructor; split. apply star_one. econstructor; eauto. constructor.
 
-(* set volatile *)
-  econstructor; split. apply star_one. econstructor; eauto. constructor.
-
-(* call none *)
+(* call *)
   econstructor; split.
   eapply star_left. econstructor; eauto. 
   eapply star_right. apply H5. simpl; auto. econstructor. reflexivity. traceEq.
   constructor.
 
-(* call some *)
-  econstructor; split.
-  eapply star_left. econstructor; eauto. 
-  eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq.
-  constructor.
+(* builtin *)
+  econstructor; split. apply star_one. econstructor; eauto. constructor.
 
 (* sequence 2 *)
   destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1.
@@ -1080,112 +996,55 @@ Proof.
 (* continue *)
   econstructor; split. apply star_refl. constructor.
 
-(* while false *)
-  econstructor; split.
-  apply star_one. eapply step_while_false; eauto. 
-  constructor.
-
-(* while stop *)
-  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
+(* loop stop 1 *)
+  destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]].
   set (S2 :=
     match out' with
     | Out_break => State f Sskip k e le' m'
     | _ => S1
     end).
   exists S2; split.
-  eapply star_left. eapply step_while_true; eauto. 
-  eapply star_trans. eexact A1.
-  unfold S2. inversion H3; subst.
-  inv B1. apply star_one. constructor.    
-  apply star_refl.
-  reflexivity. traceEq.
-  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
-
-(* while loop *)
-  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
-  destruct (H5 f k) as [S2 [A2 B2]].
-  exists S2; split.
-  eapply star_left. eapply step_while_true; eauto.
-  eapply star_trans. eexact A1.
-  eapply star_left.
-  inv H3; inv B1; apply step_skip_or_continue_while; auto.
-  eexact A2.
-  reflexivity. reflexivity. traceEq.
-  auto.
-
-(* dowhile false *)
-  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
-  exists (State f Sskip k e le1 m1); split.
-  eapply star_left. constructor. 
-  eapply star_right. eexact A1.
-  inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto.
-  reflexivity. traceEq. 
-  constructor.
-
-(* dowhile stop *)
-  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out1 with
-    | Out_break => State f Sskip k e le1 m1
-    | _ => S1
-    end).
-  exists S2; split.
-  eapply star_left. apply step_dowhile. 
+  eapply star_left. eapply step_loop. 
   eapply star_trans. eexact A1.
   unfold S2. inversion H1; subst.
-  inv B1. apply star_one. constructor.
+  inv B1. apply star_one. constructor.    
   apply star_refl.
   reflexivity. traceEq.
   unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto.
 
-(* dowhile loop *)
-  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
-  destruct (H5 f k) as [S2 [A2 B2]].
-  exists S2; split.
-  eapply star_left. apply step_dowhile. 
-  eapply star_trans. eexact A1.
-  eapply star_left.
-  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
-  eexact A2.
-  reflexivity. reflexivity. traceEq.
-  auto.
-
-(* for false *)
-  econstructor; split.
-  eapply star_one. eapply step_for_false; eauto. 
-  constructor.
-
-(* for stop *)
-  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
-  set (S2 :=
-    match out1 with
-    | Out_break => State f Sskip k e le1 m1
-    | _ => S1
+(* loop stop 2 *)
+  destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]].
+  destruct (H3 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]].
+  set (S3 :=
+    match out2 with
+    | Out_break => State f Sskip k e le2 m2
+    | _ => S2
     end).
-  exists S2; split.
-  eapply star_left. eapply step_for_true; eauto. 
+  exists S3; split.
+  eapply star_left. eapply step_loop. 
   eapply star_trans. eexact A1.
-  unfold S2. inversion H3; subst.
-  inv B1. apply star_one. constructor. 
-  apply star_refl.
-  reflexivity. traceEq.
-  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
-
-(* for loop *)
-  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
-  destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2.
-  destruct (H7 f k) as [S3 [A3 B3]].
+  eapply star_left with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1).
+  inv H1; inv B1; constructor; auto.
+  eapply star_trans. eexact A2.
+  unfold S3. inversion H4; subst.
+  inv B2. apply star_one. constructor. apply star_refl.
+  reflexivity. reflexivity. reflexivity. traceEq. 
+  unfold S3. inversion H4; subst. constructor. inv B2; econstructor; eauto.
+
+(* loop loop *)
+  destruct (H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]].
+  destruct (H3 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]].
+  destruct (H5 f k) as [S3 [A3 B3]].
   exists S3; split.
-  eapply star_left. eapply step_for_true; eauto. 
+  eapply star_left. eapply step_loop. 
   eapply star_trans. eexact A1.
-  eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e le1 m1).
-  inv H3; inv B1.
-  apply star_one. constructor. auto. 
-  apply star_one. constructor. auto. 
-  eapply star_trans. eexact A2. 
-  eapply star_left. constructor.
+  eapply star_left with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1).
+  inv H1; inv B1; constructor; auto.
+  eapply star_trans. eexact A2.
+  eapply star_left with (s2 := State f (Sloop s1 s2) k e le2 m2).
+  inversion H4; subst; inv B2; constructor; auto. 
   eexact A3.
-  reflexivity. reflexivity. reflexivity. reflexivity. traceEq.
+  reflexivity. reflexivity. reflexivity. reflexivity. traceEq. 
   auto.
 
 (* switch *)
@@ -1264,11 +1123,7 @@ Proof.
   cofix CIH_STMT.
   intros. inv H.
 
-(* call none *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_call; eauto. 
-  eapply CIH_FUN. eauto. traceEq.
-(* call some *)
+(* call  *)
   eapply forever_N_plus.
   apply plus_one. eapply step_call; eauto. 
   eapply CIH_FUN. eauto. traceEq.
@@ -1290,65 +1145,29 @@ Proof.
   apply plus_one. eapply step_ifthenelse with (b := b); eauto. 
   apply CIH_STMT; eauto. traceEq.
 
-(* while body *)
+(* loop body 1 *)
   eapply forever_N_plus.
-  eapply plus_one. eapply step_while_true; eauto.
+  eapply plus_one. constructor. 
   apply CIH_STMT; eauto. traceEq.
-(* while loop *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]].
-  eapply forever_N_plus with (s2 := State f (Swhile a s0) k e le1 m1).
-  eapply plus_left. eapply step_while_true; eauto.
+(* loop body 2 *)
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]].
+  eapply forever_N_plus with (s2 := State f s2 (Kloop2 s1 s2 k) e le1 m1).
+  eapply plus_left. constructor.
   eapply star_right. eexact A1.
-  inv H3; inv B1; apply step_skip_or_continue_while; auto. 
+  inv H1; inv B1; constructor; auto. 
   reflexivity. reflexivity.
   apply CIH_STMT; eauto. traceEq.
-
-(* dowhile body *)
-  eapply forever_N_plus.
-  eapply plus_one. eapply step_dowhile.
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* dowhile loop *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]].
-  eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e le1 m1).
-  eapply plus_left. eapply step_dowhile. 
-  eapply star_right. eexact A1.
-  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. 
-  reflexivity. reflexivity.
-  apply CIH_STMT. eauto. 
-  traceEq.
-
-(* for body *)
-  eapply forever_N_plus.
-  apply plus_one. eapply step_for_true; eauto. 
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* for next *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
-  eapply forever_N_plus.
-  eapply plus_left. eapply step_for_true; eauto.
-  eapply star_trans. eexact A1.
-  apply star_one.
-  inv H3; inv B1; apply step_skip_or_continue_for2; auto.
-  reflexivity. reflexivity. 
-  apply CIH_STMT; eauto.
-  traceEq.
-
-(* for body *)
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
-  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]].
-  inv B2.
-  eapply forever_N_plus.
-  eapply plus_left. eapply step_for_true; eauto. 
+(* loop loop *)
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kloop1 s1 s2 k)) as [S1 [A1 B1]].
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H2 f (Kloop2 s1 s2 k)) as [S2 [A2 B2]].
+  eapply forever_N_plus with (s2 := State f (Sloop s1 s2) k e le2 m2).
+  eapply plus_left. constructor.
   eapply star_trans. eexact A1.
-  eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto.
-  eapply star_right. eexact A2. 
-  constructor. 
-  reflexivity. reflexivity. reflexivity. reflexivity.  
-  apply CIH_STMT; eauto.
-  traceEq.
+  eapply star_left. inv H1; inv B1; constructor; auto.
+  eapply star_right. eexact A2.
+  inv B2. constructor.
+  reflexivity. reflexivity. reflexivity. reflexivity.
+  apply CIH_STMT; eauto. traceEq.
 
 (* switch *)
   eapply forever_N_plus.
@@ -1382,3 +1201,4 @@ Proof.
 Qed.
 
 End BIGSTEP_TO_TRANSITIONS.
+