Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



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

1 files changed, 1851 insertions, 0 deletions

diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
new file mode 100644
index 0000000..603e273
--- /dev/null
+++ b/cfrontend/SimplExprproof.v
@@ -0,0 +1,1851 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for expression simplification. *)
+
+Require Import Coq.Program.Equality.
+Require Import Axioms.
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Errors.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Events.
+Require Import Smallstep.
+Require Import Globalenvs.
+Require Import Determinism.
+Require Import Csyntax.
+Require Import Csem.
+Require Import Cstrategy.
+Require Import Clight.
+Require Import SimplExpr.
+Require Import SimplExprspec.
+
+Section PRESERVATION.
+
+Variable prog: C.program.
+Variable tprog: Clight.program.
+Hypothesis TRANSL: transl_program prog = OK tprog.
+
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+(** Invariance properties. *)
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof
+  (Genv.find_symbol_transf_partial transl_fundef _ TRANSL).
+
+Lemma function_ptr_translated:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
+Proof
+  (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  exists tf,
+  Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
+Proof
+  (Genv.find_funct_transf_partial transl_fundef _ TRANSL).
+
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof
+  (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
+
+Lemma type_of_fundef_preserved:
+  forall f tf, transl_fundef f = OK tf ->
+  type_of_fundef tf = C.type_of_fundef f.
+Proof.
+  intros. destruct f; monadInv H.
+  exploit transl_function_spec; eauto. intros [A [B [C D]]].
+  simpl. unfold type_of_function, C.type_of_function. congruence.
+  auto.
+Qed.
+
+Lemma function_return_preserved:
+  forall f tf, transl_function f = OK tf ->
+  fn_return tf = C.fn_return f.
+Proof.
+  intros. unfold transl_function in H.
+  destruct (transl_stmt (C.fn_body f) initial_generator); inv H.
+  auto.
+Qed.
+
+Lemma type_of_global_preserved:
+  forall b ty,
+  Csem.type_of_global ge b = Some ty ->
+  type_of_global tge b = Some ty.
+Proof.
+  intros until ty. unfold Csem.type_of_global, type_of_global.
+  rewrite varinfo_preserved. destruct (Genv.find_var_info ge b). auto. 
+  case_eq (Genv.find_funct_ptr ge b); intros. 
+  inv H0. exploit function_ptr_translated; eauto. intros [tf [A B]]. 
+  rewrite A. decEq. apply type_of_fundef_preserved; auto.
+  congruence.
+Qed.
+
+(** Translation of simple expressions. *)
+
+Lemma tr_simple_nil:
+  (forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
+   dst = For_val \/ dst = For_effects -> simple r -> sl = nil)
+/\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
+   simplelist rl -> sl = nil).
+Proof.
+  assert (A: forall dst a, dst = For_val \/ dst = For_effects -> final dst a = nil).
+    intros. destruct H; subst dst; auto.
+  apply tr_expr_exprlist; intros; simpl in *; try contradiction; auto.
+  rewrite H0; auto. simpl; auto.
+  rewrite H0; auto. simpl; auto.
+  destruct H1; congruence.
+  rewrite H0; auto. simpl; auto.
+  rewrite H0; auto. simpl; auto.
+  rewrite H0; auto. simpl; auto.
+  destruct H7. rewrite H0; auto. rewrite H2; auto. simpl; auto.
+  rewrite H0; auto. simpl; auto.
+  destruct H6. rewrite H0; auto.
+Qed.
+
+Lemma tr_simple_expr_nil:
+  forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
+  dst = For_val \/ dst = For_effects -> simple r -> sl = nil.
+Proof (proj1 tr_simple_nil).
+
+Lemma tr_simple_exprlist_nil:
+  forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
+  simplelist rl -> sl = nil.
+Proof (proj2 tr_simple_nil).
+
+(** Evaluation of simple expressions and of their translation *)
+
+Lemma tr_simple:
+ forall e m,
+ (forall r v,
+  eval_simple_rvalue ge e m r v ->
+  forall le dst sl a tmps,
+  tr_expr le dst r sl a tmps ->
+  match dst with
+  | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v
+  | For_effects => sl = nil
+  | For_test s1 s2 =>
+      exists b, sl = makeif b s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v
+  end)
+/\
+ (forall l b ofs,
+  eval_simple_lvalue ge e m l b ofs ->
+  forall le sl a tmps,
+  tr_expr le For_val l sl a tmps ->
+  sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs).
+Proof.
+Opaque makeif.
+  intros e m.
+  apply (eval_simple_rvalue_lvalue_ind ge e m); intros until tmps; intros TR; inv TR.
+(* value *)
+  auto.
+  auto.
+  exists a0; auto.
+(* rvalof *)
+  exploit H0; eauto. intros [A [B C]].
+  subst sl1; simpl.
+  assert (eval_expr tge e le m a v). eapply eval_Elvalue. eauto. congruence.
+  destruct dst; auto.
+  econstructor. split. simpl; eauto. auto. 
+(* addrof *)
+  exploit H0; eauto. intros [A [B C]].
+  subst sl1; simpl.
+  assert (eval_expr tge e le m (Eaddrof a1 ty) (Vptr b ofs)). econstructor; eauto.
+  destruct dst; auto. simpl; econstructor; eauto. 
+(* unop *)
+  exploit H0; eauto. intros [A [B C]].
+  subst sl1; simpl.
+  assert (eval_expr tge e le m (Eunop op a1 ty) v). econstructor; eauto. congruence.
+  destruct dst; auto. simpl; econstructor; eauto.
+(* binop *)
+  exploit H0; eauto. intros [A [B C]].
+  exploit H2; eauto. intros [D [E F]].
+  subst sl1 sl2; simpl.
+  assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. congruence.
+  destruct dst; auto. simpl; econstructor; eauto.
+(* cast *)
+  exploit H0; eauto. intros [A [B C]].
+  subst sl1; simpl.
+  assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence.
+  destruct dst; auto. simpl; econstructor; eauto.
+(* sizeof *)
+  destruct dst.
+  split; auto. split; auto. constructor.
+  auto.
+  exists (Esizeof ty1 ty). split. auto. split. auto. constructor.
+(* var local *)
+  split; auto. split; auto. apply eval_Evar_local; auto. 
+(* var global *)
+  split; auto. split; auto. apply eval_Evar_global; auto.
+    rewrite symbols_preserved; auto.
+    eapply type_of_global_preserved; eauto. 
+(* deref *)
+  exploit H0; eauto. intros [A [B C]]. subst sl1.
+  split; auto. split; auto. constructor; auto.
+(* field struct *)
+  exploit H0; eauto. intros [A [B C]]. subst sl1.
+  split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto.
+(* field union *)
+  exploit H0; eauto. intros [A [B C]]. subst sl1.
+  split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto.
+Qed.
+
+Lemma tr_simple_rvalue:
+  forall e m r v,
+  eval_simple_rvalue ge e m r v ->
+  forall le dst sl a tmps,
+  tr_expr le dst r sl a tmps ->
+  match dst with
+  | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v
+  | For_effects => sl = nil
+  | For_test s1 s2 =>
+      exists b, sl = makeif b s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v
+  end.
+Proof.
+  intros e m. exact (proj1 (tr_simple e m)).
+Qed.
+
+Lemma tr_simple_lvalue: 
+  forall e m l b ofs,
+  eval_simple_lvalue ge e m l b ofs ->
+  forall le sl a tmps,
+  tr_expr le For_val l sl a tmps ->
+  sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs.
+Proof.
+  intros e m. exact (proj2 (tr_simple e m)).
+Qed.
+
+Lemma tr_simple_exprlist:
+  forall le rl sl al tmps,
+  tr_exprlist le rl sl al tmps ->
+  forall e m tyl vl,
+  eval_simple_list ge e m rl tyl vl ->
+  sl = nil /\ eval_exprlist tge e le m al tyl vl.
+Proof.
+  induction 1; intros. 
+  inv H. split. auto. constructor.
+  inv H4.
+  exploit tr_simple_rvalue; eauto. intros [A [B C]].
+  exploit IHtr_exprlist; eauto. intros [D E].
+  split. subst; auto. econstructor; eauto. congruence.
+Qed.
+
+(** Commutation between the translation of expressions and left contexts. *)
+
+Lemma typeof_context:
+  forall k1 k2 C, leftcontext k1 k2 C ->
+  forall e1 e2, C.typeof e1 = C.typeof e2 ->
+  C.typeof (C e1) = C.typeof (C e2).
+Proof.
+  induction 1; intros; auto. 
+Qed.
+
+Inductive compat_dest: (C.expr -> C.expr) -> purpose -> purpose -> list statement -> Prop :=
+  | compat_dest_base: forall dst,
+      compat_dest (fun x => x) dst dst nil
+  | compat_dest_val: forall C dst sl,
+      compat_dest C For_val dst sl
+  | compat_dest_effects: forall C dst sl,
+      compat_dest C For_effects dst sl
+  | compat_dest_paren: forall C ty dst' dst sl,
+      compat_dest C dst' dst sl ->
+      compat_dest (fun x => C.Eparen (C x) ty) dst' dst sl.
+
+Lemma compat_dest_not_test:
+  forall  C dst' dst sl,
+  compat_dest C dst' dst sl ->
+  dst = For_val \/ dst = For_effects ->
+  dst' = For_val \/ dst' = For_effects.
+Proof.
+  induction 1; intros; auto.
+Qed.
+
+Lemma compat_dest_change:
+  forall C1 dst' dst1 sl1 C2 dst2 sl2,
+  compat_dest C1 dst' dst1 sl1 ->
+  dst1 = For_val \/ dst1 = For_effects ->
+  compat_dest C2 dst' dst2 sl2.
+Proof.
+  intros. exploit compat_dest_not_test; eauto. intros [A | A]; subst dst'; constructor.
+Qed.
+
+Scheme leftcontext_ind2 := Minimality for leftcontext Sort Prop
+  with leftcontextlist_ind2 := Minimality for leftcontextlist Sort Prop.
+Combined Scheme leftcontext_leftcontextlist_ind from leftcontext_ind2, leftcontextlist_ind2.
+
+Lemma tr_expr_leftcontext_rec:
+ (
+  forall from to C, leftcontext from to C ->
+  forall le e dst sl a tmps,
+  tr_expr le dst (C e) sl a tmps ->
+  exists dst', exists sl1, exists sl2, exists a', exists tmp',
+  tr_expr le dst' e sl1 a' tmp'
+  /\ sl = sl1 ++ sl2
+  /\ compat_dest C dst' dst sl2
+  /\ incl tmp' tmps
+  /\ (forall le' e' sl3,
+        tr_expr le' dst' e' sl3 a' tmp' ->
+        (forall id, ~In id tmp' -> le'!id = le!id) ->
+        C.typeof e' = C.typeof e ->
+        tr_expr le' dst (C e') (sl3 ++ sl2) a tmps)
+ ) /\ (
+  forall from C, leftcontextlist from C ->
+  forall le e sl a tmps,
+  tr_exprlist le (C e) sl a tmps ->
+  exists dst', exists sl1, exists sl2, exists a', exists tmp',
+  tr_expr le dst' e sl1 a' tmp'
+  /\ sl = sl1 ++ sl2
+  /\ match dst' with For_test _ _ => False | _ => True end
+  /\ incl tmp' tmps
+  /\ (forall le' e' sl3,
+        tr_expr le' dst' e' sl3 a' tmp' ->
+        (forall id, ~In id tmp' -> le'!id = le!id) ->
+        C.typeof e' = C.typeof e ->
+        tr_exprlist le' (C e') (sl3 ++ sl2) a tmps)
+).
+Proof.
+
+Ltac TR :=
+  econstructor; econstructor; econstructor; econstructor; econstructor;
+  split; [eauto | split; [idtac | split; [eauto | split]]].
+
+Ltac NOTIN :=
+  match goal with
+  | [ H1: In ?x ?l, H2: list_disjoint ?l _ |- ~In ?x _ ] =>
+        red; intro; elim (H2 x x); auto
+  | [ H1: In ?x ?l, H2: list_disjoint _ ?l |- ~In ?x _ ] =>
+        red; intro; elim (H2 x x); auto
+  end.
+
+Ltac UNCHANGED :=
+  match goal with
+  | [ H: (forall (id: ident), ~In id _ -> ?le' ! id = ?le ! id) |-
+         (forall (id: ident), In id _ -> ?le' ! id = ?le ! id) ] =>
+      intros; apply H; NOTIN
+  end.
+
+  generalize compat_dest_change; intro CDC.
+  apply leftcontext_leftcontextlist_ind; intros.
+
+(* base *)
+  TR. rewrite <- app_nil_end; auto. constructor. red; auto.
+  intros. rewrite <- app_nil_end; auto. 
+(* deref *)
+  inv H1. 
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1; rewrite app_ass; eauto. auto. 
+  intros. rewrite <- app_ass. econstructor; eauto. 
+(* field *)
+  inv H1.
+  exploit H0. eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1; rewrite app_ass; eauto. auto. 
+  intros. rewrite <- app_ass. econstructor; eauto.
+(* rvalof *)
+  inv H1.
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1; rewrite app_ass; eauto. auto. 
+  intros. rewrite <- app_ass; econstructor; eauto.
+(* addrof *)
+  inv H1. 
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1; rewrite app_ass; eauto. auto. 
+  intros. rewrite <- app_ass. econstructor; eauto.
+(* unop *) 
+  inv H1. 
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1; rewrite app_ass; eauto. auto. 
+  intros. rewrite <- app_ass. econstructor; eauto. 
+(* binop left *)
+  inv H1.
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor; eauto.
+  eapply tr_expr_invariant; eauto. UNCHANGED. 
+(* binop right *)
+  inv H2. 
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl2. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor; eauto.
+  eapply tr_expr_invariant; eauto. UNCHANGED. 
+(* cast *)
+  inv H1.
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1; rewrite app_ass; eauto. auto. 
+  intros. rewrite <- app_ass. econstructor; eauto.
+(* condition *)
+  inv H1.
+  (* for val *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. 
+  rewrite Q. rewrite app_ass. eauto. 
+  red; auto.
+  intros. rewrite <- app_ass. econstructor. apply S; auto. 
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto. auto. auto. auto. auto. 
+  (* for effects *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. 
+  rewrite Q. rewrite app_ass. eauto. 
+  red; auto.
+  intros. rewrite <- app_ass. econstructor. auto. apply S; auto. 
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto. auto. auto.
+(* assign left *)
+  inv H1.
+  (* for effects *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto.
+  (* for val *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto. auto. auto. auto.
+  eapply typeof_context; eauto.
+  auto. 
+(* assign right *)
+  inv H2. 
+  (* for effects *)
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl2. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ (sl3 ++ sl2')). rewrite app_ass. 
+  econstructor. 
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto. auto. auto. auto.
+  (* for val *)
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl2. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ (sl3 ++ sl2')). rewrite app_ass. 
+  econstructor. 
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto. auto. auto. auto. auto. auto. auto. auto. 
+  eapply typeof_context; eauto.
+(* assignop left *)
+  inv H1.
+  (* for effects *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto.
+  (* for val *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto. auto. auto. auto.
+  eapply typeof_context; eauto.
+(* assignop right *)
+  inv H2.
+  (* for effects *)
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl2. rewrite app_ass. eauto. 
+  red; auto.
+  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. 
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto. auto. auto. auto.
+  (* for val *)
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl.
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl2. rewrite app_ass. eauto. 
+  red; auto. 
+  intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. 
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto. auto. auto. auto. auto. auto. auto. auto. 
+(* postincr *)
+  inv H1.
+  (* for effects *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
+  intros. replace (C.typeof (C e)) with (C.typeof (C e')). rewrite <- app_ass.
+  econstructor; eauto. 
+  eapply typeof_context; eauto.
+  (* for val *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
+  intros. rewrite <- app_ass. econstructor; eauto. 
+  eapply typeof_context; eauto.
+(* call left *)
+  inv H1.
+  (* for effects *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_exprlist_invariant; eauto. UNCHANGED.
+  auto. auto. auto.
+  (* for val *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
+  intros. rewrite <- app_ass. econstructor. auto. apply S; auto.
+  eapply tr_exprlist_invariant; eauto. UNCHANGED.
+  auto. auto. auto. auto. 
+(* call right *)
+  inv H2.
+  (* for effects *)
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. 
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. destruct dst'; contradiction || constructor.
+  red; auto. 
+  intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto. auto. auto. auto.
+  (* for val *)
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. 
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. destruct dst'; contradiction || constructor.
+  red; auto. 
+  intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor.
+  auto. eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto.
+  auto. auto. auto. auto.
+(* comma *)
+  inv H1.
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q; rewrite app_ass; eauto. red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  auto. auto. auto.
+(* paren *)
+  inv H1. 
+  (* for val *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q. rewrite app_ass. eauto. red; auto. 
+  intros. rewrite <- app_ass. econstructor; eauto. 
+  (* for effects *)
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. rewrite Q. eauto. constructor; auto. auto.
+  intros. econstructor; eauto.
+(* cons left *)
+  inv H1.
+  exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl1. rewrite app_ass. eauto. 
+  exploit compat_dest_not_test; eauto. intros [A|A]; subst dst'; auto.
+  red; auto. 
+  intros. rewrite <- app_ass. econstructor. apply S; auto.
+  eapply tr_exprlist_invariant; eauto.  UNCHANGED.
+  auto. auto. auto.
+(* cons right *)
+  inv H2.
+  assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. 
+  exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  TR. subst sl2. eauto. 
+  red; auto. 
+  intros. change sl3 with (nil ++ sl3). rewrite app_ass. econstructor.
+  eapply tr_expr_invariant; eauto. UNCHANGED.
+  apply S; auto.
+  auto. auto. auto.
+Qed.
+
+Theorem tr_expr_leftcontext:
+  forall C le r dst sl a tmps,
+  leftcontext RV RV C ->
+  tr_expr le dst (C r) sl a tmps ->
+  exists dst', exists sl1, exists sl2, exists a', exists tmp',
+  tr_expr le dst' r sl1 a' tmp'
+  /\ sl = sl1 ++ sl2
+  /\ compat_dest C dst' dst sl2
+  /\ incl tmp' tmps
+  /\ (forall le' r' sl3,
+        tr_expr le' dst' r' sl3 a' tmp' ->
+        (forall id, ~In id tmp' -> le'!id = le!id) ->
+        C.typeof r' = C.typeof r ->
+        tr_expr le' dst (C r') (sl3 ++ sl2) a tmps).
+Proof.
+  intros. eapply (proj1 tr_expr_leftcontext_rec); eauto.
+Qed.
+
+Theorem tr_top_leftcontext:
+  forall e le m dst rtop sl a tmps,
+  tr_top tge e le m dst rtop sl a tmps ->
+  forall r C,
+  rtop = C r ->
+  leftcontext RV RV C ->
+  exists dst', exists sl1, exists sl2, exists a', exists tmp',
+  tr_top tge e le m dst' r sl1 a' tmp'
+  /\ sl = sl1 ++ sl2
+  /\ compat_dest C dst' dst sl2
+  /\ incl tmp' tmps
+  /\ (forall le' m' r' sl3,
+        tr_expr le' dst' r' sl3 a' tmp' ->
+        (forall id, ~In id tmp' -> le'!id = le!id) ->
+        C.typeof r' = C.typeof r ->
+        tr_top tge e le' m' dst (C r') (sl3 ++ sl2) a tmps).
+Proof.
+  induction 1; intros.
+(* val for val *)
+  inv H2; inv H1.
+  exists For_val; econstructor; econstructor; econstructor; econstructor.
+  split. apply tr_top_val_val; eauto.
+  split. instantiate (1 := nil); auto.
+  split. constructor.
+  split. apply incl_refl.
+  intros. rewrite <- app_nil_end. constructor; auto.
+(* val for test *)
+  inv H2; inv H1.
+  exists (For_test s1 s2); econstructor; econstructor; econstructor; econstructor.
+  split. apply tr_top_val_test; eauto.
+  split. instantiate (1 := nil); auto.
+  split. constructor.
+  split. apply incl_refl.
+  intros. rewrite <- app_nil_end. constructor; eauto.
+(* base *)
+  subst r. exploit tr_expr_leftcontext; eauto.
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R [S T]]]]]]]]].
+  exists dst'; exists sl1; exists sl2; exists a'; exists tmp'.
+  split. apply tr_top_base; auto.
+  split. auto. split. auto. split. auto.
+  intros. apply tr_top_base. apply T; auto. 
+(* paren *)
+  inv H1; inv H0.
+  (* at top *)
+  exists (For_test s1 s2); econstructor; econstructor; econstructor; econstructor.
+  split. apply tr_top_paren_test; eauto.
+  split. instantiate (1 := nil). rewrite <- app_nil_end; auto.
+  split. constructor.
+  split. apply incl_refl.
+  intros. rewrite <- app_nil_end. constructor; eauto.
+  (* below *)
+  exploit (IHtr_top r0 C0); auto. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  exists dst'; exists sl1; exists sl2; exists a'; exists tmp'.
+  split. auto.
+  split. auto.
+  split. constructor; auto.
+  split. auto.
+  intros. apply tr_top_paren_test. apply S; auto.
+Qed.
+
+Theorem tr_top_testcontext:
+  forall C s1 s2 dst sl2 r sl1 a tmps e le m,
+  compat_dest C (For_test s1 s2) dst sl2 ->
+  tr_top tge e le m (For_test s1 s2) r sl1 a tmps ->
+  dst = For_test s1 s2 /\ tr_top tge e le m dst (C r) (sl1 ++ sl2) a tmps.
+Proof.
+  intros. dependent induction H.
+  split. auto. rewrite <- app_nil_end. auto.
+  exploit IHcompat_dest; eauto. intros [A B].
+  split. auto. subst dst. apply tr_top_paren_test. auto. 
+Qed.
+
+(** Semantics of smart constructors *)
+
+Lemma step_makeif_true:
+  forall f a s1 s2 k e le m v1,
+  eval_expr tge e le m a v1 ->
+  is_true v1 (typeof a) ->
+  star step tge (State f (makeif a s1 s2) k e le m)
+             E0 (State f s1 k e le m).
+Proof.
+  intros. functional induction (makeif a s1 s2).
+  inversion H. subst v1. inversion H0. congruence. congruence.
+  inversion H1.
+  apply star_refl.
+  apply star_one. apply step_ifthenelse_true with v1; auto. 
+Qed.
+
+Lemma step_makeif_false:
+  forall f a s1 s2 k e le m v1,
+  eval_expr tge e le m a v1 ->
+  is_false v1 (typeof a) ->
+  star step tge (State f (makeif a s1 s2) k e le m)
+             E0 (State f s2 k e le m).
+Proof.
+  intros. functional induction (makeif a s1 s2).
+  apply star_refl.
+  inversion H. subst v1. inversion H0. congruence. congruence.
+  inversion H1.
+  apply star_one. apply step_ifthenelse_false with v1; auto. 
+Qed.
+
+(** Matching between continuations *)
+
+Fixpoint Kseqlist (sl: list statement) (k: cont) :=
+  match sl with
+  | nil => k
+  | s :: l => Kseq s (Kseqlist l k)
+  end.
+
+Remark Kseqlist_app:
+  forall sl1 sl2 k,
+  Kseqlist (sl1 ++ sl2) k = Kseqlist sl1 (Kseqlist sl2 k).
+Proof.
+  induction sl1; simpl; congruence.
+Qed.
+
+Inductive match_cont : Csem.cont -> cont -> Prop :=
+  | match_Kstop:
+      match_cont Csem.Kstop Kstop
+  | match_Kseq: forall s k ts tk,
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont (Csem.Kseq s k) (Kseq ts tk)
+  | match_Kwhile2: forall r s k s' ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont (Csem.Kwhile2 r s k)
+                 (Kwhile expr_true (Ssequence s' ts) tk)
+  | match_Kdowhile1: forall r s k s' ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont (Csem.Kdowhile1 r s k)
+                 (Kfor2 expr_true s' ts tk)
+  | match_Kfor3: forall r s3 s k ts3 s' ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s3 ts3 ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont (Csem.Kfor3 r s3 s k)
+                 (Kfor2 expr_true ts3 (Ssequence s' ts) tk)
+  | match_Kfor4: forall r s3 s k ts3 s' ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s3 ts3 ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont (Csem.Kfor4 r s3 s k)
+                 (Kfor3 expr_true ts3 (Ssequence s' ts) tk)
+  | match_Kswitch2: forall k tk,
+      match_cont k tk ->
+      match_cont (Csem.Kswitch2 k) (Kswitch tk)
+  | match_Kcall_none: forall f e C ty k tf le sl tk a dest tmps,
+      transl_function f = Errors.OK tf ->
+      leftcontext RV RV C ->
+      (forall v m, tr_top tge e le m dest (C (C.Eval v ty)) sl a tmps) ->
+      match_cont_exp dest a k tk ->
+      match_cont (Csem.Kcall f e C ty k)
+                 (Kcall None tf e le (Kseqlist sl tk))
+  | match_Kcall_some: forall f e C ty k dst tf le sl tk a dest tmps,
+      transl_function f = Errors.OK tf ->
+      leftcontext RV RV C ->
+      (forall v m, tr_top tge e (PTree.set dst v le) m dest (C (C.Eval v ty)) sl a tmps) ->
+      match_cont_exp dest a k tk ->
+      match_cont (Csem.Kcall f e C ty k)
+                 (Kcall (Some dst) tf e le (Kseqlist sl tk))
+
+with match_cont_exp : purpose -> expr -> Csem.cont -> cont -> Prop :=
+  | match_Kdo: forall k a tk,
+      match_cont k tk ->
+      match_cont_exp For_effects a (Csem.Kdo k) tk
+  | match_Kifthenelse_1: forall a s1 s2 k ts1 ts2 tk,
+      tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
+      match_cont k tk ->
+      match_cont_exp For_val a (Csem.Kifthenelse s1 s2 k) (Kseq (Sifthenelse a ts1 ts2) tk)
+  | match_Kifthenelse_2: forall a s1 s2 k ts1 ts2 tk,
+      tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
+      match_cont k tk ->
+      match_cont_exp (For_test ts1 ts2) a (Csem.Kifthenelse s1 s2 k) tk
+  | match_Kwhile1: forall r s k s' a ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont_exp (For_test Sskip Sbreak) a
+         (Csem.Kwhile1 r s k)
+         (Kseq ts (Kwhile expr_true (Ssequence s' ts) tk))
+  | match_Kdowhile2: forall r s k s' a ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont_exp (For_test Sskip Sbreak) a
+        (Csem.Kdowhile2 r s k)
+        (Kfor3 expr_true s' ts tk)
+  | match_Kfor2: forall r s3 s k s' a ts3 ts tk,
+      tr_if r Sskip Sbreak s' ->
+      tr_stmt s3 ts3 ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_cont_exp (For_test Sskip Sbreak) a
+        (Csem.Kfor2 r s3 s k)
+        (Kseq ts (Kfor2 expr_true ts3 (Ssequence s' ts) tk))
+  | match_Kswitch1: forall ls k a tls tk,
+      tr_lblstmts ls tls ->
+      match_cont k tk ->
+      match_cont_exp For_val a (Csem.Kswitch1 ls k) (Kseq (Sswitch a tls) tk)
+  | match_Kreturn: forall k a tk,
+      match_cont k tk ->
+      match_cont_exp For_val a (Csem.Kreturn k) (Kseq (Sreturn (Some a)) tk).
+
+Lemma match_cont_call:
+  forall k tk,
+  match_cont k tk ->
+  match_cont (Csem.call_cont k) (call_cont tk).
+Proof.
+  induction 1; simpl; auto. constructor. econstructor; eauto. econstructor; eauto.
+Qed.
+
+Lemma match_cont_exp_for_test_inv:
+  forall s1 s2 a a' k tk,
+  match_cont_exp (For_test s1 s2) a k tk ->
+  match_cont_exp (For_test s1 s2) a' k tk.
+Proof.
+  intros. inv H; econstructor; eauto.
+Qed.
+
+(** Matching between states *)
+
+Inductive match_states: Csem.state -> state -> Prop :=
+  | match_exprstates: forall f r k e m tf sl tk le dest a tmps,
+      transl_function f = Errors.OK tf ->
+      tr_top tge e le m dest r sl a tmps ->
+      match_cont_exp dest a k tk ->
+      match_states (Csem.ExprState f r k e m)
+                   (State tf Sskip (Kseqlist sl tk) e le m)
+  | match_regularstates: forall f s k e m tf ts tk le,
+      transl_function f = Errors.OK tf ->
+      tr_stmt s ts ->
+      match_cont k tk ->
+      match_states (Csem.State f s k e m)
+                   (State tf ts tk e le m)
+  | match_callstates: forall fd args k m tfd tk,
+      transl_fundef fd = Errors.OK tfd ->
+      match_cont k tk ->
+      match_states (Csem.Callstate fd args k m)
+                   (Callstate tfd args tk m)
+  | match_returnstates: forall res k m tk,
+      match_cont k tk ->
+      match_states (Csem.Returnstate res k m)
+                   (Returnstate res tk m).
+
+Lemma push_seq:
+  forall f sl k e le m,
+  star step tge (State f (makeseq sl) k e le m)
+             E0 (State f Sskip (Kseqlist sl k) e le m).
+Proof.
+  intros. unfold makeseq. generalize Sskip. revert sl k. 
+  induction sl; simpl; intros.
+  apply star_refl.
+  eapply star_right. apply IHsl. constructor. traceEq.
+Qed.
+
+(** Additional results on translation of statements *)
+
+Lemma tr_select_switch:
+  forall n ls tls,
+  tr_lblstmts ls tls ->
+  tr_lblstmts (Csem.select_switch n ls) (select_switch n tls).
+Proof.
+  induction 1; simpl.
+  constructor; auto.
+  destruct (Int.eq n0 n). constructor; auto. auto.
+Qed.
+
+Lemma tr_seq_of_labeled_statement:
+  forall ls tls,
+  tr_lblstmts ls tls ->
+  tr_stmt (Csem.seq_of_labeled_statement ls) (seq_of_labeled_statement tls).
+Proof.
+  induction 1; simpl. auto. constructor; auto.
+Qed.
+
+(** Commutation between translation and the "find label" operation. *)
+
+Section FIND_LABEL.
+
+Variable lbl: label.
+
+Definition nolabel (s: statement) : Prop :=
+  forall k, find_label lbl s k = None.
+
+Fixpoint nolabel_list (sl: list statement) : Prop :=
+  match sl with
+  | nil => True
+  | s1 :: sl' => nolabel s1 /\ nolabel_list sl'
+  end.
+
+Lemma nolabel_list_app:
+  forall sl2 sl1, nolabel_list sl1 -> nolabel_list sl2 -> nolabel_list (sl1 ++ sl2).
+Proof.
+  induction sl1; simpl; intros. auto. tauto. 
+Qed.
+
+Lemma makeseq_nolabel:
+  forall sl, nolabel_list sl -> nolabel (makeseq sl).
+Proof.
+  assert (forall sl s, nolabel s -> nolabel_list sl -> nolabel (makeseq_rec s sl)).
+  induction sl; simpl; intros. auto. destruct H0. apply IHsl; auto. 
+  red. intros; simpl. rewrite H. apply H0.
+  intros. unfold makeseq. apply H; auto. red. auto. 
+Qed.
+
+Lemma small_stmt_nolabel:
+  forall s, small_stmt s = true -> nolabel s.
+Proof.
+  induction s; simpl; intros; congruence || (red; auto).
+  destruct (andb_prop _ _ H). intros; simpl. rewrite IHs1; auto. apply IHs2; auto. 
+Qed.
+
+Lemma makeif_nolabel:
+  forall a s1 s2, nolabel s1 -> nolabel s2 -> nolabel (makeif a s1 s2).
+Proof.
+  intros. functional induction (makeif a s1 s2); auto. 
+  red; simpl; intros. rewrite H; auto.
+Qed.
+
+Definition nolabel_dest (dst: purpose) : Prop :=
+  match dst with
+  | For_val => True
+  | For_effects => True
+  | For_test s1 s2 => nolabel s1 /\ nolabel s2
+  end.
+
+Lemma nolabel_final:
+  forall dst a, nolabel_dest dst -> nolabel_list (final dst a).
+Proof.
+  destruct dst; simpl; intros. auto. auto. 
+  split; auto. destruct H. apply makeif_nolabel; auto.
+Qed. 
+
+Ltac NoLabelTac :=
+  match goal with
+  | [ |- nolabel_list nil ] => exact I
+  | [ |- nolabel_list (final _ _) ] => apply nolabel_final; NoLabelTac
+  | [ |- nolabel_list (_ :: _) ] => simpl; split; NoLabelTac
+  | [ |- nolabel_list (_ ++ _) ] => apply nolabel_list_app; NoLabelTac
+  | [ |- nolabel_dest For_val ] => exact I
+  | [ |- nolabel_dest For_effects ] => exact I
+  | [ H: _ -> nolabel_list ?x |- nolabel_list ?x ] => apply H; NoLabelTac
+  | [ |- nolabel _ ] => red; intros; simpl; auto
+  | [ |- _ /\ _ ] => split; NoLabelTac
+  | _ => auto
+  end.
+
+Lemma tr_find_label_expr:
+  (forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> nolabel_dest dst -> nolabel_list sl)
+/\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> nolabel_list sl).
+Proof.
+  apply tr_expr_exprlist; intros; NoLabelTac.
+  destruct H1. apply makeif_nolabel; auto. 
+  apply makeif_nolabel; NoLabelTac.
+  rewrite (makeseq_nolabel sl2); auto.
+  rewrite (makeseq_nolabel sl3); auto.
+  apply makeif_nolabel; NoLabelTac.
+  rewrite (makeseq_nolabel sl2); auto.
+  rewrite (makeseq_nolabel sl3); auto.
+Qed.
+
+Lemma tr_find_label_top:
+  forall e le m dst r sl a tmps,
+  tr_top tge e le m dst r sl a tmps -> nolabel_dest dst -> nolabel_list sl.
+Proof.
+  induction 1; intros; NoLabelTac.
+  destruct H1. apply makeif_nolabel; auto. 
+  eapply (proj1 tr_find_label_expr); eauto.
+Qed.
+
+Lemma tr_find_label_expression:
+  forall r s a, tr_expression r s a -> forall k, find_label lbl s k = None.
+Proof.
+  intros. inv H.
+  assert (nolabel (makeseq sl)). apply makeseq_nolabel.
+  eapply tr_find_label_top with (e := empty_env) (le := PTree.empty val) (m := Mem.empty).
+  eauto. exact I. 
+  apply H.
+Qed.
+
+Lemma tr_find_label_expr_stmt:
+  forall r s, tr_expr_stmt r s -> forall k, find_label lbl s k = None.
+Proof.
+  intros. inv H.
+  assert (nolabel (makeseq sl)). apply makeseq_nolabel.
+  eapply tr_find_label_top with (e := empty_env) (le := PTree.empty val) (m := Mem.empty).
+  eauto. exact I. 
+  apply H.
+Qed.
+
+Lemma tr_find_label_if:
+  forall r s1 s2 s,
+  tr_if r s1 s2 s ->
+  small_stmt s1 = true -> small_stmt s2 = true ->
+  forall k, find_label lbl s k = None.
+Proof.
+  intros. inv H. 
+  assert (nolabel (makeseq sl)). apply makeseq_nolabel.
+  eapply tr_find_label_top with (e := empty_env) (le := PTree.empty val) (m := Mem.empty).
+  eauto. split; apply small_stmt_nolabel; auto.
+  apply H.
+Qed.
+
+Lemma tr_find_label:
+  forall s k ts tk
+    (TR: tr_stmt s ts)
+    (MC: match_cont k tk),
+  match Csem.find_label lbl s k with
+  | None =>
+      find_label lbl ts tk = None
+  | Some (s', k') =>
+      exists ts', exists tk',
+          find_label lbl ts tk = Some (ts', tk')
+       /\ tr_stmt s' ts'
+       /\ match_cont k' tk'
+  end
+with tr_find_label_ls:
+  forall s k ts tk
+    (TR: tr_lblstmts s ts)
+    (MC: match_cont k tk),
+  match Csem.find_label_ls lbl s k with
+  | None =>
+      find_label_ls lbl ts tk = None
+  | Some (s', k') =>
+      exists ts', exists tk',
+          find_label_ls lbl ts tk = Some (ts', tk')
+       /\ tr_stmt s' ts'
+       /\ match_cont k' tk'
+  end.
+Proof.
+  induction s; intros; inversion TR; subst; clear TR; simpl.
+  auto.
+  eapply tr_find_label_expr_stmt; eauto.
+(* seq *)
+  exploit (IHs1 (Csem.Kseq s2 k)); eauto. constructor; eauto.
+  destruct (Csem.find_label lbl s1 (Csem.Kseq s2 k)) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; auto.
+  intro EQ. rewrite EQ. eapply IHs2; eauto. 
+(* if no-opt *)
+  rename s' into sr. 
+  rewrite (tr_find_label_expression _ _ _ H2).
+  exploit (IHs1 k); eauto.
+  destruct (Csem.find_label lbl s1 k) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition.
+  intro EQ. rewrite EQ. eapply IHs2; eauto.
+(* if opt *)
+  rewrite (tr_find_label_if _ _ _ _ H7); auto.
+  exploit (IHs1 k); eauto.
+  destruct (Csem.find_label lbl s1 k) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. 
+  exploit small_stmt_nolabel. eexact H4. instantiate (1 := tk). congruence.
+  intros.
+  exploit (IHs2 k); eauto.
+  destruct (Csem.find_label lbl s2 k) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. 
+  exploit small_stmt_nolabel. eexact H6. instantiate (1 := tk). congruence.
+  auto.
+(* while *)
+  rename s' into sr. 
+  rewrite (tr_find_label_if _ _ _ _ H1); auto.
+  eapply IHs; eauto. econstructor; eauto.
+(* dowhile *)
+  rename s' into sr.
+  rewrite (tr_find_label_if _ _ _ _ H1); auto.
+  exploit (IHs (Kdowhile1 e s k)); eauto. econstructor; eauto.
+  destruct (Csem.find_label lbl s (Kdowhile1 e s k)) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition.
+  intro EQ. rewrite EQ. auto. 
+(* for skip *)
+  rename s' into sr.
+  rewrite (tr_find_label_if _ _ _ _ H4); auto.
+  exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto.
+  destruct (Csem.find_label lbl s3 (Csem.Kfor3 e s2 s3 k)) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition.
+  intro EQ. rewrite EQ.
+  exploit (IHs2 (Csem.Kfor4 e s2 s3 k)); eauto. econstructor; eauto.
+(* for not skip *)
+  rename s' into sr.
+  rewrite (tr_find_label_if _ _ _ _ H3); auto.
+  exploit (IHs1 (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)); eauto. 
+    econstructor; eauto. econstructor; eauto. 
+  destruct (Csem.find_label lbl s1
+               (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition.
+  intro EQ; rewrite EQ.
+  exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto.
+  destruct (Csem.find_label lbl s3 (Csem.Kfor3 e s2 s3 k)) as [[s'' k''] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition.
+  intro EQ'. rewrite EQ'. 
+  exploit (IHs2 (Csem.Kfor4 e s2 s3 k)); eauto. econstructor; eauto.
+(* break, continue, return 0 *)
+  auto. auto. auto.
+(* return 1 *)
+  rewrite (tr_find_label_expression _ _ _ H0). auto.
+(* switch *)
+  rewrite (tr_find_label_expression _ _ _ H1). apply tr_find_label_ls. auto. constructor; auto.
+(* labeled stmt *)
+  destruct (ident_eq lbl l). exists ts0; exists tk; auto. apply IHs; auto. 
+(* goto *)
+  auto.
+
+  induction s; intros; inversion TR; subst; clear TR; simpl.
+(* default *)
+  apply tr_find_label; auto. 
+(* case *)
+  exploit (tr_find_label s (Csem.Kseq (Csem.seq_of_labeled_statement s0) k)); eauto.
+  econstructor; eauto. apply tr_seq_of_labeled_statement; eauto.
+  destruct (Csem.find_label lbl s
+    (Csem.Kseq (Csem.seq_of_labeled_statement s0) k)) as [[s' k'] | ].
+  intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; auto.
+  intro EQ. rewrite EQ. eapply IHs; eauto.
+Qed.
+ 
+End FIND_LABEL.
+
+(** Anti-stuttering measure *)
+
+(** There are some stuttering steps in the translation:
+- The execution of [Sdo a] where [a] is side-effect free,
+  which is three transitions in the source:
+<<
+    Sdo a, k  --->  a, Kdo k ---> rval v, Kdo k ---> Sskip, k
+>>
+  but the translation, which is [Sskip], makes no transitions.
+- The reduction [C.Ecomma (C.Eval v) r2 --> r2].
+- The reduction [C.Eparen (C.Eval v) --> C.Eval v] in a [For_effects] context.
+
+The following measure decreases for these stuttering steps. *)
+
+Fixpoint esize (a: C.expr) : nat :=
+  match a with
+  | C.Eloc _ _ _ => 1%nat
+  | C.Evar _ _ => 1%nat
+  | C.Ederef r1 _ => S(esize r1)
+  | C.Efield l1 _ _ => S(esize l1)
+  | C.Eval _ _ => O
+  | C.Evalof l1 _ => S(esize l1)
+  | C.Eaddrof l1 _ => S(esize l1)
+  | C.Eunop _ r1 _ => S(esize r1)
+  | C.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat
+  | C.Ecast r1 _ => S(esize r1)
+  | C.Econdition r1 _ _ _ => S(esize r1)
+  | C.Esizeof _ _ => 1%nat
+  | C.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat
+  | C.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat
+  | C.Epostincr _ l1 _ => S(esize l1)
+  | C.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat
+  | C.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat
+  | C.Eparen r1 _ => S(esize r1)
+  end
+
+with esizelist (el: C.exprlist) : nat :=
+  match el with
+  | C.Enil => O
+  | C.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat
+  end.
+
+Definition measure (st: Csem.state) : nat :=
+  match st with
+  | Csem.ExprState _ r _ _ _ => (esize r + 1)%nat
+  | Csem.State _ C.Sskip _ _ _ => 0%nat
+  | Csem.State _ (C.Sdo r) _ _ _ => (esize r + 2)%nat
+  | Csem.State _ (C.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat
+  | _ => 0%nat
+  end.
+
+Lemma leftcontext_size:
+  forall from to C,
+  leftcontext from to C ->
+  forall e1 e2,
+  (esize e1 < esize e2)%nat ->
+  (esize (C e1) < esize (C e2))%nat
+with leftcontextlist_size:
+  forall from C,
+  leftcontextlist from C ->
+  forall e1 e2,
+  (esize e1 < esize e2)%nat ->
+  (esizelist (C e1) < esizelist (C e2))%nat.
+Proof.
+  induction 1; intros; simpl; auto with arith. exploit leftcontextlist_size; eauto. auto with arith.
+  induction 1; intros; simpl; auto with arith. exploit leftcontext_size; eauto. auto with arith.
+Qed.
+
+(** Forward simulation for expressions. *)
+
+Lemma tr_val_gen:
+  forall le dst v ty a tmp,
+  typeof a = ty ->
+  (forall tge e le' m,
+      (forall id, In id tmp -> le'!id = le!id) ->
+      eval_expr tge e le' m a v) ->
+  tr_expr le dst (C.Eval v ty) (final dst a) a tmp.
+Proof.
+  intros. destruct dst; simpl; econstructor; auto.
+Qed.
+
+Lemma estep_simulation:
+  forall S1 t S2, Cstrategy.estep ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  exists S2',
+     (plus step tge S1' t S2' \/
+       (star step tge S1' t S2' /\ measure S2 < measure S1)%nat)
+  /\ match_states S2 S2'.
+Proof.
+  induction 1; intros; inv MS.
+(* expr *)
+  assert (tr_expr le dest r sl a tmps).
+    inv H9. contradiction. contradiction. auto. inv H. 
+  econstructor; split.
+  right; split. apply star_refl. destruct r; simpl; (contradiction || omega).
+  econstructor; eauto.
+  instantiate (1 := tmps).
+  exploit tr_simple_rvalue; eauto. destruct dest.
+  intros [A [B C]]. subst sl. apply tr_top_val_val; auto.
+  intros A. subst sl. apply tr_top_base. constructor. 
+  intros [b [A [B C]]]. subst sl. apply tr_top_val_test; auto. 
+(* condition true *)
+  exploit tr_top_leftcontext; eauto. clear H10. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H2. 
+  (* for value *)
+  exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
+  subst sl0; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor.
+  eapply star_trans. apply step_makeif_true with v; auto. congruence.
+  eapply star_left. constructor. apply push_seq. 
+  reflexivity. reflexivity. traceEq.
+  replace (Kseqlist sl3 (Kseq (Sset t a2) (Kseqlist sl2 tk)))
+     with (Kseqlist (sl3 ++ Sset t a2 :: sl2) tk).
+  eapply match_exprstates; eauto. 
+  change (Sset t a2 :: sl2) with ((Sset t a2 :: nil) ++ sl2). rewrite <- app_ass. 
+  apply S. econstructor; eauto.  auto. auto. 
+  rewrite Kseqlist_app. auto. 
+  (* for effects *)
+  exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
+  subst sl0; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor.
+  eapply star_trans. apply step_makeif_true with v; auto. congruence.
+  apply push_seq. 
+  reflexivity. traceEq.
+  rewrite <- Kseqlist_app.
+  econstructor. eauto. apply S.
+    econstructor; eauto. apply tr_expr_monotone with tmp2; eauto. 
+    econstructor; eauto. 
+  auto. auto.
+(* condition false *)
+  exploit tr_top_leftcontext; eauto. clear H10. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H2. 
+  (* for value *)
+  exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
+  subst sl0; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor.
+  eapply star_trans. apply step_makeif_false with v; auto. congruence.
+  eapply star_left. constructor. apply push_seq. 
+  reflexivity. reflexivity. traceEq.
+  replace (Kseqlist sl4 (Kseq (Sset t a3) (Kseqlist sl2 tk)))
+     with (Kseqlist (sl4 ++ Sset t a3 :: sl2) tk).
+  eapply match_exprstates; eauto. 
+  change (Sset t a3 :: sl2) with ((Sset t a3 :: nil) ++ sl2). rewrite <- app_ass. 
+  apply S. econstructor; eauto.  auto. auto. 
+  rewrite Kseqlist_app. auto. 
+  (* for effects *)
+  exploit tr_simple_rvalue; eauto. intros [SL [TY EV]].
+  subst sl0; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor.
+  eapply star_trans. apply step_makeif_false with v; auto. congruence.
+  apply push_seq. 
+  reflexivity. traceEq.
+  rewrite <- Kseqlist_app.
+  econstructor. eauto. apply S.
+    econstructor; eauto. apply tr_expr_monotone with tmp3; eauto. 
+  auto. auto. auto.
+(* assign *)
+  exploit tr_top_leftcontext; eauto. clear H12. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H4.
+  (* for effects *)
+  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  subst; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor.
+  apply star_one. econstructor; eauto.
+  rewrite <- TY1; rewrite <- TY2; eauto.
+  rewrite <- TY1; eauto.
+  traceEq.
+  econstructor. auto. change sl2 with (nil ++ sl2). apply S.
+  constructor. auto. auto. auto.
+  (* for value *)
+  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
+  exploit tr_simple_lvalue. eauto.
+    eapply tr_expr_invariant with (le' := PTree.set t v le). eauto. 
+    intros. apply PTree.gso. intuition congruence.
+  intros [SL1 [TY1 EV1]].
+  subst; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor. 
+  eapply star_left. constructor. eauto. 
+  eapply star_left. constructor.
+  apply star_one. econstructor; eauto. constructor. apply PTree.gss.
+  simpl. rewrite <- TY1; eauto.
+  rewrite <- TY1; eauto.
+  reflexivity. reflexivity. traceEq.
+  econstructor. auto. apply S.
+  apply tr_val_gen. auto. intros. econstructor; eauto. constructor. 
+  rewrite H4; auto. apply PTree.gss. 
+  intros. apply PTree.gso. intuition congruence.
+  auto. auto.
+(* assignop *)
+  exploit tr_top_leftcontext; eauto. clear H14. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H6.
+  (* for effects *)
+  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  subst; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor.
+  apply star_one. econstructor; eauto.
+    econstructor; eauto. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. 
+    rewrite <- TY1; rewrite <- TY2; eauto.
+    rewrite <- TY1; eauto.
+    rewrite <- TY1; eauto.
+  traceEq.
+  econstructor. auto. change sl2 with (nil ++ sl2). apply S.
+  constructor. auto. auto. auto.
+  (* for value *)
+  exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]].
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit tr_simple_lvalue. eauto.
+    eapply tr_expr_invariant with (le' := PTree.set t v3 le). eauto. 
+    intros. apply PTree.gso. intuition congruence.
+  intros [SL3 [TY3 EV3]]. 
+  subst; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor. 
+  eapply star_left. constructor.
+    econstructor. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. eauto.
+    rewrite <- TY1; rewrite <- TY2. eauto. 
+  eapply star_left. constructor.
+  apply star_one. econstructor. eauto. constructor. apply PTree.gss. 
+    rewrite <- TY1. eauto. rewrite <- TY1. eauto.
+  reflexivity. reflexivity. traceEq.
+  econstructor. auto. apply S.
+  apply tr_val_gen. auto. intros. econstructor; eauto. constructor. 
+  rewrite H6; auto. apply PTree.gss. 
+  intros. apply PTree.gso. intuition congruence.
+  auto. auto.
+(* postincr *)
+  exploit tr_top_leftcontext; eauto. clear H13. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H5.
+  (* for effects *)
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  assert (EV2: eval_expr tge e le m a1 v1). eapply eval_Elvalue; eauto. rewrite <- TY1; auto.
+  subst; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_two. constructor.
+  econstructor; eauto.
+  unfold transl_incrdecr. destruct id; simpl in H2. 
+  econstructor. eauto. constructor. simpl. rewrite <- TY1. eauto.
+  econstructor. eauto. constructor. simpl. rewrite <- TY1. eauto.
+  rewrite <- TY1. instantiate (1 := v3). destruct id; auto. 
+  rewrite <- TY1. eauto. 
+  traceEq.
+  econstructor. auto. change sl2 with (nil ++ sl2). apply S.
+  constructor. auto. auto. auto.
+  (* for value *)
+  exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit tr_simple_lvalue. eauto.
+    eapply tr_expr_invariant with (le' := PTree.set t v1 le). eauto. 
+    intros. apply PTree.gso. intuition congruence.
+  intros [SL2 [TY2 EV2]].
+  subst; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_four. constructor. 
+  constructor. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto.
+  constructor.
+  econstructor. eauto. 
+  unfold transl_incrdecr. destruct id; simpl in H2. 
+  econstructor. constructor. apply PTree.gss. constructor. simpl. eauto.
+  econstructor. constructor. apply PTree.gss. constructor. simpl. eauto.
+  rewrite <- TY1. instantiate (1 := v3). destruct id; auto. 
+  rewrite <- TY1. eauto. 
+  traceEq.
+  econstructor. auto. apply S.
+  apply tr_val_gen. auto. intros. econstructor; eauto.
+  rewrite H5; auto. apply PTree.gss. 
+  intros. apply PTree.gso. intuition congruence.
+  auto. auto.
+(* comma *)
+  exploit tr_top_leftcontext; eauto. clear H9. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H1.
+  exploit tr_simple_rvalue; eauto. simpl; intro SL1.
+  subst sl0; simpl Kseqlist.
+  econstructor; split.
+  right; split. apply star_refl. simpl. apply plus_lt_compat_r. 
+  apply (leftcontext_size _ _ _ H). simpl. omega. 
+  econstructor; eauto. apply S. 
+  eapply tr_expr_monotone; eauto. 
+  auto. auto. 
+(* paren *)
+  exploit tr_top_leftcontext; eauto. clear H9. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]].
+  inv P. inv H1.
+  (* for value *)
+  exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]].
+  subst sl0; simpl Kseqlist.
+  econstructor; split.
+  left. eapply plus_left. constructor. apply star_one.
+  econstructor. eauto. traceEq.
+  econstructor; eauto. change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S.
+  constructor. auto. intros. constructor. rewrite H1; auto. apply PTree.gss.
+  intros. apply PTree.gso. intuition congruence.
+  auto. 
+  (* for effects *)
+  econstructor; split.
+  right; split. apply star_refl. simpl. apply plus_lt_compat_r.
+  apply (leftcontext_size _ _ _ H). simpl. omega.
+  econstructor; eauto.
+  exploit tr_simple_rvalue; eauto. destruct dst'.
+  (* dst' = For_val: impossible *)
+  congruence.
+  (* dst' = For_effects: easy *)
+  intros A. subst sl1. apply S. constructor; auto. auto. auto. 
+  (* dst' = For_test: then dest is For_test as well and C is a string of C.Eparen,
+     so we can apply tr_top_paren. *)
+  intros [b [A [B D]]].
+  eapply tr_top_testcontext; eauto. 
+  subst sl1. apply tr_top_val_test; auto.
+  (* already reduced *)
+  econstructor; split.
+  right; split. apply star_refl. simpl. apply plus_lt_compat_r.
+  apply (leftcontext_size _ _ _ H). simpl. omega.
+  econstructor; eauto. instantiate (1 := @nil ident).
+  inv H7. 
+    inv H0. eapply tr_top_testcontext; eauto. constructor. auto. auto.
+    exploit tr_simple_rvalue; eauto. simpl. intros [b [A [B D]]]. 
+    eapply tr_top_testcontext; eauto. subst sl1. apply tr_top_val_test. auto. auto. 
+    inv H0.
+(* call *)
+  exploit tr_top_leftcontext; eauto. clear H12. 
+  intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [U [R S]]]]]]]]].
+  inv P. inv H5.
+  (* for effects *)
+  exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit tr_simple_exprlist; eauto. intros [SL2 EV2].
+  subst. simpl Kseqlist.
+  exploit functions_translated; eauto. intros [tfd [J K]].
+  econstructor; split. 
+  left. eapply plus_left. constructor.  apply star_one.
+  econstructor; eauto. rewrite <- TY1; eauto.
+  exploit type_of_fundef_preserved; eauto. congruence.
+  traceEq.
+  constructor; auto. econstructor; eauto.
+  intros. change sl2 with (nil ++ sl2). apply S.
+  constructor. auto. auto. 
+  (* for value *)
+  exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]].
+  exploit tr_simple_exprlist; eauto. intros [SL2 EV2].
+  subst. simpl Kseqlist.
+  exploit functions_translated; eauto. intros [tfd [J K]].
+  econstructor; split. 
+  left. eapply plus_left. constructor.  apply star_one.
+  econstructor; eauto. rewrite <- TY1; eauto.
+  exploit type_of_fundef_preserved; eauto. congruence.
+  traceEq.
+  constructor; auto. econstructor; eauto.
+  intros. apply S.
+  destruct dst'; constructor.
+  auto. intros. constructor. rewrite H5; auto. apply PTree.gss. 
+  auto. intros. constructor. rewrite H5; auto. apply PTree.gss.  
+  intros. apply PTree.gso. intuition congruence.
+  auto. 
+Qed.
+
+(** Forward simulation for statements. *)
+
+Lemma tr_top_val_for_val_inv:
+  forall e le m v ty sl a tmps,
+  tr_top tge e le m For_val (C.Eval v ty) sl a tmps ->
+  sl = nil /\ typeof a = ty /\ eval_expr tge e le m a v.
+Proof.
+  intros. inv H. auto. inv H0. auto. 
+Qed.
+
+Lemma tr_top_val_for_test_inv:
+  forall s1 s2 e le m v ty sl a tmps,
+  tr_top tge e le m (For_test s1 s2) (C.Eval v ty) sl a tmps ->
+  exists b, sl = makeif b s1 s2 :: nil /\ typeof b = ty /\ eval_expr tge e le m b v.
+Proof.
+  intros. inv H. exists a0; auto. 
+  inv H0. exists a0; auto.
+Qed.
+
+Lemma sstep_simulation:
+  forall S1 t S2, Csem.sstep ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  exists S2',
+     (plus step tge S1' t S2' \/
+       (star step tge S1' t S2' /\ measure S2 < measure S1)%nat)
+  /\ match_states S2 S2'.
+Proof.
+  induction 1; intros; inv MS.
+(* do 1 *)
+  inv H6. inv H0. 
+  econstructor; split.
+  right; split. apply push_seq. 
+  simpl. omega.
+  econstructor; eauto. constructor. auto.
+(* do 2 *)
+  inv H7. inv H6. inv H.  
+  econstructor; split. 
+  right; split. apply star_refl. simpl. omega.
+  econstructor; eauto. constructor.
+
+(* seq *)
+  inv H6. econstructor; split. left. apply plus_one. constructor.
+  econstructor; eauto. constructor; auto.
+(* skip seq *)
+  inv H6; inv H7. econstructor; split.
+  left. apply plus_one; constructor.
+  econstructor; eauto.
+(* continue seq *)
+  inv H6; inv H7. econstructor; split.
+  left. apply plus_one; constructor.
+  econstructor; eauto. constructor.
+(* break seq *)
+  inv H6; inv H7. econstructor; split.
+  left. apply plus_one; constructor.
+  econstructor; eauto. constructor.
+
+(* ifthenelse *)
+  inv H6.
+  (* not optimized *)
+  inv H2. econstructor; split.
+  left. eapply plus_left. constructor. apply push_seq. traceEq.
+  econstructor; eauto. econstructor; eauto.
+  (* optimized *)
+  inv H10. econstructor; split.
+  right; split. apply push_seq. simpl. omega.
+  econstructor; eauto. constructor; auto. 
+(* ifthenelse true *)
+  inv H8. 
+  (* not optimized *)
+  exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. 
+  econstructor; split.
+  left. eapply plus_two. constructor.
+  apply step_ifthenelse_true with v; auto. traceEq.
+  econstructor; eauto.
+  (* optimized *)
+  exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. 
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor.
+  apply step_makeif_true with v; auto. traceEq.
+  econstructor; eauto.
+(* ifthenelse false *)
+  inv H8. 
+  (* not optimized *)
+  exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. 
+  econstructor; split.
+  left. eapply plus_two. constructor.
+  apply step_ifthenelse_false with v; auto. traceEq.
+  econstructor; eauto.
+  (* optimized *)
+  exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. 
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor.
+  apply step_makeif_false with v; auto. traceEq.
+  econstructor; eauto.
+
+(* while *)
+  inv H6. inv H1. econstructor; split.
+  left. eapply plus_left. eapply step_while_true. constructor. 
+  simpl. constructor. apply Int.one_not_zero.
+  eapply star_left. constructor.
+  apply push_seq.
+  reflexivity. traceEq.
+  econstructor; eauto. econstructor; eauto. econstructor; eauto.
+(* while false *)
+  inv H8. 
+  exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. 
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor.
+  eapply star_trans. apply step_makeif_false with v; auto.
+  eapply star_two. constructor. apply step_break_while. 
+  reflexivity. reflexivity. traceEq.
+  constructor; auto. constructor.
+(* while true *)
+  inv H8. 
+  exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. 
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor.
+  eapply star_right. apply step_makeif_true with v; auto.
+  constructor.
+  reflexivity. traceEq.
+  constructor; auto. constructor; auto. 
+(* skip-or-continue while *)
+  assert (ts = Sskip \/ ts = Scontinue). destruct H; subst s0; inv H7; auto.
+  inv H8.
+  econstructor; split.
+  left. apply plus_one. apply step_skip_or_continue_while; auto. 
+  constructor; auto. constructor; auto. 
+(* break while *)
+  inv H6. inv H7. 
+  econstructor; split.
+  left. apply plus_one. apply step_break_while. 
+  constructor; auto. constructor.
+
+(* dowhile *)
+  inv H6. 
+  econstructor; split.
+  left. apply plus_one.
+  apply step_for_true with (Vint Int.one). constructor. simpl; constructor. apply Int.one_not_zero.
+  constructor; auto. constructor; auto.
+(* skip_or_continue dowhile *)
+  assert (ts = Sskip \/ ts = Scontinue). destruct H; subst s0; inv H7; auto.
+  inv H8. inv H4.
+  econstructor; split.
+  left. eapply plus_left. apply step_skip_or_continue_for2. auto.
+  apply push_seq. 
+  reflexivity. traceEq.
+  econstructor; eauto. econstructor; auto. econstructor; eauto. 
+(* dowhile false *)
+  inv H8. 
+  exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. 
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor. 
+  eapply star_right. apply step_makeif_false with v; auto. 
+  constructor. 
+  reflexivity. traceEq.
+  constructor; auto. constructor.
+(* dowhile true *)
+  inv H8. 
+  exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. 
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor. 
+  eapply star_right. apply step_makeif_true with v; auto. 
+  constructor. 
+  reflexivity. traceEq.
+  constructor; auto. constructor; auto. 
+(* break dowhile *)
+  inv H6. inv H7.
+  econstructor; split.
+  left. apply plus_one. apply step_break_for2. 
+  constructor; auto. constructor.
+
+(* for start *)
+  inv H7. congruence. 
+  econstructor; split. 
+  left; apply plus_one. constructor.
+  econstructor; eauto. constructor; auto. econstructor; eauto. 
+(* for *)
+  inv H6; try congruence. inv H2. 
+  econstructor; split.
+  left. eapply plus_left. apply step_for_true with (Vint Int.one). 
+    constructor. simpl; constructor. apply Int.one_not_zero.
+  eapply star_left. constructor. apply push_seq.
+  reflexivity. traceEq.
+  econstructor; eauto. constructor; auto. econstructor; eauto.
+(* for false *)
+  inv H8. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst.
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor.
+  eapply star_trans. apply step_makeif_false with v; auto.
+  eapply star_two. constructor. apply step_break_for2. 
+  reflexivity. reflexivity. traceEq.
+  constructor; auto. constructor.
+(* for true *)
+  inv H8. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst.
+  econstructor; split.
+  left. simpl. eapply plus_left. constructor. 
+  eapply star_right. apply step_makeif_true with v; auto.
+  constructor.
+  reflexivity. traceEq.
+  constructor; auto. constructor; auto. 
+(* skip_or_continue for3 *)
+  assert (ts = Sskip \/ ts = Scontinue). destruct H; subst x; inv H7; auto.
+  inv H8.
+  econstructor; split.
+  left. apply plus_one. apply step_skip_or_continue_for2. auto.
+  econstructor; eauto. econstructor; auto.
+(* break for3 *)
+  inv H6. inv H7. 
+  econstructor; split.
+  left. apply plus_one. apply step_break_for2.
+  econstructor; eauto. constructor.
+(* skip for4 *)
+  inv H6. inv H7. 
+  econstructor; split.
+  left. apply plus_one. constructor.
+  econstructor; eauto. constructor; auto. 
+
+(* return none *)
+  inv H8. econstructor; split.
+  left. apply plus_one. econstructor; eauto. 
+  rewrite <- H. apply function_return_preserved; auto.
+  constructor. apply match_cont_call; auto. 
+(* return some 1 *)
+  inv H7. inv H1. econstructor; split.
+  left; eapply plus_left. constructor. apply push_seq. traceEq.
+  econstructor; eauto. constructor. auto.
+(* return some 2 *)
+  inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
+  econstructor; split.
+  left. eapply plus_two. constructor. econstructor. eauto.
+  replace (fn_return tf) with (C.fn_return f). eauto.
+  exploit transl_function_spec; eauto. intuition congruence. 
+  eauto. traceEq.
+  constructor. apply match_cont_call; auto.
+(* skip return *)
+  inv H9. 
+  assert (is_call_cont tk). inv H10; simpl in *; auto.
+  econstructor; split.
+  left. apply plus_one. apply step_skip_call; eauto.
+  rewrite <- H0. apply function_return_preserved; auto.
+  constructor. auto.
+
+(* switch *)
+  inv H6. inv H1. 
+  econstructor; split. 
+  left; eapply plus_left. constructor. apply push_seq. traceEq.
+  econstructor; eauto. constructor; auto. 
+(* expr switch *)
+  inv H7. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
+  econstructor; split.
+  left; eapply plus_two. constructor. econstructor; eauto. traceEq.
+  econstructor; eauto.
+  apply tr_seq_of_labeled_statement. apply tr_select_switch. auto. 
+  constructor; auto.
+
+(* skip-or-break switch *)
+  assert (ts = Sskip \/ ts = Sbreak). destruct H; subst x; inv H7; auto.
+  inv H8.
+  econstructor; split.
+  left; apply plus_one. apply step_skip_break_switch. auto. 
+  constructor; auto. constructor.
+
+(* continue switch *)
+  inv H6. inv H7.
+  econstructor; split.
+  left; apply plus_one. apply step_continue_switch.
+  constructor; auto. constructor.
+
+(* label *)
+  inv H6. econstructor; split.
+  left; apply plus_one. constructor.
+  constructor; auto.
+
+(* goto *)
+  inv H7.
+  exploit transl_function_spec; eauto. intros [A [B [C D]]].
+  exploit tr_find_label. eexact A. apply match_cont_call. eauto. 
+  instantiate (1 := lbl). rewrite H. 
+  intros [ts' [tk' [P [Q R]]]]. 
+  econstructor; split. 
+  left. apply plus_one. econstructor; eauto.
+  econstructor; eauto. 
+
+(* internal function *)
+  monadInv H7. 
+  exploit transl_function_spec; eauto. intros [A [B [C D]]].
+  econstructor; split.
+  left; apply plus_one. eapply step_internal_function. 
+  rewrite C; rewrite D; auto.
+  rewrite C; rewrite D; eauto.
+  rewrite C; eauto.
+  constructor; auto. 
+
+(* external function *)
+  monadInv H5. 
+  econstructor; split.
+  left; apply plus_one. econstructor; eauto.
+  eapply external_call_symbols_preserved; eauto. 
+  exact symbols_preserved. exact varinfo_preserved. 
+  constructor; auto.
+
+(* return *)
+  inv H3.
+  (* none *)
+  econstructor; split.
+  left; apply plus_one. constructor.
+  econstructor; eauto.
+  (* some *)
+  econstructor; split.
+  left; apply plus_one. constructor.
+  econstructor; eauto.
+Qed.
+
+(** Semantic preservation *)
+
+Theorem simulation:
+  forall S1 t S2, Cstrategy.step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  exists S2',
+     (plus step tge S1' t S2' \/
+       (star step tge S1' t S2' /\ measure S2 < measure S1)%nat)
+  /\ match_states S2 S2'.
+Proof.
+  intros S1 t S2 STEP. destruct STEP. 
+  apply estep_simulation; auto.
+  apply sstep_simulation; auto.
+Qed.
+
+Lemma transl_initial_states:
+  forall S,
+  Csem.initial_state prog S ->
+  exists S', Clight.initial_state tprog S' /\ match_states S S'.
+Proof.
+  intros. inv H. 
+  exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
+  econstructor; split.
+  econstructor.
+  apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto. 
+  simpl. fold tge. rewrite symbols_preserved.
+  replace (prog_main tprog) with (prog_main prog). eexact H1.
+  symmetry. unfold transl_program in TRANSL.
+  eapply transform_partial_program_main; eauto.
+  eexact FIND.
+  rewrite <- H3. apply type_of_fundef_preserved. auto.
+  constructor. auto. constructor.
+Qed.
+
+Lemma transl_final_states:
+  forall S S' r,
+  match_states S S' -> Csem.final_state S r -> Clight.final_state S' r.
+Proof.
+  intros. inv H0. inv H. inv H4. constructor.
+Qed.
+
+Theorem transl_program_correct:
+  forall (beh: program_behavior),
+  not_wrong beh -> Cstrategy.exec_program prog beh ->
+  Clight.exec_program tprog beh.
+Proof.
+  unfold Cstrategy.exec_program, Clight.exec_program. intros. 
+  eapply simulation_star_wf_preservation; eauto. 
+  eexact transl_initial_states.
+  eexact transl_final_states.
+  instantiate (1 := ltof _ measure). apply well_founded_ltof. 
+  exact simulation.
+Qed.
+
+End PRESERVATION.