Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.

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

1 files changed, 616 insertions, 408 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 15f305a..e9a04fc 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -94,13 +94,13 @@ Proof.
   eauto.
 Qed.
 
-(** An RTL register environment matches a Cminor local environment and
+(** An RTL register environment matches a CminorSel local environment and
   let-environment if the value of every local or let-bound variable in
-  the Cminor environments is identical to the value of the
+  the CminorSel environments is identical to the value of the
   corresponding pseudo-register in the RTL register environment. *)
 
 Record match_env
-      (map: mapping) (e: Cminor.env) (le: Cminor.letenv) (rs: regset) : Prop :=
+      (map: mapping) (e: env) (le: letenv) (rs: regset) : Prop :=
   mk_match_env {
     me_vars:
       (forall id v,
@@ -367,6 +367,51 @@ Proof.
   split. apply Regmap.gss. intros; apply Regmap.gso; auto.
 Qed.
 
+(** Correctness of the code generated by [store_var] and [store_optvar]. *)
+
+Lemma tr_store_var_correct:
+  forall rs cs code map r id ns nd e sp m,
+  tr_store_var code map r id ns nd ->
+  map_wf map ->
+  match_env map e nil rs ->
+  exists rs',
+     star step tge (State cs code sp ns rs m)
+                E0 (State cs code sp nd rs' m)
+  /\ match_env map (PTree.set id rs#r e) nil rs'.
+Proof.
+  intros. destruct H as [rv [A B]].
+  exploit tr_move_correct; eauto. intros [rs' [EX [RES OTHER]]].
+  exists rs'; split. eexact EX.
+  apply match_env_invariant with (rs#rv <- (rs#r)).
+  apply match_env_update_var; auto.
+  intros. rewrite Regmap.gsspec. destruct (peq r0 rv).
+  subst r0; auto.
+  auto.
+Qed.
+
+Lemma tr_store_optvar_correct:
+  forall rs cs code map r optid ns nd e sp m,
+  tr_store_optvar code map r optid ns nd ->
+  map_wf map ->
+  match_env map e nil rs ->
+  exists rs',
+     star step tge (State cs code sp ns rs m)
+                E0 (State cs code sp nd rs' m)
+  /\ match_env map (set_optvar optid rs#r e) nil rs'.
+Proof.
+  intros. destruct optid; simpl in *.
+  eapply tr_store_var_correct; eauto.
+  exists rs; split. subst nd. apply star_refl. auto.  
+Qed.
+
+(** ** Semantic preservation for the translation of expressions *)
+
+Section CORRECTNESS_EXPR.
+
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
 (** The proof of semantic preservation for the translation of expressions
   is a simulation argument based on diagrams of the following form:
 <<
@@ -380,16 +425,14 @@ Qed.
                     I /\ Q
 >>
   where [tr_expr code map pr a ns nd rd] is assumed to hold.
-  The left vertical arrow represents an evaluation of the expression [a]
-  to value [v].
+  The left vertical arrow represents an evaluation of the expression [a].
   The right vertical arrow represents the execution of zero, one or
   several instructions in the generated RTL flow graph [code].
 
-  The invariant [I] is the agreement between CminorSel environments
-  [e], [le] and the RTL register environment [rs],
-  as captured by [match_envs].
+  The invariant [I] is the agreement between Cminor environments and
+  RTL register environment, as captured by [match_envs].
 
-  The precondition [P] is the well-formedness of the compilation
+  The precondition [P] includes the well-formedness of the compilation
   environment [mut].
 
   The postconditions [Q] state that in the final register environment
@@ -400,15 +443,14 @@ Qed.
   We formalize this simulation property by the following predicate
   parameterized by the CminorSel evaluation (left arrow).  *)
 
-Definition transl_expr_correct 
-  (sp: val) (le: letenv) (e: env) (m: mem) (a: expr)
-              (t: trace) (m': mem) (v: val) : Prop :=
+Definition transl_expr_prop 
+     (le: letenv) (a: expr) (v: val) : Prop :=
   forall cs code map pr ns nd rd rs
     (MWF: map_wf map)
     (TE: tr_expr code map pr a ns nd rd)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) t (State cs code sp nd rs' m')
+     star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'#rd = v
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
@@ -416,123 +458,44 @@ Definition transl_expr_correct
 (** The simulation properties for lists of expressions and for
   conditional expressions are similar. *)
 
-Definition transl_exprlist_correct 
-  (sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist)
-              (t: trace) (m': mem) (vl: list val) : Prop :=
+Definition transl_exprlist_prop 
+     (le: letenv) (al: exprlist) (vl: list val) : Prop :=
   forall cs code map pr ns nd rl rs
     (MWF: map_wf map)
     (TE: tr_exprlist code map pr al ns nd rl)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) t (State cs code sp nd rs' m')
+     star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m)
   /\ match_env map e le rs'
   /\ rs'##rl = vl
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
-Definition transl_condition_correct 
-  (sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr)
-              (t: trace) (m': mem) (vb: bool) : Prop :=
+Definition transl_condition_prop 
+     (le: letenv) (a: condexpr) (vb: bool) : Prop :=
   forall cs code map pr ns ntrue nfalse rs
     (MWF: map_wf map)
     (TE: tr_condition code map pr a ns ntrue nfalse)
     (ME: match_env map e le rs),
   exists rs',
-     star step tge (State cs code sp ns rs m) t
-                   (State cs code sp (if vb then ntrue else nfalse) rs' m')
+     star step tge (State cs code sp ns rs m) E0
+                   (State cs code sp (if vb then ntrue else nfalse) rs' m)
   /\ match_env map e le rs'
   /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
 
 
-(** The simulation diagram for the translation of statements
-  is of the following form:
-<<
-                    I /\ P
-      e, m, a -------------- State cs code sp ns rs m
-         ||                      |
-        t||                     t|*
-         ||                      |
-         \/                      v
-     e', m', out -------------- st'
-                    I /\ Q
->>
-  where [tr_stmt code map a ns ncont nexits nret rret] holds.
-  The left vertical arrow represents an execution of the statement [a]
-  with outcome [out].
-  The right vertical arrow represents the execution of
-  zero, one or several instructions in the generated RTL flow graph [code].
-
-  The invariant [I] is the agreement between CminorSel environments and
-  RTL register environment, as captured by [match_envs].
-
-  The precondition [P] is the well-formedness of the compilation
-  environment [mut].
-
-  The postcondition [Q] characterizes the final RTL state [st'].
-  It must have memory state [m'] and a register state [rs'] that matches
-  [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_correct 
-  (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 CminorSel function, returns the same value, produces
-  the same trace of events, and performs the same modifications on the
-  memory state. *)
-
-Definition transl_function_correct
-    (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').
 
 (** The correctness of the translation is a huge induction over
-  the CminorSel evaluation derivation for the source program.  To keep
+  the Cminor evaluation derivation for the source program.  To keep
   the proof manageable, we put each case of the proof in a separate
-  lemma.  There is one lemma for each CminorSel evaluation rule.
-  It takes as hypotheses the premises of the CminorSel evaluation rule,
-  plus the induction hypotheses, that is, the [transl_expr_correct], etc,
+  lemma.  There is one lemma for each Cminor evaluation rule.
+  It takes as hypotheses the premises of the Cminor evaluation rule,
+  plus the induction hypotheses, that is, the [transl_expr_prop], etc,
   corresponding to the evaluations of sub-expressions or sub-statements. *)
 
 Lemma transl_expr_Evar_correct:
-  forall (sp: val) (le: letenv) (e: env) (m: mem) (id: ident) (v: val),
-  e!id = Some v ->
-  transl_expr_correct sp le e m (Evar id) E0 m v.
+  forall (le : letenv) (id : positive) (v : val),
+  e ! id = Some v ->
+  transl_expr_prop le (Evar id) v.
 Proof.
   intros; red; intros. inv TE.
   exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. 
@@ -553,13 +516,12 @@ Proof.
 Qed.
 
 Lemma transl_expr_Eop_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation)
-         (al : exprlist) (t: trace) (m1 : mem) (vl : list val)
-         (v: val),
-  eval_exprlist ge sp le e m al t m1 vl ->
-  transl_exprlist_correct sp le e m al t m1 vl ->
-  eval_operation ge sp op vl m1 = Some v ->
-  transl_expr_correct sp le e m (Eop op al) t m1 v.
+  forall (le : letenv) (op : operation) (args : exprlist)
+         (vargs : list val) (v : val),
+  eval_exprlist ge sp e m le args vargs ->
+  transl_exprlist_prop le args vargs ->
+  eval_operation ge sp op vargs m = Some v ->
+  transl_expr_prop le (Eop op args) v.
 Proof.
   intros; red; intros. inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
@@ -567,7 +529,7 @@ Proof.
 (* Exec *)
   split. eapply star_right. eexact EX1.
   eapply exec_Iop; eauto.  
-  subst vl. 
+  subst vargs.
   rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). 
   auto. 
   exact symbols_preserved. traceEq.
@@ -580,15 +542,13 @@ Proof.
 Qed.
 
 Lemma transl_expr_Eload_correct:
- forall (sp: val) (le : letenv) (e : env) (m : mem)
-    (chunk : memory_chunk) (addr : addressing) 
-    (al : exprlist) (t: trace) (m1 : mem) (v : val) 
-    (vl : list val) (a: val),
-  eval_exprlist ge sp le e m al t m1 vl ->
-  transl_exprlist_correct sp le e m al t m1 vl ->
-  eval_addressing ge sp addr vl = Some a ->
-  Mem.loadv chunk m1 a = Some v ->
-  transl_expr_correct sp le e m (Eload chunk addr al) t m1 v.
+  forall (le : letenv) (chunk : memory_chunk) (addr : Op.addressing)
+         (args : exprlist) (vargs : list val) (vaddr v : val),
+  eval_exprlist ge sp e m le args vargs ->
+  transl_exprlist_prop le args vargs ->
+  Op.eval_addressing ge sp addr vargs = Some vaddr ->
+  loadv chunk m vaddr = Some v ->
+  transl_expr_prop le (Eload chunk addr args) v.
 Proof.
   intros; red; intros. inv TE.
   exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
@@ -605,105 +565,19 @@ Proof.
   intros. rewrite Regmap.gso. auto. intuition congruence. 
 Qed.
 
-Lemma transl_expr_Estore_correct:
- forall (sp: val) (le : letenv) (e : env) (m : mem)
-    (chunk : memory_chunk) (addr : addressing) 
-    (al : exprlist) (b : expr) (t t1: trace) (m1 : mem) 
-    (vl : list val) (t2: trace) (m2 m3 : mem) 
-    (v : val) (a: val),
-  eval_exprlist ge sp le e m al t1 m1 vl ->
-  transl_exprlist_correct sp le e m al t1 m1 vl ->
-  eval_expr ge sp le e m1 b t2 m2 v ->
-  transl_expr_correct sp le e m1 b t2 m2 v ->
-  eval_addressing ge sp addr vl = Some a -> 
-  Mem.storev chunk m2 a v = Some m3 ->
-  t = t1 ** t2 ->
-  transl_expr_correct sp le e m (Estore chunk addr al b) t m3 v.
-Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  exists rs2.
-(* 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.
-    right. apply in_or_app. auto.
-  rewrite H5; rewrite RES1. 
-  rewrite (@eval_addressing_preserved _ _ ge tge).
-  eexact H3. exact symbols_preserved. 
-  rewrite RES2. assumption.
-  reflexivity. traceEq. 
-(* Match-env *)
-  split. assumption.
-(* Result *)
-  split. assumption.
-(* Other regs *)
-  intro r'; intros. transitivity (rs1#r'). 
-  apply OTHER2. intuition.
-  auto.
-Qed.
-
-Lemma transl_expr_Ecall_correct:
- forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (sig : signature) (a : expr) (bl : exprlist) (t t1: trace)
-    (m1: mem) (t2: trace) (m2 : mem) 
-    (t3: trace) (m3: mem) (vf : val) 
-    (vargs : list val) (vres : val) (f : CminorSel.fundef),
-  eval_expr ge sp le e m a t1 m1 vf ->
-  transl_expr_correct sp le e m a t1 m1 vf ->
-  eval_exprlist ge sp le e m1 bl t2 m2 vargs ->
-  transl_exprlist_correct sp le e m1 bl t2 m2 vargs ->
-  Genv.find_funct ge vf = Some f ->
-  CminorSel.funsig f = sig ->
-  eval_funcall ge m2 f vargs t3 m3 vres ->
-  transl_function_correct m2 f vargs t3 m3 vres ->
-  t = t1 ** t2 ** t3 ->
-  transl_expr_correct sp le e m (Ecall sig a bl) t m3 vres.
-Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
-  exploit functions_translated; eauto. intros [tf [TFIND TF]].
-  exploit H6; eauto. intro EXF.
-  exists (rs2#rd <- vres).
-(* 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_right. rewrite RES2. eexact EXF.
-  apply exec_return. reflexivity. reflexivity. reflexivity. traceEq.  
-(* Match env *)
-  split. eauto with rtlg. 
-(* Result *)
-  split. apply Regmap.gss.
-(* Other regs *)
-  intros.
-  rewrite Regmap.gso. transitivity (rs1#r). 
-  apply OTHER2. simpl; tauto.
-  apply OTHER1; auto. 
-  intuition congruence.
-Qed.
-
 Lemma transl_expr_Econdition_correct:
- forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a : condexpr) (b c : expr) (t t1: trace) (m1 : mem) 
-    (v1 : bool) (t2: trace) (m2 : mem) (v2 : val),
-  eval_condexpr ge sp le e m a t1 m1 v1 ->
-  transl_condition_correct sp le e m a t1 m1 v1 ->
-  eval_expr ge sp le e m1 (if v1 then b else c) t2 m2 v2 ->
-  transl_expr_correct sp le e m1 (if v1 then b else c) t2 m2 v2 ->
-  t = t1 ** t2 ->
-  transl_expr_correct sp le e m (Econdition a b c) t m2 v2.
+  forall (le : letenv) (cond : condexpr) (ifso ifnot : expr)
+         (vcond : bool) (v : val),
+  eval_condexpr ge sp e m le cond vcond ->
+  transl_condition_prop le cond vcond ->
+  eval_expr ge sp e m le (if vcond then ifso else ifnot) v ->
+  transl_expr_prop le (if vcond then ifso else ifnot) v ->
+  transl_expr_prop le (Econdition cond ifso ifnot) v.
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_expr code map pr (if v1 then b else c) (if v1 then ntrue else nfalse) nd rd).
-    destruct v1; auto.
+  assert (tr_expr code map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd).
+    destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
   exists rs2.
 (* Exec *)
@@ -717,15 +591,12 @@ Proof.
 Qed.
 
 Lemma transl_expr_Elet_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a b : expr) (t t1: trace) (m1 : mem) (v1 : val) 
-    (t2: trace) (m2 : mem) (v2 : val),
-  eval_expr ge sp le e m a t1 m1 v1 ->
-  transl_expr_correct sp le e m a t1 m1 v1 ->
-  eval_expr ge sp (v1 :: le) e m1 b t2 m2 v2 ->
-  transl_expr_correct sp (v1 :: le) e m1 b t2 m2 v2 ->
-  t = t1 ** t2 ->
-  transl_expr_correct sp le e m (Elet a b) t m2 v2.
+  forall (le : letenv) (a1 a2 : expr) (v1 v2 : val),
+  eval_expr ge sp e m le a1 v1 ->
+  transl_expr_prop le a1 v1 ->
+  eval_expr ge sp e m (v1 :: le) a2 v2 ->
+  transl_expr_prop (v1 :: le) a2 v2 ->
+  transl_expr_prop le (Elet a1 a2) v2.
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
@@ -744,15 +615,14 @@ Proof.
   intros. transitivity (rs1#r0). 
   apply OTHER2. elim H4; intro; auto.
   unfold reg_in_map, add_letvar; simpl.
-  unfold reg_in_map in H5; tauto.
+  unfold reg_in_map in H6; tauto.
   auto.
 Qed.
 
 Lemma transl_expr_Eletvar_correct:
-  forall (sp: val) (le : list val) (e : env) 
-    (m : mem) (n : nat) (v : val),
+  forall (le : list val) (n : nat) (v : val),
   nth_error le n = Some v ->
-  transl_expr_correct sp le e m (Eletvar n) E0 m v.
+  transl_expr_prop le (Eletvar n) v.
 Proof.
   intros; red; intros; inv TE.
   exploit tr_move_correct; eauto. intros [rs1 [EX1 [RES1 OTHER1]]].
@@ -772,54 +642,29 @@ Proof.
   apply OTHER1. intuition congruence.
 Qed.
 
-Lemma transl_expr_Ealloc_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a : expr) (t: trace) (m1 : mem) (n: int)
-    (m2: mem) (b: block),
-  eval_expr ge sp le e m a t m1 (Vint n) ->
-  transl_expr_correct sp le e m a t m1 (Vint n) ->
-  Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
-  transl_expr_correct sp le e m (Ealloc a) t m2 (Vptr b Int.zero).
-Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
-  exists (rs1#rd <- (Vptr b Int.zero)).
-(* Exec *)
-  split. eapply star_right. eexact EX1. 
-  eapply exec_Ialloc. eauto with rtlg.
-  eexact RR1. assumption. traceEq. 
-(* Match-env *)
-  split. eauto with rtlg. 
-(* Result *)
-  split. apply Regmap.gss.
-(* Other regs *)
-  intros. rewrite Regmap.gso. auto. intuition congruence.
-Qed.
-
 Lemma transl_condition_CEtrue_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem),
-  transl_condition_correct sp le e m CEtrue E0 m true.
+  forall (le : letenv),
+  transl_condition_prop le CEtrue true.
 Proof.
   intros; red; intros; inv TE. 
   exists rs. split. apply star_refl. split. auto. auto.
 Qed.    
 
 Lemma transl_condition_CEfalse_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem),
-  transl_condition_correct sp le e m CEfalse E0 m false.
+  forall (le : letenv),
+  transl_condition_prop le CEfalse false.
 Proof.
   intros; red; intros; inv TE. 
   exists rs. split. apply star_refl. split. auto. auto.
 Qed.    
 
 Lemma transl_condition_CEcond_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem)
-    (cond : condition) (al : exprlist) (t1: trace)
-    (m1 : mem) (vl : list val) (b : bool),
-  eval_exprlist ge sp le e m al t1 m1 vl ->
-  transl_exprlist_correct sp le e m al t1 m1 vl ->
-  eval_condition cond vl m1 = Some b ->
-  transl_condition_correct sp le e m (CEcond cond al) t1 m1 b.
+  forall (le : letenv) (cond : condition) (args : exprlist)
+         (vargs : list val) (b : bool),
+  eval_exprlist ge sp e m le args vargs ->
+  transl_exprlist_prop le args vargs ->
+  eval_condition cond vargs m = Some b ->
+  transl_condition_prop le (CEcond cond args) b.
 Proof.
   intros; red; intros; inv TE.
   exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
@@ -839,21 +684,18 @@ Proof.
 Qed.
 
 Lemma transl_condition_CEcondition_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem)
-    (a b c : condexpr) (t t1: trace) (m1 : mem) 
-    (vb1 : bool) (t2: trace) (m2 : mem) (vb2 : bool),
-  eval_condexpr ge sp le e m a t1 m1 vb1 ->
-  transl_condition_correct sp le e m a t1 m1 vb1 ->
-  eval_condexpr ge sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
-  transl_condition_correct sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
-  t = t1 ** t2 ->
-  transl_condition_correct sp le e m (CEcondition a b c) t m2 vb2.
+  forall (le : letenv) (cond ifso ifnot : condexpr) (vcond v : bool),
+  eval_condexpr ge sp e m le cond vcond ->
+  transl_condition_prop le cond vcond ->
+  eval_condexpr ge sp e m le (if vcond then ifso else ifnot) v ->
+  transl_condition_prop le (if vcond then ifso else ifnot) v ->
+  transl_condition_prop le (CEcondition cond ifso ifnot) v.
 Proof.
   intros; red; intros; inv TE. 
   exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_condition code map pr (if vb1 then b else c)
-             (if vb1 then ntrue' else nfalse') ntrue nfalse).
-    destruct vb1; auto.
+  assert (tr_condition code map pr (if vcond then ifso else ifnot)
+             (if vcond then ntrue' else nfalse') ntrue nfalse).
+    destruct vcond; auto.
   exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]].
   exists rs2.
 (* Execution *)
@@ -865,8 +707,8 @@ Proof.
 Qed.
  
 Lemma transl_exprlist_Enil_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem),
-  transl_exprlist_correct sp le e m Enil E0 m nil.
+  forall (le : letenv),
+  transl_exprlist_prop le Enil nil.
 Proof.
   intros; red; intros; inv TE.
   exists rs.
@@ -877,15 +719,13 @@ Proof.
 Qed.
 
 Lemma transl_exprlist_Econs_correct:
-  forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a : expr) (bl : exprlist) (t t1: trace) (m1 : mem) 
-    (v : val) (t2: trace) (m2 : mem) (vl : list val),
-  eval_expr ge sp le e m a t1 m1 v ->
-  transl_expr_correct sp le e m a t1 m1 v ->
-  eval_exprlist ge sp le e m1 bl t2 m2 vl ->
-  transl_exprlist_correct sp le e m1 bl t2 m2 vl ->
-  t = t1 ** t2 ->
-  transl_exprlist_correct sp le e m (Econs a bl) t m2 (v :: vl).
+  forall (le : letenv) (a1 : expr) (al : exprlist) (v1 : val)
+         (vl : list val),
+  eval_expr ge sp e m le a1 v1 ->
+  transl_expr_prop le a1 v1 ->
+  eval_exprlist ge sp e m le al vl ->
+  transl_exprlist_prop le al vl ->
+  transl_exprlist_prop le (Econs a1 al) (v1 :: vl).
 Proof.
   intros; red; intros; inv TE.
   exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
@@ -904,6 +744,153 @@ Proof.
   apply OTHER1; auto.
 Qed.
 
+Theorem transl_expr_correct:
+  forall le a v,
+  eval_expr ge sp e m le a v ->
+  transl_expr_prop le a v.
+Proof
+  (eval_expr_ind3 ge sp e m
+     transl_expr_prop
+     transl_condition_prop
+     transl_exprlist_prop
+     transl_expr_Evar_correct
+     transl_expr_Eop_correct
+     transl_expr_Eload_correct
+     transl_expr_Econdition_correct
+     transl_expr_Elet_correct
+     transl_expr_Eletvar_correct
+     transl_condition_CEtrue_correct
+     transl_condition_CEfalse_correct
+     transl_condition_CEcond_correct
+     transl_condition_CEcondition_correct
+     transl_exprlist_Enil_correct
+     transl_exprlist_Econs_correct).
+
+Theorem transl_condexpr_correct:
+  forall le a v,
+  eval_condexpr ge sp e m le a v ->
+  transl_condition_prop le a v.
+Proof
+  (eval_condexpr_ind3 ge sp e m
+     transl_expr_prop
+     transl_condition_prop
+     transl_exprlist_prop
+     transl_expr_Evar_correct
+     transl_expr_Eop_correct
+     transl_expr_Eload_correct
+     transl_expr_Econdition_correct
+     transl_expr_Elet_correct
+     transl_expr_Eletvar_correct
+     transl_condition_CEtrue_correct
+     transl_condition_CEfalse_correct
+     transl_condition_CEcond_correct
+     transl_condition_CEcondition_correct
+     transl_exprlist_Enil_correct
+     transl_exprlist_Econs_correct).
+
+
+Theorem transl_exprlist_correct:
+  forall le a v,
+  eval_exprlist ge sp e m le a v ->
+  transl_exprlist_prop le a v.
+Proof
+  (eval_exprlist_ind3 ge sp e m
+     transl_expr_prop
+     transl_condition_prop
+     transl_exprlist_prop
+     transl_expr_Evar_correct
+     transl_expr_Eop_correct
+     transl_expr_Eload_correct
+     transl_expr_Econdition_correct
+     transl_expr_Elet_correct
+     transl_expr_Eletvar_correct
+     transl_condition_CEtrue_correct
+     transl_condition_CEfalse_correct
+     transl_condition_CEcond_correct
+     transl_condition_CEcondition_correct
+     transl_exprlist_Enil_correct
+     transl_exprlist_Econs_correct).
+
+End CORRECTNESS_EXPR.
+
+(** ** Semantic preservation for the translation of terminating statements *)   
+
+(** The simulation diagram for the translation of statements
+  is of the following form:
+<<
+                    I /\ P
+       e, m, a ---------------- State cs code sp ns rs m
+         ||                          |
+        t||                         t|*
+         ||                          |
+         \/                          v
+     e', m', out ------------------ st'
+                    I /\ Q
+>>
+  where [tr_stmt code map a ns ncont nexits nret rret] holds.
+  The left vertical arrow represents an execution of the statement [a].
+  The right vertical arrow represents the execution of
+  zero, one or several instructions in the generated RTL flow graph [code].
+
+  The invariant [I] is the agreement between Cminor environments and
+  RTL register environment, as captured by [match_envs].
+
+  The precondition [P] is the well-formedness of the compilation
+  environment [mut].
+
+  The postcondition [Q] characterizes the final RTL state [st'].
+  It must have memory state [m'] and register state [rs'] that matches
+  [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)
@@ -911,9 +898,9 @@ Lemma transl_funcall_internal_correct:
   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_correct (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_correct m (Internal f) vargs t 
+  transl_function_prop m (Internal f) vargs t 
                             (outcome_free_mem out m2 sp) vres.
 Proof.
   intros; red; intros.
@@ -976,7 +963,7 @@ 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_correct m (External ef) args t m res.
+  transl_function_prop m (External ef) args t m res.
 Proof.
   intros; red; intros. unfold transl_function in TE; simpl in TE.
   inversion TE; subst tf. 
@@ -985,7 +972,7 @@ Qed.
 
 Lemma transl_stmt_Sskip_correct:
   forall (sp: val) (e : env) (m : mem),
-  transl_stmt_correct sp e m Sskip E0 e m Out_normal.
+  transl_stmt_prop sp e m Sskip E0 e m Out_normal.
 Proof.
   intros; red; intros; inv TE.
   exists rs; econstructor.
@@ -1008,11 +995,11 @@ Lemma transl_stmt_Sseq_continue_correct:
          (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_correct 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_correct sp e1 m1 s2 t2 e2 m2 out ->
+  transl_stmt_prop sp e1 m1 s2 t2 e2 m2 out ->
   t = t1 ** t2 ->
-  transl_stmt_correct sp e m (Sseq s1 s2) t e2 m2 out.
+  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. 
@@ -1027,9 +1014,9 @@ 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_correct sp e m s1 t e1 m1 out ->
+  transl_stmt_prop sp e m s1 t e1 m1 out ->
   out <> Out_normal ->
-  transl_stmt_correct sp e m (Sseq s1 s2) t e1 m1 out.
+  transl_stmt_prop sp e m (Sseq s1 s2) t e1 m1 out.
 Proof.
   intros; red; intros; inv TE.
   exploit H0; eauto. intros [rs1 [st1 [OUT1 [EX1 ME1]]]].
@@ -1038,56 +1025,135 @@ Proof.
   auto.
 Qed.
 
-Lemma transl_stmt_Sexpr_correct:
-  forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
-    (m1 : mem) (v : val),
-  eval_expr ge sp nil e m a t m1 v ->
-  transl_expr_correct sp nil e m a t m1 v ->
-  transl_stmt_correct sp e m (Sexpr a) t e m1 Out_normal.
+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.
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exists rs1; econstructor. 
+  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.
-  eauto.
+  split. eapply star_trans. eexact EX1. eexact EX2. traceEq.
+  congruence. 
 Qed.
 
-Lemma transl_stmt_Sassign_correct:
- forall (sp: val) (e : env) (m : mem) 
-    (id : ident) (a : expr) (t: trace) (m1 : mem) (v : val),
-  eval_expr ge sp nil e m a t m1 v ->
-  transl_expr_correct sp nil e m a t m1 v ->
-  transl_stmt_correct sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal.
+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 H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit tr_move_correct; eauto. intros [rs2 [EX2 [RES2 OTHER2]]].
+  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.
-  split. eapply star_trans. eexact EX1. eexact EX2. traceEq.
-  apply match_env_invariant with (rs1#rv <- v). 
-  apply match_env_update_var; auto. 
-  intros. rewrite Regmap.gsspec. destruct (peq r rv). 
-  subst r. congruence.
+  (* 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.
 
+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.
+  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.
+  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) (t t1: trace) (m1 : mem) 
-    (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (out : outcome),
-  eval_condexpr ge sp nil e m a t1 m1 v1 ->
-  transl_condition_correct sp nil e m a t1 m1 v1 ->
-  exec_stmt ge sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
-  transl_stmt_correct sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
-  t = t1 ** t2 ->
-  transl_stmt_correct sp e m (Sifthenelse a s1 s2) t e2 m2 out.
+  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 H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_stmt code map (if v1 then s1 else s2) (if v1 then ntrue else nfalse) ncont nexits nret rret).
-    destruct v1; auto.
-  exploit H2; eauto. intros [rs2 [st2 [OUT2 [EX2 ME2]]]].
+  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.
@@ -1099,11 +1165,11 @@ Lemma transl_stmt_Sloop_loop_correct:
     (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_correct 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_correct 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_correct sp e m (Sloop sl) t e2 m2 out.
+  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.
@@ -1120,9 +1186,9 @@ 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_correct sp e m sl t e1 m1 out ->
+  transl_stmt_prop sp e m sl t e1 m1 out ->
   out <> Out_normal ->
-  transl_stmt_correct sp e m (Sloop sl) t e1 m1 out.
+  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]]]].
@@ -1135,8 +1201,8 @@ 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_correct sp e m sl t e1 m1 out ->
-  transl_stmt_correct sp e m (Sblock sl) t e1 m1 (outcome_block 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]]]].
@@ -1150,7 +1216,7 @@ Qed.
 
 Lemma transl_stmt_Sexit_correct:
   forall (sp: val) (e : env) (m : mem) (n : nat),
-  transl_stmt_correct sp e m (Sexit n) E0 e m (Out_exit n).
+  transl_stmt_prop sp e m (Sexit n) E0 e m (Out_exit n).
 Proof.
   intros; red; intros; inv TE.
   exists rs; econstructor.
@@ -1195,26 +1261,25 @@ Qed.
 
 Lemma transl_stmt_Sswitch_correct:
   forall (sp : val) (e : env) (m : mem) (a : expr)
-         (cases : list (int * nat)) (default : nat) 
-         (t1 : trace) (m1 : mem) (n : int),
-  eval_expr ge sp nil e m a t1 m1 (Vint n) ->
-  transl_expr_correct sp nil e m a t1 m1 (Vint n) ->
-  transl_stmt_correct sp e m (Sswitch a cases default) t1 e m1
+         (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.
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  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 _ _ _ H4 n). eauto.  
+  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_correct sp e m (Sreturn None) E0 e m (Out_return None).
+  transl_stmt_prop sp e m (Sreturn None) E0 e m (Out_return None).
 Proof.
   intros; red; intros; inv TE.
   exists rs; econstructor.
@@ -1224,14 +1289,13 @@ Proof.
 Qed.
 
 Lemma transl_stmt_Sreturn_some_correct:
-  forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
-    (m1 : mem) (v : val),
-  eval_expr ge sp nil e m a t m1 v ->
-  transl_expr_correct sp nil e m a t m1 v ->
-  transl_stmt_correct sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)).
+  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. 
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+  exploit transl_expr_correct; eauto.
+  intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
   exists rs1; econstructor.
   split. econstructor. reflexivity. auto.
   eauto.
@@ -1239,26 +1303,22 @@ Qed.
 
 Lemma transl_stmt_Stailcall_correct:
   forall (sp : block) (e : env) (m : mem) (sig : signature) (a : expr)
-         (bl : exprlist) (t t1 : trace) (m1 : mem) (t2 : trace) (m2 : mem)
-         (t3 : trace) (m3 : mem) (vf : val) (vargs : list val) (vres : val)
-         (f : CminorSel.fundef),
-  eval_expr ge (Vptr sp Int.zero) nil e m a t1 m1 vf ->
-  transl_expr_correct (Vptr sp Int.zero) nil e m a t1 m1 vf ->
-  eval_exprlist ge (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs ->
-  transl_exprlist_correct (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs ->
+         (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 m2 sp) f vargs t3 m3 vres ->
-  transl_function_correct (free m2 sp) f vargs t3 m3 vres ->
-  t = t1 ** t2 ** t3 ->
-  transl_stmt_correct (Vptr sp Int.zero) e m (Stailcall sig a bl)
-                                       t e m3 (Out_tailcall_return vres).
+  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 H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
+  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 H6; eauto. intro EXF.
+  exploit H4; eauto. intro EXF.
   exists rs2; econstructor. 
   split. constructor. 
   split. 
@@ -1274,41 +1334,25 @@ Proof.
 Qed.
 
 (** The correctness of the translation then follows by application
-  of the mutual induction principle for CminorSel evaluation derivations
+  of the mutual induction principle for Cminor evaluation derivations
   to the lemmas above. *)
 
-Theorem transl_function_correctness:
+Theorem transl_function_correct:
   forall m f vargs t m' vres,
   eval_funcall ge m f vargs t m' vres ->
-  transl_function_correct m f vargs t m' vres.
+  transl_function_prop m f vargs t m' vres.
 Proof
-  (eval_funcall_ind5 ge
-    transl_expr_correct
-    transl_condition_correct
-    transl_exprlist_correct
-    transl_function_correct
-    transl_stmt_correct
-
-    transl_expr_Evar_correct
-    transl_expr_Eop_correct
-    transl_expr_Eload_correct
-    transl_expr_Estore_correct
-    transl_expr_Ecall_correct
-    transl_expr_Econdition_correct
-    transl_expr_Elet_correct
-    transl_expr_Eletvar_correct
-    transl_expr_Ealloc_correct
-    transl_condition_CEtrue_correct
-    transl_condition_CEfalse_correct
-    transl_condition_CEcond_correct
-    transl_condition_CEcondition_correct
-    transl_exprlist_Enil_correct
-    transl_exprlist_Econs_correct
+  (eval_funcall_ind2 ge
+    transl_function_prop
+    transl_stmt_prop
+
     transl_funcall_internal_correct
     transl_funcall_external_correct
     transl_stmt_Sskip_correct
-    transl_stmt_Sexpr_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
@@ -1321,21 +1365,171 @@ Proof
     transl_stmt_Sreturn_some_correct
     transl_stmt_Stailcall_correct).
 
-Require Import Smallstep.
+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).
 
-(** The correctness of the translation follows: if the original CminorSel
-  program executes with trace [t] and exit code [r], then the generated
-  RTL program terminates with the same trace and exit code. *)
+(** ** 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. 
+  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.
+  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.
+  eapply forever_N_plus with (p := size_stmt (fn_body f)).
+  apply plus_one. eapply exec_function_internal; eauto.
+  simpl. eapply STMT; eauto.
+  traceEq.
+Qed.
+
+(** ** Semantic preservation for whole programs. *)
+
+(** 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. *)
 
 Theorem transl_program_correct:
-  forall (t: trace) (r: int),
-  CminorSel.exec_program prog t (Vint r) ->
-  RTL.exec_program tprog (Terminates t r).
+  forall (beh: program_behavior),
+  CminorSel.exec_program prog beh ->
+  RTL.exec_program tprog beh.
 Proof.
-  intros t r [b [f [m [SYMB [FUNC [SIG EVAL]]]]]].
-  generalize (function_ptr_translated _ _ FUNC).
-  intros [tf [TFIND TRANSLF]].
-  exploit transl_function_correctness; eauto. intro EX.
+  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. 
@@ -1347,6 +1541,20 @@ Proof.
   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. 
 Qed.
 
 End CORRECTNESS.