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

7 files changed, 1739 insertions, 1407 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 2b9945ac..1d2eea74 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -9,6 +9,7 @@ Require Import Events.
 Require Import Values.
 Require Import Mem.
 Require Import Globalenvs.
+Require Import Smallstep.
 Require Import Switch.
 
 (** * Abstract syntax *)
@@ -61,12 +62,8 @@ Inductive binary_operation : Set :=
   | Ocmpf: comparison -> binary_operation. (**r float comparison *)
 
 (** Expressions include reading local variables, constants and
-  arithmetic operations, reading and writing store locations,
-  function calls, and conditional expressions
-  (similar to [e1 ? e2 : e3] in C).
-  The [Elet] and [Eletvar] constructs enable sharing the computations
-  of subexpressions.  De Bruijn notation is used: [Eletvar n] refers
-  to the value bound by then [n+1]-th enclosing [Elet] construct. *)
+  arithmetic operations, reading store locations, and conditional
+  expressions (similar to [e1 ? e2 : e3] in C). *)
 
 Inductive expr : Set :=
   | Evar : ident -> expr
@@ -74,26 +71,20 @@ Inductive expr : Set :=
   | Eunop : unary_operation -> expr -> expr
   | Ebinop : binary_operation -> expr -> expr -> expr
   | Eload : memory_chunk -> expr -> expr
-  | Estore : memory_chunk -> expr -> expr -> expr
-  | Ecall : signature -> expr -> exprlist -> expr
-  | Econdition : expr -> expr -> expr -> expr
-  | Elet : expr -> expr -> expr
-  | Eletvar : nat -> expr
-  | Ealloc : expr -> expr
-
-with exprlist : Set :=
-  | Enil: exprlist
-  | Econs: expr -> exprlist -> exprlist.
+  | Econdition : expr -> expr -> expr -> expr.
 
 (** Statements include expression evaluation, assignment to local variables,
-  an if/then/else conditional, infinite loops, blocks and early block
-  exits, and early function returns.  [Sexit n] terminates prematurely
-  the execution of the [n+1] enclosing [Sblock] statements. *)
+  memory stores, function calls, an if/then/else conditional, infinite
+  loops, blocks and early block exits, and early function returns.
+  [Sexit n] terminates prematurely the execution of the [n+1]
+  enclosing [Sblock] statements. *)
 
 Inductive stmt : Set :=
   | Sskip: stmt
-  | Sexpr: expr -> stmt
   | Sassign : ident -> expr -> stmt
+  | Sstore : memory_chunk -> expr -> expr -> stmt
+  | Scall : option ident -> signature -> expr -> list expr -> stmt
+  | Salloc : ident -> expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -101,7 +92,7 @@ Inductive stmt : Set :=
   | Sexit: nat -> stmt
   | Sswitch: expr -> list (int * nat) -> nat -> stmt
   | Sreturn: option expr -> stmt
-  | Stailcall: signature -> expr -> exprlist -> stmt.
+  | Stailcall: signature -> expr -> list expr -> stmt.
 
 (** Functions are composed of a signature, a list of parameter names,
   a list of local variables, and a  statement representing
@@ -163,15 +154,13 @@ Definition outcome_free_mem
   | _ => Mem.free m sp
   end.
 
-(** Three kinds of evaluation environments are involved:
+(** Two kinds of evaluation environments are involved:
 - [genv]: global environments, define symbols and functions;
-- [env]: local environments, map local variables to values;
-- [lenv]: let environments, map de Bruijn indices to values.
+- [env]: local environments, map local variables to values.
 *)
 
 Definition genv := Genv.t fundef.
 Definition env := PTree.t val.
-Definition letenv := list val.
 
 (** The following functions build the initial local environment at
   function entry, binding parameters to the provided arguments and
@@ -190,6 +179,12 @@ Fixpoint set_locals (il: list ident) (e: env) {struct il} : env :=
   | i1 :: is => PTree.set i1 Vundef (set_locals is e)
   end.
 
+Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
+  match optid with
+  | None => e
+  | Some id => PTree.set id v e
+  end.
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -288,112 +283,62 @@ Definition eval_binop
   | _, _, _ => None
   end.
 
-(** Evaluation of an expression: [eval_expr ge sp le e m a t m' v]
-  states that expression [a], in initial local environment [e] and
-  memory state [m], evaluates to value [v].  [m'] is the final
-  memory state, reflecting memory stores possibly performed by [a].
-  [t] is the trace of I/O events generated during the evaluation.
-  Expressions do not assign variables, therefore the local environment
-  [e] is unchanged.  [ge] and [le] are the global environment and let
-  environment respectively, and are unchanged during evaluation.  [sp]
-  is the pointer to the memory block allocated for this function
+(** Evaluation of an expression: [eval_expr ge sp e m a v]
+  states that expression [a] evaluates to value [v].
+  [ge] is the global environment, [e] the local environment,
+  and [m] the current memory state.  They are unchanged during evaluation.
+  [sp] is the pointer to the memory block allocated for this function
   (stack frame).
 *)
 
-Inductive eval_expr:
-         val -> letenv -> env ->
-         mem -> expr -> trace -> mem -> val -> Prop :=
-  | eval_Evar:
-      forall sp le e m id v,
+Section EVAL_EXPR.
+
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+Inductive eval_expr: expr -> val -> Prop :=
+  | eval_Evar: forall id v,
       PTree.get id e = Some v ->
-      eval_expr sp le e m (Evar id) E0 m v
-  | eval_Econst:
-      forall sp le e m cst v,
+      eval_expr (Evar id) v
+  | eval_Econst: forall cst v,
       eval_constant sp cst = Some v ->
-      eval_expr sp le e m (Econst cst) E0 m v
-  | eval_Eunop:
-      forall sp le e m op a t m1 v1 v,
-      eval_expr sp le e m a t m1 v1 ->
+      eval_expr (Econst cst) v
+  | eval_Eunop: forall op a1 v1 v,
+      eval_expr a1 v1 ->
       eval_unop op v1 = Some v ->
-      eval_expr sp le e m (Eunop op a) t m1 v
-  | eval_Ebinop:
-      forall sp le e m op a1 a2 t1 m1 v1 t2 m2 v2 t v,
-      eval_expr sp le e m a1 t1 m1 v1 ->
-      eval_expr sp le e m1 a2 t2 m2 v2 ->
-      eval_binop op v1 v2 m2 = Some v ->
-      t = t1 ** t2 ->
-      eval_expr sp le e m (Ebinop op a1 a2) t m2 v
-  | eval_Eload:
-      forall sp le e m chunk a t m1 v1 v,
-      eval_expr sp le e m a t m1 v1 ->
-      Mem.loadv chunk m1 v1 = Some v ->
-      eval_expr sp le e m (Eload chunk a) t m1 v
-  | eval_Estore:
-      forall sp le e m chunk a1 a2 t t1 m1 v1 t2 m2 v2 m3,
-      eval_expr sp le e m a1 t1 m1 v1 ->
-      eval_expr sp le e m1 a2 t2 m2 v2 ->
-      Mem.storev chunk m2 v1 v2 = Some m3 ->
-      t = t1 ** t2 ->
-      eval_expr sp le e m (Estore chunk a1 a2) t m3 v2
-  | eval_Ecall:
-      forall sp le e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f,
-      eval_expr sp le e m a t1 m1 vf ->
-      eval_exprlist sp le e m1 bl t2 m2 vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall m2 f vargs t3 m3 vres ->
-      t = t1 ** t2 ** t3 ->
-      eval_expr sp le e m (Ecall sig a bl) t m3 vres
-  | eval_Econdition:
-      forall sp le e m a1 a2 a3 t t1 m1 v1 b1 t2 m2 v2,
-      eval_expr sp le e m a1 t1 m1 v1 ->
+      eval_expr (Eunop op a1) v
+  | eval_Ebinop: forall op a1 a2 v1 v2 v,
+      eval_expr a1 v1 ->
+      eval_expr a2 v2 ->
+      eval_binop op v1 v2 m = Some v ->
+      eval_expr (Ebinop op a1 a2) v
+  | eval_Eload: forall chunk addr vaddr v,
+      eval_expr addr vaddr ->
+      Mem.loadv chunk m vaddr = Some v ->     
+      eval_expr (Eload chunk addr) v
+  | eval_Econdition: forall a1 a2 a3 v1 b1 v2,
+      eval_expr a1 v1 ->
       Val.bool_of_val v1 b1 ->
-      eval_expr sp le e m1 (if b1 then a2 else a3) t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr sp le e m (Econdition a1 a2 a3) t m2 v2
-  | eval_Elet:
-      forall sp le e m a b t t1 m1 v1 t2 m2 v2,
-      eval_expr sp le e m a t1 m1 v1 ->
-      eval_expr sp (v1::le) e m1 b t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr sp le e m (Elet a b) t m2 v2
-  | eval_Eletvar:
-      forall sp le e m n v,
-      nth_error le n = Some v ->
-      eval_expr sp le e m (Eletvar n) E0 m v
-  | eval_Ealloc:
-      forall sp le e m a t m1 n m2 b,
-      eval_expr sp le e m a t m1 (Vint n) ->
-      Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
-      eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero)
-
-(** Evaluation of a list of expressions:
-  [eval_exprlist ge sp le al m a m' vl]
-  states that the list [al] of expressions evaluate 
-  to the list [vl] of values.
-  The other parameters are as in [eval_expr].
-*)
+      eval_expr (if b1 then a2 else a3) v2 ->
+      eval_expr (Econdition a1 a2 a3) v2.
 
-with eval_exprlist:
-         val -> letenv -> env ->
-         mem -> exprlist -> trace -> mem -> list val -> Prop :=
+Inductive eval_exprlist: list expr -> list val -> Prop :=
   | eval_Enil:
-      forall sp le e m,
-      eval_exprlist sp le e m Enil E0 m nil
-  | eval_Econs:
-      forall sp le e m a bl t t1 m1 v t2 m2 vl,
-      eval_expr sp le e m a t1 m1 v ->
-      eval_exprlist sp le e m1 bl t2 m2 vl ->
-      t = t1 ** t2 ->
-      eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl)
+      eval_exprlist nil nil
+  | eval_Econs: forall a1 al v1 vl,
+      eval_expr a1 v1 -> eval_exprlist al vl ->
+      eval_exprlist (a1 :: al) (v1 :: vl).
+
+End EVAL_EXPR.
 
-(** Evaluation of a function invocation: [eval_funcall ge m f args m' res]
+(** Evaluation of a function invocation: [eval_funcall ge m f args t m' res]
   means that the function [f], applied to the arguments [args] in
   memory state [m], returns the value [res] in modified memory state [m'].
   [t] is the trace of observable events generated during the invocation.
 *)
 
-with eval_funcall:
+Inductive eval_funcall:
         mem -> fundef -> list val -> trace ->
         mem -> val -> Prop :=
   | eval_funcall_internal:
@@ -408,12 +353,13 @@ with eval_funcall:
       event_match ef args t res ->
       eval_funcall m (External ef) args t m res
 
-(** Execution of a statement: [exec_stmt ge sp e m s e' m' out]
+(** Execution of a statement: [exec_stmt ge sp e m s t e' m' out]
   means that statement [s] executes with outcome [out].
   [e] is the initial environment and [m] is the initial memory state.
   [e'] is the final environment, reflecting variable assignments performed
   by [s].  [m'] is the final memory state, reflecting memory stores
-  performed by [s].  The other parameters are as in [eval_expr]. *)
+  performed by [s].  [t] is the trace of I/O events performed during
+  the execution.  The other parameters are as in [eval_expr]. *)
 
 with exec_stmt:
          val ->
@@ -422,21 +368,37 @@ with exec_stmt:
   | exec_Sskip:
       forall sp e m,
       exec_stmt sp e m Sskip E0 e m Out_normal
-  | exec_Sexpr:
-      forall sp e m a t m1 v,
-      eval_expr sp nil e m a t m1 v ->
-      exec_stmt sp e m (Sexpr a) t e m1 Out_normal
   | exec_Sassign:
-      forall sp e m id a t m1 v,
-      eval_expr sp nil e m a t m1 v ->
-      exec_stmt sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal
+      forall sp e m id a v,
+      eval_expr sp e m a v ->
+      exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
+  | exec_Sstore:
+      forall sp e m chunk addr a vaddr v m',
+      eval_expr sp e m addr vaddr ->
+      eval_expr sp e m a v ->
+      Mem.storev chunk m vaddr v = Some m' ->
+      exec_stmt sp e m (Sstore chunk addr a) E0 e m' Out_normal
+  | exec_Scall:
+      forall sp e m optid sig a bl vf vargs f t m' vres e',
+      eval_expr sp e m a vf ->
+      eval_exprlist sp e m bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      eval_funcall m f vargs t m' vres ->
+      e' = set_optvar optid vres e ->
+      exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal
+  | exec_Salloc:
+      forall sp e m id a n m' b,
+      eval_expr sp e m a (Vint n) ->
+      Mem.alloc m 0 (Int.signed n) = (m', b) ->
+      exec_stmt sp e m (Salloc id a) 
+                E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal
   | exec_Sifthenelse:
-      forall sp e m a s1 s2 t t1 m1 v1 b1 t2 e2 m2 out,
-      eval_expr sp nil e m a t1 m1 v1 ->
-      Val.bool_of_val v1 b1 ->
-      exec_stmt sp e m1 (if b1 then s1 else s2) t2 e2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt sp e m (Sifthenelse a s1 s2) t e2 m2 out
+      forall sp e m a s1 s2 v b t e' m' out,
+      eval_expr sp e m a v ->
+      Val.bool_of_val v b ->
+      exec_stmt sp e m (if b then s1 else s2) t e' m' out ->
+      exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out
   | exec_Sseq_continue:
       forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
       exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
@@ -467,46 +429,121 @@ with exec_stmt:
       forall sp e m n,
       exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
   | exec_Sswitch:
-      forall sp e m a cases default t1 m1 n,
-      eval_expr sp nil e m a t1 m1 (Vint n) ->
+      forall sp e m a cases default n,
+      eval_expr sp e m a (Vint n) ->
       exec_stmt sp e m (Sswitch a cases default)
-                t1 e m1 (Out_exit (switch_target n default cases))
+                E0 e m (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
       forall sp e m,
       exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
   | exec_Sreturn_some:
-      forall sp e m a t m1 v,
-      eval_expr sp nil e m a t m1 v ->
-      exec_stmt sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v))
+      forall sp e m a v,
+      eval_expr sp e m a v ->
+      exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
   | exec_Stailcall:
-      forall sp e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f,
-      eval_expr (Vptr sp Int.zero) nil e m a t1 m1 vf ->
-      eval_exprlist (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs ->
+      forall sp e m sig a bl vf vargs f t m' vres,
+      eval_expr (Vptr sp Int.zero) e m a vf ->
+      eval_exprlist (Vptr sp Int.zero) e m bl vargs ->
       Genv.find_funct ge vf = Some f ->
       funsig f = sig ->
-      eval_funcall (Mem.free m2 sp) f vargs t3 m3 vres ->
-      t = t1 ** t2 ** t3 ->
-      exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m3 (Out_tailcall_return vres).
+      eval_funcall (Mem.free m sp) f vargs t m' vres ->
+      exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres).
 
-Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop
-  with eval_exprlist_ind4 := Minimality for eval_exprlist Sort Prop
-  with eval_funcall_ind4 := Minimality for eval_funcall Sort Prop
-  with exec_stmt_ind4 := Minimality for exec_stmt Sort Prop.
-
-End RELSEM.
+Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
+  with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop.
 
-(** Execution of a whole program: [exec_program p t r]
-  holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] performs the input/output
-  operations described in the trace [t], and eventually returns value [r].
+(** Coinductive semantics for divergence.
+  [evalinf_funcall ge m f args t]
+  means that the function [f] diverges when applied to the arguments [args] in
+  memory state [m].  The infinite trace [t] is the trace of
+  observable events generated during the invocation.
 *)
 
-Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := Genv.globalenv p in
-  let m0 := Genv.init_mem p in
-  exists b, exists f, exists m,
-  Genv.find_symbol ge p.(prog_main) = Some b /\
-  Genv.find_funct_ptr ge b = Some f /\
-  funsig f = mksignature nil (Some Tint) /\
-  eval_funcall ge m0 f nil t m r.
+CoInductive evalinf_funcall:
+        mem -> fundef -> list val -> traceinf -> Prop :=
+  | evalinf_funcall_internal:
+      forall m f vargs m1 sp e t,
+      Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
+      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
+      execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t ->
+      evalinf_funcall m (Internal f) vargs t
+
+(** [execinf_stmt ge sp e m s t] means that statement [s] diverges.
+  [e] is the initial environment, [m] is the initial memory state,
+  and [t] the trace of observable events performed during the execution. *)
+
+with execinf_stmt:
+         val -> env -> mem -> stmt -> traceinf -> Prop :=
+  | execinf_Scall:
+      forall sp e m optid sig a bl vf vargs f t,
+      eval_expr sp e m a vf ->
+      eval_exprlist sp e m bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      evalinf_funcall m f vargs t ->
+      execinf_stmt sp e m (Scall optid sig a bl) t
+  | execinf_Sifthenelse:
+      forall sp e m a s1 s2 v b t,
+      eval_expr sp e m a v ->
+      Val.bool_of_val v b ->
+      execinf_stmt sp e m (if b then s1 else s2) t ->
+      execinf_stmt sp e m (Sifthenelse a s1 s2) t
+  | execinf_Sseq_1:
+      forall sp e m t s1 s2,
+      execinf_stmt sp e m s1 t ->
+      execinf_stmt sp e m (Sseq s1 s2) t
+  | execinf_Sseq_2:
+      forall sp e m t s1 t1 e1 m1 s2 t2,
+      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
+      execinf_stmt sp e1 m1 s2 t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt sp e m (Sseq s1 s2) t
+  | execinf_Sloop_body:
+      forall sp e m s t,
+      execinf_stmt sp e m s t ->
+      execinf_stmt sp e m (Sloop s) t
+  | execinf_Sloop_loop:
+      forall sp e m s t t1 e1 m1 t2,
+      exec_stmt sp e m s t1 e1 m1 Out_normal ->
+      execinf_stmt sp e1 m1 (Sloop s) t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt sp e m (Sloop s) t
+  | execinf_Sblock:
+      forall sp e m s t,
+      execinf_stmt sp e m s t ->
+      execinf_stmt sp e m (Sblock s) t
+  | execinf_Stailcall:
+      forall sp e m sig a bl vf vargs f t,
+      eval_expr (Vptr sp Int.zero) e m a vf ->
+      eval_exprlist (Vptr sp Int.zero) e m bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      evalinf_funcall (Mem.free m sp) f vargs t ->
+      execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t.
+
+End RELSEM.
 
+(** Execution of a whole program: [exec_program p beh]
+  holds if the application of [p]'s main function to no arguments
+  in the initial memory state for [p] has [beh] as observable
+  behavior. *)
+
+Inductive exec_program (p: program): program_behavior -> Prop :=
+  | program_terminates:
+      forall b f t m r,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      eval_funcall ge m0 f nil t m (Vint r) ->
+      exec_program p (Terminates t r)
+  | program_diverges:
+      forall b f t,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      evalinf_funcall ge m0 f nil t ->
+      exec_program p (Diverges t).
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 331105ea..859c46e7 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -12,6 +12,7 @@ Require Import Cminor.
 Require Import Op.
 Require Import Globalenvs.
 Require Import Switch.
+Require Import Smallstep.
 
 (** * Abstract syntax *)
 
@@ -19,7 +20,10 @@ Require Import Switch.
   functions, statements and expressions.  However, CminorSel uses
   machine-dependent operations, addressing modes and conditions,
   as defined in module [Op] and used in lower-level intermediate
-  languages ([RTL] and below).  Moreover, a variant [condexpr] of [expr]
+  languages ([RTL] and below).  Moreover, to express sharing of
+  sub-computations, a "let" binding is provided (constructions
+  [Elet] and [Eletvar]), using de Bruijn indices to refer to "let"-bound
+  variables.  Finally, a variant [condexpr] of [expr]
   is used to represent expressions which are evaluated for their
   boolean value only and not their exact value.
 *)
@@ -28,12 +32,9 @@ Inductive expr : Set :=
   | Evar : ident -> expr
   | Eop : operation -> exprlist -> expr
   | Eload : memory_chunk -> addressing -> exprlist -> expr
-  | Estore : memory_chunk -> addressing -> exprlist -> expr -> expr
-  | Ecall : signature -> expr -> exprlist -> expr
   | Econdition : condexpr -> expr -> expr -> expr
   | Elet : expr -> expr -> expr
   | Eletvar : nat -> expr
-  | Ealloc : expr -> expr
 
 with condexpr : Set :=
   | CEtrue: condexpr
@@ -46,12 +47,15 @@ with exprlist : Set :=
   | Econs: expr -> exprlist -> exprlist.
 
 (** Statements are as in Cminor, except that the condition of an
-  if/then/else conditional is a [condexpr]. *)
+  if/then/else conditional is a [condexpr], and the [Sstore] construct
+  uses a machine-dependent addressing mode. *)
 
 Inductive stmt : Set :=
   | Sskip: stmt
-  | Sexpr: expr -> stmt
   | Sassign : ident -> expr -> stmt
+  | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
+  | Scall : option ident -> signature -> expr -> exprlist -> stmt
+  | Salloc : ident -> expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -87,6 +91,7 @@ Definition funsig (fd: fundef) :=
 *)
 
 Definition genv := Genv.t fundef.
+Definition letenv := list val.
 
 Section RELSEM.
 
@@ -96,101 +101,68 @@ Variable ge: genv.
     of Cminor.  Refer to the description of Cminor semantics for
     the meaning of the parameters of the predicates.
     One additional predicate is introduced:
-    [eval_condexpr ge sp le e m a t m' b], meaning that the conditional
+    [eval_condexpr ge sp e m le a b], meaning that the conditional
     expression [a] evaluates to the boolean [b]. *)
 
-Inductive eval_expr:
-         val -> letenv -> env ->
-         mem -> expr -> trace -> mem -> val -> Prop :=
-  | eval_Evar:
-      forall sp le e m id v,
+Section EVAL_EXPR.
+
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+Inductive eval_expr: letenv -> expr -> val -> Prop :=
+  | eval_Evar: forall le id v,
       PTree.get id e = Some v ->
-      eval_expr sp le e m (Evar id) E0 m v
-  | eval_Eop:
-      forall sp le e m op al t m1 vl v,
-      eval_exprlist sp le e m al t m1 vl ->
-      eval_operation ge sp op vl m1 = Some v ->
-      eval_expr sp le e m (Eop op al) t m1 v
-  | eval_Eload:
-      forall sp le e m chunk addr al t m1 v vl a,
-      eval_exprlist sp le e m al t m1 vl ->
-      eval_addressing ge sp addr vl = Some a ->
-      Mem.loadv chunk m1 a = Some v ->
-      eval_expr sp le e m (Eload chunk addr al) t m1 v
-  | eval_Estore:
-      forall sp le e m chunk addr al b t t1 m1 vl t2 m2 m3 v a,
-      eval_exprlist sp le e m al t1 m1 vl ->
-      eval_expr 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 ->
-      eval_expr sp le e m (Estore chunk addr al b) t m3 v
-  | eval_Ecall:
-      forall sp le e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f,
-      eval_expr sp le e m a t1 m1 vf ->
-      eval_exprlist sp le e m1 bl t2 m2 vargs ->
-      Genv.find_funct ge vf = Some f ->
-      funsig f = sig ->
-      eval_funcall m2 f vargs t3 m3 vres ->
-      t = t1 ** t2 ** t3 ->
-      eval_expr sp le e m (Ecall sig a bl) t m3 vres
-  | eval_Econdition:
-      forall sp le e m a b c t t1 m1 v1 t2 m2 v2,
-      eval_condexpr sp le e m a t1 m1 v1 ->
-      eval_expr sp le e m1 (if v1 then b else c) t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr sp le e m (Econdition a b c) t m2 v2
-  | eval_Elet:
-      forall sp le e m a b t t1 m1 v1 t2 m2 v2,
-      eval_expr sp le e m a t1 m1 v1 ->
-      eval_expr sp (v1::le) e m1 b t2 m2 v2 ->
-      t = t1 ** t2 ->
-      eval_expr sp le e m (Elet a b) t m2 v2
-  | eval_Eletvar:
-      forall sp le e m n v,
+      eval_expr le (Evar id) v
+  | eval_Eop: forall le op al vl v,
+      eval_exprlist le al vl ->
+      eval_operation ge sp op vl m = Some v ->
+      eval_expr le (Eop op al) v
+  | eval_Eload: forall le chunk addr al vl vaddr v,
+      eval_exprlist le al vl ->
+      eval_addressing ge sp addr vl = Some vaddr ->
+      Mem.loadv chunk m vaddr = Some v ->     
+      eval_expr le (Eload chunk addr al) v
+  | eval_Econdition: forall le a b c v1 v2,
+      eval_condexpr le a v1 ->
+      eval_expr le (if v1 then b else c) v2 ->
+      eval_expr le (Econdition a b c) v2
+  | eval_Elet: forall le a b v1 v2,
+      eval_expr le a v1 ->
+      eval_expr (v1 :: le) b v2 ->
+      eval_expr le (Elet a b) v2
+  | eval_Eletvar: forall le n v,
       nth_error le n = Some v ->
-      eval_expr sp le e m (Eletvar n) E0 m v
-  | eval_Ealloc:
-      forall sp le e m a t m1 n m2 b,
-      eval_expr sp le e m a t m1 (Vint n) ->
-      Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
-      eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero)
-
-with eval_condexpr:
-         val -> letenv -> env ->
-         mem -> condexpr -> trace -> mem -> bool -> Prop :=
-  | eval_CEtrue:
-      forall sp le e m,
-      eval_condexpr sp le e m CEtrue E0 m true
-  | eval_CEfalse:
-      forall sp le e m,
-      eval_condexpr sp le e m CEfalse E0 m false
-  | eval_CEcond:
-      forall sp le e m cond al t1 m1 vl b,
-      eval_exprlist sp le e m al t1 m1 vl ->
-      eval_condition cond vl m1 = Some b ->
-      eval_condexpr sp le e m (CEcond cond al) t1 m1 b
-  | eval_CEcondition:
-      forall sp le e m a b c t t1 m1 vb1 t2 m2 vb2,
-      eval_condexpr sp le e m a t1 m1 vb1 ->
-      eval_condexpr sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
-      t = t1 ** t2 ->
-      eval_condexpr sp le e m (CEcondition a b c) t m2 vb2
-
-with eval_exprlist:
-         val -> letenv -> env ->
-         mem -> exprlist -> trace -> mem -> list val -> Prop :=
-  | eval_Enil:
-      forall sp le e m,
-      eval_exprlist sp le e m Enil E0 m nil
-  | eval_Econs:
-      forall sp le e m a bl t t1 m1 v t2 m2 vl,
-      eval_expr sp le e m a t1 m1 v ->
-      eval_exprlist sp le e m1 bl t2 m2 vl ->
-      t = t1 ** t2 ->
-      eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl)
+      eval_expr le (Eletvar n) v
+
+with eval_condexpr: letenv -> condexpr -> bool -> Prop :=
+  | eval_CEtrue: forall le,
+      eval_condexpr le CEtrue true
+  | eval_CEfalse: forall le,
+      eval_condexpr le CEfalse false
+  | eval_CEcond: forall le cond al vl b,
+      eval_exprlist le al vl ->
+      eval_condition cond vl m = Some b ->
+      eval_condexpr le (CEcond cond al) b
+  | eval_CEcondition: forall le a b c vb1 vb2,
+      eval_condexpr le a vb1 ->
+      eval_condexpr le (if vb1 then b else c) vb2 ->
+      eval_condexpr le (CEcondition a b c) vb2
+
+with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
+  | eval_Enil: forall le,
+      eval_exprlist le Enil nil
+  | eval_Econs: forall le a1 al v1 vl,
+      eval_expr le a1 v1 -> eval_exprlist le al vl ->
+      eval_exprlist le (Econs a1 al) (v1 :: vl).
 
-with eval_funcall:
+Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop
+  with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop
+  with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop.
+
+End EVAL_EXPR.
+
+Inductive eval_funcall:
         mem -> fundef -> list val -> trace ->
         mem -> val -> Prop :=
   | eval_funcall_internal:
@@ -212,20 +184,37 @@ with exec_stmt:
   | exec_Sskip:
       forall sp e m,
       exec_stmt sp e m Sskip E0 e m Out_normal
-  | exec_Sexpr:
-      forall sp e m a t m1 v,
-      eval_expr sp nil e m a t m1 v ->
-      exec_stmt sp e m (Sexpr a) t e m1 Out_normal
   | exec_Sassign:
-      forall sp e m id a t m1 v,
-      eval_expr sp nil e m a t m1 v ->
-      exec_stmt sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal
+      forall sp e m id a v,
+      eval_expr sp e m nil a v ->
+      exec_stmt sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
+  | exec_Sstore:
+      forall sp e m chunk addr al b vl v vaddr m',
+      eval_exprlist sp e m nil al vl ->
+      eval_expr sp e m nil b v ->
+      eval_addressing ge sp addr vl = Some vaddr ->
+      Mem.storev chunk m vaddr v = Some m' ->
+      exec_stmt sp e m (Sstore chunk addr al b) E0 e m' Out_normal
+  | exec_Scall:
+      forall sp e m optid sig a bl vf vargs f t m' vres e',
+      eval_expr sp e m nil a vf ->
+      eval_exprlist sp e m nil bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      eval_funcall m f vargs t m' vres ->
+      e' = set_optvar optid vres e ->
+      exec_stmt sp e m (Scall optid sig a bl) t e' m' Out_normal
+  | exec_Salloc:
+      forall sp e m id a n m' b,
+      eval_expr sp e m nil a (Vint n) ->
+      Mem.alloc m 0 (Int.signed n) = (m', b) ->
+      exec_stmt sp e m (Salloc id a) 
+                E0 (PTree.set id (Vptr b Int.zero) e) m' Out_normal
   | exec_Sifthenelse:
-      forall sp e m a s1 s2 t t1 m1 v1 t2 e2 m2 out,
-      eval_condexpr sp nil e m a t1 m1 v1 ->
-      exec_stmt sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
-      t = t1 ** t2 ->
-      exec_stmt sp e m (Sifthenelse a s1 s2) t e2 m2 out
+      forall sp e m a s1 s2 v t e' m' out,
+      eval_condexpr sp e m nil a v ->
+      exec_stmt sp e m (if v then s1 else s2) t e' m' out ->
+      exec_stmt sp e m (Sifthenelse a s1 s2) t e' m' out
   | exec_Sseq_continue:
       forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
       exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
@@ -256,41 +245,115 @@ with exec_stmt:
       forall sp e m n,
       exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
   | exec_Sswitch:
-      forall sp e m a cases default t1 m1 n,
-      eval_expr sp nil e m a t1 m1 (Vint n) ->
+      forall sp e m a cases default n,
+      eval_expr sp e m nil a (Vint n) ->
       exec_stmt sp e m (Sswitch a cases default)
-                t1 e m1 (Out_exit (switch_target n default cases))
+                E0 e m (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
       forall sp e m,
       exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
   | exec_Sreturn_some:
-      forall sp e m a t m1 v,
-      eval_expr sp nil e m a t m1 v ->
-      exec_stmt sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v))
+      forall sp e m a v,
+      eval_expr sp e m nil a v ->
+      exec_stmt sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
   | exec_Stailcall:
-      forall sp e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f,
-      eval_expr (Vptr sp Int.zero) nil e m a t1 m1 vf ->
-      eval_exprlist (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs ->
+      forall sp e m sig a bl vf vargs f t m' vres,
+      eval_expr (Vptr sp Int.zero) e m nil a vf ->
+      eval_exprlist (Vptr sp Int.zero) e m nil bl vargs ->
       Genv.find_funct ge vf = Some f ->
       funsig f = sig ->
-      eval_funcall (Mem.free m2 sp) f vargs t3 m3 vres ->
-      t = t1 ** t2 ** t3 ->
-      exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m3 (Out_tailcall_return vres).
+      eval_funcall (Mem.free m sp) f vargs t m' vres ->
+      exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m' (Out_tailcall_return vres).
+
+Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
+  with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop.
+
+(** Coinductive semantics for divergence. *)
+
+CoInductive evalinf_funcall:
+        mem -> fundef -> list val -> traceinf -> Prop :=
+  | evalinf_funcall_internal:
+      forall m f vargs m1 sp e t,
+      Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
+      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
+      execinf_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t ->
+      evalinf_funcall m (Internal f) vargs t
 
-Scheme eval_expr_ind5 := Minimality for eval_expr Sort Prop
-  with eval_condexpr_ind5 := Minimality for eval_condexpr Sort Prop
-  with eval_exprlist_ind5 := Minimality for eval_exprlist Sort Prop
-  with eval_funcall_ind5 := Minimality for eval_funcall Sort Prop
-  with exec_stmt_ind5 := Minimality for exec_stmt Sort Prop.
+(** [execinf_stmt ge sp e m s t] means that statement [s] diverges.
+  [e] is the initial environment, [m] is the initial memory state,
+  and [t] the trace of observable events performed during the execution. *)
+
+with execinf_stmt:
+         val -> env -> mem -> stmt -> traceinf -> Prop :=
+  | execinf_Scall:
+      forall sp e m optid sig a bl vf vargs f t,
+      eval_expr sp e m nil a vf ->
+      eval_exprlist sp e m nil bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      evalinf_funcall m f vargs t ->
+      execinf_stmt sp e m (Scall optid sig a bl) t
+  | execinf_Sifthenelse:
+      forall sp e m a s1 s2 v t,
+      eval_condexpr sp e m nil a v ->
+      execinf_stmt sp e m (if v then s1 else s2) t ->
+      execinf_stmt sp e m (Sifthenelse a s1 s2) t
+  | execinf_Sseq_1:
+      forall sp e m t s1 s2,
+      execinf_stmt sp e m s1 t ->
+      execinf_stmt sp e m (Sseq s1 s2) t
+  | execinf_Sseq_2:
+      forall sp e m t s1 t1 e1 m1 s2 t2,
+      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
+      execinf_stmt sp e1 m1 s2 t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt sp e m (Sseq s1 s2) t
+  | execinf_Sloop_body:
+      forall sp e m s t,
+      execinf_stmt sp e m s t ->
+      execinf_stmt sp e m (Sloop s) t
+  | execinf_Sloop_loop:
+      forall sp e m s t t1 e1 m1 t2,
+      exec_stmt sp e m s t1 e1 m1 Out_normal ->
+      execinf_stmt sp e1 m1 (Sloop s) t2 ->
+      t = t1 *** t2 ->
+      execinf_stmt sp e m (Sloop s) t
+  | execinf_Sblock:
+      forall sp e m s t,
+      execinf_stmt sp e m s t ->
+      execinf_stmt sp e m (Sblock s) t
+  | execinf_Stailcall:
+      forall sp e m sig a bl vf vargs f t,
+      eval_expr (Vptr sp Int.zero) e m nil a vf ->
+      eval_exprlist (Vptr sp Int.zero) e m nil bl vargs ->
+      Genv.find_funct ge vf = Some f ->
+      funsig f = sig ->
+      evalinf_funcall (Mem.free m sp) f vargs t ->
+      execinf_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t.
 
 End RELSEM.
 
-Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := Genv.globalenv p in
-  let m0 := Genv.init_mem p in
-  exists b, exists f, exists m,
-  Genv.find_symbol ge p.(prog_main) = Some b /\
-  Genv.find_funct_ptr ge b = Some f /\
-  funsig f = mksignature nil (Some Tint) /\
-  eval_funcall ge m0 f nil t m r.
+(** Execution of a whole program: [exec_program p beh]
+  holds if the application of [p]'s main function to no arguments
+  in the initial memory state for [p] has [beh] as observable
+  behavior. *)
 
+Inductive exec_program (p: program): program_behavior -> Prop :=
+  | program_terminates:
+      forall b f t m r,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      eval_funcall ge m0 f nil t m (Vint r) ->
+      exec_program p (Terminates t r)
+  | program_diverges:
+      forall b f t,
+      let ge := Genv.globalenv p in
+      let m0 := Genv.init_mem p in
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = mksignature nil (Some Tint) ->
+      evalinf_funcall ge m0 f nil t ->
+      exec_program p (Diverges t).
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 117631ef..2fe13e5c 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -266,17 +266,6 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do rl <- alloc_regs map al;
       do no <- add_instr (Iload chunk addr rl rd nd);
          transl_exprlist map al rl no
-  | Estore chunk addr al b =>
-      do rl <- alloc_regs map al;
-      do no <- add_instr (Istore chunk addr rl rd nd);
-      do ns <- transl_expr map b rd no;
-         transl_exprlist map al rl ns
-  | Ecall sig b cl =>
-      do rf <- alloc_reg map b;
-      do rargs <- alloc_regs map cl;
-      do n1 <- add_instr (Icall sig (inl _ rf) rargs rd nd);
-      do n2 <- transl_exprlist map cl rargs n1;
-         transl_expr map b rf n2
   | Econdition b c d =>
       do nfalse <- transl_expr map d rd nd;
       do ntrue  <- transl_expr map c rd nd;
@@ -287,10 +276,6 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
          transl_expr map b r nc
   | Eletvar n =>
       do r <- find_letvar map n; add_move r rd nd
-  | Ealloc a =>
-      do r <- alloc_reg map a;
-      do no <- add_instr (Ialloc r rd nd);
-         transl_expr map a r no
   end
 
 (** Translation of a conditional expression.  Similar to [transl_expr],
@@ -329,6 +314,20 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
       error node (Errors.msg "RTLgen.transl_exprlist")
   end.
 
+(** Generation of code for variable assignments. *)
+
+Definition store_var
+       (map: mapping) (rs: reg) (id: ident) (nd: node) : mon node :=
+  do rv <- find_var map id;
+  add_move rs rv nd.
+
+Definition store_optvar
+       (map: mapping) (rs: reg) (optid: option ident) (nd: node) : mon node :=
+  match optid with
+  | None => ret nd
+  | Some id => store_var map rs id nd
+  end.
+
 (** Auxiliary for branch prediction.  When compiling an if/then/else
   statement, we have a choice between translating the ``then'' branch
   first or the ``else'' branch first.  Linearization of RTL control-flow
@@ -379,13 +378,30 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   match s with
   | Sskip =>
       ret nd
-  | Sexpr a =>
-      do r <- alloc_reg map a; transl_expr map a r nd
   | Sassign v b =>
-      do rv <- find_var map v;
       do rt <- alloc_reg map b;
-      do no <- add_move rt rv nd;
+      do no <- store_var map rt v nd;
       transl_expr map b rt no
+  | Sstore chunk addr al b =>
+      do rl <- alloc_regs map al;
+      do r <- alloc_reg map b;
+      do no <- add_instr (Istore chunk addr rl r nd);
+      do ns <- transl_expr map b r no;
+         transl_exprlist map al rl ns
+  | Scall optid sig b cl =>
+      do rf <- alloc_reg map b;
+      do rargs <- alloc_regs map cl;
+      do r <- new_reg;
+      do n1 <- store_optvar map r optid nd;
+      do n2 <- add_instr (Icall sig (inl _ rf) rargs r n1);
+      do n3 <- transl_exprlist map cl rargs n2;
+         transl_expr map b rf n3
+  | Salloc id a =>
+      do ra <- alloc_reg map a;
+      do rr <- new_reg;
+      do n1 <- store_var map rr id nd;
+      do n2 <- add_instr (Ialloc ra rr n1);
+         transl_expr map a ra n2
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits nret rret;
       transl_stmt map s1 ns nexits nret rret
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 15f305a8..e9a04fcc 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.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index c46bdbba..a291d321 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -799,17 +799,6 @@ Inductive tr_expr (c: code):
       c!n1 = Some (Iload chunk addr rl rd nd) ->
       ~reg_in_map map rd -> ~In rd pr ->
       tr_expr c map pr (Eload chunk addr al) ns nd rd
-  | tr_Estore: forall map pr chunk addr al b ns nd rd n1 rl n2,
-      tr_exprlist c map pr al ns n1 rl ->
-      tr_expr c map (rl ++ pr) b n1 n2 rd ->
-      c!n2 = Some (Istore chunk addr rl rd nd) ->
-      tr_expr c map pr (Estore chunk addr al b) ns nd rd
-  | tr_Ecall: forall map pr sig b cl ns nd rd n1 rf n2 rargs,
-      tr_expr c map pr b ns n1 rf ->
-      tr_exprlist c map (rf :: pr) cl n1 n2 rargs ->
-      c!n2 = Some (Icall sig (inl _ rf) rargs rd nd) ->
-      ~reg_in_map map rd -> ~In rd pr ->
-      tr_expr c map pr (Ecall sig b cl) ns nd rd
   | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse,
       tr_condition c map pr b ns ntrue nfalse ->
       tr_expr c map pr ifso ntrue nd rd ->
@@ -825,13 +814,8 @@ Inductive tr_expr (c: code):
       (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) ->
       tr_move c ns r nd rd ->
       tr_expr c map pr (Eletvar n) ns nd rd
-  | tr_Ealloc: forall map pr a ns nd rd n1 r,
-      tr_expr c map pr a ns n1 r ->
-      c!n1 = Some (Ialloc r rd nd) ->
-      ~reg_in_map map rd -> ~In rd pr ->
-      tr_expr c map pr (Ealloc a) ns nd rd
 
-(** [tr_expr c map pr cond ns ntrue nfalse rd] holds if the graph [c],
+(** [tr_condition c map pr cond ns ntrue nfalse rd] holds if the graph [c],
   starting at node [ns], contains instructions that compute the truth
   value of the Cminor conditional expression [cond] and terminate
   on node [ntrue] if the condition holds and on node [nfalse] otherwise. *)
@@ -866,6 +850,19 @@ with tr_exprlist (c: code):
       tr_exprlist c map (r1 :: pr) al n1 nd rl ->
       tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl).
 
+(** Auxiliary for the compilation of variable assignments. *)
+
+Definition tr_store_var (c: code) (map: mapping)
+                        (rs: reg) (id: ident) (ns nd: node): Prop :=
+  exists rv, map.(map_vars)!id = Some rv /\ tr_move c ns rs nd rv.
+
+Definition tr_store_optvar (c: code) (map: mapping)
+                 (rs: reg) (optid: option ident) (ns nd: node): Prop :=
+  match optid with
+  | None => ns = nd
+  | Some id => tr_store_var c map rs id ns nd
+  end.
+
 (** Auxiliary for the compilation of [switch] statements. *)
 
 Inductive tr_switch
@@ -898,14 +895,28 @@ Inductive tr_stmt (c: code) (map: mapping):
      stmt -> node -> node -> list node -> node -> option reg -> Prop :=
   | tr_Sskip: forall ns nexits nret rret,
      tr_stmt c map Sskip ns ns nexits nret rret
-  | tr_Sexpr: forall a ns nd nexits nret rret r,
-     tr_expr c map nil a ns nd r ->
-     tr_stmt c map (Sexpr a) ns nd nexits nret rret
-  | tr_Sassign: forall id a ns nd nexits nret rret rv rt n,
-     map.(map_vars)!id = Some rv ->
-     tr_move c n rt nd rv ->
+  | tr_Sassign: forall id a ns nd nexits nret rret rt n,
      tr_expr c map nil a ns n rt ->
+     tr_store_var c map rt id n nd ->
      tr_stmt c map (Sassign id a) ns nd nexits nret rret
+  | tr_Sstore: forall chunk addr al b ns nd nexits nret rret rd n1 rl n2,
+     tr_exprlist c map nil al ns n1 rl ->
+     tr_expr c map rl b n1 n2 rd ->
+     c!n2 = Some (Istore chunk addr rl rd nd) ->
+     tr_stmt c map (Sstore chunk addr al b) ns nd nexits nret rret
+  | tr_Scall: forall optid sig b cl ns nd nexits nret rret rd n1 rf n2 n3 rargs,
+     tr_expr c map nil b ns n1 rf ->
+     tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
+     c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) ->
+     tr_store_optvar c map rd optid n3 nd ->
+     ~reg_in_map map rd ->
+     tr_stmt c map (Scall optid sig b cl) ns nd nexits nret rret
+  | tr_Salloc: forall id a ns nd nexits nret rret rd n1 n2 r,
+     tr_expr c map nil a ns n1 r ->
+     c!n1 = Some (Ialloc r rd n2) ->
+     tr_store_var c map rd id n2 nd ->
+     ~reg_in_map map rd ->
+     tr_stmt c map (Salloc id a) ns nd nexits nret rret
   | tr_Sseq: forall s1 s2 ns nd nexits nret rret n,
      tr_stmt c map s2 n nd nexits nret rret ->
      tr_stmt c map s1 ns n nexits nret rret ->
@@ -975,10 +986,10 @@ Definition tr_expr_condition_exprlist_ind3
   (P : mapping -> list reg -> expr -> node -> node -> reg -> Prop)
   (P0 : mapping -> list reg -> condexpr -> node -> node -> node -> Prop)
   (P1 : mapping -> list reg -> exprlist -> node -> node -> list reg -> Prop) :=
-  fun a b c' d e f g h i j k l m n o =>
-  conj (tr_expr_ind3 c P P0 P1 a b c' d e f g h i j k l m n o)
-       (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l m n o)
-             (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l m n o)).
+  fun a b c' d e f g h i j k l =>
+  conj (tr_expr_ind3 c P P0 P1 a b c' d e f g h i j k l)
+       (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l)
+             (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)).
 
 Lemma tr_move_extends:
   forall s1 s2, state_extends s1 s2 ->
@@ -1048,10 +1059,10 @@ Scheme expr_ind3 := Induction for expr Sort Prop
 
 Definition expr_condexpr_exprlist_ind 
     (P1: expr -> Prop) (P2: condexpr -> Prop) (P3: exprlist -> Prop) :=
-  fun a b c d e f g h i j k l m n o =>
-  conj (expr_ind3 P1 P2 P3 a b c d e f g h i j k l m n o)
-    (conj (condexpr_ind3 P1 P2 P3 a b c d e f g h i j k l m n o)
-          (exprlist_ind3 P1 P2 P3 a b c d e f g h i j k l m n o)).
+  fun a b c d e f g h i j k l =>
+  conj (expr_ind3 P1 P2 P3 a b c d e f g h i j k l)
+    (conj (condexpr_ind3 P1 P2 P3 a b c d e f g h i j k l)
+          (exprlist_ind3 P1 P2 P3 a b c d e f g h i j k l)).
 
 Lemma add_move_charact:
   forall s ns rs nd rd s',
@@ -1109,49 +1120,6 @@ Proof.
   split. econstructor; eauto.
   eapply instr_at_incr; eauto.
   apply state_incr_trans with s1; eauto with rtlg.
-  (* Estore *)
-  inv OK.
-  assert (state_incr s s1). eauto with rtlg. 
-  exploit (H0 _ _ _ _ _ _ (x ++ pr) EQ0).
-  eauto with rtlg.
-  apply target_reg_ok_append. constructor; auto. 
-  intros. exploit alloc_regs_fresh_or_in_map; eauto.
-  intros [A|B]. auto. right. apply sym_not_equal.
-  eapply valid_fresh_different; eauto with rtlg. 
-  red; intros. elim (in_app_or _ _ _ H4); intro. 
-  exploit alloc_regs_valid; eauto with rtlg.
-  generalize (VALID _ H5). eauto with rtlg. 
-  eauto with rtlg. 
-  intros [A B].
-  exploit (H _ _ _ _ _ _ pr EQ3); eauto with rtlg. 
-  intros [C D].
-  split. econstructor; eauto.
-  apply tr_expr_incr with s2; eauto with rtlg. 
-  apply instr_at_incr with s1; eauto with rtlg. 
-  eauto with rtlg.
-  (* Ecall *)
-  inv OK.
-  assert (state_incr s0 s3).
-    apply state_incr_trans with s1. eauto with rtlg.
-    apply state_incr_trans with s2; eauto with rtlg.
-  assert (regs_valid (x :: pr) s1).
-    apply regs_valid_cons; eauto with rtlg. 
-  exploit (H0 _ _ _ _ _ _ (x :: pr) EQ2).
-  eauto with rtlg. 
-  apply alloc_regs_target_ok with s1 s2; eauto with rtlg.
-  eauto with rtlg.
-  apply regs_valid_incr with s2; eauto with rtlg.
-  intros [A B].
-  exploit (H _ _ _ _ _ _ pr EQ4).
-  eauto with rtlg.
-  eauto with rtlg.
-  apply regs_valid_incr with s0; eauto with rtlg.
-  apply reg_valid_incr with s1; eauto with rtlg.
-  intros [C D].
-  split. econstructor; eauto.
-  apply tr_exprlist_incr with s4; eauto.
-  apply instr_at_incr with s3; eauto with rtlg. 
-  eauto with rtlg.
   (* Econdition *)
   inv OK.
   exploit (H1 _ _ _ _ _ _ pr EQ); eauto with rtlg.
@@ -1192,13 +1160,6 @@ Proof.
     inv OK. left; congruence. right; eauto.
   auto.
   monadInv EQ1.
-  (* Ealloc *)
-  inv OK. 
-  exploit (H _ _ _ _ _ _ pr EQ2); eauto with rtlg.
-  intros [A B].
-  split. econstructor; eauto.
-  eapply instr_at_incr; eauto.
-  apply state_incr_trans with s1; eauto with rtlg.
 
   (* CEtrue *)
   split. constructor. auto with rtlg.
@@ -1264,6 +1225,27 @@ Proof.
   intros. eapply B; eauto with rtlg.
 Qed.
 
+Lemma tr_store_var_extends:
+  forall s1 s2, state_extends s1 s2 ->
+  forall map rs id ns nd,
+  tr_store_var s1.(st_code) map rs id ns nd ->
+  tr_store_var s2.(st_code) map rs id ns nd.
+Proof.
+  intros. destruct H0 as [rv [A B]]. 
+  econstructor; split. eauto. eapply tr_move_extends; eauto.
+Qed.
+ 
+Lemma tr_store_optvar_extends:
+  forall s1 s2, state_extends s1 s2 ->
+  forall map rs optid ns nd,
+  tr_store_optvar s1.(st_code) map rs optid ns nd ->
+  tr_store_optvar s2.(st_code) map rs optid ns nd.
+Proof.
+  intros until nd. destruct optid; simpl. 
+  apply tr_store_var_extends; auto.
+  auto.
+Qed.
+
 Lemma tr_switch_extends:
   forall s1 s2, state_extends s1 s2 ->
   forall r nexits t ns,
@@ -1284,8 +1266,9 @@ Proof.
   intros s1 s2 EXT.
   destruct (tr_expr_condition_exprlist_extends s1 s2 EXT) as [A [B C]].
   pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT).
+  pose (STV := tr_store_var_extends s1 s2 EXT).
+  pose (STOV := tr_store_optvar_extends s1 s2 EXT).
   induction 1; econstructor; eauto.
-  eapply tr_move_extends; eauto.
   eapply tr_switch_extends; eauto.
 Qed.
 
@@ -1298,6 +1281,28 @@ Proof.
   intros. eapply tr_stmt_extends; eauto with rtlg.
 Qed.
 
+
+Lemma store_var_charact:
+  forall map rs id nd s ns s',
+  store_var map rs id nd s = OK ns s' ->
+  tr_store_var s'.(st_code) map rs id ns nd /\ state_incr s s'.
+Proof.
+  intros. monadInv H. generalize EQ. unfold find_var.
+  caseEq ((map_vars map)!id). 2: intros; discriminate. intros. monadInv EQ1.
+  exploit add_move_charact; eauto. intros [A B]. 
+  split; auto. exists x; auto.
+Qed.
+
+Lemma store_optvar_charact:
+  forall map rs optid nd s ns s',
+  store_optvar map rs optid nd s = OK ns s' ->
+  tr_store_optvar s'.(st_code) map rs optid ns nd /\ state_incr s s'.
+Proof.
+  intros. destruct optid; simpl in H; simpl.
+  eapply store_var_charact; eauto.
+  monadInv H. split. auto. apply state_incr_refl. 
+Qed. 
+
 Lemma transl_exit_charact:
   forall nexits n s ne s',
   transl_exit nexits n s = OK ne s' ->
@@ -1344,18 +1349,85 @@ Proof.
   induction stmt; intros; simpl in TR; try (monadInv TR).
   (* Sskip *)
   split. constructor. auto with rtlg.
-  (* Sexpr *)
-  exploit transl_expr_charact; eauto with rtlg. intros [A B].
-  split. econstructor; eauto. eauto with rtlg.
   (* Sassign *)
-  exploit add_move_charact; eauto. intros [A B].
+  exploit store_var_charact; eauto. intros [A B].
   exploit transl_expr_charact; eauto with rtlg. 
-    apply map_valid_incr with s; eauto with rtlg. 
   intros [C D].
-  generalize EQ. unfold find_var. caseEq (map_vars map)!i; intros; inv EQ2.
   split. econstructor; eauto.
-  apply tr_move_extends with s2; eauto with rtlg.
+  apply tr_store_var_extends with s1; eauto with rtlg.
   eauto with rtlg. 
+  (* Sstore *)
+  assert (state_incr s s1). eauto with rtlg.
+  assert (state_incr s s2). eauto with rtlg.
+  assert (map_valid map s2). eauto with rtlg. 
+  destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
+  exploit (P1 _ _ _ _ _ _ _ x EQ2).
+    auto.
+    eapply alloc_reg_target_ok with (s1 := s0); eauto with rtlg.  
+    apply regs_valid_incr with s0; eauto with rtlg. 
+    apply reg_valid_incr with s1; eauto with rtlg.
+  intros [A B].
+  exploit (P3 _ _ _ _ _ _ _ nil EQ4).
+    apply map_valid_incr with s2; auto.
+    eapply alloc_regs_target_ok with (s1 := s); eauto with rtlg.
+    auto with rtlg.
+    apply regs_valid_incr with s0; eauto with rtlg. 
+  intros [C D].
+  split. econstructor; eauto.
+  apply tr_expr_incr with s3; eauto with rtlg. 
+  apply instr_at_incr with s2; eauto with rtlg.
+  eauto with rtlg.
+  (* Scall *)
+  assert (state_incr s0 s3).
+    apply state_incr_trans with s1. eauto with rtlg.
+    apply state_incr_trans with s2; eauto with rtlg.
+  exploit store_optvar_charact; eauto. intros [A B].
+  assert (state_incr s0 s5) by eauto with rtlg.
+  destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
+  exploit (P3 _ _ _ _ _ _ _ (x :: nil) EQ4).
+    apply map_valid_incr with s0; auto.
+    eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg.
+    apply regs_valid_cons; eauto with rtlg.
+    apply regs_valid_incr with s1. 
+    apply state_incr_trans with s3; eauto with rtlg. 
+    apply regs_valid_cons; eauto with rtlg.
+    apply regs_valid_incr with s2.
+    apply state_incr_trans with s3; eauto with rtlg.
+    eauto with rtlg.
+  intros [C D].
+  exploit (P1 _ _ _ _ _ _ _ nil EQ6).
+    apply map_valid_incr with s0; eauto with rtlg.
+    eapply alloc_reg_target_ok with (s1 := s0); eauto with rtlg.
+    auto with rtlg.
+    apply reg_valid_incr with s1.
+    apply state_incr_trans with s3; eauto with rtlg. 
+    eauto with rtlg.
+  intros [E F].
+  split. econstructor; eauto. 
+  apply tr_exprlist_incr with s6; eauto. 
+  apply instr_at_incr with s5; eauto with rtlg.
+  apply tr_store_optvar_extends with s4; eauto with rtlg.
+  red; intro.
+  apply valid_fresh_absurd with x1 s2. 
+  apply reg_valid_incr with s0; eauto with rtlg. 
+  eauto with rtlg.
+  eauto with rtlg.
+  (* Salloc *)
+  exploit store_var_charact; eauto. intros [A B].
+  exploit transl_expr_charact; eauto.
+    apply map_valid_incr with s; auto.
+    apply state_incr_trans with s1; eauto with rtlg.
+    eapply alloc_reg_target_ok with (s1 := s); eauto with rtlg.
+    apply reg_valid_incr with s0; eauto with rtlg.
+  intros [C D].
+  split. econstructor; eauto.
+  apply instr_at_incr with s3; eauto with rtlg.
+  apply tr_store_var_extends with s2; eauto with rtlg.
+  red; intro.
+  apply valid_fresh_absurd with x0 s0. 
+  apply reg_valid_incr with s; eauto with rtlg. 
+  eauto with rtlg.
+  apply state_incr_trans with s2; eauto with rtlg. 
   (* Sseq *)
   exploit IHstmt2; eauto with rtlg. intros [A B].
   exploit IHstmt1; eauto with rtlg. intros [C D].
diff --git a/backend/Selection.v b/backend/Selection.v
index c98e55e4..0183ee7d 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -38,16 +38,11 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
   | Evar id => Evar id
   | Eop op bl => Eop op (lift_exprlist p bl)
   | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl)
-  | Estore chunk addr bl c =>
-      Estore chunk addr (lift_exprlist p bl) (lift_expr p c)
-  | Ecall sig b cl => Ecall sig (lift_expr p b) (lift_exprlist p cl)
   | Econdition b c d =>
       Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d)
   | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c)
   | Eletvar n =>
       if le_gt_dec p n then Eletvar (S n) else Eletvar n
-  | Ealloc b =>
-      Ealloc (lift_expr p b)
   end
 
 with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr :=
@@ -981,7 +976,7 @@ Definition load (chunk: memory_chunk) (e1: expr) :=
 
 Definition store (chunk: memory_chunk) (e1 e2: expr) :=
   match addressing e1 with
-  | (mode, args) => Estore chunk mode args e2
+  | (mode, args) => Sstore chunk mode args e2
   end.
 
 (** * Translation from Cminor to CminorSel *)
@@ -1046,20 +1041,15 @@ Fixpoint sel_expr (a: Cminor.expr) : expr :=
   | Cminor.Eunop op arg => sel_unop op (sel_expr arg)
   | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2)
   | Cminor.Eload chunk addr => load chunk (sel_expr addr)
-  | Cminor.Estore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
-  | Cminor.Ecall sg fn args => Ecall sg (sel_expr fn) (sel_exprlist args)
   | Cminor.Econdition cond ifso ifnot =>
       Econdition (condexpr_of_expr (sel_expr cond))
                  (sel_expr ifso) (sel_expr ifnot)
-  | Cminor.Elet b c => Elet (sel_expr b) (sel_expr c)
-  | Cminor.Eletvar n => Eletvar n
-  | Cminor.Ealloc b => Ealloc (sel_expr b)
-  end
+  end.
 
-with sel_exprlist (al: Cminor.exprlist) : exprlist :=
+Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
   match al with
-  | Cminor.Enil => Enil
-  | Cminor.Econs a bl => Econs (sel_expr a) (sel_exprlist bl)
+  | nil => Enil
+  | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
   end.
 
 (** Conversion from Cminor statements to Cminorsel statements. *)
@@ -1067,8 +1057,11 @@ with sel_exprlist (al: Cminor.exprlist) : exprlist :=
 Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
   match s with
   | Cminor.Sskip => Sskip
-  | Cminor.Sexpr e => Sexpr (sel_expr e)
   | Cminor.Sassign id e => Sassign id (sel_expr e)
+  | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
+  | Cminor.Scall optid sg fn args =>
+      Scall optid sg (sel_expr fn) (sel_exprlist args)
+  | Cminor.Salloc id b => Salloc id (sel_expr b)
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
   | Cminor.Sifthenelse e ifso ifnot =>
       Sifthenelse (condexpr_of_expr (sel_expr e))
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index e41765a7..177e3211 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -19,6 +19,9 @@ Open Local Scope selection_scope.
 Section CMCONSTR.
 
 Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
 
 (** * Lifting of let-bound variables *)
 
@@ -57,72 +60,34 @@ Proof.
   apply IHinsert_lenv. exact H0. omega.
 Qed.
 
-Scheme eval_expr_ind_3 := Minimality for eval_expr Sort Prop
-  with eval_condexpr_ind_3 := Minimality for eval_condexpr Sort Prop
-  with eval_exprlist_ind_3 := Minimality for eval_exprlist Sort Prop.
-
-Hint Resolve eval_Evar eval_Eop eval_Eload eval_Estore
-             eval_Ecall eval_Econdition eval_Ealloc
+Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition
              eval_Elet eval_Eletvar 
              eval_CEtrue eval_CEfalse eval_CEcond
              eval_CEcondition eval_Enil eval_Econs: evalexpr.
 
-Lemma eval_list_one:
-  forall sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_exprlist ge sp le e m1 (a ::: Enil) t m2 (v :: nil).
-Proof.
-  intros. econstructor. eauto. constructor. traceEq.
-Qed.
-
-Lemma eval_list_two:
-  forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 t,
-  eval_expr ge sp le e m1 a1 t1 m2 v1 ->
-  eval_expr ge sp le e m2 a2 t2 m3 v2 ->
-  t = t1 ** t2 ->
-  eval_exprlist ge sp le e m1 (a1 ::: a2 ::: Enil) t m3 (v1 :: v2 :: nil).
-Proof.
-  intros. econstructor. eauto. econstructor. eauto. constructor. 
-  reflexivity. traceEq.
-Qed.
-
-Lemma eval_list_three:
-  forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 a3 t3 m4 v3 t,
-  eval_expr ge sp le e m1 a1 t1 m2 v1 ->
-  eval_expr ge sp le e m2 a2 t2 m3 v2 ->
-  eval_expr ge sp le e m3 a3 t3 m4 v3 ->
-  t = t1 ** t2 ** t3 ->
-  eval_exprlist ge sp le e m1 (a1 ::: a2 ::: a3 ::: Enil) t m4 (v1 :: v2 :: v3 :: nil).
-Proof.
-  intros. econstructor. eauto. econstructor. eauto. econstructor. eauto. constructor. 
-  reflexivity. reflexivity. traceEq.
-Qed.
-
-Hint Resolve eval_list_one eval_list_two eval_list_three: evalexpr.
-
 Lemma eval_lift_expr:
-  forall w sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
+  forall w le a v,
+  eval_expr ge sp e m le a v ->
   forall p le', insert_lenv le p w le' ->
-  eval_expr ge sp le' e m1 (lift_expr p a) t m2 v.
+  eval_expr ge sp e m le' (lift_expr p a) v.
 Proof.
-  intros w.
-  apply (eval_expr_ind_3 ge
-    (fun sp le e m1 a t m2 v =>
+  intro w.
+  apply (eval_expr_ind3 ge sp e m
+    (fun le a v =>
       forall p le', insert_lenv le p w le' ->
-      eval_expr ge sp le' e m1 (lift_expr p a) t m2 v)
-    (fun sp le e m1 a t m2 vb =>
+      eval_expr ge sp e m le' (lift_expr p a) v)
+    (fun le a v =>
       forall p le', insert_lenv le p w le' ->
-      eval_condexpr ge sp le' e m1 (lift_condexpr p a) t m2 vb)
-    (fun sp le e m1 al t m2 vl =>
+      eval_condexpr ge sp e m le' (lift_condexpr p a) v)
+    (fun le al vl =>
       forall p le', insert_lenv le p w le' ->
-      eval_exprlist ge sp le' e m1 (lift_exprlist p al) t m2 vl));
+      eval_exprlist ge sp e m le' (lift_exprlist p al) vl));
   simpl; intros; eauto with evalexpr.
 
   destruct v1; eapply eval_Econdition;
   eauto with evalexpr; simpl; eauto with evalexpr.
 
-  eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. auto.
+  eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto.
 
   case (le_gt_dec p n); intro. 
   apply eval_Eletvar. eapply insert_lenv_lookup2; eauto.
@@ -133,13 +98,14 @@ Proof.
 Qed.
 
 Lemma eval_lift:
-  forall sp le e m1 a t m2 v w,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_expr ge sp (w::le) e m1 (lift a) t m2 v.
+  forall le a v w,
+  eval_expr ge sp e m le a v ->
+  eval_expr ge sp e m (w::le) (lift a) v.
 Proof.
   intros. unfold lift. eapply eval_lift_expr.
   eexact H. apply insert_lenv_0. 
 Qed.
+
 Hint Resolve eval_lift: evalexpr.
 
 (** * Useful lemmas and tactics *)
@@ -152,75 +118,37 @@ Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.
 
 Ltac TrivialOp cstr := unfold cstr; intros; EvalOp.
 
-Lemma inv_eval_Eop_0:
-  forall sp le e m1 op t m2 v,
-  eval_expr ge sp le e m1 (Eop op Enil) t m2 v ->
-  t = E0 /\ m2 = m1 /\ eval_operation ge sp op nil m1 = Some v.
-Proof.
-  intros. inversion H. inversion H6. 
-  intuition. congruence.
-Qed.
-  
-Lemma inv_eval_Eop_1:
-  forall sp le e m1 op t a1 m2 v,
-  eval_expr ge sp le e m1 (Eop op (a1 ::: Enil)) t m2 v ->
-  exists v1,
-  eval_expr ge sp le e m1 a1 t m2 v1 /\
-  eval_operation ge sp op (v1 :: nil) m2 = Some v.
-Proof.
-  intros. 
-  inversion H. inversion H6. inversion H18. 
-  subst. exists v1; intuition. rewrite E0_right. auto.
-Qed.
-
-Lemma inv_eval_Eop_2:
-  forall sp le e m1 op a1 a2 t3 m3 v,
-  eval_expr ge sp le e m1 (Eop op (a1 ::: a2 ::: Enil)) t3 m3 v ->
-  exists t1, exists t2, exists m2, exists v1, exists v2,
-  eval_expr ge sp le e m1 a1 t1 m2 v1 /\
-  eval_expr ge sp le e m2 a2 t2 m3 v2 /\
-  t3 = t1 ** t2 /\
-  eval_operation ge sp op (v1 :: v2 :: nil) m3 = Some v.
-Proof.
-  intros. 
-  inversion H. subst. inversion H6. subst. inversion H8. subst.
-  inversion H11. subst. 
-  exists t1; exists t0; exists m0; exists v0; exists v1.
-  intuition. traceEq.
-Qed.
+Ltac InvEval1 :=
+  match goal with
+  | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] =>
+      inv H; InvEval1
+  | _ =>
+      idtac
+  end.
 
-Ltac SimplEval :=
+Ltac InvEval2 :=
   match goal with
-  | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op Enil) ?t ?m2 ?v) -> _] =>
-      intro XX1;
-      generalize (inv_eval_Eop_0 sp le e m1 op t m2 v XX1);
-      clear XX1;
-      intros [XX1 [XX2 XX3]];
-      subst t m2; simpl in XX3; 
-      try (simplify_eq XX3; clear XX3;
-      let EQ := fresh "EQ" in (intro EQ; rewrite EQ))
-  | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: Enil)) ?t ?m2 ?v) -> _] =>
-      intro XX1;
-      generalize (inv_eval_Eop_1 sp le e m1 op t a1 m2 v XX1);
-      clear XX1;
-      let v1 := fresh "v" in let EV := fresh "EV" in
-      let EQ := fresh "EQ" in
-      (intros [v1 [EV EQ]]; simpl in EQ)
-  | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?t ?m2 ?v) -> _] =>
-      intro XX1;
-      generalize (inv_eval_Eop_2 sp le e m1 op a1 a2 t m2 v XX1);
-      clear XX1;
-      let t1 := fresh "t" in let t2 := fresh "t" in
-      let m := fresh "m" in
-      let v1 := fresh "v" in let v2 := fresh "v" in
-      let EV1 := fresh "EV" in let EV2 := fresh "EV" in
-      let EQ := fresh "EQ" in let TR := fresh "TR" in
-      (intros [t1 [t2 [m [v1 [v2 [EV1 [EV2 [TR EQ]]]]]]]]; simpl in EQ)
-  | _ => idtac
+  | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
+      simpl in H; inv H
+  | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
+      simpl in H; FuncInv
+  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
+      simpl in H; FuncInv
+  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
+      simpl in H; FuncInv
+  | _ =>
+      idtac
   end.
 
-Ltac InvEval H :=
-  generalize H; SimplEval; clear H.
+Ltac InvEval := InvEval1; InvEval2; InvEval2.
 
 (** * Correctness of the smart constructors *)
 
@@ -244,31 +172,31 @@ Ltac InvEval H :=
   by the smart constructor.
 *)
 
-Lemma eval_notint:
-  forall sp le e m1 a t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
-  eval_expr ge sp le e m1 (notint a) t m2 (Vint (Int.not x)).
+Theorem eval_notint:
+  forall le a x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (notint a) (Vint (Int.not x)).
 Proof.
-  unfold notint; intros until x; case (notint_match a); intros.
-  InvEval H. FuncInv. EvalOp. simpl. congruence. 
-  InvEval H. FuncInv. EvalOp. simpl. congruence. 
-  InvEval H. FuncInv. EvalOp. simpl. congruence. 
+  unfold notint; intros until x; case (notint_match a); intros; InvEval.
+  EvalOp. simpl. congruence.
+  EvalOp. simpl. congruence.
+  EvalOp. simpl. congruence.
   eapply eval_Elet. eexact H. 
   eapply eval_Eop.
   eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity.
   eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity.
-  apply eval_Enil. reflexivity. reflexivity. 
-  simpl. rewrite Int.or_idem. auto. traceEq.
+  apply eval_Enil.  
+  simpl. rewrite Int.or_idem. auto.
 Qed.
 
 Lemma eval_notbool_base:
-  forall sp le e m1 a t m2 v b,
-  eval_expr ge sp le e m1 a t m2 v ->
+  forall le a v b,
+  eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
-  eval_expr ge sp le e m1 (notbool_base a) t m2 (Val.of_bool (negb b)).
+  eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)).
 Proof. 
   TrivialOp notbool_base. simpl. 
-  inversion H0. 
+  inv H0. 
   rewrite Int.eq_false; auto.
   rewrite Int.eq_true; auto.
   reflexivity.
@@ -277,245 +205,203 @@ Qed.
 Hint Resolve Val.bool_of_true_val Val.bool_of_false_val
              Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof.
 
-Lemma eval_notbool:
-  forall a sp le e m1 t m2 v b,
-  eval_expr ge sp le e m1 a t m2 v ->
+Theorem eval_notbool:
+  forall le a v b,
+  eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
-  eval_expr ge sp le e m1 (notbool a) t m2 (Val.of_bool (negb b)).
+  eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)).
 Proof.
-  assert (N1: forall v b, Val.is_false v -> Val.bool_of_val v b -> Val.is_true (Val.of_bool (negb b))).
-    intros. inversion H0; simpl; auto; subst v; simpl in H.
-    congruence. apply Int.one_not_zero. contradiction.
-  assert (N2: forall v b, Val.is_true v -> Val.bool_of_val v b -> Val.is_false (Val.of_bool (negb b))).
-    intros. inversion H0; simpl; auto; subst v; simpl in H.
-    congruence. 
-
   induction a; simpl; intros; try (eapply eval_notbool_base; eauto).
   destruct o; try (eapply eval_notbool_base; eauto).
 
-  destruct e. InvEval H. injection XX3; clear XX3; intro; subst v.
-  inversion H0. rewrite Int.eq_false; auto. 
+  destruct e0. InvEval. 
+  inv H0. rewrite Int.eq_false; auto. 
   simpl; eauto with evalexpr.
   rewrite Int.eq_true; simpl; eauto with evalexpr.
   eapply eval_notbool_base; eauto.
 
-  inversion H. subst. 
-  simpl in H11. eapply eval_Eop; eauto.
-  simpl. caseEq (eval_condition c vl m2); intros.
-  rewrite H1 in H11. 
-  assert (b0 = b). 
-  destruct b0; inversion H11; subst v; inversion H0; auto.
-  subst b0. rewrite (Op.eval_negate_condition _ _ _ H1). 
+  inv H. eapply eval_Eop; eauto.
+  simpl. assert (eval_condition c vl m = Some b).
+  generalize H6. simpl. 
+  case (eval_condition c vl m); intros.
+  destruct b0; inv H1; inversion H0; auto; congruence.
+  congruence.
+  rewrite (Op.eval_negate_condition _ _ _ H). 
   destruct b; reflexivity.
-  rewrite H1 in H11; discriminate.
 
-  inversion H; eauto 10 with evalexpr valboolof.
-  inversion H; eauto 10 with evalexpr valboolof.
-
-  inversion H. subst. eapply eval_Econdition with (t2 := t8). eexact H34.
-  destruct v4; eauto. auto.
+  inv H. eapply eval_Econdition; eauto. 
+  destruct v1; eauto.
 Qed.
 
-Lemma eval_addimm:
-  forall sp le e m1 n a t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
-  eval_expr ge sp le e m1 (addimm n a) t m2 (Vint (Int.add x n)).
+Theorem eval_addimm:
+  forall le n a x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)).
 Proof.
   unfold addimm; intros until x.
   generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro.
   subst n. rewrite Int.add_zero. auto.
-  case (addimm_match a); intros.
-  InvEval H0. EvalOp. simpl. rewrite Int.add_commut. auto.
-  InvEval H0. destruct (Genv.find_symbol ge s); discriminate.
-  InvEval H0. 
-  destruct sp; simpl in XX3; discriminate.
-  InvEval H0. FuncInv. EvalOp. simpl. subst x. 
-  rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut.
-  EvalOp. 
+  case (addimm_match a); intros; InvEval; EvalOp; simpl.
+  rewrite Int.add_commut. auto.
+  destruct (Genv.find_symbol ge s); discriminate.
+  destruct sp; simpl in H1; discriminate.
+  subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut.
 Qed. 
 
-Lemma eval_addimm_ptr:
-  forall sp le e m1 n t a m2 b ofs,
-  eval_expr ge sp le e m1 a t m2 (Vptr b ofs) ->
-  eval_expr ge sp le e m1 (addimm n a) t m2 (Vptr b (Int.add ofs n)).
+Theorem eval_addimm_ptr:
+  forall le n a b ofs,
+  eval_expr ge sp e m le a (Vptr b ofs) ->
+  eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)).
 Proof.
   unfold addimm; intros until ofs.
   generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro.
   subst n. rewrite Int.add_zero. auto.
-  case (addimm_match a); intros.
-  InvEval H0. 
-  InvEval H0. EvalOp. simpl. 
-    destruct (Genv.find_symbol ge s). 
-    rewrite Int.add_commut. congruence.
-    discriminate.
-  InvEval H0. destruct sp; simpl in XX3; try discriminate.
-  inversion XX3. EvalOp. simpl. decEq. decEq. 
+  case (addimm_match a); intros; InvEval; EvalOp; simpl.
+  destruct (Genv.find_symbol ge s). 
+  rewrite Int.add_commut. congruence.
+  discriminate.
+  destruct sp; simpl in H1; try discriminate.
+  inv H1. simpl. decEq. decEq. 
   rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  InvEval H0. FuncInv. subst b0; subst ofs. EvalOp. simpl. 
-    rewrite (Int.add_commut n m). rewrite Int.add_assoc. auto.
-  EvalOp. 
+  subst. rewrite (Int.add_commut n m0). rewrite Int.add_assoc. auto.
 Qed.
 
-Lemma eval_add:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vint (Int.add x y)).
+Theorem eval_add:
+  forall le a b x y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (add a b) (Vint (Int.add x y)).
 Proof.
-  intros until y. unfold add; case (add_match a b); intros.
-  InvEval H. rewrite Int.add_commut. apply eval_addimm. 
-  rewrite E0_left; assumption.
-  InvEval H. FuncInv. InvEval H0. FuncInv. 
-    replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)).
-    apply eval_addimm. EvalOp. 
+  intros until y.
+  unfold add; case (add_match a b); intros; InvEval.
+  rewrite Int.add_commut. apply eval_addimm. auto. 
+  replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)).
+    apply eval_addimm. EvalOp.  
     subst x; subst y. 
     repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. 
-  InvEval H. FuncInv. 
-    replace (Int.add x y) with (Int.add (Int.add i y) n1).
+  replace (Int.add x y) with (Int.add (Int.add i y) n1).
     apply eval_addimm. EvalOp.
     subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  InvEval H0. FuncInv.
-    apply eval_addimm. rewrite E0_right. auto.
-  InvEval H0. FuncInv. 
-    replace (Int.add x y) with (Int.add (Int.add x i) n2).
+  apply eval_addimm. auto.
+  replace (Int.add x y) with (Int.add (Int.add x i) n2).
     apply eval_addimm. EvalOp.
     subst y. rewrite Int.add_assoc. auto.
   EvalOp.
 Qed.
 
-Lemma eval_add_ptr:
-  forall sp le e m1 a t1 m2 p x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add x y)).
+Theorem eval_add_ptr:
+  forall le a b p x y,
+  eval_expr ge sp e m le a (Vptr p x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)).
 Proof.
-  intros until y. unfold add; case (add_match a b); intros.
-  InvEval H. 
-  InvEval H. FuncInv. InvEval H0. FuncInv. 
-    replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)).
+  intros until y. unfold add; case (add_match a b); intros; InvEval.
+  replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)).
     apply eval_addimm_ptr. subst b0. EvalOp. 
     subst x; subst y.
     repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. 
-  InvEval H. FuncInv. 
-    replace (Int.add x y) with (Int.add (Int.add i y) n1).
+  replace (Int.add x y) with (Int.add (Int.add i y) n1).
     apply eval_addimm_ptr. subst b0. EvalOp.
     subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  InvEval H0. apply eval_addimm_ptr. rewrite E0_right. auto.
-  InvEval H0. FuncInv. 
-    replace (Int.add x y) with (Int.add (Int.add x i) n2).
+  apply eval_addimm_ptr. auto.
+  replace (Int.add x y) with (Int.add (Int.add x i) n2).
     apply eval_addimm_ptr. EvalOp.
     subst y. rewrite Int.add_assoc. auto.
   EvalOp.
 Qed.
 
-Lemma eval_add_ptr_2:
-  forall sp le e m1 a t1 m2 p x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vptr p y) ->
-  eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add y x)).
+Theorem eval_add_ptr_2:
+  forall le a b x p y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vptr p y) ->
+  eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)).
 Proof.
-  intros until y. unfold add; case (add_match a b); intros.
-  InvEval H. 
-    apply eval_addimm_ptr. rewrite E0_left. auto.
-  InvEval H. FuncInv. InvEval H0. FuncInv. 
-    replace (Int.add y x) with (Int.add (Int.add i0 i) (Int.add n1 n2)).
+  intros until y. unfold add; case (add_match a b); intros; InvEval.
+  apply eval_addimm_ptr. auto.
+  replace (Int.add y x) with (Int.add (Int.add i i0) (Int.add n1 n2)).
     apply eval_addimm_ptr. subst b0. EvalOp. 
     subst x; subst y.
     repeat rewrite Int.add_assoc. decEq. 
     rewrite (Int.add_commut n1 n2). apply Int.add_permut. 
-  InvEval H. FuncInv. 
-    replace (Int.add y x) with (Int.add (Int.add y i) n1).
+  replace (Int.add y x) with (Int.add (Int.add y i) n1).
     apply eval_addimm_ptr. EvalOp. 
     subst x. repeat rewrite Int.add_assoc. auto.
-  InvEval H0. 
-  InvEval H0. FuncInv. 
-    replace (Int.add y x) with (Int.add (Int.add i x) n2).
+  replace (Int.add y x) with (Int.add (Int.add i x) n2).
     apply eval_addimm_ptr. EvalOp. subst b0; reflexivity.
     subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
   EvalOp.
 Qed.
 
-Lemma eval_sub:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)).
+Theorem eval_sub:
+  forall le a b x y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)).
 Proof.
   intros until y.
-  unfold sub; case (sub_match a b); intros.
-  InvEval H0. rewrite Int.sub_add_opp. 
-    apply eval_addimm. rewrite E0_right. assumption.
-  InvEval H. FuncInv. InvEval H0. FuncInv.
-    replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)).
+  unfold sub; case (sub_match a b); intros; InvEval.
+  rewrite Int.sub_add_opp. 
+    apply eval_addimm. assumption.
+  replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)).
     apply eval_addimm. EvalOp.
     subst x; subst y.
     repeat rewrite Int.sub_add_opp.
     repeat rewrite Int.add_assoc. decEq. 
     rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr.
-  InvEval H. FuncInv. 
-    replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
+  replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
     apply eval_addimm. EvalOp.
     subst x. rewrite Int.sub_add_l. auto.
-  InvEval H0. FuncInv. 
-    replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
+  replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
     apply eval_addimm. EvalOp.
     subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. 
   EvalOp.
 Qed.
 
-Lemma eval_sub_ptr_int:
-  forall sp le e m1 a t1 m2 p x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vptr p (Int.sub x y)).
+Theorem eval_sub_ptr_int:
+  forall le a b p x y,
+  eval_expr ge sp e m le a (Vptr p x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)).
 Proof.
   intros until y.
-  unfold sub; case (sub_match a b); intros.
-  InvEval H0. rewrite Int.sub_add_opp. 
-    apply eval_addimm_ptr. rewrite E0_right. assumption.
-  InvEval H. FuncInv. InvEval H0. FuncInv.
-    subst b0.
-    replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)).
+  unfold sub; case (sub_match a b); intros; InvEval.
+  rewrite Int.sub_add_opp. 
+    apply eval_addimm_ptr. assumption.
+  subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)).
     apply eval_addimm_ptr. EvalOp.
     subst x; subst y.
     repeat rewrite Int.sub_add_opp.
     repeat rewrite Int.add_assoc. decEq. 
     rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr.
-  InvEval H. FuncInv. subst b0.
-    replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
+  subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
     apply eval_addimm_ptr. EvalOp.
     subst x. rewrite Int.sub_add_l. auto.
-  InvEval H0. FuncInv. 
-    replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
+  replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
     apply eval_addimm_ptr. EvalOp.
     subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. 
   EvalOp.
 Qed.
 
-Lemma eval_sub_ptr_ptr:
-  forall sp le e m1 a t1 m2 p x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vptr p y) ->
-  eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)).
+Theorem eval_sub_ptr_ptr:
+  forall le a b p x y,
+  eval_expr ge sp e m le a (Vptr p x) ->
+  eval_expr ge sp e m le b (Vptr p y) ->
+  eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)).
 Proof.
   intros until y.
-  unfold sub; case (sub_match a b); intros.
-  InvEval H0. 
-  InvEval H. FuncInv. InvEval H0. FuncInv.
-    replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)).
+  unfold sub; case (sub_match a b); intros; InvEval.
+  replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)).
     apply eval_addimm. EvalOp. 
     simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto.
     subst x; subst y.
     repeat rewrite Int.sub_add_opp.
     repeat rewrite Int.add_assoc. decEq. 
     rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr.
-  InvEval H. FuncInv. subst b0.
-    replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
+  subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
     apply eval_addimm. EvalOp.
     simpl. unfold eq_block. rewrite zeq_true. auto.
     subst x. rewrite Int.sub_add_l. auto.
-  InvEval H0. FuncInv. subst b0.
-    replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
+  subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
     apply eval_addimm. EvalOp.
     simpl. unfold eq_block. rewrite zeq_true. auto.
     subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. 
@@ -523,29 +409,29 @@ Proof.
 Qed.
 
 Lemma eval_rolm:
-  forall sp le e m1 a amount mask t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
-  eval_expr ge sp le e m1 (rolm a amount mask) t m2 (Vint (Int.rolm x amount mask)).
+  forall le a amount mask x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (rolm a amount mask) (Vint (Int.rolm x amount mask)).
 Proof.
-  intros until x. unfold rolm; case (rolm_match a); intros.
-  InvEval H. eauto with evalexpr. 
+  intros until x. unfold rolm; case (rolm_match a); intros; InvEval.
+  eauto with evalexpr. 
   case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
-  InvEval H. FuncInv. EvalOp. simpl. subst x. 
+  EvalOp. simpl. subst x. 
   decEq. decEq. 
   replace (Int.and (Int.add amount1 amount) (Int.repr 31))
      with (Int.modu (Int.add amount1 amount) (Int.repr 32)).
   symmetry. apply Int.rolm_rolm. 
   change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one).
   apply Int.modu_and with (Int.repr 5). reflexivity.
-  EvalOp. 
+  EvalOp. econstructor. EvalOp. simpl. rewrite H. reflexivity. constructor. auto.  
   EvalOp.
 Qed.
 
-Lemma eval_shlimm:
-  forall sp le e m1 a n t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
+Theorem eval_shlimm:
+  forall le a n x,
+  eval_expr ge sp e m le a (Vint x) ->
   Int.ltu n (Int.repr 32) = true ->
-  eval_expr ge sp le e m1 (shlimm a n) t m2 (Vint (Int.shl x n)).
+  eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)).
 Proof.
   intros.  unfold shlimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
@@ -555,11 +441,11 @@ Proof.
   apply eval_rolm. auto. symmetry. apply Int.shl_rolm. exact H0.
 Qed.
 
-Lemma eval_shruimm:
-  forall sp le e m1 a n t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
+Theorem eval_shruimm:
+  forall le a n x,
+  eval_expr ge sp e m le a (Vint x) ->
   Int.ltu n (Int.repr 32) = true ->
-  eval_expr ge sp le e m1 (shruimm a n) t m2 (Vint (Int.shru x n)).
+  eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)).
 Proof.
   intros.  unfold shruimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
@@ -570,9 +456,9 @@ Proof.
 Qed.
 
 Lemma eval_mulimm_base:
-  forall sp le e m1 a t n m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
-  eval_expr ge sp le e m1 (mulimm_base n a) t m2 (Vint (Int.mul x n)).
+  forall le a n x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)).
 Proof.
   intros; unfold mulimm_base. 
   generalize (Int.one_bits_decomp n). 
@@ -585,7 +471,7 @@ Proof.
   rewrite Int.add_zero. rewrite <- Int.shl_mul.
   apply eval_shlimm. auto. auto with coqlib. 
   destruct l.
-  intros. apply eval_Elet with t m2 (Vint x) E0. auto.
+  intros. apply eval_Elet with (Vint x). auto.
   rewrite H1. simpl. rewrite Int.add_zero. 
   rewrite Int.mul_add_distr_r.
   rewrite <- Int.shl_mul.
@@ -597,50 +483,48 @@ Proof.
   apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity.
   auto with coqlib.
   auto with evalexpr.
-  reflexivity. traceEq. reflexivity. traceEq. 
+  reflexivity.
   intros. EvalOp. 
 Qed.
 
-Lemma eval_mulimm:
-  forall sp le e m1 a n t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
-  eval_expr ge sp le e m1 (mulimm n a) t m2 (Vint (Int.mul x n)).
+Theorem eval_mulimm:
+  forall le a n x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)).
 Proof.
   intros until x; unfold mulimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
   subst n. rewrite Int.mul_zero. 
-  intro. eapply eval_Elet; eauto with evalexpr. traceEq.
+  intro. eapply eval_Elet; eauto with evalexpr. 
   generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro.
   subst n. rewrite Int.mul_one. auto.
-  case (mulimm_match a); intros.
-  InvEval H1. EvalOp. rewrite Int.mul_commut. reflexivity.
-  InvEval H1. FuncInv. 
+  case (mulimm_match a); intros; InvEval.
+  EvalOp. rewrite Int.mul_commut. reflexivity.
   replace (Int.mul x n) with (Int.add (Int.mul i n) (Int.mul n n2)).
   apply eval_addimm. apply eval_mulimm_base. auto.
   subst x. rewrite Int.mul_add_distr_l. decEq. apply Int.mul_commut.
   apply eval_mulimm_base. assumption.
 Qed.
 
-Lemma eval_mul:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (mul a b) (t1**t2) m3 (Vint (Int.mul x y)).
+Theorem eval_mul:
+  forall le a b x y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)).
 Proof.
   intros until y.
-  unfold mul; case (mul_match a b); intros.
-  InvEval H. rewrite Int.mul_commut. apply eval_mulimm. 
-  rewrite E0_left; auto.
-  InvEval H0. rewrite E0_right. apply eval_mulimm. auto.
+  unfold mul; case (mul_match a b); intros; InvEval.
+  rewrite Int.mul_commut. apply eval_mulimm. auto. 
+  apply eval_mulimm. auto.
   EvalOp.
 Qed.
 
-Lemma eval_divs:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+Theorem eval_divs:
+  forall le a b x y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   y <> Int.zero ->
-  eval_expr ge sp le e m1 (divs a b) (t1**t2) m3 (Vint (Int.divs x y)).
+  eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)).
 Proof.
   TrivialOp divs. simpl. 
   predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto.
@@ -652,11 +536,11 @@ Lemma eval_mod_aux:
    y <> Int.zero ->
    eval_operation ge sp divop (Vint x :: Vint y :: nil) m =
    Some (Vint (semdivop x y))) ->
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+  forall le a b x y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   y <> Int.zero ->
-  eval_expr ge sp le e m1 (mod_aux divop a b) (t1**t2) m3
+  eval_expr ge sp e m le (mod_aux divop a b)
    (Vint (Int.sub x (Int.mul (semdivop x y) y))).
 Proof.
   intros; unfold mod_aux.
@@ -668,21 +552,20 @@ Proof.
   eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil. reflexivity. reflexivity. 
+  apply eval_Enil.  
   apply H. assumption.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil. reflexivity. reflexivity. 
+  apply eval_Enil.  
   simpl; reflexivity. apply eval_Enil. 
-  reflexivity. reflexivity. reflexivity.
-  reflexivity. traceEq.
+  reflexivity.
 Qed.
 
-Lemma eval_mods:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+Theorem eval_mods:
+  forall le a b x y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   y <> Int.zero ->
-  eval_expr ge sp le e m1 (mods a b) (t1**t2) m3 (Vint (Int.mods x y)).
+  eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)).
 Proof.
   intros; unfold mods. 
   rewrite Int.mods_divs. 
@@ -692,232 +575,217 @@ Proof.
 Qed.
 
 Lemma eval_divu_base:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   y <> Int.zero ->
-  eval_expr ge sp le e m1 (Eop Odivu (a ::: b ::: Enil)) (t1**t2) m3 (Vint (Int.divu x y)).
+  eval_expr ge sp e m le (Eop Odivu (a ::: b ::: Enil)) (Vint (Int.divu x y)).
 Proof.
   intros. EvalOp. simpl. 
   predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto.
 Qed.
 
-Lemma eval_divu:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+Theorem eval_divu:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   y <> Int.zero ->
-  eval_expr ge sp le e m1 (divu a b) (t1**t2) m3 (Vint (Int.divu x y)).
+  eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)).
 Proof.
   intros until y.
-  unfold divu; case (divu_match b); intros.
-  InvEval H0. caseEq (Int.is_power2 y). 
+  unfold divu; case (divu_match b); intros; InvEval.
+  caseEq (Int.is_power2 y). 
   intros. rewrite (Int.divu_pow2 x y i H0).
-  apply eval_shruimm. rewrite E0_right. auto.
+  apply eval_shruimm. auto.
   apply Int.is_power2_range with y. auto.
-  intros. subst n2. eapply eval_divu_base. eexact H. EvalOp. auto.
+  intros. apply eval_divu_base. auto. EvalOp. auto.
   eapply eval_divu_base; eauto.
 Qed.
 
-Lemma eval_modu:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+Theorem eval_modu:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   y <> Int.zero ->
-  eval_expr ge sp le e m1 (modu a b) (t1**t2) m3 (Vint (Int.modu x y)).
+  eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)).
 Proof.
-  intros until y; unfold modu; case (divu_match b); intros.
-  InvEval H0. caseEq (Int.is_power2 y). 
+  intros until y; unfold modu; case (divu_match b); intros; InvEval.
+  caseEq (Int.is_power2 y). 
   intros. rewrite (Int.modu_and x y i H0).
-  rewrite <- Int.rolm_zero. apply eval_rolm. rewrite E0_right; auto.
+  rewrite <- Int.rolm_zero. apply eval_rolm. auto.
   intro. rewrite Int.modu_divu. eapply eval_mod_aux. 
   intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero.
   contradiction. auto.
-  eexact H. EvalOp. auto. auto.
+  auto. EvalOp. auto. auto.
   rewrite Int.modu_divu. eapply eval_mod_aux. 
   intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero.
-  contradiction. auto.
-  eexact H. eexact H0. auto. auto.
+  contradiction. auto. auto. auto. auto. auto.
 Qed.
 
-Lemma eval_andimm:
-  forall sp le e m1 n a t m2 x,
-  eval_expr ge sp le e m1 a t m2 (Vint x) ->
-  eval_expr ge sp le e m1 (andimm n a) t m2 (Vint (Int.and x n)).
+Theorem eval_andimm:
+  forall le n a x,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).
 Proof.
   intros.  unfold andimm. case (Int.is_rlw_mask n).
   rewrite <- Int.rolm_zero. apply eval_rolm; auto.
   EvalOp. 
 Qed.
 
-Lemma eval_and:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (and a b) (t1**t2) m3 (Vint (Int.and x y)).
+Theorem eval_and:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (and a b) (Vint (Int.and x y)).
 Proof.
-  intros until y; unfold and; case (mul_match a b); intros.
-  InvEval H. rewrite Int.and_commut. 
-  rewrite E0_left; apply eval_andimm; auto.
-  InvEval H0. rewrite E0_right; apply eval_andimm; auto.
+  intros until y; unfold and; case (mul_match a b); intros; InvEval.
+  rewrite Int.and_commut. apply eval_andimm; auto.
+  apply eval_andimm; auto.
   EvalOp.
 Qed.
 
-Remark eval_same_expr_pure:
-  forall a1 a2 sp le e m1 t1 m2 v1 t2 m3 v2,
+Remark eval_same_expr:
+  forall a1 a2 le v1 v2,
   same_expr_pure a1 a2 = true ->
-  eval_expr ge sp le e m1 a1 t1 m2 v1 ->
-  eval_expr ge sp le e m2 a2 t2 m3 v2 ->
-  t1 = E0 /\ t2 = E0 /\ a2 = a1 /\ v2 = v1 /\ m2 = m1.
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  a1 = a2 /\ v1 = v2.
 Proof.
   intros until v2.
   destruct a1; simpl; try (intros; discriminate). 
   destruct a2; simpl; try (intros; discriminate).
   case (ident_eq i i0); intros.
-  subst i0. inversion H0. inversion H1. 
-  assert (v2 = v1). congruence. tauto.
+  subst i0. inversion H0. inversion H1. split. auto. congruence. 
   discriminate.
 Qed.
 
 Lemma eval_or:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
-  eval_expr ge sp le e m1 (or a b) (t1**t2) m3 (Vint (Int.or x y)).
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).
 Proof.
-  intros until y; unfold or; case (or_match a b); intros.
-  generalize (Int.eq_spec amount1 amount2); case (Int.eq amount1 amount2); intro.
-  case (Int.is_rlw_mask (Int.or mask1 mask2)).
-  caseEq (same_expr_pure t0 t3); intro.
-  simpl. InvEval H. FuncInv. InvEval H0. FuncInv. 
-  generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0).
-  intros [EQ1 [EQ2 [EQ3 [EQ4 EQ5]]]]. 
-  injection EQ4; intro EQ7. subst.
-  EvalOp. simpl. rewrite Int.or_rolm. auto.
-  simpl. EvalOp. 
-  simpl. EvalOp. 
-  simpl. EvalOp. 
+  intros until y; unfold or; case (or_match a b); intros; InvEval.
+  caseEq (Int.eq amount1 amount2 
+          && Int.is_rlw_mask (Int.or mask1 mask2) 
+          && same_expr_pure t1 t2); intro.
+  destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4).
+  generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2.
+  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. 
+  simpl. EvalOp. simpl. rewrite Int.or_rolm. auto.
+  simpl. apply eval_Eop with (Vint x :: Vint y :: nil).
+  econstructor. EvalOp. simpl. congruence. 
+  econstructor. EvalOp. simpl. congruence. constructor. auto.
   EvalOp.
 Qed.
 
-Lemma eval_shl:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+Theorem eval_shl:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   Int.ltu y (Int.repr 32) = true ->
-  eval_expr ge sp le e m1 (shl a b) (t1**t2) m3 (Vint (Int.shl x y)).
+  eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)).
 Proof.
   intros until y; unfold shl; case (shift_match b); intros.
-  InvEval H0. rewrite E0_right. apply eval_shlimm; auto.
+  InvEval. apply eval_shlimm; auto.
   EvalOp. simpl. rewrite H1. auto.
 Qed.
 
-Lemma eval_shru:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+Theorem eval_shru:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
   Int.ltu y (Int.repr 32) = true ->
-  eval_expr ge sp le e m1 (shru a b) (t1**t2) m3 (Vint (Int.shru x y)).
+  eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)).
 Proof.
   intros until y; unfold shru; case (shift_match b); intros.
-  InvEval H0. rewrite E0_right; apply eval_shruimm; auto.
+  InvEval. apply eval_shruimm; auto.
   EvalOp. simpl. rewrite H1. auto.
 Qed.
 
-Lemma eval_addf:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
-  eval_expr ge sp le e m1 (addf a b) (t1**t2) m3 (Vfloat (Float.add x y)).
+Theorem eval_addf:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le b (Vfloat y) ->
+  eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)).
 Proof.
-  intros until y; unfold addf; case (addf_match a b); intros.
-  InvEval H. FuncInv. EvalOp. 
-  econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor.
-  traceEq. simpl. subst x. reflexivity.
-  InvEval H0. FuncInv. eapply eval_Elet. eexact H. EvalOp. 
-  econstructor; eauto with evalexpr. 
-  econstructor; eauto with evalexpr. 
-  econstructor. apply eval_Eletvar. simpl; reflexivity.
-  constructor. reflexivity. traceEq.
-  subst y. rewrite Float.addf_commut. reflexivity. auto.
+  intros until y; unfold addf; case (addf_match a b); intros; InvEval.
+  EvalOp. simpl. congruence.
+  econstructor. eauto. EvalOp. econstructor. eauto with evalexpr. 
+  econstructor. eauto with evalexpr. econstructor. 
+  econstructor. simpl. reflexivity. constructor.
+  simpl. subst y. rewrite Float.addf_commut. auto.
   EvalOp.
 Qed.
  
-Lemma eval_subf:
-  forall sp le e m1 a t1 m2 x b t2 m3 y,
-  eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
-  eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
-  eval_expr ge sp le e m1 (subf a b) (t1**t2) m3 (Vfloat (Float.sub x y)).
+Theorem eval_subf:
+  forall le a x b y,
+  eval_expr ge sp e m le a (Vfloat x) ->
+  eval_expr ge sp e m le b (Vfloat y) ->
+  eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)).
 Proof.
   intros until y; unfold subf; case (subf_match a b); intros.
-  InvEval H. FuncInv. EvalOp. 
-  econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor.
-  traceEq. subst x. reflexivity.
+  InvEval. EvalOp. simpl. congruence. 
   EvalOp.
 Qed.
 
-Lemma eval_cast8signed:
-  forall sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_expr ge sp le e m1 (cast8signed a) t m2 (Val.cast8signed v).
+Theorem eval_cast8signed:
+  forall le a v,
+  eval_expr ge sp e m le a v ->
+  eval_expr ge sp e m le (cast8signed a) (Val.cast8signed v).
 Proof. 
-  intros until v; unfold cast8signed; case (cast8signed_match a); intros.
-  replace (Val.cast8signed v) with v. auto. 
-  InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity.
+  intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity.
   EvalOp.
 Qed.
 
-Lemma eval_cast8unsigned:
-  forall sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_expr ge sp le e m1 (cast8unsigned a) t m2 (Val.cast8unsigned v).
+Theorem eval_cast8unsigned:
+  forall le a v,
+  eval_expr ge sp e m le a v ->
+  eval_expr ge sp e m le (cast8unsigned a) (Val.cast8unsigned v).
 Proof. 
-  intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros.
-  replace (Val.cast8unsigned v) with v. auto. 
-  InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity.
+  intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity.
   EvalOp.
 Qed.
 
-Lemma eval_cast16signed:
-  forall sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_expr ge sp le e m1 (cast16signed a) t m2 (Val.cast16signed v).
+Theorem eval_cast16signed:
+  forall le a v,
+  eval_expr ge sp e m le a v ->
+  eval_expr ge sp e m le (cast16signed a) (Val.cast16signed v).
 Proof. 
-  intros until v; unfold cast16signed; case (cast16signed_match a); intros.
-  replace (Val.cast16signed v) with v. auto. 
-  InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity.
+  intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity.
   EvalOp.
 Qed.
 
-Lemma eval_cast16unsigned:
-  forall sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_expr ge sp le e m1 (cast16unsigned a) t m2 (Val.cast16unsigned v).
+Theorem eval_cast16unsigned:
+  forall le a v,
+  eval_expr ge sp e m le a v ->
+  eval_expr ge sp e m le (cast16unsigned a) (Val.cast16unsigned v).
 Proof. 
-  intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros.
-  replace (Val.cast16unsigned v) with v. auto. 
-  InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity.
+  intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity.
   EvalOp.
 Qed.
 
-Lemma eval_singleoffloat:
-  forall sp le e m1 a t m2 v,
-  eval_expr ge sp le e m1 a t m2 v ->
-  eval_expr ge sp le e m1 (singleoffloat a) t m2 (Val.singleoffloat v).
+Theorem eval_singleoffloat:
+  forall le a v,
+  eval_expr ge sp e m le a v ->
+  eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v).
 Proof. 
-  intros until v; unfold singleoffloat; case (singleoffloat_match a); intros.
-  replace (Val.singleoffloat v) with v. auto. 
-  InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity.
+  intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity.
   EvalOp.
 Qed.
 
 Lemma eval_base_condition_of_expr:
-  forall sp le a e m1 t m2 v (b: bool),
-  eval_expr ge sp le e m1 a t m2 v ->
+  forall le a v b,
+  eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
-  eval_condexpr ge sp le e m1 
+  eval_condexpr ge sp e m le 
                 (CEcond (Ccompimm Cne Int.zero) (a ::: Enil))
-                t m2 b.
+                b.
 Proof.
   intros. 
   eapply eval_CEcond. eauto with evalexpr. 
@@ -925,90 +793,81 @@ Proof.
 Qed.
 
 Lemma eval_condition_of_expr:
-  forall a sp le e m1 t m2 v (b: bool),
-  eval_expr ge sp le e m1 a t m2 v ->
+  forall a le v b,
+  eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
-  eval_condexpr ge sp le e m1 (condexpr_of_expr a) t m2 b.
+  eval_condexpr ge sp e m le (condexpr_of_expr a) b.
 Proof.
   induction a; simpl; intros;
     try (eapply eval_base_condition_of_expr; eauto; fail).
+  
   destruct o; try (eapply eval_base_condition_of_expr; eauto; fail).
 
-  destruct e. InvEval H. inversion XX3; subst v.
+  destruct e0. InvEval. 
   inversion H0. 
   rewrite Int.eq_false; auto. constructor.
   subst i; rewrite Int.eq_true. constructor.
   eapply eval_base_condition_of_expr; eauto.
 
-  inversion H. subst. eapply eval_CEcond; eauto. simpl in H11.
-  destruct (eval_condition c vl); try discriminate.
-  destruct b0; inversion H11; subst; inversion H0; congruence.
+  inv H. eapply eval_CEcond; eauto. simpl in H6. 
+  destruct (eval_condition c vl m); try discriminate.
+  destruct b0; inv H6; inversion H0; congruence.
 
-  inversion H. subst.
-  destruct v1; eauto with evalexpr.
+  inv H. destruct v1; eauto with evalexpr.
 Qed.
 
 Lemma eval_addressing:
-  forall sp le e m1 a t m2 v b ofs,
-  eval_expr ge sp le e m1 a t m2 v ->
+  forall le a v b ofs,
+  eval_expr ge sp e m le a v ->
   v = Vptr b ofs ->
   match addressing a with (mode, args) =>
     exists vl,
-    eval_exprlist ge sp le e m1 args t m2 vl /\ 
+    eval_exprlist ge sp e m le args vl /\ 
     eval_addressing ge sp mode vl = Some v
   end.
 Proof.
-  intros until v. unfold addressing; case (addressing_match a); intros.
-  InvEval H. exists (@nil val). split. eauto with evalexpr. 
-  simpl. auto.
-  InvEval H. exists (@nil val). split. eauto with evalexpr. 
-  simpl. auto.
-  InvEval H. InvEval EV. rewrite E0_left in TR. subst t1. FuncInv. 
-    congruence.
-    destruct (Genv.find_symbol ge s); congruence.
-    exists (Vint i0 :: nil). split. eauto with evalexpr. 
-    simpl. subst v. destruct (Genv.find_symbol ge s). congruence.
-    discriminate.
-  InvEval H. FuncInv. 
-    congruence.
-    exists (Vptr b0 i :: nil). split. eauto with evalexpr. 
+  intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
+  exists (@nil val). split. eauto with evalexpr. simpl. auto.
+  exists (@nil val). split. eauto with evalexpr. simpl. auto.
+  destruct (Genv.find_symbol ge s); congruence.
+  exists (Vint i0 :: nil). split. eauto with evalexpr. 
+    simpl. destruct (Genv.find_symbol ge s). congruence. discriminate.
+  exists (Vptr b0 i :: nil). split. eauto with evalexpr. 
     simpl. congruence.
-  InvEval H. FuncInv. 
-    congruence.
-    exists (Vint i :: Vptr b0 i0 :: nil).
+  exists (Vint i :: Vptr b0 i0 :: nil).
     split. eauto with evalexpr. simpl. 
     rewrite Int.add_commut. congruence.
-    exists (Vptr b0 i :: Vint i0 :: nil).
+  exists (Vptr b0 i :: Vint i0 :: nil).
     split. eauto with evalexpr. simpl. congruence.
   exists (v :: nil). split. eauto with evalexpr. 
     subst v. simpl. rewrite Int.add_zero. auto.
 Qed.
 
 Lemma eval_load:
-  forall sp le e m1 a t m2 v chunk v',
-  eval_expr ge sp le e m1 a t m2 v ->
-  Mem.loadv chunk m2 v = Some v' ->
-  eval_expr ge sp le e m1 (load chunk a) t m2 v'.
+  forall le a v chunk v',
+  eval_expr ge sp e m le a v ->
+  Mem.loadv chunk m v = Some v' ->
+  eval_expr ge sp e m le (load chunk a) v'.
 Proof.
   intros. generalize H0; destruct v; simpl; intro; try discriminate.
   unfold load. 
-  generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)).
+  generalize (eval_addressing _ _ _ _ _ H (refl_equal _)).
   destruct (addressing a). intros [vl [EV EQ]]. 
   eapply eval_Eload; eauto. 
 Qed.
 
 Lemma eval_store:
-  forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 chunk m4,
-  eval_expr ge sp le e m1 a1 t1 m2 v1 ->
-  eval_expr ge sp le e m2 a2 t2 m3 v2 ->
-  Mem.storev chunk m3 v1 v2 = Some m4 ->
-  eval_expr ge sp le e m1 (store chunk a1 a2) (t1**t2) m4 v2.
+  forall chunk a1 a2 v1 v2 m',
+  eval_expr ge sp e m nil a1 v1 ->
+  eval_expr ge sp e m nil a2 v2 ->
+  Mem.storev chunk m v1 v2 = Some m' ->
+  exec_stmt ge sp e m (store chunk a1 a2) E0 e m' Out_normal.
 Proof.
   intros. generalize H1; destruct v1; simpl; intro; try discriminate.
   unfold store.
-  generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)).
+  generalize (eval_addressing _ _ _ _ _ H (refl_equal _)).
   destruct (addressing a1). intros [vl [EV EQ]]. 
-  eapply eval_Estore; eauto. 
+  eapply exec_Sstore; eauto. 
 Qed.
 
 (** * Correctness of instruction selection for operators *)
@@ -1018,10 +877,10 @@ Qed.
   the results of the previous section. *)
 
 Lemma eval_sel_unop:
-  forall sp le e m op a1 t m1 v1 v,
-  eval_expr ge sp le e m a1 t m1 v1 ->
+  forall le op a1 v1 v,
+  eval_expr ge sp e m le a1 v1 ->
   eval_unop op v1 = Some v ->
-  eval_expr ge sp le e m (sel_unop op a1) t m1 v.
+  eval_expr ge sp e m le (sel_unop op a1) v.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   apply eval_cast8unsigned; auto.
@@ -1044,39 +903,39 @@ Proof.
 Qed.
 
 Lemma eval_sel_binop:
-  forall sp le e m op a1 a2 t1 m1 v1 t2 m2 v2 v,
-  eval_expr ge sp le e m a1 t1 m1 v1 ->
-  eval_expr ge sp le e m1 a2 t2 m2 v2 ->
-  eval_binop op v1 v2 m2 = Some v ->
-  eval_expr ge sp le e m (sel_binop op a1 a2) (t1 ** t2) m2 v.
+  forall le op a1 a2 v1 v2 v,
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_binop op v1 v2 m = Some v ->
+  eval_expr ge sp e m le (sel_binop op a1 a2) v.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
-  eapply eval_add; eauto.
-  eapply eval_add_ptr_2; eauto.
-  eapply eval_add_ptr; eauto.
-  eapply eval_sub; eauto.
-  eapply eval_sub_ptr_int; eauto.
+  apply eval_add; auto.
+  apply eval_add_ptr_2; auto.
+  apply eval_add_ptr; auto.
+  apply eval_sub; auto.
+  apply eval_sub_ptr_int; auto.
   destruct (eq_block b b0); inv H1. 
   eapply eval_sub_ptr_ptr; eauto.
-  eapply eval_mul; eauto.
-  generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1.
-  eapply eval_divs; eauto.
-  generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1.
-  eapply eval_divu; eauto.
-  generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1.
-  eapply eval_mods; eauto.
-  generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1.
-  eapply eval_modu; eauto.
-  eapply eval_and; eauto.
-  eapply eval_or; eauto.
+  apply eval_mul; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_divs; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_divu; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_mods; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_modu; eauto.
+  apply eval_and; auto.
+  apply eval_or; auto.
   EvalOp.
   caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
-  eapply eval_shl; eauto.
+  apply eval_shl; auto.
   EvalOp.
   caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
-  eapply eval_shru; eauto.
-  eapply eval_addf; eauto.
-  eapply eval_subf; eauto.
+  apply eval_shru; auto.
+  apply eval_addf; auto.
+  apply eval_subf; auto.
   EvalOp.
   EvalOp.
   EvalOp. simpl. destruct (Int.cmp c i i0); auto. 
@@ -1087,7 +946,7 @@ Proof.
   destruct (Int.eq i0 Int.zero). destruct c; intro EQ; inv EQ; auto.
   auto.
   EvalOp. simpl. 
-  destruct (valid_pointer m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)).
+  destruct (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)).
   destruct (eq_block b b0); inv H1. 
   destruct (Int.cmp c i i0); auto.
   auto.
@@ -1141,21 +1000,15 @@ Proof.
   intros. destruct f; reflexivity.
 Qed.
 
-(** This is the main semantic preservation theorem:
-  instruction selection preserves the semantics of function invocations.
-  The proof is an induction over the Cminor evaluation derivation. *)
+(** Semantic preservation for expressions. *)
 
-Lemma sel_function_correct:
-  forall m fd vargs t m' vres,
-  Cminor.eval_funcall ge m fd vargs t m' vres ->
-  CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres.
+Lemma sel_expr_correct:
+  forall sp e m a v,
+  Cminor.eval_expr ge sp e m a v ->
+  forall le,
+  eval_expr tge sp e m le (sel_expr a) v.
 Proof.
-  apply (Cminor.eval_funcall_ind4 ge
-          (fun sp le e m a t m' v => eval_expr tge sp le e m (sel_expr a) t m' v)
-          (fun sp le e m a t m' v => eval_exprlist tge sp le e m (sel_exprlist a) t m' v)
-          (fun m fd vargs t m' vres => eval_funcall tge m (sel_fundef fd) vargs t m' vres)
-          (fun sp e m s t e' m' out => exec_stmt tge sp e m (sel_stmt s) t e' m' out));
-  intros; simpl.
+  induction 1; intros; simpl.
   (* Evar *)
   constructor; auto.
   (* Econst *)
@@ -1164,40 +1017,65 @@ Proof.
   (* Eunop *)
   eapply eval_sel_unop; eauto.
   (* Ebinop *)
-  subst t. eapply eval_sel_binop; eauto.
+  eapply eval_sel_binop; eauto.
   (* Eload *)
   eapply eval_load; eauto.
-  (* Estore *)
-  subst t. eapply eval_store; eauto.
-  (* Ecall *)
-  econstructor; eauto. apply functions_translated; auto.
-  rewrite <- H4. apply sig_function_translated.
   (* Econdition *)
   econstructor; eauto. eapply eval_condition_of_expr; eauto. 
   destruct b1; auto.
-  (* Elet *)
-  econstructor; eauto.
-  (* Eletvar *)
-  constructor; auto.
-  (* Ealloc *)
-  econstructor; eauto.
-  (* Enil *)
-  constructor.
-  (* Econs *)
-  econstructor; eauto.
+Qed.
+
+Hint Resolve sel_expr_correct: evalexpr.
+
+Lemma sel_exprlist_correct:
+  forall sp e m a v,
+  Cminor.eval_exprlist ge sp e m a v ->
+  forall le,
+  eval_exprlist tge sp e m le (sel_exprlist a) v.
+Proof.
+  induction 1; intros; simpl; constructor; auto with evalexpr.
+Qed.
+
+Hint Resolve sel_exprlist_correct: evalexpr.
+
+(** Semantic preservation for terminating function calls and statements. *)
+
+Definition eval_funcall_exec_stmt_ind2
+  (P1 : mem -> Cminor.fundef -> list val -> trace -> mem -> val -> Prop)
+  (P2 : val -> env -> mem -> Cminor.stmt -> trace -> env -> mem -> outcome -> Prop) :=
+  fun a b c d e f g h i j k l m n o p q r =>
+  conj (Cminor.eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r)
+       (Cminor.exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r).
+
+Lemma sel_function_stmt_correct:
+     (forall m fd vargs t m' vres,
+      Cminor.eval_funcall ge m fd vargs t m' vres ->
+      CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres)
+  /\ (forall sp e m s t e' m' out,
+      Cminor.exec_stmt ge sp e m s t e' m' out ->
+      CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out).
+Proof.
+  apply eval_funcall_exec_stmt_ind2; intros; simpl.
   (* Internal function *)
   econstructor; eauto. 
   (* External function *)
   econstructor; eauto.
   (* Sskip *)
   constructor.
-  (* Sexpr *)
-  econstructor; eauto.
   (* Sassign *)
-  econstructor; eauto.
+  econstructor; eauto with evalexpr. 
+  (* Sstore *)
+  eapply eval_store; eauto with evalexpr. 
+  (* Scall *)
+  econstructor; eauto with evalexpr.
+  apply functions_translated; auto.
+  rewrite <- H2. apply sig_function_translated.
+  (* Salloc *)
+  econstructor; eauto with evalexpr.
   (* Sifthenelse *)
-  econstructor; eauto. eapply eval_condition_of_expr; eauto.
-  destruct b1; auto.
+  econstructor; eauto with evalexpr.
+  eapply eval_condition_of_expr; eauto with evalexpr.
+  destruct b; auto.
   (* Sseq *)
   eapply exec_Sseq_continue; eauto.
   eapply exec_Sseq_stop; eauto.
@@ -1209,32 +1087,97 @@ Proof.
   (* Sexit *)
   constructor.
   (* Sswitch *)
-  econstructor; eauto.
+  econstructor; eauto with evalexpr.
   (* Sreturn *)
   constructor.
-  econstructor; eauto.
+  econstructor; eauto with evalexpr.
   (* Stailcall *)
-  econstructor; eauto. apply functions_translated; auto.
-  rewrite <- H4. apply sig_function_translated.
+  econstructor; eauto with evalexpr.
+  apply functions_translated; auto.
+  rewrite <- H2. apply sig_function_translated.
 Qed.
 
+Lemma sel_function_correct:
+      forall m fd vargs t m' vres,
+      Cminor.eval_funcall ge m fd vargs t m' vres ->
+      CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres.
+Proof (proj1 sel_function_stmt_correct).
+
+Lemma sel_stmt_correct:
+      forall sp e m s t e' m' out,
+      Cminor.exec_stmt ge sp e m s t e' m' out ->
+      CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out.
+Proof (proj2 sel_function_stmt_correct).
+
+Hint Resolve sel_stmt_correct: evalexpr.
+
+(** Semantic preservation for diverging function calls and statements. *)
+
+Lemma sel_function_divergence_correct:
+  forall m fd vargs t,
+  Cminor.evalinf_funcall ge m fd vargs t ->
+  CminorSel.evalinf_funcall tge m (sel_fundef fd) vargs t.
+Proof.
+  cofix FUNCALL.
+  assert (STMT: forall sp e m s t,
+            Cminor.execinf_stmt ge sp e m s t ->
+            CminorSel.execinf_stmt tge sp e m (sel_stmt s) t).
+  cofix STMT; intros.
+  inversion H; subst; simpl.
+  (* Call *)
+  econstructor; eauto with evalexpr.
+  apply functions_translated; auto.
+  apply sig_function_translated.
+  (* Ifthenelse *)
+  econstructor; eauto with evalexpr.
+  eapply eval_condition_of_expr; eauto with evalexpr.
+  destruct b; eapply STMT; eauto.
+  (* Seq *)
+  apply execinf_Sseq_1; eauto.
+  eapply execinf_Sseq_2; eauto with evalexpr.
+  (* Loop *)
+  eapply execinf_Sloop_body; eauto.
+  eapply execinf_Sloop_loop; eauto with evalexpr.
+  change (Sloop (sel_stmt s0)) with (sel_stmt (Cminor.Sloop s0)).
+  apply STMT. auto.
+  (* Block *)
+  apply execinf_Sblock; eauto.
+  (* Tailcall *)
+  econstructor; eauto with evalexpr.
+  apply functions_translated; auto.
+  apply sig_function_translated.
+
+  intros. inv H; simpl.
+  (* Internal functions *)
+  econstructor; eauto with evalexpr.
+  unfold sel_function; simpl. eapply STMT; eauto. 
+Qed. 
+
 End PRESERVATION.
 
 (** As a corollary, instruction selection preserves the observable
    behaviour of programs. *)
 
 Theorem sel_program_correct:
-  forall prog t r,
-  Cminor.exec_program prog t r ->
-  CminorSel.exec_program (sel_program prog) t r.
+  forall prog beh,
+  Cminor.exec_program prog beh ->
+  CminorSel.exec_program (sel_program prog) beh.
 Proof.
-  intros.
-  destruct H as [b [f [m [FINDS [FINDF [SIG EXEC]]]]]].
-  exists b; exists (sel_fundef f); exists m.
-  split. simpl. rewrite <- FINDS. apply symbols_preserved.
-  split. apply function_ptr_translated. auto.
-  split. rewrite <- SIG. apply sig_function_translated. 
+  intros. inv H. 
+  (* Terminating *)
+  apply program_terminates with b (sel_fundef f) m.
+  simpl. rewrite <- H0. unfold ge. apply symbols_preserved.
+  apply function_ptr_translated. auto.
+  rewrite <- H2. apply sig_function_translated. 
   replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog).
   apply sel_function_correct; auto.
   symmetry. unfold sel_program. apply Genv.init_mem_transf.
+  (* Diverging *)
+  apply program_diverges with b (sel_fundef f).
+  simpl. rewrite <- H0. unfold ge. apply symbols_preserved.
+  apply function_ptr_translated. auto.
+  rewrite <- H2. apply sig_function_translated. 
+  replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog).
+  apply sel_function_divergence_correct; auto.
+  symmetry. unfold sel_program. apply Genv.init_mem_transf.
 Qed.