Fusion partielle de la branche contsem:

- semantiques a continuation pour Cminor et CminorSel
- goto dans Cminor

Suppression de backend/RTLbigstep.v, devenu inutile.


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

11 files changed, 1778 insertions, 1789 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index f2eb84fd..910eaa44 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -95,11 +95,14 @@ Inductive expr : Set :=
   [Sexit n] terminates prematurely the execution of the [n+1]
   enclosing [Sblock] statements. *)
 
+Definition label := ident.
+
 Inductive stmt : Set :=
   | Sskip: stmt
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
   | Scall : option ident -> signature -> expr -> list expr -> stmt
+  | Stailcall: signature -> expr -> list expr -> stmt
   | Salloc : ident -> expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
@@ -108,7 +111,8 @@ Inductive stmt : Set :=
   | Sexit: nat -> stmt
   | Sswitch: expr -> list (int * nat) -> nat -> stmt
   | Sreturn: option expr -> stmt
-  | Stailcall: signature -> expr -> list expr -> stmt.
+  | Slabel: label -> stmt -> stmt
+  | Sgoto: label -> stmt.
 
 (** Functions are composed of a signature, a list of parameter names,
   a list of local variables, and a  statement representing
@@ -134,41 +138,7 @@ Definition funsig (fd: fundef) :=
   | External ef => ef.(ef_sig)
   end.
 
-(** * Operational semantics *)
-
-(** The operational semantics for Cminor is given in big-step operational
-  style.  Expressions evaluate to values, and statements evaluate to
-  ``outcomes'' indicating how execution should proceed afterwards. *)
-
-Inductive outcome: Set :=
-  | Out_normal: outcome                (**r continue in sequence *)
-  | Out_exit: nat -> outcome           (**r terminate [n+1] enclosing blocks *)
-  | Out_return: option val -> outcome  (**r return immediately to caller *)
-  | Out_tailcall_return: val -> outcome. (**r already returned to caller via a tailcall *)
-
-Definition outcome_block (out: outcome) : outcome :=
-  match out with
-  | Out_exit O => Out_normal
-  | Out_exit (S n) => Out_exit n
-  | out => out
-  end.
-
-Definition outcome_result_value
-    (out: outcome) (retsig: option typ) (vres: val) : Prop :=
-  match out, retsig with
-  | Out_normal, None => vres = Vundef
-  | Out_return None, None => vres = Vundef
-  | Out_return (Some v), Some ty => vres = v
-  | Out_tailcall_return v, _ => vres = v
-  | _, _ => False
-  end.
-
-Definition outcome_free_mem
-    (out: outcome) (m: mem) (sp: block) : mem :=
-  match out with
-  | Out_tailcall_return _ => m
-  | _ => Mem.free m sp
-  end.
+(** * Operational semantics (small-step) *)
 
 (** Two kinds of evaluation environments are involved:
 - [genv]: global environments, define symbols and functions;
@@ -201,6 +171,38 @@ Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
   | Some id => PTree.set id v e
   end.
 
+(** Continuations *)
+
+Inductive cont: Set :=
+  | Kstop: cont                         (**r stop program execution *)
+  | Kseq: stmt -> cont -> cont          (**r execute stmt, then cont *)
+  | Kblock: cont -> cont                (**r exit a block, then do cont *)
+  | Kcall: option ident -> function -> val -> env -> cont -> cont.
+                                        (**r return to caller *)
+
+(** States *)
+
+Inductive state: Set :=
+  | State:                      (**r Execution within a function *)
+      forall (f: function)              (**r currently executing function  *)
+             (s: stmt)                  (**r statement under consideration *)
+             (k: cont)                  (**r its continuation -- what to do next *)
+             (sp: val)                  (**r current stack pointer *)
+             (e: env)                   (**r current local environment *)
+             (m: mem),                  (**r current memory state *)
+      state
+  | Callstate:                  (**r Invocation of a function *)
+      forall (f: fundef)                (**r function to invoke *)
+             (args: list val)           (**r arguments provided by caller *)
+             (k: cont)                  (**r what to do next  *)
+             (m: mem),                  (**r memory state *)
+      state
+  | Returnstate:                (**r Return from a function *)
+      forall (v: val)                   (**r Return value *)
+             (k: cont)                  (**r what to do next *)
+             (m: mem),                  (**r memory state *)
+      state.
+             
 Section RELSEM.
 
 Variable ge: genv.
@@ -351,6 +353,233 @@ Inductive eval_exprlist: list expr -> list val -> Prop :=
 
 End EVAL_EXPR.
 
+(** Pop continuation until a call or stop *)
+
+Fixpoint call_cont (k: cont) : cont :=
+  match k with
+  | Kseq s k => call_cont k
+  | Kblock k => call_cont k
+  | _ => k
+  end.
+
+Definition is_call_cont (k: cont) : Prop :=
+  match k with
+  | Kstop => True
+  | Kcall _ _ _ _ _ => True
+  | _ => False
+  end.
+
+(** Find the statement and manufacture the continuation 
+  corresponding to a label *)
+
+Fixpoint find_label (lbl: label) (s: stmt) (k: cont) 
+                    {struct s}: option (stmt * cont) :=
+  match s with
+  | Sseq s1 s2 =>
+      match find_label lbl s1 (Kseq s2 k) with
+      | Some sk => Some sk
+      | None => find_label lbl s2 k
+      end
+  | Sifthenelse a s1 s2 =>
+      match find_label lbl s1 k with
+      | Some sk => Some sk
+      | None => find_label lbl s2 k
+      end
+  | Sloop s1 =>
+      find_label lbl s1 (Kseq (Sloop s1) k)
+  | Sblock s1 =>
+      find_label lbl s1 (Kblock k)
+  | Slabel lbl' s' =>
+      if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
+  | _ => None
+  end.
+
+(** One step of execution *)
+
+Inductive step: state -> trace -> state -> Prop :=
+
+  | step_skip_seq: forall f s k sp e m,
+      step (State f Sskip (Kseq s k) sp e m)
+        E0 (State f s k sp e m)
+  | step_skip_block: forall f k sp e m,
+      step (State f Sskip (Kblock k) sp e m)
+        E0 (State f Sskip k sp e m)
+  | step_skip_call: forall f k sp e m,
+      is_call_cont k ->
+      f.(fn_sig).(sig_res) = None ->
+      step (State f Sskip k (Vptr sp Int.zero) e m)
+        E0 (Returnstate Vundef k (Mem.free m sp))
+
+  | step_assign: forall f id a k sp e m v,
+      eval_expr sp e m a v ->
+      step (State f (Sassign id a) k sp e m)
+        E0 (State f Sskip k sp (PTree.set id v e) m)
+
+  | step_store: forall f chunk addr a k sp e m vaddr v m',
+      eval_expr sp e m addr vaddr ->
+      eval_expr sp e m a v ->
+      Mem.storev chunk m vaddr v = Some m' ->
+      step (State f (Sstore chunk addr a) k sp e m)
+        E0 (State f Sskip k sp e m')
+
+  | step_call: forall f optid sig a bl k sp e m vf vargs fd,
+      eval_expr sp e m a vf ->
+      eval_exprlist sp e m bl vargs ->
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      step (State f (Scall optid sig a bl) k sp e m)
+        E0 (Callstate fd vargs (Kcall optid f sp e k) m)
+
+  | step_tailcall: forall f sig a bl k sp e m vf vargs fd,
+      eval_expr (Vptr sp Int.zero) e m a vf ->
+      eval_exprlist (Vptr sp Int.zero) e m bl vargs ->
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
+        E0 (Callstate fd vargs (call_cont k) (Mem.free m sp))
+
+  | step_alloc: forall f id a k sp e m n m' b,
+      eval_expr sp e m a (Vint n) ->
+      Mem.alloc m 0 (Int.signed n) = (m', b) ->
+      step (State f (Salloc id a) k sp e m)
+        E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m')
+
+  | step_seq: forall f s1 s2 k sp e m,
+      step (State f (Sseq s1 s2) k sp e m)
+        E0 (State f s1 (Kseq s2 k) sp e m)
+
+  | step_ifthenelse: forall f a s1 s2 k sp e m v b,
+      eval_expr sp e m a v ->
+      Val.bool_of_val v b ->
+      step (State f (Sifthenelse a s1 s2) k sp e m)
+        E0 (State f (if b then s1 else s2) k sp e m)
+
+  | step_loop: forall f s k sp e m,
+      step (State f (Sloop s) k sp e m)
+        E0 (State f s (Kseq (Sloop s) k) sp e m)
+
+  | step_block: forall f s k sp e m,
+      step (State f (Sblock s) k sp e m)
+        E0 (State f s (Kblock k) sp e m)
+
+  | step_exit_seq: forall f n s k sp e m,
+      step (State f (Sexit n) (Kseq s k) sp e m)
+        E0 (State f (Sexit n) k sp e m)
+  | step_exit_block_0: forall f k sp e m,
+      step (State f (Sexit O) (Kblock k) sp e m)
+        E0 (State f Sskip k sp e m)
+  | step_exit_block_S: forall f n k sp e m,
+      step (State f (Sexit (S n)) (Kblock k) sp e m)
+        E0 (State f (Sexit n) k sp e m)
+
+  | step_switch: forall f a cases default k sp e m n,
+      eval_expr sp e m a (Vint n) ->
+      step (State f (Sswitch a cases default) k sp e m)
+        E0 (State f (Sexit (switch_target n default cases)) k sp e m)
+
+  | step_return_0: forall f k sp e m,
+      f.(fn_sig).(sig_res) = None ->
+      step (State f (Sreturn None) k (Vptr sp Int.zero) e m)
+        E0 (Returnstate Vundef (call_cont k) (Mem.free m sp))
+  | step_return_1: forall f a k sp e m v,
+      f.(fn_sig).(sig_res) <> None ->
+      eval_expr (Vptr sp Int.zero) e m a v ->
+      step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m)
+        E0 (Returnstate v (call_cont k) (Mem.free m sp))
+
+  | step_label: forall f lbl s k sp e m,
+      step (State f (Slabel lbl s) k sp e m)
+        E0 (State f s k sp e m)
+
+  | step_goto: forall f lbl k sp e m s' k',
+      find_label lbl f.(fn_body) (call_cont k) = Some(s', k') ->
+      step (State f (Sgoto lbl) k sp e m)
+        E0 (State f s' k' sp e m)
+
+  | step_internal_function: forall f vargs k m m' sp e,
+      Mem.alloc m 0 f.(fn_stackspace) = (m', sp) ->
+      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
+      step (Callstate (Internal f) vargs k m)
+        E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
+  | step_external_function: forall ef vargs k m t vres,
+      event_match ef vargs t vres ->
+      step (Callstate (External ef) vargs k m)
+         t (Returnstate vres k m)        
+
+  | step_return: forall v optid f sp e k m,
+      step (Returnstate v (Kcall optid f sp e k) m)
+        E0 (State f Sskip k sp (set_optvar optid v e) m).
+
+End RELSEM.
+
+(** 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,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      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.
+
+(** Execution of a whole program: [exec_program p beh]
+  holds if the application of [p]'s main function to no arguments
+  in the initial memory state for [p] has [beh] as observable
+  behavior. *)
+
+Definition exec_program (p: program) (beh: program_behavior) : Prop :=
+  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
+
+(** * Alternate operational semantics (big-step) *)
+
+(** In big-step style, just like expressions evaluate to values, 
+    statements evaluate to``outcomes'' indicating how execution should
+    proceed afterwards. *)
+
+Inductive outcome: Set :=
+  | Out_normal: outcome                (**r continue in sequence *)
+  | Out_exit: nat -> outcome           (**r terminate [n+1] enclosing blocks *)
+  | Out_return: option val -> outcome  (**r return immediately to caller *)
+  | Out_tailcall_return: val -> outcome. (**r already returned to caller via a tailcall *)
+
+Definition outcome_block (out: outcome) : outcome :=
+  match out with
+  | Out_exit O => Out_normal
+  | Out_exit (S n) => Out_exit n
+  | out => out
+  end.
+
+Definition outcome_result_value
+    (out: outcome) (retsig: option typ) (vres: val) : Prop :=
+  match out, retsig with
+  | Out_normal, None => vres = Vundef
+  | Out_return None, None => vres = Vundef
+  | Out_return (Some v), Some ty => vres = v
+  | Out_tailcall_return v, _ => vres = v
+  | _, _ => False
+  end.
+
+Definition outcome_free_mem
+    (out: outcome) (m: mem) (sp: block) : mem :=
+  match out with
+  | Out_tailcall_return _ => m
+  | _ => Mem.free m sp
+  end.
+
+Section NATURALSEM.
+
+Variable ge: genv.
+
 (** Evaluation of a function invocation: [eval_funcall ge m f args t m' res]
   means that the function [f], applied to the arguments [args] in
   memory state [m], returns the value [res] in modified memory state [m'].
@@ -389,18 +618,18 @@ with exec_stmt:
       exec_stmt sp e m Sskip E0 e m Out_normal
   | exec_Sassign:
       forall sp e m id a v,
-      eval_expr sp e m a v ->
+      eval_expr ge sp e m a v ->
       exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
   | exec_Sstore:
       forall sp e m chunk addr a vaddr v m',
-      eval_expr sp e m addr vaddr ->
-      eval_expr sp e m a v ->
+      eval_expr ge sp e m addr vaddr ->
+      eval_expr ge sp e m a v ->
       Mem.storev chunk m vaddr v = Some m' ->
       exec_stmt sp e m (Sstore chunk addr a) E0 e m' Out_normal
   | exec_Scall:
       forall sp e m optid sig a bl vf vargs f t m' vres e',
-      eval_expr sp e m a vf ->
-      eval_exprlist sp e m bl vargs ->
+      eval_expr ge sp e m a vf ->
+      eval_exprlist ge sp e m bl vargs ->
       Genv.find_funct ge vf = Some f ->
       funsig f = sig ->
       eval_funcall m f vargs t m' vres ->
@@ -408,13 +637,13 @@ with exec_stmt:
       exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal
   | exec_Salloc:
       forall sp e m id a n m' b,
-      eval_expr sp e m a (Vint n) ->
+      eval_expr ge sp e m a (Vint n) ->
       Mem.alloc m 0 (Int.signed n) = (m', b) ->
       exec_stmt sp e m (Salloc id a) 
                 E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal
   | exec_Sifthenelse:
       forall sp e m a s1 s2 v b t e' m' out,
-      eval_expr sp e m a v ->
+      eval_expr ge sp e m a v ->
       Val.bool_of_val v b ->
       exec_stmt sp e m (if b then s1 else s2) t e' m' out ->
       exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out
@@ -449,7 +678,7 @@ with exec_stmt:
       exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
   | exec_Sswitch:
       forall sp e m a cases default n,
-      eval_expr sp e m a (Vint n) ->
+      eval_expr ge sp e m a (Vint n) ->
       exec_stmt sp e m (Sswitch a cases default)
                 E0 e m (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
@@ -457,12 +686,12 @@ with exec_stmt:
       exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
   | exec_Sreturn_some:
       forall sp e m a v,
-      eval_expr sp e m a v ->
+      eval_expr ge sp e m a v ->
       exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
   | exec_Stailcall:
       forall sp e m sig a bl vf vargs f t m' vres,
-      eval_expr (Vptr sp Int.zero) e m a vf ->
-      eval_exprlist (Vptr sp Int.zero) e m bl vargs ->
+      eval_expr ge (Vptr sp Int.zero) e m a vf ->
+      eval_exprlist ge (Vptr sp Int.zero) e m bl vargs ->
       Genv.find_funct ge vf = Some f ->
       funsig f = sig ->
       eval_funcall (Mem.free m sp) f vargs t m' vres ->
@@ -495,15 +724,15 @@ with execinf_stmt:
          val -> env -> mem -> stmt -> traceinf -> Prop :=
   | execinf_Scall:
       forall sp e m optid sig a bl vf vargs f t,
-      eval_expr sp e m a vf ->
-      eval_exprlist sp e m bl vargs ->
+      eval_expr ge sp e m a vf ->
+      eval_exprlist ge sp e m bl vargs ->
       Genv.find_funct ge vf = Some f ->
       funsig f = sig ->
       evalinf_funcall m f vargs t ->
       execinf_stmt sp e m (Scall optid sig a bl) t
   | execinf_Sifthenelse:
       forall sp e m a s1 s2 v b t,
-      eval_expr sp e m a v ->
+      eval_expr ge sp e m a v ->
       Val.bool_of_val v b ->
       execinf_stmt sp e m (if b then s1 else s2) t ->
       execinf_stmt sp e m (Sifthenelse a s1 s2) t
@@ -533,21 +762,21 @@ with execinf_stmt:
       execinf_stmt sp e m (Sblock s) t
   | execinf_Stailcall:
       forall sp e m sig a bl vf vargs f t,
-      eval_expr (Vptr sp Int.zero) e m a vf ->
-      eval_exprlist (Vptr sp Int.zero) e m bl vargs ->
+      eval_expr ge (Vptr sp Int.zero) e m a vf ->
+      eval_exprlist ge (Vptr sp Int.zero) e m bl vargs ->
       Genv.find_funct ge vf = Some f ->
       funsig f = sig ->
       evalinf_funcall (Mem.free m sp) f vargs t ->
       execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t.
 
-End RELSEM.
+End NATURALSEM.
 
 (** Execution of a whole program: [exec_program p beh]
   holds if the application of [p]'s main function to no arguments
   in the initial memory state for [p] has [beh] as observable
   behavior. *)
 
-Inductive exec_program (p: program): program_behavior -> Prop :=
+Inductive exec_program_bigstep (p: program): program_behavior -> Prop :=
   | program_terminates:
       forall b f t m r,
       let ge := Genv.globalenv p in
@@ -556,7 +785,7 @@ Inductive exec_program (p: program): program_behavior -> Prop :=
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
       eval_funcall ge m0 f nil t m (Vint r) ->
-      exec_program p (Terminates t r)
+      exec_program_bigstep p (Terminates t r)
   | program_diverges:
       forall b f t,
       let ge := Genv.globalenv p in
@@ -565,4 +794,340 @@ Inductive exec_program (p: program): program_behavior -> Prop :=
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
       evalinf_funcall ge m0 f nil t ->
-      exec_program p (Diverges t).
+      exec_program_bigstep p (Diverges t).
+
+(** ** Correctness of the big-step semantics with respect to the transition semantics *)
+
+Section BIGSTEP_TO_TRANSITION.
+
+Variable prog: program.
+Let ge := Genv.globalenv prog.
+
+Definition eval_funcall_exec_stmt_ind2 
+  (P1: mem -> fundef -> list val -> trace -> mem -> val -> Prop)
+  (P2: val -> env -> mem -> stmt -> trace ->
+              env -> mem -> outcome -> Prop) :=
+  fun a b c d e f g h i j k l m n o p q r =>
+  conj
+    (eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r)
+    (exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r ).
+
+Inductive outcome_state_match
+        (sp: val) (e: env) (m: mem) (f: function) (k: cont):
+        outcome -> state -> Prop :=
+  | osm_normal:
+      outcome_state_match sp e m f k 
+                          Out_normal
+                          (State f Sskip k sp e m)
+  | osm_exit: forall n,
+      outcome_state_match sp e m f k 
+                          (Out_exit n)
+                          (State f (Sexit n) k sp e m)
+  | osm_return_none: forall k',
+      call_cont k' = call_cont k ->
+      outcome_state_match sp e m f k 
+                          (Out_return None)
+                          (State f (Sreturn None) k' sp e m)
+  | osm_return_some: forall k' a v,
+      call_cont k' = call_cont k ->
+      eval_expr ge sp e m a v ->
+      outcome_state_match sp e m f k 
+                          (Out_return (Some v))
+                          (State f (Sreturn (Some a)) k' sp e m)
+  | osm_tail: forall v,
+      outcome_state_match sp e m f k
+                          (Out_tailcall_return v)
+                          (Returnstate v (call_cont k) m).
+
+Remark is_call_cont_call_cont:
+  forall k, is_call_cont (call_cont k).
+Proof.
+  induction k; simpl; auto.
+Qed.
+
+Remark call_cont_is_call_cont:
+  forall k, is_call_cont k -> call_cont k = k.
+Proof.
+  destruct k; simpl; intros; auto || contradiction.
+Qed.
+
+Lemma eval_funcall_exec_stmt_steps:
+  (forall m fd args t m' res,
+   eval_funcall ge m fd args t m' res ->
+   forall k,
+   is_call_cont k ->
+   star step ge (Callstate fd args k m)
+              t (Returnstate res k m'))
+/\(forall sp e m s t e' m' out,
+   exec_stmt ge sp e m s t e' m' out ->
+   forall f k,
+   exists S,
+   star step ge (State f s k sp e m) t S
+   /\ outcome_state_match sp e' m' f k out S).
+Proof.
+  apply eval_funcall_exec_stmt_ind2; intros.
+
+(* funcall internal *)
+  destruct (H2 f k) as [S [A B]].
+  assert (call_cont k = k) by (apply call_cont_is_call_cont; auto).
+  eapply star_left. econstructor; eauto. 
+  eapply star_trans. eexact A.
+  inversion B; clear B; subst out; simpl in H3; simpl; try contradiction.
+  (* Out normal *)
+  assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef).
+    destruct f.(fn_sig).(sig_res). contradiction. auto.
+  destruct H6. subst vres.
+  apply star_one. apply step_skip_call; auto. 
+  (* Out_return None *)
+  assert (f.(fn_sig).(sig_res) = None /\ vres = Vundef).
+    destruct f.(fn_sig).(sig_res). contradiction. auto.
+  destruct H7. subst vres.
+  replace k with (call_cont k') by congruence.
+  apply star_one. apply step_return_0; auto.
+  (* Out_return Some *)
+  assert (f.(fn_sig).(sig_res) <> None /\ vres = v).
+    destruct f.(fn_sig).(sig_res). split; congruence. contradiction.
+  destruct H8. subst vres.
+  replace k with (call_cont k') by congruence.
+  apply star_one. eapply step_return_1; eauto.
+  (* Out_tailcall_return *)
+  subst vres. rewrite H5. apply star_refl.
+
+  reflexivity. traceEq.
+
+(* funcall external *)
+  apply star_one. constructor; auto. 
+
+(* skip *)
+  econstructor; split.
+  apply star_refl. 
+  constructor.
+
+(* assign *)
+  exists (State f Sskip k sp (PTree.set id v e) m); split.
+  apply star_one. constructor. auto.
+  constructor.
+
+(* store *)
+  econstructor; split.
+  apply star_one. econstructor; eauto.
+  constructor.
+
+(* call *)
+  econstructor; split.
+  eapply star_left. econstructor; eauto. 
+  eapply star_right. apply H4. red; auto. 
+  constructor. reflexivity. traceEq.
+  subst e'. constructor.
+
+(* alloc *)
+  exists (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m'); split.
+  apply star_one. econstructor; eauto.
+  constructor.
+
+(* ifthenelse *)
+  destruct (H2 f k) as [S [A B]].
+  exists S; split.
+  apply star_left with E0 (State f (if b then s1 else s2) k sp e m) t.
+  econstructor; eauto. exact A.
+  traceEq.
+  auto.
+
+(* seq continue *)
+  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
+  destruct (H2 f k) as [S2 [A2 B2]].
+  inv B1.
+  exists S2; split.
+  eapply star_left. constructor. 
+  eapply star_trans. eexact A1. 
+  eapply star_left. constructor. eexact A2.
+  reflexivity. reflexivity. traceEq.
+  auto.
+
+(* seq stop *)
+  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
+  set (S2 :=
+    match out with
+    | Out_exit n => State f (Sexit n) k sp e1 m1
+    | _ => S1
+    end).
+  exists S2; split.
+  eapply star_left. constructor. eapply star_trans. eexact A1.
+  unfold S2; destruct out; try (apply star_refl).
+  inv B1. apply star_one. constructor.
+  reflexivity. traceEq.
+  unfold S2; inv B1; congruence || simpl; constructor; auto.
+
+(* loop loop *)
+  destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]].
+  destruct (H2 f k) as [S2 [A2 B2]].
+  inv B1.
+  exists S2; split.
+  eapply star_left. constructor. 
+  eapply star_trans. eexact A1. 
+  eapply star_left. constructor. eexact A2.
+  reflexivity. reflexivity. traceEq.
+  auto.
+
+(* loop stop *)
+  destruct (H0 f (Kseq (Sloop s) k)) as [S1 [A1 B1]].
+  set (S2 :=
+    match out with
+    | Out_exit n => State f (Sexit n) k sp e1 m1
+    | _ => S1
+    end).
+  exists S2; split.
+  eapply star_left. constructor. eapply star_trans. eexact A1.
+  unfold S2; destruct out; try (apply star_refl).
+  inv B1. apply star_one. constructor.
+  reflexivity. traceEq.
+  unfold S2; inv B1; congruence || simpl; constructor; auto.
+
+(* block *)
+  destruct (H0 f (Kblock k)) as [S1 [A1 B1]].
+  set (S2 :=
+    match out with
+    | Out_normal => State f Sskip k sp e1 m1
+    | Out_exit O => State f Sskip k sp e1 m1
+    | Out_exit (S m) => State f (Sexit m) k sp e1 m1
+    | _ => S1
+    end).
+  exists S2; split.
+  eapply star_left. constructor. eapply star_trans. eexact A1.
+  unfold S2; destruct out; try (apply star_refl).
+  inv B1. apply star_one. constructor.
+  inv B1. apply star_one. destruct n; constructor.
+  reflexivity. traceEq.
+  unfold S2; inv B1; simpl; try constructor; auto.
+  destruct n; constructor.
+
+(* exit *)
+  econstructor; split. apply star_refl. constructor.
+
+(* switch *)
+  econstructor; split.
+  apply star_one. econstructor; eauto. 
+  constructor.
+
+(* return none *)
+  econstructor; split. apply star_refl. constructor; auto.
+
+(* return some *)
+  econstructor; split. apply star_refl. constructor; auto.
+
+(* tailcall *)
+  econstructor; split.
+  eapply star_left. econstructor; eauto.  
+  apply H4. apply is_call_cont_call_cont. traceEq.
+  constructor. 
+Qed.
+
+Lemma eval_funcall_steps:
+   forall m fd args t m' res,
+   eval_funcall ge m fd args t m' res ->
+   forall k,
+   is_call_cont k ->
+   star step ge (Callstate fd args k m)
+              t (Returnstate res k m').
+Proof (proj1 eval_funcall_exec_stmt_steps).
+
+Lemma exec_stmt_steps:
+   forall sp e m s t e' m' out,
+   exec_stmt ge sp e m s t e' m' out ->
+   forall f k,
+   exists S,
+   star step ge (State f s k sp e m) t S
+   /\ outcome_state_match sp e' m' f k out S.
+Proof (proj2 eval_funcall_exec_stmt_steps).
+
+Lemma evalinf_funcall_forever:
+  forall m fd args T k,
+  evalinf_funcall ge m fd args T ->
+  forever_plus step ge (Callstate fd args k m) T.
+Proof.
+  cofix CIH_FUN.
+  assert (forall sp e m s T f k,
+          execinf_stmt ge sp e m s T ->
+          forever_plus step ge (State f s k sp e m) T).
+  cofix CIH_STMT.
+  intros. inv H.
+
+(* call *)
+  eapply forever_plus_intro.
+  apply plus_one. econstructor; eauto. 
+  apply CIH_FUN. eauto. traceEq.
+
+(* ifthenelse *)
+  eapply forever_plus_intro with (s2 := State f (if b then s1 else s2) k sp e m).
+  apply plus_one. econstructor; eauto. 
+  apply CIH_STMT. eauto. traceEq.
+
+(* seq 1 *)
+  eapply forever_plus_intro.
+  apply plus_one. constructor.
+  apply CIH_STMT. eauto. traceEq.
+
+(* seq 2 *)
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq s2 k))
+  as [S [A B]]. inv B.
+  eapply forever_plus_intro.
+  eapply plus_left. constructor.
+  eapply star_right. eexact A. constructor. 
+  reflexivity. reflexivity.
+  apply CIH_STMT. eauto. traceEq. 
+
+(* loop body *)
+  eapply forever_plus_intro.
+  apply plus_one. econstructor; eauto.
+  apply CIH_STMT. eauto. traceEq.
+
+(* loop loop *)
+  destruct (exec_stmt_steps _ _ _ _ _ _ _ _ H0 f (Kseq (Sloop s0) k))
+  as [S [A B]]. inv B.
+  eapply forever_plus_intro.
+  eapply plus_left. constructor.
+  eapply star_right. eexact A. constructor. 
+  reflexivity. reflexivity.
+  apply CIH_STMT. eauto. traceEq.
+
+(* block *)
+  eapply forever_plus_intro.
+  apply plus_one. econstructor; eauto.
+  apply CIH_STMT. eauto. traceEq.
+
+(* tailcall *)
+  eapply forever_plus_intro.
+  apply plus_one. econstructor; eauto. 
+  apply CIH_FUN. eauto. traceEq.
+
+(* function call *)
+  intros. inv H0.
+  eapply forever_plus_intro.
+  apply plus_one. econstructor; eauto.
+  apply H. eauto. 
+  traceEq.
+Qed.
+
+Theorem exec_program_bigstep_transition:
+  forall beh,
+  exec_program_bigstep prog beh ->
+  exec_program prog beh.
+Proof.
+  intros. inv H.
+  (* termination *)
+  econstructor.
+  econstructor. eauto. eauto. auto. 
+  apply eval_funcall_steps. eauto. red; auto. 
+  econstructor. 
+  (* divergence *)
+  econstructor.
+  econstructor. eauto. eauto. auto. 
+  apply forever_plus_forever. 
+  apply evalinf_funcall_forever. auto.
+Qed.
+
+End BIGSTEP_TO_TRANSITION.
+
+
+
+
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 35788685..60c1d57a 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -67,6 +67,7 @@ Inductive stmt : Set :=
   | Sassign : ident -> expr -> stmt
   | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
   | Scall : option ident -> signature -> expr -> exprlist -> stmt
+  | Stailcall: signature -> expr -> exprlist -> stmt
   | Salloc : ident -> expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
@@ -75,7 +76,8 @@ Inductive stmt : Set :=
   | Sexit: nat -> stmt
   | Sswitch: expr -> list (int * nat) -> nat -> stmt
   | Sreturn: option expr -> stmt
-  | Stailcall: signature -> expr -> exprlist -> stmt.
+  | Slabel: label -> stmt -> stmt
+  | Sgoto: label -> stmt.
 
 Record function : Set := mkfunction {
   fn_sig: signature;
@@ -105,6 +107,38 @@ Definition funsig (fd: fundef) :=
 Definition genv := Genv.t fundef.
 Definition letenv := list val.
 
+(** Continuations *)
+
+Inductive cont: Set :=
+  | Kstop: cont                         (**r stop program execution *)
+  | Kseq: stmt -> cont -> cont          (**r execute stmt, then cont *)
+  | Kblock: cont -> cont                (**r exit a block, then do cont *)
+  | Kcall: option ident -> function -> val -> env -> cont -> cont.
+                                        (**r return to caller *)
+
+(** States *)
+
+Inductive state: Set :=
+  | State:                              (**r execution within a function *)
+      forall (f: function)              (**r currently executing function  *)
+             (s: stmt)                  (**r statement under consideration *)
+             (k: cont)                  (**r its continuation -- what to do next *)
+             (sp: val)                  (**r current stack pointer *)
+             (e: env)                   (**r current local environment *)
+             (m: mem),                  (**r current memory state *)
+      state
+  | Callstate:                          (**r invocation of a fundef  *)
+      forall (f: fundef)                (**r fundef to invoke *)
+             (args: list val)           (**r arguments provided by caller *)
+             (k: cont)                  (**r what to do next  *)
+             (m: mem),                  (**r memory state *)
+      state
+  | Returnstate:
+      forall (v: val)                   (**r return value *)
+             (k: cont)                  (**r what to do next *)
+             (m: mem),                  (**r memory state *)
+      state.
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -174,198 +208,177 @@ Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop
 
 End EVAL_EXPR.
 
-Inductive eval_funcall:
-        mem -> fundef -> list val -> trace ->
-        mem -> val -> Prop :=
-  | eval_funcall_internal:
-      forall m f vargs m1 sp e t e2 m2 out vres,
-      Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
-      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
-      exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out ->
-      outcome_result_value out f.(fn_sig).(sig_res) vres ->
-      eval_funcall m (Internal f) vargs t (outcome_free_mem out m2 sp) vres
-  | eval_funcall_external:
-      forall ef m args t res,
-      event_match ef args t res ->
-      eval_funcall m (External ef) args t m res
-
-with exec_stmt:
-         val ->
-         env -> mem -> stmt -> trace ->
-         env -> mem -> outcome -> Prop :=
-  | exec_Sskip:
-      forall sp e m,
-      exec_stmt sp e m Sskip E0 e m Out_normal
-  | exec_Sassign:
-      forall sp e m id a v,
+(** Pop continuation until a call or stop *)
+
+Fixpoint call_cont (k: cont) : cont :=
+  match k with
+  | Kseq s k => call_cont k
+  | Kblock k => call_cont k
+  | _ => k
+  end.
+
+Definition is_call_cont (k: cont) : Prop :=
+  match k with
+  | Kstop => True
+  | Kcall _ _ _ _ _ => True
+  | _ => False
+  end.
+
+(** Find the statement and manufacture the continuation 
+  corresponding to a label *)
+
+Fixpoint find_label (lbl: label) (s: stmt) (k: cont) 
+                    {struct s}: option (stmt * cont) :=
+  match s with
+  | Sseq s1 s2 =>
+      match find_label lbl s1 (Kseq s2 k) with
+      | Some sk => Some sk
+      | None => find_label lbl s2 k
+      end
+  | Sifthenelse a s1 s2 =>
+      match find_label lbl s1 k with
+      | Some sk => Some sk
+      | None => find_label lbl s2 k
+      end
+  | Sloop s1 =>
+      find_label lbl s1 (Kseq (Sloop s1) k)
+  | Sblock s1 =>
+      find_label lbl s1 (Kblock k)
+  | Slabel lbl' s' =>
+      if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
+  | _ => None
+  end.
+
+(** One step of execution *)
+
+Inductive step: state -> trace -> state -> Prop :=
+
+  | step_skip_seq: forall f s k sp e m,
+      step (State f Sskip (Kseq s k) sp e m)
+        E0 (State f s k sp e m)
+  | step_skip_block: forall f k sp e m,
+      step (State f Sskip (Kblock k) sp e m)
+        E0 (State f Sskip k sp e m)
+  | step_skip_call: forall f k sp e m,
+      is_call_cont k ->
+      f.(fn_sig).(sig_res) = None ->
+      step (State f Sskip k (Vptr sp Int.zero) e m)
+        E0 (Returnstate Vundef k (Mem.free m sp))
+
+  | step_assign: forall f id a k sp e m v,
       eval_expr sp e m nil a v ->
-      exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
-  | exec_Sstore:
-      forall sp e m chunk addr al b vl v vaddr m',
+      step (State f (Sassign id a) k sp e m)
+        E0 (State f Sskip k sp (PTree.set id v e) m)
+
+  | step_store: forall f chunk addr al b k sp e m vl v vaddr m',
       eval_exprlist sp e m nil al vl ->
       eval_expr sp e m nil b v ->
       eval_addressing ge sp addr vl = Some vaddr ->
       Mem.storev chunk m vaddr v = Some m' ->
-      exec_stmt sp e m (Sstore chunk addr al b) E0 e m' Out_normal
-  | exec_Scall:
-      forall sp e m optid sig a bl vf vargs f t m' vres e',
+      step (State f (Sstore chunk addr al b) k sp e m)
+        E0 (State f Sskip k sp e m')
+
+  | step_call: forall f optid sig a bl k sp e m vf vargs fd,
       eval_expr sp e m nil a vf ->
       eval_exprlist sp e m nil bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall m f vargs t m' vres ->
-      e' = set_optvar optid vres e ->
-      exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal
-  | exec_Salloc:
-      forall sp e m id a n m' b,
-      eval_expr sp e m nil a (Vint n) ->
-      Mem.alloc m 0 (Int.signed n) = (m', b) ->
-      exec_stmt sp e m (Salloc id a) 
-                E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal
-  | exec_Sifthenelse:
-      forall sp e m a s1 s2 v t e' m' out,
-      eval_condexpr sp e m nil a v ->
-      exec_stmt sp e m (if v then s1 else s2) t e' m' out ->
-      exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out
-  | exec_Sseq_continue:
-      forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
-      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
-      exec_stmt sp e1 m1 s2 t2 e2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt sp e m (Sseq s1 s2) t e2 m2 out
-  | exec_Sseq_stop:
-      forall sp e m t s1 s2 e1 m1 out,
-      exec_stmt sp e m s1 t e1 m1 out ->
-      out <> Out_normal ->
-      exec_stmt sp e m (Sseq s1 s2) t e1 m1 out
-  | exec_Sloop_loop:
-      forall sp e m s t t1 e1 m1 t2 e2 m2 out,
-      exec_stmt sp e m s t1 e1 m1 Out_normal ->
-      exec_stmt sp e1 m1 (Sloop s) t2 e2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt sp e m (Sloop s) t e2 m2 out
-  | exec_Sloop_stop:
-      forall sp e m t s e1 m1 out,
-      exec_stmt sp e m s t e1 m1 out ->
-      out <> Out_normal ->
-      exec_stmt sp e m (Sloop s) t e1 m1 out
-  | exec_Sblock:
-      forall sp e m s t e1 m1 out,
-      exec_stmt sp e m s t e1 m1 out ->
-      exec_stmt sp e m (Sblock s) t e1 m1 (outcome_block out)
-  | exec_Sexit:
-      forall sp e m n,
-      exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
-  | exec_Sswitch:
-      forall sp e m a cases default n,
-      eval_expr sp e m nil a (Vint n) ->
-      exec_stmt sp e m (Sswitch a cases default)
-                E0 e m (Out_exit (switch_target n default cases))
-  | exec_Sreturn_none:
-      forall sp e m,
-      exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
-  | exec_Sreturn_some:
-      forall sp e m a v,
-      eval_expr sp e m nil a v ->
-      exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
-  | exec_Stailcall:
-      forall sp e m sig a bl vf vargs f t m' vres,
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      step (State f (Scall optid sig a bl) k sp e m)
+        E0 (Callstate fd vargs (Kcall optid f sp e k) m)
+
+  | step_tailcall: forall f sig a bl k sp e m vf vargs fd,
       eval_expr (Vptr sp Int.zero) e m nil a vf ->
       eval_exprlist (Vptr sp Int.zero) e m nil bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall (Mem.free m sp) f vargs t m' vres ->
-      exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres).
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
+        E0 (Callstate fd vargs (call_cont k) (Mem.free m sp))
 
-Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
-  with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop.
-
-(** Coinductive semantics for divergence. *)
-
-CoInductive evalinf_funcall:
-        mem -> fundef -> list val -> traceinf -> Prop :=
-  | evalinf_funcall_internal:
-      forall m f vargs m1 sp e t,
-      Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
+  | step_alloc: forall f id a k sp e m n m' b,
+      eval_expr sp e m nil a (Vint n) ->
+      Mem.alloc m 0 (Int.signed n) = (m', b) ->
+      step (State f (Salloc id a) k sp e m)
+        E0 (State f Sskip k sp (PTree.set id (Vptr b Int.zero) e) m')
+
+  | step_seq: forall f s1 s2 k sp e m,
+      step (State f (Sseq s1 s2) k sp e m)
+        E0 (State f s1 (Kseq s2 k) sp e m)
+
+  | step_ifthenelse: forall f a s1 s2 k sp e m b,
+      eval_condexpr sp e m nil a b ->
+      step (State f (Sifthenelse a s1 s2) k sp e m)
+        E0 (State f (if b then s1 else s2) k sp e m)
+
+  | step_loop: forall f s k sp e m,
+      step (State f (Sloop s) k sp e m)
+        E0 (State f s (Kseq (Sloop s) k) sp e m)
+
+  | step_block: forall f s k sp e m,
+      step (State f (Sblock s) k sp e m)
+        E0 (State f s (Kblock k) sp e m)
+
+  | step_exit_seq: forall f n s k sp e m,
+      step (State f (Sexit n) (Kseq s k) sp e m)
+        E0 (State f (Sexit n) k sp e m)
+  | step_exit_block_0: forall f k sp e m,
+      step (State f (Sexit O) (Kblock k) sp e m)
+        E0 (State f Sskip k sp e m)
+  | step_exit_block_S: forall f n k sp e m,
+      step (State f (Sexit (S n)) (Kblock k) sp e m)
+        E0 (State f (Sexit n) k sp e m)
+
+  | step_switch: forall f a cases default k sp e m n,
+      eval_expr sp e m nil a (Vint n) ->
+      step (State f (Sswitch a cases default) k sp e m)
+        E0 (State f (Sexit (switch_target n default cases)) k sp e m)
+
+  | step_return_0: forall f k sp e m,
+      f.(fn_sig).(sig_res) = None ->
+      step (State f (Sreturn None) k (Vptr sp Int.zero) e m)
+        E0 (Returnstate Vundef (call_cont k) (Mem.free m sp))
+  | step_return_1: forall f a k sp e m v,
+      f.(fn_sig).(sig_res) <> None ->
+      eval_expr (Vptr sp Int.zero) e m nil a v ->
+      step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m)
+        E0 (Returnstate v (call_cont k) (Mem.free m sp))
+
+  | step_label: forall f lbl s k sp e m,
+      step (State f (Slabel lbl s) k sp e m)
+        E0 (State f s k sp e m)
+
+  | step_goto: forall f lbl k sp e m s' k',
+      find_label lbl f.(fn_body) (call_cont k) = Some(s', k') ->
+      step (State f (Sgoto lbl) k sp e m)
+        E0 (State f s' k' sp e m)
+
+  | step_internal_function: forall f vargs k m m' sp e,
+      Mem.alloc m 0 f.(fn_stackspace) = (m', sp) ->
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
-      execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t ->
-      evalinf_funcall m (Internal f) vargs t
+      step (Callstate (Internal f) vargs k m)
+        E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
+  | step_external_function: forall ef vargs k m t vres,
+      event_match ef vargs t vres ->
+      step (Callstate (External ef) vargs k m)
+         t (Returnstate vres k m)        
 
-(** [execinf_stmt ge sp e m s t] means that statement [s] diverges.
-  [e] is the initial environment, [m] is the initial memory state,
-  and [t] the trace of observable events performed during the execution. *)
-
-with execinf_stmt:
-         val -> env -> mem -> stmt -> traceinf -> Prop :=
-  | execinf_Scall:
-      forall sp e m optid sig a bl vf vargs f t,
-      eval_expr sp e m nil a vf ->
-      eval_exprlist sp e m nil bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      evalinf_funcall m f vargs t ->
-      execinf_stmt sp e m (Scall optid sig a bl) t
-  | execinf_Sifthenelse:
-      forall sp e m a s1 s2 v t,
-      eval_condexpr sp e m nil a v ->
-      execinf_stmt sp e m (if v then s1 else s2) t ->
-      execinf_stmt sp e m (Sifthenelse a s1 s2) t
-  | execinf_Sseq_1:
-      forall sp e m t s1 s2,
-      execinf_stmt sp e m s1 t ->
-      execinf_stmt sp e m (Sseq s1 s2) t
-  | execinf_Sseq_2:
-      forall sp e m t s1 t1 e1 m1 s2 t2,
-      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
-      execinf_stmt sp e1 m1 s2 t2 ->
-      t = t1 *** t2 ->
-      execinf_stmt sp e m (Sseq s1 s2) t
-  | execinf_Sloop_body:
-      forall sp e m s t,
-      execinf_stmt sp e m s t ->
-      execinf_stmt sp e m (Sloop s) t
-  | execinf_Sloop_loop:
-      forall sp e m s t t1 e1 m1 t2,
-      exec_stmt sp e m s t1 e1 m1 Out_normal ->
-      execinf_stmt sp e1 m1 (Sloop s) t2 ->
-      t = t1 *** t2 ->
-      execinf_stmt sp e m (Sloop s) t
-  | execinf_Sblock:
-      forall sp e m s t,
-      execinf_stmt sp e m s t ->
-      execinf_stmt sp e m (Sblock s) t
-  | execinf_Stailcall:
-      forall sp e m sig a bl vf vargs f t,
-      eval_expr (Vptr sp Int.zero) e m nil a vf ->
-      eval_exprlist (Vptr sp Int.zero) e m nil bl vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      evalinf_funcall (Mem.free m sp) f vargs t ->
-      execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t.
+  | step_return: forall v optid f sp e k m,
+      step (Returnstate v (Kcall optid f sp e k) m)
+        E0 (State f Sskip k sp (set_optvar optid v e) m).
 
 End RELSEM.
 
-(** Execution of a whole program: [exec_program p beh]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] has [beh] as observable
-  behavior. *)
-
-Inductive exec_program (p: program): program_behavior -> Prop :=
-  | program_terminates:
-      forall b f t m r,
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b f,
       let ge := Genv.globalenv p in
       let m0 := Genv.init_mem p in
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
-      eval_funcall ge m0 f nil t m (Vint r) ->
-      exec_program p (Terminates t r)
-  | program_diverges:
-      forall b f t,
-      let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      funsig f = mksignature nil (Some Tint) ->
-      evalinf_funcall ge m0 f nil t ->
-      exec_program p (Diverges t).
+      initial_state p (Callstate f nil Kstop m0).
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall r m,
+      final_state (Returnstate (Vint r) Kstop m) r.
+
+Definition exec_program (p: program) (beh: program_behavior) : Prop :=
+  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
diff --git a/backend/RTLbigstep.v b/backend/RTLbigstep.v
deleted file mode 100644
index 182f5935..00000000
--- a/backend/RTLbigstep.v
+++ /dev/null
@@ -1,412 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** An alternate, mixed-step semantics for the RTL intermediate language. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Events.
-Require Import Mem.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-
-Section BIGSTEP.
-
-Variable ge: genv.
-
-(** The dynamic semantics of RTL is a combination of small-step (transition)
-  semantics and big-step semantics.  Execution of an instruction performs
-  a single transition to the next instruction (small-step), except if
-  the instruction is a function call.  In this case, the whole body of
-  the called function is executed at once and the transition terminates
-  on the instruction immediately following the call in the caller function.
-  Such ``mixed-step'' semantics is convenient for reasoning over
-  intra-procedural analyses and transformations.  It also dispenses us
-  from making the call stack explicit in the semantics.
-
-  The semantics is organized in three mutually inductive predicates.
-  The first is [exec_instr ge c sp pc rs m pc' rs' m'].  [ge] is the
-  global environment (see module [Genv]), [c] the CFG for the current
-  function, and [sp] the pointer to the stack block for its
-  current activation (as in Cminor).  [pc], [rs] and [m] is the 
-  initial state of the transition: program point (CFG node) [pc],
-  register state (mapping of pseudo-registers to values) [rs],
-  and memory state [m].  The final state is [pc'], [rs'] and [m']. *)
-
-Inductive exec_instr: code -> val ->
-                      node -> regset -> mem -> trace ->
-                      node -> regset -> mem -> Prop :=
-  | exec_Inop:
-      forall c sp pc rs m pc',
-      c!pc = Some(Inop pc') ->
-      exec_instr c sp  pc rs m  E0 pc' rs m
-  | exec_Iop:
-      forall c sp pc rs m op args res pc' v,
-      c!pc = Some(Iop op args res pc') ->
-      eval_operation ge sp op rs##args m = Some v ->
-      exec_instr c sp  pc rs m  E0 pc' (rs#res <- v) m
-  | exec_Iload:
-      forall c sp pc rs m chunk addr args dst pc' a v,
-      c!pc = Some(Iload chunk addr args dst pc') ->
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      exec_instr c sp  pc rs m  E0 pc' (rs#dst <- v) m
-  | exec_Istore:
-      forall c sp pc rs m chunk addr args src pc' a m',
-      c!pc = Some(Istore chunk addr args src pc') ->
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a rs#src = Some m' ->
-      exec_instr c sp  pc rs m  E0 pc' rs m'
-  | exec_Icall:
-      forall c sp pc rs m sig ros args res pc' f vres m' t,
-      c!pc = Some(Icall sig ros args res pc') ->
-      find_function ge ros rs = Some f ->
-      funsig f = sig ->
-      exec_function f rs##args m t vres m' ->
-      exec_instr c sp  pc rs m  t pc' (rs#res <- vres) m'
-  | exec_Ialloc:
-      forall c sp pc rs m pc' arg res sz m' b,
-      c!pc = Some(Ialloc arg res pc') ->
-      rs#arg = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-      exec_instr c sp  pc rs m E0 pc' (rs#res <- (Vptr b Int.zero)) m'
-  | exec_Icond_true:
-      forall c sp pc rs m cond args ifso ifnot,
-      c!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args m = Some true ->
-      exec_instr c sp  pc rs m  E0 ifso rs m
-  | exec_Icond_false:
-      forall c sp pc rs m cond args ifso ifnot,
-      c!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args m = Some false ->
-      exec_instr c sp  pc rs m  E0 ifnot rs m
-
-(** [exec_body ge c sp pc rs m res m'] repeatedly executes
-   instructions starting at [pc] in [c], until it
-   reaches a return or tailcall instruction.  It performs
-   that instruction and sets [res] to the return value
-   and [m'] to the final memory state. *)
-
-with exec_body: code -> val ->
-                node -> regset -> mem -> trace ->
-                val -> mem -> Prop :=
-  | exec_body_step: forall c sp pc rs m t1 pc1 rs1 m1 t2 t res m2,
-      exec_instr c sp  pc rs m  t1  pc1 rs1 m1 ->
-      exec_body c sp  pc1 rs1 m1  t2  res m2 ->
-      t = t1 ** t2 ->
-      exec_body c sp  pc rs m  t  res m2
-  | exec_Ireturn: forall c stk pc rs m or res,
-      c!pc = Some(Ireturn or) ->
-      res = regmap_optget or Vundef rs ->
-      exec_body c (Vptr stk Int.zero)  pc rs m  E0  res (Mem.free m stk)
-  | exec_Itailcall: forall c stk pc rs m sig ros args f t res m',
-      c!pc = Some(Itailcall sig ros args) ->
-      find_function ge ros rs = Some f ->
-      funsig f = sig ->
-      exec_function f rs##args (Mem.free m stk) t res m' ->
-      exec_body c (Vptr stk Int.zero)  pc rs m  t  res m'
-
-(** [exec_function ge f args m res m'] executes a function application.
-  [f] is the called function, [args] the values of its arguments,
-  and [m] the memory state at the beginning of the call.  [res] is
-  the returned value: the value of [r] if the function terminates with 
-  a [Ireturn (Some r)], or [Vundef] if it terminates with [Ireturn None].
-  Evaluation proceeds by executing transitions from the function's entry
-  point to the first [Ireturn] instruction encountered.  It is preceeded
-  by the allocation of the stack activation block and the binding
-  of register parameters to the provided arguments.
-  (Non-parameter registers are initialized to [Vundef].)  Before returning,
-  the stack activation block is freed. *)
-
-with exec_function: fundef -> list val -> mem -> trace ->
-                              val -> mem -> Prop :=
-  | exec_funct_internal:
-      forall f m m1 stk args t m2 vres,
-      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
-      exec_body f.(fn_code) (Vptr stk Int.zero) 
-                f.(fn_entrypoint) (init_regs args f.(fn_params)) m1
-                t vres m2 ->
-      exec_function (Internal f) args m t vres m2
-  | exec_funct_external:
-      forall ef args m t res,
-      event_match ef args t res ->
-      exec_function (External ef) args m t res m.
-
-Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop
-  with exec_body_ind_3 := Minimality for exec_body Sort Prop
-  with exec_function_ind_3 := Minimality for exec_function Sort Prop.
-
-(** The reflexive transitive closure of [exec_instr]. *)
-
-Inductive exec_instrs: code -> val ->
-                       node -> regset -> mem -> trace ->
-                       node -> regset -> mem -> Prop :=
-  | exec_refl:
-      forall c sp pc rs m,
-      exec_instrs c sp pc rs m E0 pc rs m
-  | exec_one:
-      forall c sp pc rs m t pc' rs' m',
-      exec_instr c sp pc rs m t pc' rs' m' ->
-      exec_instrs c sp pc rs m t pc' rs' m'
-  | exec_trans:
-      forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3,
-      exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
-      exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 ->
-      t3 = t1 ** t2 ->
-      exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3.
-
-(** Some derived execution rules. *)
-
-Lemma exec_instrs_exec_body:
-  forall c sp pc1 rs1 m1 t1 pc2 rs2 m2,
-  exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
-  forall res t2 m3 t3,
-  exec_body c sp pc2 rs2 m2 t2 res m3 ->
-  t3 = t1 ** t2 ->
-  exec_body c sp pc1 rs1 m1 t3 res m3.
-Proof.
-  induction 1; intros.
-  subst t3. rewrite E0_left. auto.
-  eapply exec_body_step; eauto.
-  eapply IHexec_instrs1. eapply IHexec_instrs2. eauto. 
-  eauto. traceEq. 
-Qed.
-
-Lemma exec_step:
-  forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3,
-  exec_instr c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
-  exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 ->
-  t3 = t1 ** t2 ->
-  exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3.
-Proof.
-  intros. eapply exec_trans. apply exec_one. eauto. eauto. auto.
-Qed.
-
-Lemma exec_Iop':
-  forall c sp pc rs m op args res pc' rs' v,
-  c!pc = Some(Iop op args res pc') ->
-  eval_operation ge sp op rs##args m = Some v ->
-  rs' = (rs#res <- v) ->
-  exec_instr c sp  pc rs m  E0 pc' rs' m.
-Proof.
-  intros. subst rs'. eapply exec_Iop; eauto.
-Qed.
-
-Lemma exec_Iload':
-  forall c sp pc rs m chunk addr args dst pc' rs' a v,
-  c!pc = Some(Iload chunk addr args dst pc') ->
-  eval_addressing ge sp addr rs##args = Some a ->
-  Mem.loadv chunk m a = Some v ->
-  rs' = (rs#dst <- v) ->
-  exec_instr c sp  pc rs m E0 pc' rs' m.
-Proof.
-  intros. subst rs'. eapply exec_Iload; eauto.
-Qed.
-
-(** Experimental: coinductive big-step semantics for divergence. *)
-
-CoInductive diverge_body:
-      code -> val -> node -> regset -> mem -> traceinf -> Prop :=
-  | diverge_step: forall c sp pc rs m t1 pc1 rs1 m1 T2 T,
-      exec_instr c sp  pc rs m  t1  pc1 rs1 m1 ->
-      diverge_body c sp  pc1 rs1 m1  T2 ->
-      T = t1 *** T2 ->
-      diverge_body c sp  pc rs m  T
-  | diverge_Icall:
-      forall c sp pc rs m sig ros args res pc' f T,
-      c!pc = Some(Icall sig ros args res pc') ->
-      find_function ge ros rs = Some f ->
-      funsig f = sig ->
-      diverge_function f rs##args m T ->
-      diverge_body c sp  pc rs m  T
-  | diverge_Itailcall: forall c stk pc rs m sig ros args f T,
-      c!pc = Some(Itailcall sig ros args) ->
-      find_function ge ros rs = Some f ->
-      funsig f = sig ->
-      diverge_function f rs##args (Mem.free m stk) T ->
-      diverge_body c (Vptr stk Int.zero)  pc rs m  T
-
-with diverge_function: fundef -> list val -> mem -> traceinf -> Prop :=
-  | diverge_funct_internal:
-      forall f m m1 stk args T,
-      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
-      diverge_body f.(fn_code) (Vptr stk Int.zero) 
-                   f.(fn_entrypoint) (init_regs args f.(fn_params)) m1
-                   T ->
-      diverge_function (Internal f) args m T.
-
-End BIGSTEP.
-
-(** Execution of whole programs. *)
-
-Inductive exec_program (p: program): program_behavior -> Prop :=
-  | exec_program_terminates: forall b f t r m,
-      let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      funsig f = mksignature nil (Some Tint) ->
-      exec_function ge f nil m0 t (Vint r) m ->
-      exec_program p (Terminates t r)
-  | exec_program_diverges: forall b f T,
-      let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      funsig f = mksignature nil (Some Tint) ->
-      diverge_function ge f nil m0 T ->
-      exec_program p (Diverges T).
-
-(** * Equivalence with the transition semantics. *)
-
-Section EQUIVALENCE.
-
-Variable ge: genv.
-
-Definition exec_instr_prop
-  (c: code) (sp: val) (pc1: node) (rs1: regset) (m1: mem)
-           (t: trace) (pc2: node) (rs2: regset) (m2: mem) : Prop :=
-  forall s,
-  plus step ge (State s c sp pc1 rs1 m1)
-             t (State s c sp pc2 rs2 m2).
-
-Definition exec_body_prop
-  (c: code) (sp: val) (pc1: node) (rs1: regset) (m1: mem)
-           (t: trace) (res: val) (m2: mem) : Prop :=
-  forall s,
-  plus step ge (State s c sp pc1 rs1 m1)
-             t (Returnstate s res m2).
-
-Definition exec_function_prop
-  (f: fundef) (args: list val) (m1: mem)
-  (t: trace) (res: val) (m2: mem) : Prop :=
-  forall s,
-  plus step ge (Callstate s f args m1)
-             t (Returnstate s res m2).
-
-Lemma exec_steps:
-  (forall c sp pc1 rs1 m1 t pc2 rs2 m2,
-   exec_instr ge c sp pc1 rs1 m1 t pc2 rs2 m2 ->
-   exec_instr_prop c sp pc1 rs1 m1 t pc2 rs2 m2) /\
-  (forall c sp pc1 rs1 m1 t res m2,
-   exec_body ge c sp pc1 rs1 m1 t res m2 ->
-   exec_body_prop c sp pc1 rs1 m1 t res m2) /\
-  (forall f args m1 t res m2,
-   exec_function ge f args m1 t res m2 ->
-   exec_function_prop f args m1 t res m2).
-Proof.
-  set (IND := fun a b c d e f g h i j k l m =>
-          conj (exec_instr_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m)
-               (conj (exec_body_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m)
-                     (exec_function_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m))).
-  apply IND; clear IND;
-  intros; red; intros.
-  (* nop *)
-  apply plus_one. eapply RTL.exec_Inop; eauto.
-  (* op *)
-  apply plus_one. eapply RTL.exec_Iop'; eauto. 
-  (* load *)
-  apply plus_one. eapply RTL.exec_Iload'; eauto.
-  (* store *)
-  apply plus_one. eapply RTL.exec_Istore; eauto.
-  (* call *)
-  eapply plus_left'. eapply RTL.exec_Icall; eauto.
-  eapply plus_right'. apply H3. apply RTL.exec_return. 
-  eauto. traceEq.
-  (* alloc *)
-  apply plus_one. eapply RTL.exec_Ialloc; eauto. 
-  (* cond true *)
-  apply plus_one. eapply RTL.exec_Icond_true; eauto.  
-  (* cond false *)
-  apply plus_one. eapply RTL.exec_Icond_false; eauto.
-  (* body step *)
-  eapply plus_trans. apply H0. apply H2. auto.
-  (* body return *)
-  apply plus_one. rewrite H0. eapply RTL.exec_Ireturn; eauto.
-  (* body tailcall *)
-  eapply plus_left'. eapply RTL.exec_Itailcall; eauto. 
-  apply H3. traceEq.
-  (* internal function *)
-  eapply plus_left'. eapply RTL.exec_function_internal; eauto. 
-  apply H1. traceEq.
-  (* external function *)
-  apply plus_one. eapply RTL.exec_function_external; eauto.
-Qed.
-
-Lemma diverge_function_steps:
-  forall fd args m T s,
-  diverge_function ge fd args m T ->
-  forever step ge (Callstate s fd args m) T.
-Proof.
-  assert (diverge_function_steps':
-          forall fd args m T s,
-          diverge_function ge fd args m T ->
-          forever_N step ge O (Callstate s fd args m) T).
-  cofix COINDHYP1.
-  assert (diverge_body_steps: forall c sp pc rs m T s,
-          diverge_body ge c sp pc rs m T ->
-          forever_N step ge O (State s c sp pc rs m) T).
-  cofix COINDHYP2; intros.
-  inv H. 
-  (* step *)
-  apply forever_N_plus with (State s c sp pc1 rs1 m1) O.
-  destruct exec_steps as [E [F G]].
-  apply E. assumption.
-  apply COINDHYP2. assumption.
-  (* call *)
-  change T with (E0 *** T).
-  apply forever_N_plus with (Callstate (Stackframe res c sp pc' rs :: s)
-                                       f rs##args m) O.
-  apply plus_one. eapply RTL.exec_Icall; eauto. 
-  apply COINDHYP1. assumption.
-  (* tailcall *)
-  change T with (E0 *** T).
-  apply forever_N_plus with (Callstate s f rs##args (free m stk)) O.
-  apply plus_one. eapply RTL.exec_Itailcall; eauto. 
-  apply COINDHYP1. assumption.
-  (* internal function *)
-  intros. inv H. 
-  change T with (E0 *** T).
-  apply forever_N_plus with
-    (State s f.(fn_code) (Vptr stk Int.zero)
-             f.(fn_entrypoint) (init_regs args f.(fn_params)) m1) O.
-  apply plus_one. eapply RTL.exec_function_internal; eauto.
-  apply diverge_body_steps. assumption.
-  (* conclusion *)
-  intros. eapply forever_N_forever. eauto.
-Qed.
-
-End EQUIVALENCE.
-
-Theorem exec_program_bigstep_smallstep:
-  forall p beh,
-  exec_program p beh ->
-  RTL.exec_program p beh.
-Proof.
-  intros. unfold RTL.exec_program. inv H. 
-  econstructor. 
-  econstructor; eauto. 
-  apply plus_star.
-  destruct (exec_steps (Genv.globalenv p)) as [E [F G]].
-  apply (G _ _ _ _ _ _ H3).
-  constructor.
-  econstructor.
-  econstructor; eauto.
-  apply diverge_function_steps. auto. 
-Qed.
-
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 3cc0eebf..5fde3d88 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -64,7 +64,8 @@ Inductive state_incr: state -> state -> Prop :=
     forall (s1 s2: state),
     Ple s1.(st_nextnode) s2.(st_nextnode) ->
     Ple s1.(st_nextreg) s2.(st_nextreg) ->
-    (forall pc, Plt pc s1.(st_nextnode) -> s2.(st_code)!pc = s1.(st_code)!pc) ->
+    (forall pc,
+      s1.(st_code)!pc = None \/ s2.(st_code)!pc = s1.(st_code)!pc) ->
     state_incr s1 s2.
 
 Lemma state_incr_refl:
@@ -73,19 +74,15 @@ Proof.
   intros. apply state_incr_intro.
   apply Ple_refl. apply Ple_refl. intros; auto.
 Qed.
-Hint Resolve state_incr_refl: rtlg.
 
 Lemma state_incr_trans:
   forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3.
 Proof.
-  intros. inversion H. inversion H0. apply state_incr_intro.
+  intros. inv H; inv H0. apply state_incr_intro.
   apply Ple_trans with (st_nextnode s2); assumption. 
   apply Ple_trans with (st_nextreg s2); assumption.
-  intros. transitivity (s2.(st_code)!pc).
-  apply H8. apply Plt_Ple_trans with s1.(st_nextnode); auto.
-  apply H3; auto.
+  intros. generalize (H3 pc) (H5 pc). intuition congruence.
 Qed.
-Hint Resolve state_incr_trans: rtlg.
 
 (** ** The state and error monad *)
 
@@ -148,6 +145,15 @@ Notation "'do' X <- A ; B" := (bind A (fun X => B))
 Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
    (at level 200, X ident, Y ident, A at level 100, B at level 200).
 
+Definition handle_error (A: Set) (f g: mon A) : mon A :=
+  fun (s: state) =>
+    match f s with
+    | OK a s' i => OK a s' i
+    | Error _ => g s
+    end.
+
+Implicit Arguments handle_error [A].
+
 (** ** Operations on state *)
 
 (** The initial state (empty CFG). *)
@@ -186,16 +192,14 @@ Proof.
   constructor; simpl.
   apply Ple_succ.
   apply Ple_refl.
-  intros. apply PTree.gso. apply Plt_ne; auto.
+  intros. destruct (st_wf s pc). right. apply PTree.gso. apply Plt_ne; auto. auto.
 Qed.
 
 Definition add_instr (i: instruction) : mon node :=
   fun s =>
     let n := s.(st_nextnode) in
     OK n
-       (mkstate s.(st_nextreg)
-                (Psucc n)
-                (PTree.set n i s.(st_code))
+       (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) 
                 (add_instr_wf s i))
        (add_instr_incr s i).
 
@@ -212,12 +216,26 @@ Proof.
   right; auto.
 Qed.
 
-Definition reserve_instr (s: state): (node * state)%type :=
+Remark reserve_instr_incr:
+  forall s,
+  let n := s.(st_nextnode) in
+  state_incr s (mkstate s.(st_nextreg)
+                (Psucc n)
+                s.(st_code)
+                (reserve_instr_wf s)).
+Proof.
+  intros; constructor; simpl.
+  apply Ple_succ.
+  apply Ple_refl.
+  auto.
+Qed.
+
+Definition reserve_instr: mon node :=
+  fun (s: state) =>
   let n := s.(st_nextnode) in
-  (n, mkstate s.(st_nextreg)
-              (Psucc n)
-              s.(st_code)
-              (reserve_instr_wf s)).
+  OK n
+     (mkstate s.(st_nextreg) (Psucc n) s.(st_code) (reserve_instr_wf s))
+     (reserve_instr_incr s).
 
 Remark update_instr_wf:
   forall s n i,
@@ -231,44 +249,36 @@ Proof.
   rewrite PTree.gso; auto. exact (st_wf s pc).
 Qed.
 
-Definition update_instr (n: node) (i: instruction) (s: state) : state :=
-  match plt n s.(st_nextnode) with
-  | left PLT =>
-      mkstate s.(st_nextreg) 
-              s.(st_nextnode)
-              (PTree.set n i s.(st_code))
-              (update_instr_wf s n i PLT)
-  | right _ => s (* never happens *)
-  end.
-
-Remark add_loop_incr:
-  forall s1 s3 i,
-  let n := fst (reserve_instr s1) in
-  let s2 := snd (reserve_instr s1) in
-  state_incr s2 s3 ->
-  state_incr s1 (update_instr n i s3).
+Remark update_instr_incr:
+  forall s n i (LT: Plt n s.(st_nextnode)),
+  s.(st_code)!n = None ->
+  state_incr s
+             (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set n i s.(st_code))
+                     (update_instr_wf s n i LT)).
 Proof.
-  intros. inv H. unfold update_instr. destruct (plt n (st_nextnode s3)).
-  constructor; simpl.
-  apply Ple_trans with (st_nextnode s2).
-  unfold s2; simpl. apply Ple_succ. auto.
-  assumption.
-  intros. rewrite PTree.gso. rewrite H2. reflexivity. 
-  unfold s2; simpl. apply Plt_trans_succ. auto. 
-  apply Plt_ne. assumption.
-  elim n0. apply Plt_Ple_trans with (st_nextnode s2). 
-  unfold n, s2; simpl; apply Plt_succ. auto.
+  intros.
+  constructor; simpl; intros.
+  apply Ple_refl.
+  apply Ple_refl.
+  rewrite PTree.gsspec. destruct (peq pc n). left; congruence. right; auto.
 Qed.
 
-Definition add_loop (body: node -> mon node) : mon node :=
-  fun (s1: state) =>
-    let nloop := fst(reserve_instr s1) in
-    let s2 := snd(reserve_instr s1) in
-    match body nloop s2 with
-    | Error msg => Error msg
-    | OK nbody s3 i => 
-        OK nbody (update_instr nloop (Inop nbody) s3)
-                 (add_loop_incr s1 s3 (Inop nbody) i)
+Definition check_empty_node:
+  forall (s: state) (n: node), { s.(st_code)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_code)!n); intros. right; auto. left; auto.
+Defined.
+
+Definition update_instr (n: node) (i: instruction) : mon unit :=
+  fun s =>
+    match plt n s.(st_nextnode), check_empty_node s n with
+    | left LT, left EMPTY =>
+        OK tt
+           (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set n i s.(st_code))
+                    (update_instr_wf s n i LT))
+           (update_instr_incr s n i LT EMPTY)
+    | _, _ =>
+        Error (Errors.msg "RTLgen.update_instr")
     end.
 
 (** Generate a fresh RTL register. *)
@@ -284,8 +294,7 @@ Qed.
 Definition new_reg : mon reg :=
   fun s =>
     OK s.(st_nextreg)
-       (mkstate (Psucc s.(st_nextreg))
-                s.(st_nextnode) s.(st_code) s.(st_wf))
+       (mkstate (Psucc s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf))
        (new_reg_incr s).
 
 (** ** Operations on mappings *)
@@ -489,8 +498,10 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
   [nlist] if it terminates by an [exit n] construct.  [rret] is the
   register where the return value of the function must be stored, if any. *)
 
+Definition labelmap : Set := PTree.t node.
+
 Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
-                     (nexits: list node) (nret: node) (rret: option reg)
+                     (nexits: list node) (ngoto: labelmap) (nret: node) (rret: option reg)
                      {struct s} : mon node :=
   match s with
   | Sskip =>
@@ -513,6 +524,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do n2 <- add_instr (Icall sig (inl _ rf) rargs r n1);
       do n3 <- transl_exprlist map cl rargs n2;
          transl_expr map b rf n3
+  | Stailcall sig b cl =>
+      do rf <- alloc_reg map b;
+      do rargs <- alloc_regs map cl;
+      do n1 <- add_instr (Itailcall sig (inl _ rf) rargs);
+      do n2 <- transl_exprlist map cl rargs n1;
+         transl_expr map b rf n2
   | Salloc id a =>
       do ra <- alloc_reg map a;
       do rr <- new_reg;
@@ -520,21 +537,24 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do n2 <- add_instr (Ialloc ra rr n1);
          transl_expr map a ra n2
   | Sseq s1 s2 =>
-      do ns <- transl_stmt map s2 nd nexits nret rret;
-      transl_stmt map s1 ns nexits nret rret
+      do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
+      transl_stmt map s1 ns nexits ngoto nret rret
   | Sifthenelse a strue sfalse =>
       if more_likely a strue sfalse then
-        do nfalse <- transl_stmt map sfalse nd nexits nret rret;
-        do ntrue  <- transl_stmt map strue  nd nexits nret rret;
+        do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
+        do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
         transl_condition map a ntrue nfalse
       else
-        do ntrue  <- transl_stmt map strue  nd nexits nret rret;
-        do nfalse <- transl_stmt map sfalse nd nexits nret rret;
+        do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
+        do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
         transl_condition map a ntrue nfalse
   | Sloop sbody =>
-      add_loop (fun nloop => transl_stmt map sbody nloop nexits nret rret)
+      do n1 <- reserve_instr;
+      do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret;
+      do xx <- update_instr n1 (Inop n2);
+      ret n1
   | Sblock sbody =>
-      transl_stmt map sbody nd (nd :: nexits) nret rret
+      transl_stmt map sbody nd (nd :: nexits) ngoto nret rret
   | Sexit n =>
       transl_exit nexits n
   | Sswitch a cases default =>
@@ -551,12 +571,42 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       | Some a, Some r => transl_expr map a r nret
       | _, _ => error (Errors.msg "RTLgen: type mismatch on return")
       end
-  | Stailcall sig b cl =>
-      do rf <- alloc_reg map b;
-      do rargs <- alloc_regs map cl;
-      do n1 <- add_instr (Itailcall sig (inl _ rf) rargs);
-      do n2 <- transl_exprlist map cl rargs n1;
-         transl_expr map b rf n2
+  | Slabel lbl s' =>
+      do ns <- transl_stmt map s' nd nexits ngoto nret rret;
+      match ngoto!lbl with
+      | None => error (Errors.msg "RTLgen: unbound label")
+      | Some n =>
+          do xx <-
+            (handle_error (update_instr n (Inop ns))
+                          (error (Errors.MSG "Multiply-defined label " ::
+                                  Errors.CTX lbl :: nil)));
+          ret ns
+      end
+  | Sgoto lbl =>
+      match ngoto!lbl with
+      | None => error (Errors.MSG "Undefined defined label " ::
+                       Errors.CTX lbl :: nil)
+      | Some n => ret n
+      end
+  end.
+
+(** Preallocate CFG nodes for each label defined in the function body. *)
+
+Definition alloc_label (lbl: Cminor.label) (maps: labelmap * state) : labelmap * state :=
+  let (map, s) := maps in
+  let n := s.(st_nextnode) in
+  (PTree.set lbl n map,
+   mkstate s.(st_nextreg) (Psucc s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)).
+
+Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
+                        {struct s} : labelmap * state :=
+  match s with
+  | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
+  | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
+  | Sloop s1 => reserve_labels s1 ms
+  | Sblock s1 => reserve_labels s1 ms
+  | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms)
+  | _ => ms
   end.
 
 (** Translation of a CminorSel function. *)
@@ -567,17 +617,18 @@ Definition ret_reg (sig: signature) (rd: reg) : option reg :=
   | Some ty => Some rd
   end.
 
-Definition transl_fun (f: CminorSel.function) : mon (node * list reg) :=
+Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) :=
   do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params);
   do (rvars, map2) <- add_vars map1 f.(CminorSel.fn_vars);
   do rret <- new_reg;
   let orret := ret_reg f.(CminorSel.fn_sig) rret in
   do nret <- add_instr (Ireturn orret);
-  do nentry <- transl_stmt map2 f.(CminorSel.fn_body) nret nil nret orret;
+  do nentry <- transl_stmt map2 f.(CminorSel.fn_body) nret nil ngoto nret orret;
   ret (nentry, rparams).
 
 Definition transl_function (f: CminorSel.function) : Errors.res RTL.function :=
-  match transl_fun f init_state with
+  let (ngoto, s0) := reserve_labels f.(fn_body) (PTree.empty node, init_state) in
+  match transl_fun f ngoto s0 with
   | Error msg => Errors.Error msg
   | OK (nentry, rparams) s i =>
       Errors.OK (RTL.mkfunction
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index e02463a2..1074dddb 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -355,7 +355,8 @@ Proof.
   intros until tf. unfold transl_fundef, transf_partial_fundef.
   case f; intro.
   unfold transl_function. 
-  case (transl_fun f0 init_state); simpl; intros.
+  destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0].
+  case (transl_fun f0 ngoto s0); simpl; intros.
   discriminate.
   destruct p. simpl in H. inversion H. reflexivity.
   intro. inversion H. reflexivity.
@@ -415,6 +416,42 @@ Proof.
   exists rs; split. subst nd. apply star_refl. auto.  
 Qed.
 
+(** Correctness of the translation of [switch] statements *)
+
+Lemma transl_switch_correct:
+  forall cs sp rs m i code r nexits t ns,
+  tr_switch code r nexits t ns ->
+  rs#r = Vint i ->
+  exists nd,
+  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\
+  nth_error nexits (comptree_match i t) = Some nd.
+Proof.
+  induction 1; intros; simpl.
+  exists n. split. apply star_refl. auto. 
+
+  caseEq (Int.eq i key); intros.
+  exists nfound; split. 
+  apply star_one. eapply exec_Icond_true; eauto. 
+  simpl. rewrite H2. congruence. auto.
+  exploit IHtr_switch; eauto. intros [nd [EX MATCH]].
+  exists nd; split.
+  eapply star_step. eapply exec_Icond_false; eauto. 
+  simpl. rewrite H2. congruence. eexact EX. traceEq.
+  auto.
+
+  caseEq (Int.ltu i key); intros.
+  exploit IHtr_switch1; eauto. intros [nd [EX MATCH]].
+  exists nd; split. 
+  eapply star_step. eapply exec_Icond_true; eauto. 
+  simpl. rewrite H2. congruence. eexact EX. traceEq.
+  auto.
+  exploit IHtr_switch2; eauto. intros [nd [EX MATCH]].
+  exists nd; split. 
+  eapply star_step. eapply exec_Icond_false; eauto. 
+  simpl. rewrite H2. congruence. eexact EX. traceEq.
+  auto.
+Qed.
+
 (** ** Semantic preservation for the translation of expressions *)
 
 Section CORRECTNESS_EXPR.
@@ -429,7 +466,7 @@ Variable m: mem.
                     I /\ P
     e, le, m, a ------------- State cs code sp ns rs m
          ||                      |
-        t||                     t|*
+         ||                      |*
          ||                      |
          \/                      v
     e, le, m', v ------------ State cs code sp nd rs' m'
@@ -824,7 +861,73 @@ Proof
 
 End CORRECTNESS_EXPR.
 
-(** ** Semantic preservation for the translation of terminating statements *)   
+(** ** Measure over CminorSel states *)
+
+Open Local Scope nat_scope.
+
+Fixpoint size_stmt (s: stmt) : nat :=
+  match s with
+  | Sskip => 0
+  | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
+  | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
+  | Sloop s1 => (size_stmt s1 + 1)
+  | Sblock s1 => (size_stmt s1 + 1)
+  | Sexit n => 0
+  | Slabel lbl s1 => (size_stmt s1 + 1)
+  | _ => 1
+  end.
+
+Fixpoint size_cont (k: cont) : nat :=
+  match k with
+  | Kseq s k1 => (size_stmt s + size_cont k1 + 1)
+  | Kblock k1 => (size_cont k1 + 1)
+  | _ => 0%nat
+  end.
+
+Definition measure_state (S: CminorSel.state) :=
+  match S with
+  | CminorSel.State _ s k _ _ _ =>
+      existS (fun (x: nat) => nat)
+             (size_stmt s + size_cont k)
+             (size_stmt s)
+  | _ =>
+      existS (fun (x: nat) => nat) 0 0
+  end.
+
+Require Import Relations.
+Require Import Wellfounded.
+
+Definition lt_state (S1 S2: CminorSel.state) :=
+  lexprod nat (fun (x: nat) => nat)
+          lt (fun (x: nat) => lt)
+          (measure_state S1) (measure_state S2).
+
+Lemma lt_state_intro:
+  forall f1 s1 k1 sp1 e1 m1 f2 s2 k2 sp2 e2 m2,
+  size_stmt s1 + size_cont k1 < size_stmt s2 + size_cont k2
+  \/ (size_stmt s1 + size_cont k1 = size_stmt s2 + size_cont k2
+      /\ size_stmt s1 < size_stmt s2) ->
+  lt_state (CminorSel.State f1 s1 k1 sp1 e1 m1)
+           (CminorSel.State f2 s2 k2 sp2 e2 m2).
+Proof.
+  intros. unfold lt_state. simpl. destruct H as [A | [A B]].
+  apply left_lex. auto.
+  rewrite A. apply right_lex. auto.
+Qed.
+
+Ltac Lt_state :=
+  apply lt_state_intro; simpl; try omega.
+
+Require Import Wf_nat.
+
+Lemma lt_state_wf:
+  well_founded lt_state.
+Proof.
+  unfold lt_state. apply wf_inverse_image with (f := measure_state).
+  apply wf_lexprod. apply lt_wf. intros. apply lt_wf. 
+Qed.
+
+(** ** Semantic preservation for the translation of statements *)   
 
 (** The simulation diagram for the translation of statements
   is of the following form:
@@ -854,718 +957,369 @@ End CORRECTNESS_EXPR.
   [e'].  Moreover, the program point reached must correspond to the outcome
   [out].  This is captured by the following [state_for_outcome] predicate. *)
 
-Inductive state_for_outcome
-           (ncont: node) (nexits: list node) (nret: node) (rret: option reg)
-           (cs: list stackframe) (c: code) (sp: val) (rs: regset) (m: mem):
-           outcome -> RTL.state -> Prop :=
-  | state_for_normal:
-      state_for_outcome ncont nexits nret rret cs c sp rs m
-                        Out_normal (State cs c sp ncont rs m)
-  | state_for_exit: forall n nexit,
-      nth_error nexits n = Some nexit ->
-      state_for_outcome ncont nexits nret rret cs c sp rs m
-                        (Out_exit n) (State cs c sp nexit rs m)
-  | state_for_return_none:
-      rret = None ->
-      state_for_outcome ncont nexits nret rret cs c sp rs m
-                        (Out_return None) (State cs c sp nret rs m)
-  | state_for_return_some: forall r v,
-      rret = Some r ->
-      rs#r = v ->
-      state_for_outcome ncont nexits nret rret cs c sp rs m
-                        (Out_return (Some v)) (State cs c sp nret rs m)
-  | state_for_return_tail: forall v,
-      state_for_outcome ncont nexits nret rret cs c sp rs m
-                        (Out_tailcall_return v) (Returnstate cs v m).
-
-Definition transl_stmt_prop 
-  (sp: val) (e: env) (m: mem) (a: stmt)
-  (t: trace) (e': env) (m': mem) (out: outcome) : Prop :=
-  forall cs code map ns ncont nexits nret rret rs
-    (MWF: map_wf map)
-    (TE: tr_stmt code map a ns ncont nexits nret rret)
-    (ME: match_env map e nil rs),
-  exists rs', exists st,
-     state_for_outcome ncont nexits nret rret cs code sp rs' m' out st
-  /\ star step tge (State cs code sp ns rs m) t st
-  /\ match_env map e' nil rs'.
-
-(** Finally, the correctness condition for the translation of functions
-  is that the translated RTL function, when applied to the same arguments
-  as the original Cminor function, returns the same value and performs
-  the same modifications on the memory state. *)
-
-Definition transl_function_prop
-    (m: mem) (f: CminorSel.fundef) (vargs: list val)
-    (t: trace) (m': mem) (vres: val) : Prop :=
-  forall cs tf
-    (TE: transl_fundef f = OK tf),
-  star step tge (Callstate cs tf vargs m) t (Returnstate cs vres m').
-
-Lemma transl_funcall_internal_correct:
-  forall (m : mem) (f : CminorSel.function)
-         (vargs : list val) (m1 : mem) (sp : block) (e : env) (t : trace)
-         (e2 : env) (m2 : mem) (out: outcome) (vres : val),
-  Mem.alloc m 0 (fn_stackspace f) = (m1, sp) ->
-  set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f)) = e ->
-  exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out ->
-  transl_stmt_prop (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out ->
-  outcome_result_value out f.(CminorSel.fn_sig).(sig_res) vres ->
-  transl_function_prop m (Internal f) vargs t 
-                            (outcome_free_mem out m2 sp) vres.
+Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function)
+                     (ngoto: labelmap) (nret: node) (rret: option reg) : Prop :=
+  | tr_funbody_intro: forall nentry r,
+      rret = ret_reg f.(CminorSel.fn_sig) r ->
+      tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret ->
+      tr_funbody c map f ngoto nret rret.
+
+Inductive tr_cont: RTL.code -> mapping -> 
+                   CminorSel.cont -> node -> list node -> labelmap -> node -> option reg ->
+                   list RTL.stackframe -> Prop :=
+  | tr_Kseq: forall c map s k nd nexits ngoto nret rret cs n,
+      tr_stmt c map s nd n nexits ngoto nret rret ->
+      tr_cont c map k n nexits ngoto nret rret cs ->
+      tr_cont c map (Kseq s k) nd nexits ngoto nret rret cs
+  | tr_Kblock: forall c map k nd nexits ngoto nret rret cs,
+      tr_cont c map k nd nexits ngoto nret rret cs ->
+      tr_cont c map (Kblock k) nd (nd :: nexits) ngoto nret rret cs
+  | tr_Kstop: forall c map ngoto nret rret cs,
+      c!nret = Some(Ireturn rret) ->
+      match_stacks Kstop cs ->
+      tr_cont c map Kstop nret nil ngoto nret rret cs
+  | tr_Kcall: forall c map optid f sp e k ngoto nret rret cs,
+      c!nret = Some(Ireturn rret) ->
+      match_stacks (Kcall optid f sp e k) cs ->
+      tr_cont c map (Kcall optid f sp e k) nret nil ngoto nret rret cs
+
+with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop :=
+  | match_stacks_stop:
+      match_stacks Kstop nil
+  | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n',
+      map_wf map ->
+      tr_funbody c map f ngoto nret rret ->
+      match_env map e nil rs ->
+      tr_store_optvar c map r optid n n' ->
+      ~reg_in_map map r ->
+      tr_cont c map k n' nexits ngoto nret rret cs ->
+      match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs).
+
+Inductive match_states: CminorSel.state -> RTL.state -> Prop :=
+  | match_state:
+      forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret
+        (MWF: map_wf map)
+        (TS: tr_stmt c map s ns ncont nexits ngoto nret rret)
+        (TF: tr_funbody c map f ngoto nret rret)
+        (TK: tr_cont c map k ncont nexits ngoto nret rret cs)
+        (ME: match_env map e nil rs),
+      match_states (CminorSel.State f s k sp e m)
+                   (RTL.State cs c sp ns rs m)
+  | match_callstate:
+      forall f args k m cs tf
+        (TF: transl_fundef f = OK tf)
+        (MS: match_stacks k cs),
+      match_states (CminorSel.Callstate f args k m)
+                   (RTL.Callstate cs tf args m)
+  | match_returnstate:
+      forall v k m cs
+        (MS: match_stacks k cs),
+      match_states (CminorSel.Returnstate v k m)
+                   (RTL.Returnstate cs v m).
+
+Lemma match_stacks_call_cont:
+  forall c map k ncont nexits ngoto nret rret cs,
+  tr_cont c map k ncont nexits ngoto nret rret cs ->
+  match_stacks (call_cont k) cs /\ c!nret = Some(Ireturn rret).
 Proof.
-  intros; red; intros.
-  generalize TE; simpl. caseEq (transl_function f); simpl. 2: congruence.
-  intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2.
-  assert (TR: tr_function f tfi). apply transl_function_charact; auto.
-  rewrite <- EQ2. inversion TR. subst f0. 
-
-  pose (rs := init_regs vargs rparams).
-  assert (ME: match_env map2 e nil rs).
-  rewrite <- H0. unfold rs. 
-  eapply match_init_env_init_reg; eauto.
-
-  assert (MWF: map_wf map2).
-    assert (map_valid init_mapping init_state) by apply init_mapping_valid.
-    exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B].
-    eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf.
-
-  exploit H2; eauto. intros [rs' [st [OUT [EX ME']]]].
-
-  eapply star_left.
-  eapply exec_function_internal; eauto. simpl.
-  inversion OUT; clear OUT; subst out st; simpl in H3; simpl.
-
-  (* Out_normal *)
-  unfold ret_reg in H6. destruct (sig_res (CminorSel.fn_sig f)). contradiction. 
-  subst vres orret. 
-  eapply star_right. unfold rs in EX. eexact EX.
-  change Vundef with (regmap_optget None Vundef rs').
-  apply exec_Ireturn. auto. reflexivity.
-
-  (* Out_exit *)
-  contradiction.
-
-  (* Out_return None *)
-  subst orret.
-  unfold ret_reg in H8. destruct (sig_res (CminorSel.fn_sig f)). contradiction.
-  subst vres. 
-  eapply star_right. unfold rs in EX. eexact EX. 
-  change Vundef with (regmap_optget None Vundef rs').
-  apply exec_Ireturn. auto.
-  reflexivity. 
-
-  (* Out_return Some *)
-  subst orret. 
-  unfold ret_reg in H8. unfold ret_reg in H9.
-  destruct (sig_res (CminorSel.fn_sig f)). inversion H9.
-  subst vres.    
-  eapply star_right. unfold rs in EX. eexact EX.
-  replace v with (regmap_optget (Some rret) Vundef rs').
-  apply exec_Ireturn. auto.
-  simpl. congruence. 
-  reflexivity.
-  contradiction.
-
-  (* a tail call *)
-  subst v. rewrite E0_right. auto. traceEq.
+  induction 1; simpl; auto.
 Qed.
 
-Lemma transl_funcall_external_correct:
-  forall (ef : external_function) (m : mem) (args : list val) (t: trace) (res : val),
-  event_match ef args t res ->
-  transl_function_prop m (External ef) args t m res.
+Lemma tr_cont_call_cont:
+  forall c map k ncont nexits ngoto nret rret cs,
+  tr_cont c map k ncont nexits ngoto nret rret cs ->
+  tr_cont c map (call_cont k) nret nil ngoto nret rret cs.
 Proof.
-  intros; red; intros. unfold transl_function in TE; simpl in TE.
-  inversion TE; subst tf. 
-  apply star_one. apply exec_function_external. auto.
+  induction 1; simpl; auto; econstructor; eauto.
 Qed.
 
-Lemma transl_stmt_Sskip_correct:
-  forall (sp: val) (e : env) (m : mem),
-  transl_stmt_prop sp e m Sskip E0 e m Out_normal.
+Lemma tr_find_label:
+  forall c map lbl n (ngoto: labelmap) nret rret s' k' cs,
+  ngoto!lbl = Some n ->
+  forall s k ns1 nd1 nexits1,
+  find_label lbl s k = Some (s', k') ->
+  tr_stmt c map s ns1 nd1 nexits1 ngoto nret rret ->
+  tr_cont c map k nd1 nexits1 ngoto nret rret cs ->
+  exists ns2, exists nd2, exists nexits2,
+     c!n = Some(Inop ns2)
+  /\ tr_stmt c map s' ns2 nd2 nexits2 ngoto nret rret
+  /\ tr_cont c map k' nd2 nexits2 ngoto nret rret cs.
 Proof.
-  intros; red; intros; inv TE.
-  exists rs; econstructor.
-  split. constructor.
-  split. apply star_refl.
-  auto.
-Qed.
-
-Remark state_for_outcome_stop:
-  forall ncont1 ncont2 nexits nret rret cs code sp rs m out st,
-  state_for_outcome ncont1 nexits nret rret cs code sp rs m out st ->
-  out <> Out_normal ->
-  state_for_outcome ncont2 nexits nret rret cs code sp rs m out st.
-Proof.
-  intros. inv H; congruence || econstructor; eauto.
-Qed.
-
-Lemma transl_stmt_Sseq_continue_correct:
-  forall (sp : val) (e : env) (m : mem) (t: trace) (s1 : stmt)
-         (t1: trace) (e1 : env) (m1 : mem) (s2 : stmt) (t2: trace)
-         (e2 : env) (m2 : mem) (out : outcome),
-  exec_stmt ge sp e m s1 t1 e1 m1 Out_normal ->
-  transl_stmt_prop sp e m s1 t1 e1 m1 Out_normal ->
-  exec_stmt ge sp e1 m1 s2 t2 e2 m2 out ->
-  transl_stmt_prop sp e1 m1 s2 t2 e2 m2 out ->
-  t = t1 ** t2 ->
-  transl_stmt_prop sp e m (Sseq s1 s2) t e2 m2 out.
-Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1. 
-  exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]].
-  exists rs2; exists st2.
-  split. eauto.
-  split. eapply star_trans; eauto.
-  auto.
+  induction s; intros until nexits1; simpl; try congruence.
+  (* seq *)
+  caseEq (find_label lbl s1 (Kseq s2 k)); intros.
+  inv H1. inv H2. eapply IHs1; eauto. econstructor; eauto.
+  inv H2. eapply IHs2; eauto. 
+  (* ifthenelse *)
+  caseEq (find_label lbl s1 k); intros.
+  inv H1. inv H2. eapply IHs1; eauto.
+  inv H2. eapply IHs2; eauto.
+  (* loop *)
+  intros. inversion H1; subst.
+  eapply IHs; eauto. econstructor; eauto.
+  (* block *)
+  intros. inv H1.
+  eapply IHs; eauto. econstructor; eauto.
+  (* label *)
+  destruct (ident_eq lbl l); intros.
+  inv H0. inv H1.
+  assert (n0 = n). change positive with node in H4. congruence. subst n0.
+  exists ns1; exists nd1; exists nexits1; auto.
+  inv H1. eapply IHs; eauto.
 Qed.
 
-Lemma transl_stmt_Sseq_stop_correct:
-  forall (sp : val) (e : env) (m : mem) (t: trace) (s1 s2 : stmt) (e1 : env)
-         (m1 : mem) (out : outcome),
-  exec_stmt ge sp e m s1 t e1 m1 out ->
-  transl_stmt_prop sp e m s1 t e1 m1 out ->
-  out <> Out_normal ->
-  transl_stmt_prop sp e m (Sseq s1 s2) t e1 m1 out.
+Theorem transl_step_correct:
+  forall S1 t S2, CminorSel.step ge S1 t S2 ->
+  forall R1, match_states S1 R1 ->
+  exists R2,
+  (plus RTL.step tge R1 t R2 \/ (star RTL.step tge R1 t R2 /\ lt_state S2 S1))
+  /\ match_states S2 R2.
 Proof.
-  intros; red; intros; inv TE.
-  exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]].
-  exists rs1; exists st1.
-  split. eapply state_for_outcome_stop; eauto. 
-  auto.
-Qed.
-
-Lemma transl_stmt_Sassign_correct:
-  forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr)
-         (v : val),
-  eval_expr ge sp e m nil a v ->
-  transl_stmt_prop sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal.
-Proof.
-  intros; red; intros; inv TE.
+  induction 1; intros R1 MSTATE; inv MSTATE.
+
+  (* skip seq *)
+  inv TS. inv TK. econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto.
+
+  (* skip block *)
+  inv TS. inv TK. econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto. constructor.
+
+  (* skip return *)
+  inv TS. 
+  assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs).
+    inv TK; simpl in H; try contradiction; auto.
+  destruct H1.
+  assert (rret = None). 
+    inv TF. unfold ret_reg. rewrite H0. auto.
+  subst rret.
+  econstructor; split.
+  left; apply plus_one. eapply exec_Ireturn. eauto.
+  simpl. constructor; auto.
+  
+  (* assign *)
+  inv TS. 
+  exploit transl_expr_correct; eauto. 
+  intros [rs' [A [B [C D]]]].
+  exploit tr_store_var_correct; eauto. 
+  intros [rs'' [E F]].
+  rewrite C in F.
+  econstructor; split.
+  right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state.
+  econstructor; eauto. constructor.
+
+  (* store *)
+  inv TS.
+  exploit transl_exprlist_correct; eauto.
+  intros [rs' [A [B [C D]]]].
   exploit transl_expr_correct; eauto.
-  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit tr_store_var_correct; eauto. intros [rs2 [EX2 ME2]].
-  exists rs2; econstructor.
-  split. constructor.
-  split. eapply star_trans. eexact EX1. eexact EX2. traceEq.
-  congruence. 
-Qed.
-
-Lemma transl_stmt_Sstore_correct:
-  forall (sp : val) (e : env) (m : mem) (chunk : memory_chunk)
-         (addr: addressing) (al: exprlist) (b: expr)
-         (vl: list val) (v: val) (vaddr: val) (m' : mem),
-  eval_exprlist ge sp e m nil al vl ->
-  eval_expr ge sp e m nil b v ->
-  eval_addressing ge sp addr vl = Some vaddr ->
-  storev chunk m vaddr v = Some m' ->
-  transl_stmt_prop sp e m (Sstore chunk addr al b) E0 e m' Out_normal.
-Proof.
-  intros; red; intros; inv TE.
-  exploit transl_exprlist_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit transl_expr_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  exists rs2; econstructor.
-  (* Outcome *)
-  split. constructor.
-  (* Exec *)
-  split. eapply star_trans. eexact EX1. 
-  eapply star_right. eexact EX2.
-  eapply exec_Istore; eauto.
-  assert (rs2##rl = rs1##rl).
-    apply list_map_exten. intros r' IN. symmetry. apply OTHER2. auto.
-  rewrite H3; rewrite RES1. 
-  rewrite (@eval_addressing_preserved _ _ ge tge). eexact H1.
-  exact symbols_preserved.
-  rewrite RES2. auto.
-  reflexivity. traceEq.
-  (* Match-env *)
-  auto.
-Qed.
+  intros [rs'' [E [F [G J]]]].
+  assert (rs''##rl = vl).
+    rewrite <- C. apply list_map_exten. intros. symmetry. apply J. auto.
+  econstructor; split.
+  left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
+  eapply exec_Istore with (a := vaddr); eauto.
+  rewrite H3. rewrite <- H1. apply eval_addressing_preserved. exact symbols_preserved.
+  rewrite G. eauto.
+  traceEq.
+  econstructor; eauto. constructor.
 
-Lemma transl_stmt_Scall_correct:
-  forall (sp : val) (e : env) (m : mem) (optid : option ident)
-         (sig : signature) (a : expr) (bl : exprlist) (vf : val)
-         (vargs : list val) (f : CminorSel.fundef) (t : trace) (m' : mem)
-         (vres : val) (e' : env),
-  eval_expr ge sp e m nil a vf ->
-  eval_exprlist ge sp e m nil bl vargs ->
-  Genv.find_funct ge vf = Some f ->
-  CminorSel.funsig f = sig ->
-  eval_funcall ge m f vargs t m' vres ->
-  transl_function_prop m f vargs t m' vres ->
-  e' = set_optvar optid vres e ->
-  transl_stmt_prop sp e m (Scall optid sig a bl) t e' m' Out_normal.
-Proof.
-  intros; red; intros; inv TE.
+  (* call *)
+  inv TS. 
   exploit transl_expr_correct; eauto.
-  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  intros [rs' [A [B [C D]]]].
   exploit transl_exprlist_correct; eauto.
-  intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  exploit functions_translated; eauto. intros [tf [TFIND TF]].
-  exploit H4; eauto. intro EXF.
-  exploit (tr_store_optvar_correct (rs2#rd <- vres)); eauto.
-    apply match_env_update_temp; eauto.
-  intros [rs3 [EX3 ME3]].
-  exists rs3; econstructor.
-  (* Outcome *)
-  split. constructor.
-  (* Exec *)
-  split. eapply star_trans. eexact EX1.
-  eapply star_trans. eexact EX2. 
-  eapply star_left. eapply exec_Icall; eauto.
-  simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. 
-  eapply sig_transl_function; eauto.
-  eapply star_trans. rewrite RES2. eexact EXF.
-  eapply star_left. apply exec_return.
-  eexact EX3. 
-  reflexivity. reflexivity. reflexivity. reflexivity. traceEq.
-  (* Match-env *)
-  rewrite Regmap.gss in ME3. auto.
-Qed. 
-
-Lemma transl_stmt_Salloc_correct:
-  forall (sp : val) (e : env) (m : mem) (id : ident) (a : expr)
-         (n : int) (m' : mem) (b : block),
-  eval_expr ge sp e m nil a (Vint n) ->
-  alloc m 0 (Int.signed n) = (m', b) ->
-  transl_stmt_prop sp e m (Salloc id a) E0
-                      (PTree.set id (Vptr b Int.zero) e) m' Out_normal.
-Proof.
-  intros; red; intros; inv TE.
-  exploit transl_expr_correct; eauto.
-  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit (tr_store_var_correct (rs1#rd <- (Vptr b Int.zero))); eauto.
-    apply match_env_update_temp; eauto.
-  intros [rs2 [EX2 ME2]].
-  exists rs2; econstructor.
-  (* Outcome *)
-  split. constructor.
-  (* Execution *)
-  split. eapply star_trans. eexact EX1. 
-  eapply star_left. 2: eexact EX2. 
-  eapply exec_Ialloc; eauto. 
-  reflexivity. traceEq.
-  (* Match-env *)
-  rewrite Regmap.gss in ME2. auto.
-Qed.
-
-Lemma transl_stmt_Sifthenelse_correct:
-  forall (sp : val) (e : env) (m : mem) (a : condexpr) (s1 s2 : stmt)
-         (v : bool) (t : trace) (e' : env) (m' : mem) (out : outcome),
-  eval_condexpr ge sp e m nil a v ->
-  exec_stmt ge sp e m (if v then s1 else s2) t e' m' out ->
-  transl_stmt_prop sp e m (if v then s1 else s2) t e' m' out ->
-  transl_stmt_prop sp e m (Sifthenelse a s1 s2) t e' m' out.
-Proof.
-  intros; red; intros; inv TE.
-  exploit transl_condexpr_correct; eauto.
-  intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_stmt code map (if v then s1 else s2) (if v then ntrue else nfalse)
-                  ncont nexits nret rret).
-    destruct v; auto. 
-  exploit H1; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]].
-  exists rs2; exists st2.
-  split. eauto.
-  split. eapply star_trans. eexact EX1. eexact EX2. auto.
-  auto.
-Qed.
-
-Lemma transl_stmt_Sloop_loop_correct:
-  forall (sp: val) (e : env) (m : mem) (sl : stmt) (t t1: trace)
-    (e1 : env) (m1 : mem) (t2: trace) (e2 : env) (m2 : mem) 
-    (out : outcome),
-  exec_stmt ge sp e m sl t1 e1 m1 Out_normal ->
-  transl_stmt_prop sp e m sl t1 e1 m1 Out_normal ->
-  exec_stmt ge sp e1 m1 (Sloop sl) t2 e2 m2 out ->
-  transl_stmt_prop sp e1 m1 (Sloop sl) t2 e2 m2 out ->
-  t = t1 ** t2 ->
-  transl_stmt_prop sp e m (Sloop sl) t e2 m2 out.
-Proof.
-  intros; red; intros; inversion TE. subst. 
-  exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]]. inv OUT1.
-  exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]].
-  exists rs2; exists st2. 
-  split. eauto.
-  split. eapply star_trans. eexact EX1. 
-  eapply star_left. apply exec_Inop; eauto. eexact EX2. 
-  reflexivity. traceEq.
-  auto.
-Qed.
-
-Lemma transl_stmt_Sloop_stop_correct:
-  forall (sp: val) (e : env) (m : mem) (t: trace) (sl : stmt) 
-    (e1 : env) (m1 : mem) (out : outcome),
-  exec_stmt ge sp e m sl t e1 m1 out ->
-  transl_stmt_prop sp e m sl t e1 m1 out ->
-  out <> Out_normal ->
-  transl_stmt_prop sp e m (Sloop sl) t e1 m1 out.
-Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]].
-  exists rs1; exists st1.
-  split. eapply state_for_outcome_stop; eauto.
-  auto.
-Qed.
-
-Lemma transl_stmt_Sblock_correct:
-  forall (sp: val) (e : env) (m : mem) (sl : stmt) (t: trace)
-    (e1 : env) (m1 : mem) (out : outcome),
-  exec_stmt ge sp e m sl t e1 m1 out ->
-  transl_stmt_prop sp e m sl t e1 m1 out ->
-  transl_stmt_prop sp e m (Sblock sl) t e1 m1 (outcome_block out).
-Proof.
-  intros; red; intros; inv TE.
-  exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]].
-  exists rs1; exists st1.
-  split. inv OUT1; simpl; try (econstructor; eauto).
-  destruct n; simpl in H1.
-    inv H1. constructor.
-    constructor. auto.
-  auto.
-Qed.
-
-Lemma transl_stmt_Sexit_correct:
-  forall (sp: val) (e : env) (m : mem) (n : nat),
-  transl_stmt_prop sp e m (Sexit n) E0 e m (Out_exit n).
-Proof.
-  intros; red; intros; inv TE.
-  exists rs; econstructor.
-  split. econstructor; eauto.
-  split. apply star_refl.
-  auto.
-Qed.
-
-Lemma transl_switch_correct:
-  forall cs sp rs m i code r nexits t ns,
-  tr_switch code r nexits t ns ->
-  rs#r = Vint i ->
-  exists nd,
-  star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\
-  nth_error nexits (comptree_match i t) = Some nd.
-Proof.
-  induction 1; intros; simpl.
-  exists n. split. apply star_refl. auto. 
-
-  caseEq (Int.eq i key); intros.
-  exists nfound; split. 
-  apply star_one. eapply exec_Icond_true; eauto. 
-  simpl. rewrite H2. congruence. auto.
-  exploit IHtr_switch; eauto. intros [nd [EX MATCH]].
-  exists nd; split.
-  eapply star_step. eapply exec_Icond_false; eauto. 
-  simpl. rewrite H2. congruence. eexact EX. traceEq.
-  auto.
+  intros [rs'' [E [F [G J]]]].
+  exploit functions_translated; eauto. intros [tf [P Q]].
+  econstructor; split.
+  left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
+  eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto.
+  apply sig_transl_function; auto.
+  traceEq.
+  rewrite G. constructor. auto. econstructor; eauto.
 
-  caseEq (Int.ltu i key); intros.
-  exploit IHtr_switch1; eauto. intros [nd [EX MATCH]].
-  exists nd; split. 
-  eapply star_step. eapply exec_Icond_true; eauto. 
-  simpl. rewrite H2. congruence. eexact EX. traceEq.
-  auto.
-  exploit IHtr_switch2; eauto. intros [nd [EX MATCH]].
-  exists nd; split. 
-  eapply star_step. eapply exec_Icond_false; eauto. 
-  simpl. rewrite H2. congruence. eexact EX. traceEq.
-  auto.
-Qed.
+  (* tailcall *)
+  inv TS. 
+  exploit transl_expr_correct; eauto.
+  intros [rs' [A [B [C D]]]].
+  exploit transl_exprlist_correct; eauto.
+  intros [rs'' [E [F [G J]]]].
+  exploit functions_translated; eauto. intros [tf [P Q]].
+  exploit match_stacks_call_cont; eauto. intros [U V].
+  econstructor; split.
+  left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity.
+  eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto.
+  apply sig_transl_function; auto.
+  traceEq.
+  rewrite G. constructor; auto.
 
-Lemma transl_stmt_Sswitch_correct:
-  forall (sp : val) (e : env) (m : mem) (a : expr)
-         (cases : list (int * nat)) (default : nat) (n : int),
-  eval_expr ge sp e m nil a (Vint n) ->
-  transl_stmt_prop sp e m (Sswitch a cases default) E0 e m
-         (Out_exit (switch_target n default cases)).
-Proof.
-  intros; red; intros; inv TE.
+  (* alloc *)
+  inv TS. 
   exploit transl_expr_correct; eauto. 
-  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit transl_switch_correct; eauto. intros [nd [EX2 MO2]].
-  exists rs1; econstructor.
-  split. econstructor. 
-  rewrite (validate_switch_correct _ _ _ H3 n). eauto.  
-  split. eapply star_trans. eexact EX1. eexact EX2. traceEq.
-  auto.
-Qed.
-
-Lemma transl_stmt_Sreturn_none_correct:
-  forall (sp: val) (e : env) (m : mem),
-  transl_stmt_prop sp e m (Sreturn None) E0 e m (Out_return None).
-Proof.
-  intros; red; intros; inv TE.
-  exists rs; econstructor.
-  split. constructor. auto.
-  split. apply star_refl. 
-  auto.
-Qed.
-
-Lemma transl_stmt_Sreturn_some_correct:
-  forall (sp : val) (e : env) (m : mem) (a : expr) (v : val),
-  eval_expr ge sp e m nil a v ->
-  transl_stmt_prop sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v)).
-Proof.
-  intros; red; intros; inv TE. 
+  intros [rs1 [A [B [C D]]]].
+  set (rs2 := rs1#rd <- (Vptr b Int.zero)).
+  assert (match_env map e nil rs2). unfold rs2; eauto with rtlg. 
+  exploit tr_store_var_correct. eauto. auto. eexact H1. 
+  intros [rs3 [E F]].
+  unfold rs2 in F. rewrite Regmap.gss in F.
+  econstructor; split.
+  left. apply plus_star_trans with E0 (State cs c sp n2 rs2 m') E0.
+  eapply plus_right. eexact A. unfold rs2. eapply exec_Ialloc; eauto. traceEq.
+  eexact E. traceEq.
+  econstructor; eauto. constructor.
+
+  (* seq *)
+  inv TS. 
+  econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto. econstructor; eauto. 
+
+  (* ifthenelse *)
+  inv TS.
+  exploit transl_condexpr_correct; eauto. 
+  intros [rs' [A [B C]]].
+  econstructor; split.
+  right; split. eexact A. destruct b; Lt_state.
+  destruct b; econstructor; eauto. 
+
+  (* loop *)
+  inversion TS; subst.
+  econstructor; split.
+  left. apply plus_one. eapply exec_Inop; eauto. 
+  econstructor; eauto. 
+  econstructor; eauto.
+
+  (* block *)
+  inv TS.
+  econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto. econstructor; eauto.
+
+  (* exit seq *)
+  inv TS. inv TK. 
+  econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto. econstructor; eauto.
+
+  (* exit block 0 *)
+  inv TS. inv TK. simpl in H0. inv H0.
+  econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto. econstructor; eauto.
+
+  (* exit block n+1 *)
+  inv TS. inv TK. simpl in H0.
+  econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto. econstructor; eauto.
+
+  (* switch *)
+  inv TS. 
+  exploit transl_expr_correct; eauto. 
+  intros [rs' [A [B [C D]]]].
+  exploit transl_switch_correct; eauto. 
+  intros [nd [E F]].
+  econstructor; split.
+  right; split. eapply star_trans. eexact A. eexact E.  traceEq. Lt_state. 
+  econstructor; eauto. 
+  rewrite (validate_switch_correct _ _ _ H3 n). constructor. auto.
+
+  (* return none *)
+  inv TS.
+  exploit match_stacks_call_cont; eauto. intros [U V].
+  econstructor; split.
+  left; apply plus_one. eapply exec_Ireturn; eauto.
+  simpl. constructor; auto.
+
+  (* return some *)
+  inv TS.
   exploit transl_expr_correct; eauto.
-  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exists rs1; econstructor.
-  split. econstructor. reflexivity. auto.
-  eauto.
-Qed.
-
-Lemma transl_stmt_Stailcall_correct:
-  forall (sp : block) (e : env) (m : mem) (sig : signature) (a : expr)
-         (bl : exprlist) (vf : val) (vargs : list val) (f : CminorSel.fundef)
-         (t : trace) (m' : mem) (vres : val),
-  eval_expr ge (Vptr sp Int.zero) e m nil a vf ->
-  eval_exprlist ge (Vptr sp Int.zero) e m nil bl vargs ->
-  Genv.find_funct ge vf = Some f ->
-  CminorSel.funsig f = sig ->
-  eval_funcall ge (free m sp) f vargs t m' vres ->
-  transl_function_prop (free m sp) f vargs t m' vres ->
-  transl_stmt_prop (Vptr sp Int.zero) e m (Stailcall sig a bl) t e
-          m' (Out_tailcall_return vres).
-Proof.
-  intros; red; intros; inv TE.
-  exploit transl_expr_correct; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit transl_exprlist_correct; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  exploit functions_translated; eauto. intros [tf [TFIND TF]].
-  exploit H4; eauto. intro EXF.
-  exists rs2; econstructor. 
-  split. constructor. 
-  split. 
-  eapply star_trans. eexact EX1. 
-  eapply star_trans. eexact EX2. 
-  eapply star_step. 
-  eapply exec_Itailcall; eauto.
-  simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto.
-  eapply sig_transl_function; eauto.
-  rewrite RES2. eexact EXF. 
-  reflexivity. reflexivity. traceEq.
-  auto.
-Qed.
-
-(** The correctness of the translation then follows by application
-  of the mutual induction principle for Cminor evaluation derivations
-  to the lemmas above. *)
-
-Theorem transl_function_correct:
-  forall m f vargs t m' vres,
-  eval_funcall ge m f vargs t m' vres ->
-  transl_function_prop m f vargs t m' vres.
-Proof
-  (eval_funcall_ind2 ge
-    transl_function_prop
-    transl_stmt_prop
-
-    transl_funcall_internal_correct
-    transl_funcall_external_correct
-    transl_stmt_Sskip_correct
-    transl_stmt_Sassign_correct
-    transl_stmt_Sstore_correct
-    transl_stmt_Scall_correct
-    transl_stmt_Salloc_correct
-    transl_stmt_Sifthenelse_correct
-    transl_stmt_Sseq_continue_correct
-    transl_stmt_Sseq_stop_correct
-    transl_stmt_Sloop_loop_correct
-    transl_stmt_Sloop_stop_correct
-    transl_stmt_Sblock_correct
-    transl_stmt_Sexit_correct
-    transl_stmt_Sswitch_correct
-    transl_stmt_Sreturn_none_correct
-    transl_stmt_Sreturn_some_correct
-    transl_stmt_Stailcall_correct).
-
-Theorem transl_stmt_correct:
-  forall sp e m s t e' m' out,
-  exec_stmt ge sp e m s t e' m' out ->
-  transl_stmt_prop sp e m s t e' m' out.
-Proof
-  (exec_stmt_ind2 ge
-    transl_function_prop
-    transl_stmt_prop
-
-    transl_funcall_internal_correct
-    transl_funcall_external_correct
-    transl_stmt_Sskip_correct
-    transl_stmt_Sassign_correct
-    transl_stmt_Sstore_correct
-    transl_stmt_Scall_correct
-    transl_stmt_Salloc_correct
-    transl_stmt_Sifthenelse_correct
-    transl_stmt_Sseq_continue_correct
-    transl_stmt_Sseq_stop_correct
-    transl_stmt_Sloop_loop_correct
-    transl_stmt_Sloop_stop_correct
-    transl_stmt_Sblock_correct
-    transl_stmt_Sexit_correct
-    transl_stmt_Sswitch_correct
-    transl_stmt_Sreturn_none_correct
-    transl_stmt_Sreturn_some_correct
-    transl_stmt_Stailcall_correct).
-
-(** ** Semantic preservation for the translation of divering statements *)   
-
-Fixpoint size_stmt (s: stmt) : nat :=
-  match s with
-  | Sseq s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat
-  | Sifthenelse e s1 s2 => (1 + size_stmt s1 + size_stmt s2)%nat
-  | Sloop s1 => (1 + size_stmt s1)%nat
-  | Sblock s1 => (1 + size_stmt s1)%nat
-  | _ => 1%nat
-  end.
-
-Theorem transl_function_correct_divergence:
-  forall m fd vargs t tfd cs,
-  evalinf_funcall ge m fd vargs t ->
-  transl_fundef fd = OK tfd ->
-  forever_N step tge O (Callstate cs tfd vargs m) t.
-Proof.
-  cofix FUNCALL.
-  assert (STMT: forall sp e m s t,
-     execinf_stmt ge sp e m s t ->
-     forall cs code map ns ncont nexits nret rret rs
-       (MWF: map_wf map)
-       (TE: tr_stmt code map s ns ncont nexits nret rret)
-       (ME: match_env map e nil rs),
-     forever_N step tge (size_stmt s) (State cs code sp ns rs m) t).
-  cofix STMT; intros. 
-  inv H; inversion TE; subst.
-  (* Scall *)
-  destruct (transl_expr_correct _ _ _ _ _ _ H0
-              cs _ _ _ _ _ _ _ MWF H7 ME)
-  as [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  destruct (transl_exprlist_correct _ _ _ _ _ _ H1
-              cs _ _ _ _ _ _ _ MWF H8 ME1)
-  as [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  destruct (functions_translated _ _ H2) as [tf [TFIND TF]].
-  eapply forever_N_star with (p := O).
-  eapply star_trans. eexact EX1. eexact EX2. reflexivity.
-  simpl; omega. 
-  eapply forever_N_plus with (p := O).
-  apply plus_one. eapply exec_Icall; eauto. 
-  simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. 
-  eapply sig_transl_function; eauto.
-  eapply FUNCALL. rewrite RES2. eexact H4. assumption.
-  reflexivity. traceEq.    
-  (* Sifthenelse *)
-  destruct (transl_condexpr_correct _ _ _ _ _ _ H0
-              cs _ _ _ _ _ _ _ MWF H11 ME)
-  as [rs1 [EX1 [ME1 OTHER1]]].
-  eapply forever_N_star with (p := size_stmt (if v then s1 else s2)).
-  eexact EX1. destruct v; simpl; omega.
-  eapply STMT. eexact H1. eauto. destruct v; eauto. eauto.
-  traceEq. 
-  (* Sseq, 1 *)
-  eapply forever_N_star with (p := size_stmt s1).
-  apply star_refl. simpl; omega.
-  eapply STMT; eauto.
-  traceEq.
-  (* Sseq, 2 *)
-  destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0
-              cs _ _ _ _ _ _ _ _ MWF H9 ME)
-  as [rs1 [st1 [OUT1 [EX1 ME1]]]].
-  inv OUT1. 
-  eapply forever_N_star with (p := size_stmt s2).
-  eexact EX1. simpl; omega.
-  eapply STMT; eauto.
-  traceEq.
-  (* Sloop, body *)
-  eapply forever_N_star with (p := size_stmt s0).
-  apply star_refl. simpl; omega.
-  eapply STMT; eauto.
-  traceEq.
-  (* Sloop, loop *)
-  destruct (transl_stmt_correct _ _ _ _ _ _ _ _ H0
-              cs _ _ _ _ _ _ _ _ MWF H2 ME)
-  as [rs1 [st1 [OUT1 [EX1 ME1]]]].
-  inv OUT1. 
-  eapply forever_N_plus with (p := size_stmt (Sloop s0)).
-  eapply plus_right. eexact EX1. eapply exec_Inop; eauto. reflexivity.
-  eapply STMT; eauto.
-  traceEq. 
-  (* Sblock *)
-  eapply forever_N_star with (p := size_stmt s0).
-  apply star_refl. simpl; omega.
-  eapply STMT; eauto.
-  traceEq.
-  (* Stailcall *)
-  destruct (transl_expr_correct _ _ _ _ _ _ H0
-              cs _ _ _ _ _ _ _ MWF H6 ME)
-  as [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  destruct (transl_exprlist_correct _ _ _ _ _ _ H1
-              cs _ _ _ _ _ _ _ MWF H12 ME1)
-  as [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  destruct (functions_translated _ _ H2) as [tf [TFIND TF]].
-  eapply forever_N_star with (p := O).
-  eapply star_trans. eexact EX1. eexact EX2. reflexivity.
-  simpl; omega. 
-  eapply forever_N_plus with (p := O).
-  apply plus_one. eapply exec_Itailcall; eauto. 
-  simpl. rewrite OTHER2. rewrite RES1. eauto. simpl; tauto. 
-  eapply sig_transl_function; eauto.
-  eapply FUNCALL. rewrite RES2. eexact H4. assumption.
-  reflexivity. traceEq.
-  (* funcall *)
-  intros. inversion H. subst m0 fd vargs0 t0. 
-  generalize H0; simpl. caseEq (transl_function f); simpl. 2: congruence.
-  intros tfi EQ1 EQ2. injection EQ2; clear EQ2; intro EQ2.
-  assert (TR: tr_function f tfi). apply transl_function_charact; auto.
-  rewrite <- EQ2. inversion TR. subst f0. 
+  intros [rs' [A [B [C D]]]].
+  exploit match_stacks_call_cont; eauto. intros [U V].  
+  econstructor; split.
+  left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq.
+  simpl. rewrite C. constructor; auto.
+
+  (* label *)
+  inv TS.
+  econstructor; split.
+  right; split. apply star_refl. Lt_state.
+  econstructor; eauto.
+
+  (* goto *)
+  inv TS. inversion TF; subst.
+  exploit tr_find_label; eauto. eapply tr_cont_call_cont; eauto. 
+  intros [ns2 [nd2 [nexits2 [A [B C]]]]].
+  econstructor; split.
+  left; apply plus_one. eapply exec_Inop; eauto.
+  econstructor; eauto. 
+
+  (* internal call *)
+  monadInv TF. exploit transl_function_charact; eauto. intro TRF.
+  inversion TRF. subst f0.
+  pose (e := set_locals (fn_vars f) (set_params vargs (CminorSel.fn_params f))).
   pose (rs := init_regs vargs rparams).
   assert (ME: match_env map2 e nil rs).
-  rewrite <- H2. unfold rs. 
-  eapply match_init_env_init_reg; eauto.
+    unfold rs, e. eapply match_init_env_init_reg; eauto.
   assert (MWF: map_wf map2).
-    assert (map_valid init_mapping init_state) by apply init_mapping_valid.
+    assert (map_valid init_mapping s0) by apply init_mapping_valid.
     exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B].
     eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf.
-  eapply forever_N_plus with (p := size_stmt (fn_body f)).
-  apply plus_one. eapply exec_function_internal; eauto.
-  simpl. eapply STMT; eauto.
-  traceEq.
+  econstructor; split.
+  left; apply plus_one. eapply exec_function_internal; simpl; eauto.
+  simpl. econstructor; eauto.
+  econstructor; eauto.
+  inversion MS; subst; econstructor; eauto.
+
+  (* external call *)
+  monadInv TF. 
+  econstructor; split.
+  left; apply plus_one. eapply exec_function_external; eauto. 
+  constructor; auto.
+
+  (* return *)
+  inv MS.
+  set (rs' := (rs#r <- v)).
+  assert (match_env map e nil rs'). unfold rs'; eauto with rtlg. 
+  exploit tr_store_optvar_correct. eauto. eauto. eexact H. intros [rs'' [A B]].
+  econstructor; split.
+  left; eapply plus_left. constructor. eexact A. traceEq.
+  econstructor; eauto. constructor. unfold rs' in B. rewrite Regmap.gss in B. auto.
 Qed.
 
-(** ** Semantic preservation for whole programs. *)
+Lemma transl_initial_states:
+  forall S, CminorSel.initial_state prog S ->
+  exists R, RTL.initial_state tprog R /\ match_states S R.
+Proof.
+  induction 1.
+  exploit function_ptr_translated; eauto. intros [tf [A B]].
+  econstructor; split.
+  econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge.
+  rewrite symbols_preserved. eexact H.
+  eexact A.
+  rewrite <- H1. apply sig_transl_function; auto.
+  rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor.
+Qed.
 
-(** The correctness of the translation follows: 
-  if the original Cminor program executes with observable behavior [beh],
-  then the generated RTL program executes with the same behavior. *)
+Lemma transl_final_states:
+  forall S R r,
+  match_states S R -> CminorSel.final_state S r -> RTL.final_state R r.
+Proof.
+  intros. inv H0. inv H. inv MS. constructor.
+Qed.
 
-Theorem transl_program_correct:
+Theorem transf_program_correct:
   forall (beh: program_behavior),
-  CminorSel.exec_program prog beh ->
-  RTL.exec_program tprog beh.
+  CminorSel.exec_program prog beh -> RTL.exec_program tprog beh.
 Proof.
-  intros. inv H.
-  (* termination *)
-  exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]].
-  exploit transl_function_correct; eauto. intro EX.
-  econstructor.
-  econstructor. 
-  rewrite symbols_preserved. 
-  replace (prog_main tprog) with (prog_main prog). eauto.
-  symmetry; apply transform_partial_program_main with transl_fundef.
-  exact TRANSL.
-  eexact TFIND.
-  generalize (sig_transl_function _ _ TRANSLF). congruence.
-  unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL).
-  eexact EX. 
-  constructor.
-  (* divergence *)
-  exploit function_ptr_translated; eauto. intros [tf [TFIND TRANSLF]].
-  exploit transl_function_correct_divergence; eauto. intro EX.
-  econstructor.
-  econstructor. 
-  rewrite symbols_preserved. 
-  replace (prog_main tprog) with (prog_main prog). eauto.
-  symmetry; apply transform_partial_program_main with transl_fundef.
-  exact TRANSL.
-  eexact TFIND.
-  generalize (sig_transl_function _ _ TRANSLF). congruence.
-  eapply forever_N_forever. 
-  unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL).
-  eexact EX. 
+  unfold CminorSel.exec_program, RTL.exec_program; intros.
+  eapply simulation_star_wf_preservation with (order := lt_state); eauto.
+  eexact transl_initial_states.
+  eexact transl_final_states.
+  apply lt_state_wf. 
+  exact transl_step_correct. 
 Qed.
 
 End CORRECTNESS.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index b8061a3f..59a5dd7e 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -136,39 +136,27 @@ Lemma instr_at_incr:
   forall s1 s2 n i,
   state_incr s1 s2 -> s1.(st_code)!n = Some i -> s2.(st_code)!n = Some i.
 Proof.
-  intros. inversion H.
-  rewrite H3. auto. elim (st_wf s1 n); intro.
-  assumption. congruence.
+  intros. inv H.
+  destruct (H3 n); congruence.
 Qed.
 Hint Resolve instr_at_incr: rtlg.
 
-(** The following relation between two states is a weaker version of
-  [state_incr].  It permits changing the contents at an already reserved
-  graph node, but only from [None] to [Some i]. *)
+(*
+(** A useful tactic to reason over transitivity and reflexivity of [state_incr]. *)
 
-Definition state_extends (s1 s2: state): Prop :=
-  forall pc,
-  s1.(st_code)!pc = None \/ s2.(st_code)!pc = s1.(st_code)!pc.
+Ltac Show_state_incr :=
+  eauto;
+  match goal with
+  | |- (state_incr ?c ?c) => 
+         apply state_incr_refl
+  | |- (state_incr ?c1 ?c2) =>
+         eapply state_incr_trans; [eauto; fail | idtac]; Show_state_incr
+  end.
 
-Lemma instr_at_extends:
-  forall s1 s2 pc i,
-  state_extends s1 s2 -> 
-  s1.(st_code)!pc = Some i -> s2.(st_code)!pc = Some i.
-Proof.
-  intros. elim (H pc); intro. congruence. congruence.
-Qed.
+Hint Extern 2 (state_incr _ _) => Show_state_incr : rtlg.
+*)
 
-Lemma state_incr_extends:
-  forall s1 s2,
-  state_incr s1 s2 -> state_extends s1 s2.
-Proof.
-  unfold state_extends; intros. inversion H.   
-  case (plt pc s1.(st_nextnode)); intro.
-  right; apply H2; auto.
-  left. elim (s1.(st_wf) pc); intro.
-  elim (n H5). auto.
-Qed.
-Hint Resolve state_incr_extends: rtlg.
+Hint Resolve state_incr_refl state_incr_trans: rtlg.
 
 (** * Validity and freshness of registers *)
 
@@ -273,70 +261,18 @@ Proof.
 Qed.
 Hint Resolve add_instr_at: rtlg.
 
-(** Properties of [update_instr] and [add_loop].  The following diagram
-  shows the evolutions of the code component of the state during [add_loop].
-  The vertical bar materializes the [st_nextnode] pointer.
-<<
-  s1:  I1   I2   ...   In  |None None None None None None None
-reserve_instr
-  s2:  I1   I2   ...   In   None|None None None None None None
-body n
-  s3:  I1   I2   ...   In   None Ip   ...  Iq  |None None None
-update_instr
-  s4:  I1   I2   ...   In   Inop Ip   ...  Iq  |None None None
->>
-  It is apparent that [state_incr s1 s2] and [state_incr s1 s4] hold.
-  Moreover, [state_extends s3 s4] holds but not [state_incr s3 s4].
-*)
+(** Properties of [update_instr]. *)
 
-Lemma update_instr_extends:
-  forall s1 s2 s3 i n,
-  reserve_instr s1 = (n, s2) ->
-  state_incr s2 s3 ->
-  state_extends s3 (update_instr n i s3).
+Lemma update_instr_at:
+  forall n i s1 s2 incr u,
+  update_instr n i s1 = OK u s2 incr -> s2.(st_code)!n = Some i.
 Proof.
-  intros. injection H. intros EQ1 EQ2.
-  unfold update_instr. destruct (plt n (st_nextnode s3)).  
-  red; simpl; intros. rewrite PTree.gsspec.  
-  case (peq pc n); intro.
-  subst pc. left. inversion H0. subst s0 s4. rewrite H3. 
-  rewrite <- EQ1; simpl.
-  destruct (s1.(st_wf) n).
-  rewrite <- EQ2 in H4. elim (Plt_strict _ H4).
-  auto.
-  rewrite <- EQ1; rewrite <- EQ2; simpl. apply Plt_succ.
-  auto.
-  red; intros; auto.
-Qed.
-
-Lemma add_loop_inversion:
-  forall f s1 nbody s4 i,
-  add_loop f s1 = OK nbody s4 i ->
-  exists nloop, exists s2, exists s3, exists i',
-     state_incr s1 s2
-  /\ f nloop s2 = OK nbody s3 i'
-  /\ state_extends s3 s4
-  /\ s4.(st_code)!nloop = Some(Inop nbody).
-Proof.
-  intros until i. unfold add_loop.
-  unfold reserve_instr; simpl.
-  set (s2 := mkstate (st_nextreg s1) (Psucc (st_nextnode s1)) (st_code s1)
-                     (reserve_instr_wf s1)).
-  set (nloop := st_nextnode s1).
-  case_eq (f nloop s2). intros; discriminate.
-  intros n s3 i' EQ1 EQ2. inv EQ2. 
-  exists nloop; exists s2; exists s3; exists i'.
-  split. 
-    unfold s2; constructor; simpl. 
-    apply Ple_succ. apply Ple_refl. auto.
-  split. auto.
-  split. apply update_instr_extends with s1 s2; auto. 
-  unfold update_instr. destruct (plt nloop (st_nextnode s3)).
-  simpl. apply PTree.gss. 
-  elim n. apply Plt_Ple_trans with (st_nextnode s2).
-  unfold nloop, s2; simpl; apply Plt_succ.
-  inversion i'; auto.
+  intros. unfold update_instr in H. 
+  destruct (plt n (st_nextnode s1)); try discriminate.
+  destruct (check_empty_node s1 n); try discriminate.
+  inv H. simpl. apply PTree.gss.
 Qed.
+Hint Resolve update_instr_at: rtlg.
 
 (** Properties of [new_reg]. *)
 
@@ -819,76 +755,84 @@ Inductive tr_switch
   its value is deposited in register [rret]. *)
 
 Inductive tr_stmt (c: code) (map: mapping):
-     stmt -> node -> node -> list node -> node -> option reg -> Prop :=
-  | tr_Sskip: forall ns nexits nret rret,
-     tr_stmt c map Sskip ns ns nexits nret rret
-  | tr_Sassign: forall id a ns nd nexits nret rret rt n,
+     stmt -> node -> node -> list node -> labelmap -> node -> option reg -> Prop :=
+  | tr_Sskip: forall ns nexits ngoto nret rret,
+     tr_stmt c map Sskip ns ns nexits ngoto nret rret
+  | tr_Sassign: forall id a ns nd nexits ngoto nret rret rt n,
      tr_expr c map nil a ns n rt ->
      tr_store_var c map rt id n nd ->
-     tr_stmt c map (Sassign id a) ns nd nexits nret rret
-  | tr_Sstore: forall chunk addr al b ns nd nexits nret rret rd n1 rl n2,
+     tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret
+  | tr_Sstore: forall chunk addr al b ns nd nexits ngoto nret rret rd n1 rl n2,
      tr_exprlist c map nil al ns n1 rl ->
      tr_expr c map rl b n1 n2 rd ->
      c!n2 = Some (Istore chunk addr rl rd nd) ->
-     tr_stmt c map (Sstore chunk addr al b) ns nd nexits nret rret
-  | tr_Scall: forall optid sig b cl ns nd nexits nret rret rd n1 rf n2 n3 rargs,
+     tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret
+  | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs,
      tr_expr c map nil b ns n1 rf ->
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) ->
      tr_store_optvar c map rd optid n3 nd ->
      ~reg_in_map map rd ->
-     tr_stmt c map (Scall optid sig b cl) ns nd nexits nret rret
-  | tr_Salloc: forall id a ns nd nexits nret rret rd n1 n2 r,
+     tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret
+  | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs,
+     tr_expr c map nil b ns n1 rf ->
+     tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
+     c!n2 = Some (Itailcall sig (inl _ rf) rargs) ->
+     tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret
+  | tr_Salloc: forall id a ns nd nexits ngoto nret rret rd n1 n2 r,
      tr_expr c map nil a ns n1 r ->
      c!n1 = Some (Ialloc r rd n2) ->
      tr_store_var c map rd id n2 nd ->
      ~reg_in_map map rd ->
-     tr_stmt c map (Salloc id a) ns nd nexits nret rret
-  | tr_Sseq: forall s1 s2 ns nd nexits nret rret n,
-     tr_stmt c map s2 n nd nexits nret rret ->
-     tr_stmt c map s1 ns n nexits nret rret ->
-     tr_stmt c map (Sseq s1 s2) ns nd nexits nret rret
-  | tr_Sifthenelse: forall a strue sfalse ns nd nexits nret rret ntrue nfalse,
-     tr_stmt c map strue ntrue nd nexits nret rret ->
-     tr_stmt c map sfalse nfalse nd nexits nret rret ->
+     tr_stmt c map (Salloc id a) ns nd nexits ngoto nret rret
+  | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n,
+     tr_stmt c map s2 n nd nexits ngoto nret rret ->
+     tr_stmt c map s1 ns n nexits ngoto nret rret ->
+     tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret
+  | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse,
+     tr_stmt c map strue ntrue nd nexits ngoto nret rret ->
+     tr_stmt c map sfalse nfalse nd nexits ngoto nret rret ->
      tr_condition c map nil a ns ntrue nfalse ->
-     tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits nret rret
-  | tr_Sloop: forall sbody ns nd nexits nret rret nloop,
-     tr_stmt c map sbody ns nloop nexits nret rret ->
-     c!nloop = Some(Inop ns) ->
-     tr_stmt c map (Sloop sbody) ns nd nexits nret rret
-  | tr_Sblock: forall sbody ns nd nexits nret rret,
-     tr_stmt c map sbody ns nd (nd :: nexits) nret rret ->
-     tr_stmt c map (Sblock sbody) ns nd nexits nret rret
-  | tr_Sexit: forall n ns nd nexits nret rret,
+     tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret
+  | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop,
+     tr_stmt c map sbody nloop ns nexits ngoto nret rret ->
+     c!ns = Some(Inop nloop) ->
+     tr_stmt c map (Sloop sbody) ns nd nexits ngoto nret rret
+  | tr_Sblock: forall sbody ns nd nexits ngoto nret rret,
+     tr_stmt c map sbody ns nd (nd :: nexits) ngoto nret rret ->
+     tr_stmt c map (Sblock sbody) ns nd nexits ngoto nret rret
+  | tr_Sexit: forall n ns nd nexits ngoto nret rret,
      nth_error nexits n = Some ns ->
-     tr_stmt c map (Sexit n) ns nd nexits nret rret
-  | tr_Sswitch: forall a cases default ns nd nexits nret rret n r t,
+     tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret
+  | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t,
      validate_switch default cases t = true ->
      tr_expr c map nil a ns n r ->
      tr_switch c r nexits t n ->
-     tr_stmt c map (Sswitch a cases default) ns nd nexits nret rret
-  | tr_Sreturn_none: forall nret nd nexits,
-     tr_stmt c map (Sreturn None) nret nd nexits nret None
-  | tr_Sreturn_some: forall a ns nd nexits nret rret,
+     tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret
+  | tr_Sreturn_none: forall nret nd nexits ngoto,
+     tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None
+  | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret,
      tr_expr c map nil a ns nret rret ->
-     tr_stmt c map (Sreturn (Some a)) ns nd nexits nret (Some rret)
-  | tr_Stailcall: forall sig b cl ns nd nexits nret rret n1 rf n2 rargs,
-     tr_expr c map nil b ns n1 rf ->
-     tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
-     c!n2 = Some (Itailcall sig (inl _ rf) rargs) ->
-     tr_stmt c map (Stailcall sig b cl) ns nd nexits nret rret.
+     tr_stmt c map (Sreturn (Some a)) ns nd nexits ngoto nret (Some rret)
+  | tr_Slabel: forall lbl s ns nd nexits ngoto nret rret n,
+     ngoto!lbl = Some n ->
+     c!n = Some (Inop ns) ->
+     tr_stmt c map s ns nd nexits ngoto nret rret ->
+     tr_stmt c map (Slabel lbl s) ns nd nexits ngoto nret rret
+  | tr_Sgoto: forall lbl ns nd nexits ngoto nret rret,
+     ngoto!lbl = Some ns ->
+     tr_stmt c map (Sgoto lbl) ns nd nexits ngoto nret rret.
 
 (** [tr_function f tf] specifies the RTL function [tf] that 
   [RTLgen.transl_function] returns.  *)
 
 Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
   | tr_function_intro:
-      forall f code rparams map1 s1 i1 rvars map2 s2 i2 nentry nret rret orret nextnode wfcode,
-      add_vars init_mapping f.(CminorSel.fn_params) init_state = OK (rparams, map1) s1 i1 ->
+      forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret nextnode wfcode,
+      add_vars init_mapping f.(CminorSel.fn_params) s0 = OK (rparams, map1) s1 i1 ->
       add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 ->
       orret = ret_reg f.(CminorSel.fn_sig) rret ->
-      tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil nret orret ->
+      tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil ngoto nret orret ->
       code!nret = Some(Ireturn orret) -> 
       tr_function f (RTL.mkfunction
                        f.(CminorSel.fn_sig)
@@ -918,18 +862,17 @@ Definition tr_expr_condition_exprlist_ind3
        (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l)
              (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)).
 
-Lemma tr_move_extends:
-  forall s1 s2, state_extends s1 s2 ->
+Lemma tr_move_incr:
+  forall s1 s2, state_incr s1 s2 ->
   forall ns rs nd rd,
   tr_move s1.(st_code) ns rs nd rd ->
   tr_move s2.(st_code) ns rs nd rd.
 Proof.
-  induction 2; econstructor; eauto.
-  eapply instr_at_extends; eauto.
+  induction 2; econstructor; eauto with rtlg.
 Qed.
 
-Lemma tr_expr_condition_exprlist_extends:
-  forall s1 s2, state_extends s1 s2 ->
+Lemma tr_expr_condition_exprlist_incr:
+  forall s1 s2, state_incr s1 s2 ->
   (forall map pr a ns nd rd,
    tr_expr s1.(st_code) map pr a ns nd rd ->
    tr_expr s2.(st_code) map pr a ns nd rd)
@@ -941,10 +884,10 @@ Lemma tr_expr_condition_exprlist_extends:
    tr_exprlist s2.(st_code) map pr al ns nd rl).
 Proof.
   intros s1 s2 EXT. 
-  pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT).
+  pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
   apply tr_expr_condition_exprlist_ind3; intros; econstructor; eauto.
-  eapply tr_move_extends; eauto.
-  eapply tr_move_extends; eauto.
+  eapply tr_move_incr; eauto.
+  eapply tr_move_incr; eauto.
 Qed.
 
 Lemma tr_expr_incr:
@@ -954,8 +897,8 @@ Lemma tr_expr_incr:
   tr_expr s2.(st_code) map pr a ns nd rd.
 Proof.
   intros.
-  exploit tr_expr_condition_exprlist_extends. 
-  apply state_incr_extends; eauto. intros [A [B C]]. eauto.
+  exploit tr_expr_condition_exprlist_incr; eauto.
+  intros [A [B C]]. eauto.
 Qed.
 
 Lemma tr_condition_incr:
@@ -965,8 +908,8 @@ Lemma tr_condition_incr:
   tr_condition s2.(st_code) map pr a ns ntrue nfalse.
 Proof.
   intros.
-  exploit tr_expr_condition_exprlist_extends. 
-  apply state_incr_extends; eauto. intros [A [B C]]. eauto.
+  exploit tr_expr_condition_exprlist_incr; eauto. 
+  intros [A [B C]]. eauto.
 Qed.
 
 Lemma tr_exprlist_incr:
@@ -976,8 +919,8 @@ Lemma tr_exprlist_incr:
   tr_exprlist s2.(st_code) map pr al ns nd rl.
 Proof.
   intros.
-  exploit tr_expr_condition_exprlist_extends. 
-  apply state_incr_extends; eauto. intros [A [B C]]. eauto.
+  exploit tr_expr_condition_exprlist_incr; eauto.
+  intros [A [B C]]. eauto.
 Qed.
 
 Scheme expr_ind3 := Induction for expr Sort Prop
@@ -1117,63 +1060,51 @@ Proof.
   intros. eapply B; eauto with rtlg.
 Qed.
 
-Lemma tr_store_var_extends:
-  forall s1 s2, state_extends s1 s2 ->
+Lemma tr_store_var_incr:
+  forall s1 s2, state_incr s1 s2 ->
   forall map rs id ns nd,
   tr_store_var s1.(st_code) map rs id ns nd ->
   tr_store_var s2.(st_code) map rs id ns nd.
 Proof.
   intros. destruct H0 as [rv [A B]]. 
-  econstructor; split. eauto. eapply tr_move_extends; eauto.
+  econstructor; split. eauto. eapply tr_move_incr; eauto.
 Qed.
  
-Lemma tr_store_optvar_extends:
-  forall s1 s2, state_extends s1 s2 ->
+Lemma tr_store_optvar_incr:
+  forall s1 s2, state_incr s1 s2 ->
   forall map rs optid ns nd,
   tr_store_optvar s1.(st_code) map rs optid ns nd ->
   tr_store_optvar s2.(st_code) map rs optid ns nd.
 Proof.
   intros until nd. destruct optid; simpl. 
-  apply tr_store_var_extends; auto.
+  apply tr_store_var_incr; auto.
   auto.
 Qed.
 
-Lemma tr_switch_extends:
-  forall s1 s2, state_extends s1 s2 ->
+Lemma tr_switch_incr:
+  forall s1 s2, state_incr s1 s2 ->
   forall r nexits t ns,
   tr_switch s1.(st_code) r nexits t ns ->
   tr_switch s2.(st_code) r nexits t ns.
 Proof.
   induction 2; econstructor; eauto with rtlg.
-  eapply instr_at_extends; eauto.
-  eapply instr_at_extends; eauto.
-Qed.
-
-Lemma tr_stmt_extends:
-  forall s1 s2, state_extends s1 s2 ->
-  forall map s ns nd nexits nret rret,
-  tr_stmt s1.(st_code) map s ns nd nexits nret rret ->
-  tr_stmt s2.(st_code) map s ns nd nexits nret rret.
-Proof.
-  intros s1 s2 EXT.
-  destruct (tr_expr_condition_exprlist_extends s1 s2 EXT) as [A [B C]].
-  pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT).
-  pose (STV := tr_store_var_extends s1 s2 EXT).
-  pose (STOV := tr_store_optvar_extends s1 s2 EXT).
-  induction 1; econstructor; eauto.
-  eapply tr_switch_extends; eauto.
 Qed.
 
 Lemma tr_stmt_incr:
   forall s1 s2, state_incr s1 s2 ->
-  forall map s ns nd nexits nret rret,
-  tr_stmt s1.(st_code) map s ns nd nexits nret rret ->
-  tr_stmt s2.(st_code) map s ns nd nexits nret rret.
+  forall map s ns nd nexits ngoto nret rret,
+  tr_stmt s1.(st_code) map s ns nd nexits ngoto nret rret ->
+  tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret.
 Proof.
-  intros. eapply tr_stmt_extends; eauto with rtlg.
+  intros s1 s2 EXT.
+  destruct (tr_expr_condition_exprlist_incr s1 s2 EXT) as [A [B C]].
+  pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+  pose (STV := tr_store_var_incr s1 s2 EXT).
+  pose (STOV := tr_store_optvar_incr s1 s2 EXT).
+  induction 1; econstructor; eauto.
+  eapply tr_switch_incr; eauto.
 Qed.
 
-
 Lemma store_var_charact:
   forall map rs id nd s ns s' incr,
   store_var map rs id nd s = OK ns s' incr ->
@@ -1215,27 +1146,27 @@ Proof.
   monadInv H.
   exploit transl_exit_charact; eauto. intros [A B]. subst s1.
   econstructor; eauto with rtlg. 
-  apply tr_switch_extends with s0; eauto with rtlg.
+  apply tr_switch_incr with s0; eauto with rtlg.
 
   monadInv H.
   econstructor; eauto with rtlg. 
-  apply tr_switch_extends with s1; eauto with rtlg.
-  apply tr_switch_extends with s0; eauto with rtlg.
+  apply tr_switch_incr with s1; eauto with rtlg.
+  apply tr_switch_incr with s0; eauto with rtlg.
 Qed.
  
 Lemma transl_stmt_charact:
-  forall map stmt nd nexits nret rret s ns s' INCR
-    (TR: transl_stmt map stmt nd nexits nret rret s = OK ns s' INCR)
+  forall map stmt nd nexits ngoto nret rret s ns s' INCR
+    (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR)
     (WF: map_valid map s)
     (OK: return_reg_ok s map rret),
-  tr_stmt s'.(st_code) map stmt ns nd nexits nret rret.
+  tr_stmt s'.(st_code) map stmt ns nd nexits ngoto nret rret.
 Proof.
   induction stmt; intros; simpl in TR; try (monadInv TR).
   (* Sskip *)
   constructor.
   (* Sassign *)
   econstructor. eapply transl_expr_charact; eauto with rtlg.
-  apply tr_store_var_extends with s1; auto with rtlg.
+  apply tr_store_var_incr with s1; auto with rtlg.
   eapply store_var_charact; eauto.
   (* Sstore *)
   destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
@@ -1256,12 +1187,20 @@ Proof.
   apply regs_valid_incr with s1; eauto with rtlg.
   apply regs_valid_cons; eauto with rtlg.
   apply regs_valid_incr with s2; eauto with rtlg.
-  apply tr_store_optvar_extends with s4; eauto with rtlg.
+  apply tr_store_optvar_incr with s4; eauto with rtlg.
   eapply store_optvar_charact; eauto with rtlg.
+  (* Stailcall *)
+  destruct transl_expr_condexpr_list_charact as [A [B C]].
+  assert (RV: regs_valid (x :: nil) s1).
+    apply regs_valid_cons; eauto with rtlg. 
+  econstructor; eauto with rtlg.
+  eapply A; eauto with rtlg.
+  apply tr_exprlist_incr with s4; auto.
+  eapply C; eauto with rtlg.
   (* Salloc *)
   econstructor; eauto with rtlg.
   eapply transl_expr_charact; eauto with rtlg.
-  apply tr_store_var_extends with s2; eauto with rtlg.
+  apply tr_store_var_incr with s2; eauto with rtlg.
   eapply store_var_charact; eauto with rtlg.
   (* Sseq *)
   econstructor. 
@@ -1283,12 +1222,10 @@ Proof.
   eapply IHstmt2; eauto with rtlg.
   eapply transl_condexpr_charact; eauto with rtlg.
   (* Sloop *)
-  exploit add_loop_inversion; eauto. 
-  intros [nloop [s2 [s3 [INCR23 [INCR02 [EQ [EXT CODEAT]]]]]]].
   econstructor. 
-  apply tr_stmt_extends with s3; auto. 
-  eapply IHstmt; eauto with rtlg. 
-  auto.
+  apply tr_stmt_incr with s1; auto. 
+  eapply IHstmt; eauto with rtlg.
+  eauto with rtlg.
   (* Sblock *)
   econstructor. 
   eapply IHstmt; eauto with rtlg.
@@ -1302,7 +1239,7 @@ Proof.
   monadInv TR.
   econstructor; eauto with rtlg.
   eapply transl_expr_charact; eauto with rtlg.
-  apply tr_switch_extends with s1; auto with rtlg.
+  apply tr_switch_incr with s1; auto with rtlg.
   eapply transl_switch_charact; eauto with rtlg.
   monadInv TR. 
   (* Sreturn *)
@@ -1312,14 +1249,15 @@ Proof.
   eapply transl_expr_charact; eauto with rtlg.
   constructor. auto. simpl; tauto. 
   constructor.
-  (* Stailcall *)
-  destruct transl_expr_condexpr_list_charact as [A [B C]].
-  assert (RV: regs_valid (x :: nil) s1).
-    apply regs_valid_cons; eauto with rtlg. 
-  econstructor; eauto with rtlg.
-  eapply A; eauto with rtlg.
-  apply tr_exprlist_incr with s4; auto.
-  eapply C; eauto with rtlg.
+  (* Slabel *)
+  generalize EQ0; clear EQ0. case_eq (ngoto!l); intros; monadInv EQ0.
+  generalize EQ1; clear EQ1. unfold handle_error. 
+  case_eq (update_instr n (Inop ns) s0); intros; inv EQ1.
+  econstructor. eauto. eauto with rtlg.
+  eapply tr_stmt_incr with s0; eauto with rtlg.
+  (* Sgoto *)
+  generalize TR; clear TR. case_eq (ngoto!l); intros; monadInv TR.
+  econstructor. auto.
 Qed.
 
 Lemma transl_function_charact:
@@ -1327,8 +1265,10 @@ Lemma transl_function_charact:
   transl_function f = Errors.OK tf ->
   tr_function f tf.
 Proof.
-  intros until tf. unfold transl_function. 
-  caseEq (transl_fun f init_state). congruence. 
+  intros until tf. unfold transl_function.
+  caseEq (reserve_labels (fn_body f) (PTree.empty node, init_state)). 
+  intros ngoto s0 RESERVE.
+  caseEq (transl_fun f ngoto s0). congruence. 
   intros [nentry rparams] sfinal INCR TR E. inv E. 
   monadInv TR.
   exploit add_vars_valid. eexact EQ. apply init_mapping_valid.
diff --git a/backend/Selection.v b/backend/Selection.v
index a55b1918..6554e429 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -1153,6 +1153,8 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
   | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
   | Cminor.Scall optid sg fn args =>
       Scall optid sg (sel_expr fn) (sel_exprlist args)
+  | Cminor.Stailcall sg fn args => 
+      Stailcall sg (sel_expr fn) (sel_exprlist args)
   | Cminor.Salloc id b => Salloc id (sel_expr b)
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
   | Cminor.Sifthenelse e ifso ifnot =>
@@ -1164,8 +1166,8 @@ Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
   | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl
   | Cminor.Sreturn None => Sreturn None
   | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e))
-  | Cminor.Stailcall sg fn args => 
-      Stailcall sg (sel_expr fn) (sel_exprlist args)
+  | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body)
+  | Cminor.Sgoto lbl => Sgoto lbl
   end.
 
 (** Conversion of functions and programs. *)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 8b4713db..bd4dd233 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -21,6 +21,7 @@ Require Import Values.
 Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Smallstep.
 Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
@@ -1060,17 +1061,18 @@ Proof.
 Qed.
 
 Lemma eval_store:
-  forall chunk a1 a2 v1 v2 m',
+  forall chunk a1 a2 v1 v2 f k m',
   eval_expr ge sp e m nil a1 v1 ->
   eval_expr ge sp e m nil a2 v2 ->
   Mem.storev chunk m v1 v2 = Some m' ->
-  exec_stmt ge sp e m (store chunk a1 a2) E0 e m' Out_normal.
+  step ge (State f (store chunk a1 a2) k sp e m)
+       E0 (State f Sskip k sp e m').
 Proof.
   intros. generalize H1; destruct v1; simpl; intro; try discriminate.
   unfold store.
   generalize (eval_addressing _ _ _ _ _ H (refl_equal _)).
   destruct (addressing a1). intros [vl [EV EQ]]. 
-  eapply exec_Sstore; eauto. 
+  eapply step_store; eauto. 
 Qed.
 
 (** * Correctness of instruction selection for operators *)
@@ -1241,144 +1243,149 @@ Hint Resolve sel_exprlist_correct: evalexpr.
 
 (** Semantic preservation for terminating function calls and statements. *)
 
-Definition eval_funcall_exec_stmt_ind2
-  (P1 : mem -> Cminor.fundef -> list val -> trace -> mem -> val -> Prop)
-  (P2 : val -> env -> mem -> Cminor.stmt -> trace -> env -> mem -> outcome -> Prop) :=
-  fun a b c d e f g h i j k l m n o p q r =>
-  conj (Cminor.eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r)
-       (Cminor.exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r).
-
-Lemma sel_function_stmt_correct:
-     (forall m fd vargs t m' vres,
-      Cminor.eval_funcall ge m fd vargs t m' vres ->
-      CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres)
-  /\ (forall sp e m s t e' m' out,
-      Cminor.exec_stmt ge sp e m s t e' m' out ->
-      CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out).
+Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont :=
+  match k with
+  | Cminor.Kstop => Kstop
+  | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1)
+  | Cminor.Kblock k1 => Kblock (sel_cont k1)
+  | Cminor.Kcall id f sp e k1 =>
+      Kcall id (sel_function f) sp e (sel_cont k1)
+  end.
+
+Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
+  | match_state: forall f s k s' k' sp e m,
+      s' = sel_stmt s ->
+      k' = sel_cont k ->
+      match_states
+        (Cminor.State f s k sp e m)
+        (State (sel_function f) s' k' sp e m)
+  | match_callstate: forall f args k k' m,
+      k' = sel_cont k ->
+      match_states
+        (Cminor.Callstate f args k m)
+        (Callstate (sel_fundef f) args k' m)
+  | match_returnstate: forall v k k' m,
+      k' = sel_cont k ->
+      match_states
+        (Cminor.Returnstate v k m)
+        (Returnstate v k' m).
+
+Remark call_cont_commut:
+  forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k).
 Proof.
-  apply eval_funcall_exec_stmt_ind2; intros; simpl.
-  (* Internal function *)
-  econstructor; eauto. 
-  (* External function *)
-  econstructor; eauto.
-  (* Sskip *)
-  constructor.
-  (* Sassign *)
-  econstructor; eauto with evalexpr. 
-  (* Sstore *)
-  eapply eval_store; eauto with evalexpr. 
-  (* Scall *)
-  econstructor; eauto with evalexpr.
-  apply functions_translated; auto.
-  rewrite <- H2. apply sig_function_translated.
-  (* Salloc *)
-  econstructor; eauto with evalexpr.
-  (* Sifthenelse *)
-  econstructor; eauto with evalexpr.
-  eapply eval_condition_of_expr; eauto with evalexpr.
-  destruct b; auto.
-  (* Sseq *)
-  eapply exec_Sseq_continue; eauto.
-  eapply exec_Sseq_stop; eauto.
-  (* Sloop *)
-  eapply exec_Sloop_loop; eauto.
-  eapply exec_Sloop_stop; eauto.
-  (* Sblock *)
-  econstructor; eauto.
-  (* Sexit *)
-  constructor.
-  (* Sswitch *)
-  econstructor; eauto with evalexpr.
-  (* Sreturn *)
-  constructor.
-  econstructor; eauto with evalexpr.
-  (* Stailcall *)
-  econstructor; eauto with evalexpr.
-  apply functions_translated; auto.
-  rewrite <- H2. apply sig_function_translated.
+  induction k; simpl; auto.
 Qed.
 
-Lemma sel_function_correct:
-      forall m fd vargs t m' vres,
-      Cminor.eval_funcall ge m fd vargs t m' vres ->
-      CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres.
-Proof (proj1 sel_function_stmt_correct).
-
-Lemma sel_stmt_correct:
-      forall sp e m s t e' m' out,
-      Cminor.exec_stmt ge sp e m s t e' m' out ->
-      CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out.
-Proof (proj2 sel_function_stmt_correct).
-
-Hint Resolve sel_stmt_correct: evalexpr.
-
-(** Semantic preservation for diverging function calls and statements. *)
+Remark find_label_commut:
+  forall lbl s k,
+  find_label lbl (sel_stmt s) (sel_cont k) =
+  option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk)))
+             (Cminor.find_label lbl s k).
+Proof.
+  induction s; intros; simpl; auto.
+  unfold store. destruct (addressing (sel_expr e)); auto.
+  change (Kseq (sel_stmt s2) (sel_cont k))
+    with (sel_cont (Cminor.Kseq s2 k)).
+  rewrite IHs1. rewrite IHs2. 
+  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto.
+  rewrite IHs1. rewrite IHs2. 
+  destruct (Cminor.find_label lbl s1 k); auto.
+  change (Kseq (Sloop (sel_stmt s)) (sel_cont k))
+    with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)).
+  auto.
+  change (Kblock (sel_cont k))
+    with (sel_cont (Cminor.Kblock k)).
+  auto.
+  destruct o; auto.
+  destruct (ident_eq lbl l); auto.
+Qed.
 
-Lemma sel_function_divergence_correct:
-  forall m fd vargs t,
-  Cminor.evalinf_funcall ge m fd vargs t ->
-  CminorSel.evalinf_funcall tge m (sel_fundef fd) vargs t.
+Lemma sel_step_correct:
+  forall S1 t S2, Cminor.step ge S1 t S2 ->
+  forall T1, match_states S1 T1 ->
+  exists T2, step tge T1 t T2 /\ match_states S2 T2.
 Proof.
-  cofix FUNCALL.
-  assert (STMT: forall sp e m s t,
-            Cminor.execinf_stmt ge sp e m s t ->
-            CminorSel.execinf_stmt tge sp e m (sel_stmt s) t).
-  cofix STMT; intros.
-  inversion H; subst; simpl.
-  (* Call *)
+  induction 1; intros T1 ME; inv ME; simpl;
+  try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail).
+
+  (* skip call *)
+  econstructor; split. 
+  econstructor. destruct k; simpl in H; simpl; auto. 
+  rewrite <- H0; reflexivity.
+  constructor; auto.
+  (* assign *)
+  exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split.
+  constructor. auto with evalexpr.
+  constructor; auto.
+  (* store *)
+  econstructor; split.
+  eapply eval_store; eauto with evalexpr.
+  constructor; auto.
+  (* Scall *)
+  econstructor; split.
   econstructor; eauto with evalexpr.
-  apply functions_translated; auto.
+  apply functions_translated; eauto. 
   apply sig_function_translated.
-  (* Ifthenelse *)
-  econstructor; eauto with evalexpr.
-  eapply eval_condition_of_expr; eauto with evalexpr.
-  destruct b; eapply STMT; eauto.
-  (* Seq *)
-  apply execinf_Sseq_1; eauto.
-  eapply execinf_Sseq_2; eauto with evalexpr.
-  (* Loop *)
-  eapply execinf_Sloop_body; eauto.
-  eapply execinf_Sloop_loop; eauto with evalexpr.
-  change (Sloop (sel_stmt s0)) with (sel_stmt (Cminor.Sloop s0)).
-  apply STMT. auto.
-  (* Block *)
-  apply execinf_Sblock; eauto.
-  (* Tailcall *)
+  constructor; auto.
+  (* Stailcall *)
+  econstructor; split.
   econstructor; eauto with evalexpr.
-  apply functions_translated; auto.
+  apply functions_translated; eauto. 
   apply sig_function_translated.
-
-  intros. inv H; simpl.
-  (* Internal functions *)
+  constructor; auto. apply call_cont_commut.
+  (* Salloc *)
+  exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id (Vptr b Int.zero) e) m'); split.
   econstructor; eauto with evalexpr.
-  unfold sel_function; simpl. eapply STMT; eauto. 
-Qed. 
+  constructor; auto.
+  (* Sifthenelse *)
+  exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split.
+  constructor. eapply eval_condition_of_expr; eauto with evalexpr.
+  constructor; auto. destruct b; auto.
+  (* Sreturn None *)
+  econstructor; split. 
+  econstructor. rewrite <- H; reflexivity.
+  constructor; auto. apply call_cont_commut.
+  (* Sreturn Some *)
+  econstructor; split. 
+  econstructor. simpl. auto. eauto with evalexpr. 
+  constructor; auto. apply call_cont_commut.
+  (* Sgoto *)
+  econstructor; split.
+  econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
+  rewrite H. simpl. reflexivity. 
+  constructor; auto.
+Qed.
 
-End PRESERVATION.
+Lemma sel_initial_states:
+  forall S, Cminor.initial_state prog S ->
+  exists R, initial_state tprog R /\ match_states S R.
+Proof.
+  induction 1.
+  econstructor; split.
+  econstructor.
+  simpl. fold tge. rewrite symbols_preserved. eexact H.
+  apply function_ptr_translated. eauto. 
+  rewrite <- H1. apply sig_function_translated; auto.
+  unfold tprog, sel_program. rewrite Genv.init_mem_transf.
+  constructor; auto.
+Qed.
 
-(** As a corollary, instruction selection preserves the observable
-   behaviour of programs. *)
+Lemma sel_final_states:
+  forall S R r,
+  match_states S R -> Cminor.final_state S r -> final_state R r.
+Proof.
+  intros. inv H0. inv H. simpl. constructor.
+Qed.
 
-Theorem sel_program_correct:
-  forall prog beh,
-  Cminor.exec_program prog beh ->
-  CminorSel.exec_program (sel_program prog) beh.
+Theorem transf_program_correct:
+  forall (beh: program_behavior),
+  Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.
 Proof.
-  intros. inv H. 
-  (* Terminating *)
-  apply program_terminates with b (sel_fundef f) m.
-  simpl. rewrite <- H0. unfold ge. apply symbols_preserved.
-  apply function_ptr_translated. auto.
-  rewrite <- H2. apply sig_function_translated. 
-  replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog).
-  apply sel_function_correct; auto.
-  symmetry. unfold sel_program. apply Genv.init_mem_transf.
-  (* Diverging *)
-  apply program_diverges with b (sel_fundef f).
-  simpl. rewrite <- H0. unfold ge. apply symbols_preserved.
-  apply function_ptr_translated. auto.
-  rewrite <- H2. apply sig_function_translated. 
-  replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog).
-  apply sel_function_divergence_correct; auto.
-  symmetry. unfold sel_program. apply Genv.init_mem_transf.
+  unfold CminorSel.exec_program, Cminor.exec_program; intros.
+  eapply simulation_step_preservation; eauto.
+  eexact sel_initial_states.
+  eexact sel_final_states.
+  exact sel_step_correct. 
 Qed.
+
+End PRESERVATION.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index a6038758..9dfb5732 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -2461,7 +2461,7 @@ Theorem transl_program_correct:
   Csharpminor.exec_program prog beh ->
   exec_program tprog beh.
 Proof.
-  intros.
+  intros. apply exec_program_bigstep_transition.
   set (m0 := Genv.init_mem prog) in *.
   set (f := meminj_init m0).
   assert (MINJ0: mem_inject f m0 m0).
diff --git a/common/Main.v b/common/Main.v
index e5f6280c..f50640ae 100644
--- a/common/Main.v
+++ b/common/Main.v
@@ -283,8 +283,8 @@ Proof.
   destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]].
   generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1.
   apply transf_rtl_program_correct with p3. auto.
-  apply RTLgenproof.transl_program_correct with p2; auto.
-  rewrite <- P1. apply Selectionproof.sel_program_correct; auto.
+  apply RTLgenproof.transf_program_correct with p2; auto.
+  rewrite <- P1. apply Selectionproof.transf_program_correct; auto.
 Qed.
 
 Theorem transf_c_program_correct:
diff --git a/common/Smallstep.v b/common/Smallstep.v
index ec7a416d..a2634be1 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -19,6 +19,8 @@
   the one-step transition relations that are used to specify
   operational semantics in small-step style. *)
 
+Require Import Wf.
+Require Import Wf_nat.
 Require Import Coqlib.
 Require Import AST.
 Require Import Events.
@@ -157,7 +159,8 @@ Proof.
 Qed.
 
 Lemma plus_inv:
-  forall ge s1 t s2,  plus ge s1 t s2 ->
+  forall ge s1 t s2, 
+  plus ge s1 t s2 ->
   step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2.
 Proof.
   intros. inversion H; subst. inversion H1; subst.
@@ -166,6 +169,14 @@ Proof.
   split. econstructor; eauto. auto.
 Qed.
 
+Lemma star_inv:
+  forall ge s1 t s2,
+  star ge s1 t s2 ->
+  (s2 = s1 /\ t = E0) \/ plus ge s1 t s2.
+Proof.
+  intros. inv H. left; auto. right; econstructor; eauto.
+Qed.
+
 (** Infinitely many transitions *)
 
 CoInductive forever (ge: genv): state -> traceinf -> Prop :=
@@ -186,61 +197,86 @@ Qed.
 (** An alternate, equivalent definition of [forever] that is useful
     for coinductive reasoning. *)
 
-CoInductive forever_N (ge: genv): nat -> state -> traceinf -> Prop :=
-  | forever_N_star: forall s1 t s2 p q T1 T2,
+Variable A: Set.
+Variable order: A -> A -> Prop.
+
+CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop :=
+  | forever_N_star: forall s1 t s2 a1 a2 T1 T2,
       star ge s1 t s2 -> 
-      (p < q)%nat ->
-      forever_N ge p s2 T2 ->
+      order a2 a1 ->
+      forever_N ge a2 s2 T2 ->
       T1 = t *** T2 ->
-      forever_N ge q s1 T1
-  | forever_N_plus: forall s1 t s2 p q T1 T2,
+      forever_N ge a1 s1 T1
+  | forever_N_plus: forall s1 t s2 a1 a2 T1 T2,
       plus ge s1 t s2 ->
-      forever_N ge p s2 T2 ->
+      forever_N ge a2 s2 T2 ->
       T1 = t *** T2 ->
-      forever_N ge q s1 T1.
+      forever_N ge a1 s1 T1.
 
-Remark Peano_induction:
-  forall (P: nat -> Prop),
-  (forall p, (forall q, (q < p)%nat -> P q) -> P p) ->
-  forall p, P p.
-Proof.
-  intros P IH.
-  assert (forall p, forall q, (q < p)%nat -> P q).
-  induction p; intros. elimtype False; omega.
-  apply IH. intros. apply IHp. omega.
-  intro. apply H with (S p). omega.
-Qed.
+Hypothesis order_wf: well_founded order.
 
 Lemma forever_N_inv:
-  forall ge p s T,
-  forever_N ge p s T ->
-  exists t, exists s', exists q, exists T',
-  step ge s t s' /\ forever_N ge q s' T' /\ T = t *** T'.
+  forall ge a s T,
+  forever_N ge a s T ->
+  exists t, exists s', exists a', exists T',
+  step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'.
 Proof.
-  intros ge p. pattern p. apply Peano_induction; intros.
-  inv H0.
+  intros ge a0. pattern a0. apply (well_founded_ind order_wf).
+  intros. inv H0.
   (* star case *)
   inv H1.
   (* no transition *)
-  change (E0 *** T2) with T2. apply H with p1. auto. auto. 
+  change (E0 *** T2) with T2. apply H with a2. auto. auto. 
   (* at least one transition *)
-  exists t1; exists s0; exists p0; exists (t2 *** T2).
+  exists t1; exists s0; exists x; exists (t2 *** T2).
   split. auto. split. eapply forever_N_star; eauto.
   apply Eappinf_assoc.
   (* plus case *)
   inv H1.
-  exists t1; exists s0; exists (S p1); exists (t2 *** T2).
-  split. auto. split. eapply forever_N_star; eauto. 
+  exists t1; exists s0; exists a2; exists (t2 *** T2).
+  split. auto.
+  split. inv H3. auto.  
+  eapply forever_N_plus. econstructor; eauto. eauto. auto.
   apply Eappinf_assoc.
 Qed.
 
 Lemma forever_N_forever:
-  forall ge p s T, forever_N ge p s T -> forever ge s T.
+  forall ge a s T, forever_N ge a s T -> forever ge s T.
 Proof.
   cofix COINDHYP; intros.
-  destruct (forever_N_inv H) as [t [s' [q [T' [A [B C]]]]]].
-  rewrite C. apply forever_intro with s'. auto. 
-  apply COINDHYP with q; auto.
+  destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]].
+  rewrite R. apply forever_intro with s'. auto. 
+  apply COINDHYP with a'; auto.
+Qed.
+
+(** Yet another alternative definition of [forever]. *)
+
+CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop :=
+  | forever_plus_intro: forall s1 t s2 T1 T2,
+      plus ge s1 t s2 -> 
+      forever_plus ge s2 T2 ->
+      T1 = t *** T2 ->
+      forever_plus ge s1 T1.
+
+Lemma forever_plus_inv:
+  forall ge s T,
+  forever_plus ge s T ->
+  exists s', exists t, exists T',
+  step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'.
+Proof.
+  intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2).
+  split. auto.
+  split. exploit star_inv; eauto. intros [[P Q] | R]. 
+    subst. simpl. auto. econstructor; eauto. 
+  traceEq.
+Qed.
+
+Lemma forever_plus_forever:
+  forall ge s T, forever_plus ge s T -> forever ge s T.
+Proof.
+  cofix COINDHYP; intros.
+  destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]].
+  subst. econstructor; eauto.
 Qed.
 
 (** * Outcomes for program executions *)
@@ -329,19 +365,21 @@ Hypothesis match_final_states:
     in the source program must correspond to infinitely many
     transitions in the second program. *)
 
-Section SIMULATION_STAR.
+Section SIMULATION_STAR_WF.
 
-(** [measure] is a nonnegative integer associated with states
-  of the first semantics.  It must decrease when we take 
-  a stuttering step. *)
+(** [order] is a well-founded ordering associated with states
+  of the first semantics.  Stuttering steps must correspond
+  to states that decrease w.r.t. [order]. *)
 
-Variable measure: state1 -> nat.
+Variable order: state1 -> state1 -> Prop.
+Hypothesis order_wf: well_founded order.
 
 Hypothesis simulation:
   forall st1 t st1', step1 ge1 st1 t st1' ->
   forall st2, match_states st1 st2 ->
-  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
-  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
+  exists st2',
+  (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1))
+  /\ match_states st1' st2'.
 
 Lemma simulation_star_star:
   forall st1 t st1', star step1 ge1 st1 t st1' ->
@@ -350,12 +388,13 @@ Lemma simulation_star_star:
 Proof.
   induction 1; intros.
   exists st2; split. apply star_refl. auto.
-  elim (simulation H H2).
-  intros [st2' [A B]]. 
+  destruct (simulation H H2) as [st2' [A B]].
   destruct (IHstar _ B) as [st3' [C D]].
-  exists st3'; split. apply star_trans with t1 st2' t2.
-  apply plus_star; auto. auto. auto. auto.
-  intros [A [B C]]. rewrite H1. rewrite B. simpl. apply IHstar; auto.
+  exists st3'; split; auto.
+  apply star_trans with t1 st2' t2; auto. 
+  destruct A as [F | [F G]].
+  apply plus_star; auto.
+  auto.
 Qed.
 
 Lemma simulation_star_forever:
@@ -365,19 +404,19 @@ Lemma simulation_star_forever:
 Proof.
   assert (forall st1 st2 T,
     forever step1 ge1 st1 T -> match_states st1 st2 ->
-    forever_N step2 ge2 (measure st1) st2 T).
+    forever_N step2 order ge2 st1 st2 T).
   cofix COINDHYP; intros.
-  inversion H; subst. elim (simulation H1 H0).
-  intros [st2' [A B]]. apply forever_N_plus with t st2' (measure s2) T0.
+  inversion H; subst.
+  destruct (simulation H1 H0) as [st2' [A B]].
+  destruct A as [C | [C D]].
+  apply forever_N_plus with t st2' s2 T0.
   auto. apply COINDHYP. assumption. assumption. auto.
-  intros [A [B C]].
-  apply forever_N_star with t st2 (measure s2) T0.
-  rewrite B. apply star_refl. auto.
-  apply COINDHYP. assumption. auto. auto.
+  apply forever_N_star with t st2' s2 T0.
+  auto. auto. apply COINDHYP. assumption. auto. auto.
   intros. eapply forever_N_forever; eauto.
 Qed.
 
-Lemma simulation_star_preservation:
+Lemma simulation_star_wf_preservation:
   forall beh,
   program_behaves step1 initial_state1 final_state1 ge1 beh ->
   program_behaves step2 initial_state2 final_state2 ge2 beh.
@@ -391,6 +430,36 @@ Proof.
   eapply simulation_star_forever; eauto.
 Qed.
 
+End SIMULATION_STAR_WF.
+
+Section SIMULATION_STAR.
+
+(** We now consider the case where we have a nonnegative integer measure
+  associated with states of the first semantics.  It must decrease when we take 
+  a stuttering step. *)
+
+Variable measure: state1 -> nat.
+
+Hypothesis simulation:
+  forall st1 t st1', step1 ge1 st1 t st1' ->
+  forall st2, match_states st1 st2 ->
+  (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2')
+  \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat.
+
+Lemma simulation_star_preservation:
+  forall beh,
+  program_behaves step1 initial_state1 final_state1 ge1 beh ->
+  program_behaves step2 initial_state2 final_state2 ge2 beh.
+Proof.
+  intros.
+  apply simulation_star_wf_preservation with (ltof _ measure).
+  apply well_founded_ltof. intros.
+  destruct (simulation H0 H1) as [[st2' [A B]] | [A [B C]]].
+  exists st2'; auto.
+  exists st2; split. right; split. rewrite B. apply star_refl. auto. auto.
+  auto.
+Qed.
+
 End SIMULATION_STAR.
 
 (** Lock-step simulation: each transition in the first semantics