Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


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

16 files changed, 570 insertions, 1300 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index ae86ee8..a9477e0 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -705,22 +705,13 @@ Proof.
   eapply agree_assign_live; eauto.
   eapply agree_reg_list_live; eauto.
 
-  (* Icond, true *)
-  assert (COND: eval_condition cond (map ls (map assign args)) m = Some true).
+  (* Icond *)
+  assert (COND: eval_condition cond (map ls (map assign args)) m = Some b).
     replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
-  eapply exec_Lcond_true; eauto. TranslInstr.
-  MatchStates.
-  eapply agree_undef_temps; eauto.
-  eapply agree_reg_list_live. eauto.
-  (* Icond, false *)
-  assert (COND: eval_condition cond (map ls (map assign args)) m = Some false).
-    replace (map ls (map assign args)) with (rs##args). auto.
-    eapply agree_eval_regs; eauto.
-  econstructor; split.
-  eapply exec_Lcond_false; eauto. TranslInstr.
-  MatchStates.
+  eapply exec_Lcond; eauto. TranslInstr.
+  MatchStates. destruct b; simpl; auto.
   eapply agree_undef_temps; eauto.
   eapply agree_reg_list_live. eauto.
 
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 77da538..c685ef6 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -899,21 +899,14 @@ Proof.
   apply add_unknown_satisfiable. apply wf_kill_loads. apply wf_analyze.
   eapply kill_load_satisfiable; eauto. 
 
-  (* Icond true *)
+  (* Icond *)
   econstructor; split.
-  eapply exec_Icond_true; eauto. 
+  eapply exec_Icond; eauto. 
   econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Icond false *)
-  econstructor; split.
-  eapply exec_Icond_false; eauto. 
-  econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto.
+  destruct b; eapply analysis_correct_1; eauto; simpl; auto;
   unfold transfer; rewrite H; auto.
 
-  (* Icond false *)
+  (* Ijumptable *)
   econstructor; split.
   eapply exec_Ijumptable; eauto. 
   econstructor; eauto.
diff --git a/backend/CastOptim.v b/backend/CastOptim.v
deleted file mode 100644
index 19d0065..0000000
--- a/backend/CastOptim.v
+++ /dev/null
@@ -1,276 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Elimination of redundant conversions to small numerical types. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Globalenvs.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
-
-(** * Static analysis *)
-
-(** Compile-time approximations *)
-
-Inductive approx : Type :=
-  | Unknown               (**r any value *)
-  | Int7                  (**r [[0,127]] *)
-  | Int8s                 (**r [[-128,127]] *)
-  | Int8u                 (**r [[0,255]] *)
-  | Int15                 (**r [[0,32767]] *)
-  | Int16s                (**r [[-32768,32767]] *)
-  | Int16u                (**r [[0,65535]] *)
-  | Single                (**r single-precision float *)
-  | Novalue.              (**r empty *)
-
-(** We equip this type of approximations with a semi-lattice structure.
-  The ordering is inclusion between the sets of values denoted by
-  the approximations. *)
-
-Module Approx <: SEMILATTICE_WITH_TOP.
-  Definition t := approx.
-  Definition eq (x y: t) := (x = y).
-  Definition eq_refl: forall x, eq x x := (@refl_equal t).
-  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
-  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
-  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
-  Proof.
-    decide equality.
-  Qed.
-  Definition beq (x y: t) := if eq_dec x y then true else false.
-  Lemma beq_correct: forall x y, beq x y = true -> x = y.
-  Proof.
-    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
-  Qed.
-  Definition ge (x y: t) : Prop :=
-    match x, y with
-    | Unknown, _ => True
-    | _, Novalue => True
-    | Int7, Int7 => True
-    | Int8s, (Int7 | Int8s) => True
-    | Int8u, (Int7 | Int8u) => True
-    | Int15, (Int7 | Int8u | Int15) => True
-    | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => True
-    | Int16u, (Int7 | Int8u | Int15 | Int16u) => True
-    | Single, Single => True
-    | _, _ => False
-    end.
-  Lemma ge_refl: forall x y, eq x y -> ge x y.
-  Proof.
-    unfold eq, ge; intros. subst y. destruct x; auto.
-  Qed.
-  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Proof.
-    unfold ge; intros.
-    destruct x; auto; (destruct y; auto; try contradiction; destruct z; auto).
-  Qed.
-  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-  Proof.
-    unfold eq; intros. congruence.
-  Qed.
-  Definition bge (x y: t) : bool :=
-    match x, y with
-    | Unknown, _ => true
-    | _, Novalue => true
-    | Int7, Int7 => true
-    | Int8s, (Int7 | Int8s) => true
-    | Int8u, (Int7 | Int8u) => true
-    | Int15, (Int7 | Int8u | Int15) => true
-    | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => true
-    | Int16u, (Int7 | Int8u | Int15 | Int16u) => true
-    | Single, Single => true
-    | _, _ => false
-    end.
-  Lemma bge_correct: forall x y, bge x y = true -> ge x y.
-  Proof.
-    destruct x; destruct y; simpl; auto || congruence.
-  Qed.
-  Definition bot := Novalue.
-  Definition top := Unknown.
-  Lemma ge_bot: forall x, ge x bot.
-  Proof.
-    unfold ge, bot. destruct x; auto. 
-  Qed.
-  Lemma ge_top: forall x, ge top x.
-  Proof.
-    unfold ge, top. auto.
-  Qed.
-  Definition lub (x y: t) : t :=
-    match x, y with
-    | Novalue, _ => y
-    | _, Novalue => x
-    | Int7, Int7 => Int7
-    | Int7, Int8u => Int8u
-    | Int7, Int8s => Int8s
-    | Int7, Int15 => Int15
-    | Int7, Int16u => Int16u
-    | Int7, Int16s => Int16s
-    | Int8u, (Int7|Int8u) => Int8u
-    | Int8u, Int15 => Int15
-    | Int8u, Int16u => Int16u
-    | Int8u, Int16s => Int16s
-    | Int8s, (Int7|Int8s) => Int8s
-    | Int8s, (Int15|Int16s) => Int16s
-    | Int15, (Int7|Int8u|Int15) => Int15
-    | Int15, Int16u => Int16u
-    | Int15, (Int8s|Int16s) => Int16s
-    | Int16u, (Int7|Int8u|Int15|Int16u) => Int16u
-    | Int16s, (Int7|Int8u|Int8s|Int15|Int16s) => Int16s
-    | Single, Single => Single
-    | _, _ => Unknown
-    end.
-  Lemma ge_lub_left: forall x y, ge (lub x y) x.
-  Proof.
-    unfold lub, ge; intros.
-    destruct x; destruct y; auto. 
-  Qed.
-  Lemma ge_lub_right: forall x y, ge (lub x y) y.
-  Proof.
-    unfold lub, ge; intros.
-    destruct x; destruct y; auto. 
-  Qed.
-End Approx.
-
-Module D := LPMap Approx.
-
-(** Abstract interpretation of operators *)
-
-Definition approx_bitwise_op (v1 v2: approx) : approx :=
-  if Approx.bge Int8u v1 && Approx.bge Int8u v2 then Int8u
-  else if Approx.bge Int16u v1 && Approx.bge Int16u v2 then Int16u
-  else Unknown.
-
-Function approx_operation (op: operation) (vl: list approx) : approx :=
-  match op, vl with
-  | Omove, v1 :: nil => v1
-  | Ointconst n, _ =>
-      if Int.eq_dec n (Int.zero_ext 7 n) then Int7
-      else if Int.eq_dec n (Int.zero_ext 8 n) then Int8u
-      else if Int.eq_dec n (Int.sign_ext 8 n) then Int8s
-      else if Int.eq_dec n (Int.zero_ext 15 n) then Int15
-      else if Int.eq_dec n (Int.zero_ext 16 n) then Int16u
-      else if Int.eq_dec n (Int.sign_ext 16 n) then Int16s
-      else Unknown
-  | Ofloatconst n, _ =>
-      if Float.eq_dec n (Float.singleoffloat n) then Single else Unknown
-  | Ocast8signed, _ => Int8s
-  | Ocast8unsigned, _ => Int8u
-  | Ocast16signed, _ => Int16s
-  | Ocast16unsigned, _ => Int16u
-  | Osingleoffloat, _ => Single
-  | Oand, v1 :: v2 :: nil => approx_bitwise_op v1 v2
-  | Oor, v1 :: v2 :: nil => approx_bitwise_op v1 v2
-  | Oxor, v1 :: v2 :: nil => approx_bitwise_op v1 v2
-  (* Problem: what about and/or/xor immediate? and other
-     machine-specific operators? *)
-  | Ocmp c, _ => Int7
-  | _, _ => Unknown
-  end.
-
-Definition approx_of_chunk (chunk: memory_chunk) :=
-  match chunk with
-  | Mint8signed => Int8s
-  | Mint8unsigned => Int8u
-  | Mint16signed => Int16s
-  | Mint16unsigned => Int16u
-  | Mint32 => Unknown
-  | Mfloat32 => Single
-  | Mfloat64 => Unknown
-  end.
-
-(** Transfer function for the analysis *)
-
-Definition approx_reg (app: D.t) (r: reg) := 
-  D.get r app.
-
-Definition approx_regs (app: D.t) (rl: list reg):=
-  List.map (approx_reg app) rl.
-
-Definition transfer (f: function) (pc: node) (before: D.t) :=
-  match f.(fn_code)!pc with
-  | None => before
-  | Some i =>
-      match i with
-      | Iop op args res s =>
-          let a := approx_operation op (approx_regs before args) in
-          D.set res a before
-      | Iload chunk addr args dst s =>
-          D.set dst (approx_of_chunk chunk) before
-      | Icall sig ros args res s =>
-          D.set res Unknown before
-      | Ibuiltin ef args res s =>
-          D.set res Unknown before
-      | _ =>
-          before
-      end
-  end.
-
-(** The static analysis is a forward dataflow analysis. *)
-
-Module DS := Dataflow_Solver(D)(NodeSetForward).
-
-Definition analyze (f: RTL.function): PMap.t D.t :=
-  match DS.fixpoint (successors f) (transfer f) 
-                    ((f.(fn_entrypoint), D.top) :: nil) with
-  | None => PMap.init D.top
-  | Some res => res
-  end.
-
-(** * Code transformation *)
-
-(** Cast operations that have no effect (because the argument is already
-    in the right range) are turned into moves. *)
-
-Function transf_operation (op: operation) (vl: list approx) : operation :=
-  match op, vl with
-  | Ocast8signed, v :: nil => if Approx.bge Int8s v then Omove else op
-  | Ocast8unsigned, v :: nil => if Approx.bge Int8u v then Omove else op
-  | Ocast16signed, v :: nil => if Approx.bge Int16s v then Omove else op
-  | Ocast16unsigned, v :: nil => if Approx.bge Int16u v then Omove else op
-  | Osingleoffloat, v :: nil => if Approx.bge Single v then Omove else op
-  | _, _ => op
-  end.
-
-Definition transf_instr (app: D.t) (instr: instruction) :=
-  match instr with
-  | Iop op args res s =>
-      let op' := transf_operation op (approx_regs app args) in
-      Iop op' args res s
-  | _ =>
-      instr
-  end.
-
-Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code :=
-  PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs.
-
-Definition transf_function (f: function) : function :=
-  let approxs := analyze f in
-  mkfunction
-    f.(fn_sig)
-    f.(fn_params)
-    f.(fn_stacksize)
-    (transf_code approxs f.(fn_code))
-    f.(fn_entrypoint).
-
-Definition transf_fundef (fd: fundef) : fundef :=
-  AST.transf_fundef transf_function fd.
-
-Definition transf_program (p: program) : program :=
-  transform_program transf_fundef p.
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v
deleted file mode 100644
index 0afc208..0000000
--- a/backend/CastOptimproof.v
+++ /dev/null
@@ -1,577 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Correctness proof for cast optimization. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Events.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
-Require Import CastOptim.
-
-(** * Correctness of the static analysis *)
-
-Section ANALYSIS.
-
-Definition val_match_approx (a: approx) (v: val) : Prop :=
-  match a with
-  | Novalue => False
-  | Int7 => v = Val.zero_ext 8 v /\ v = Val.sign_ext 8 v
-  | Int8u => v = Val.zero_ext 8 v
-  | Int8s => v = Val.sign_ext 8 v
-  | Int15 => v = Val.zero_ext 16 v /\ v = Val.sign_ext 16 v
-  | Int16u => v = Val.zero_ext 16 v
-  | Int16s => v = Val.sign_ext 16 v
-  | Single => v = Val.singleoffloat v
-  | Unknown => True
-  end.
-
-Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
-  forall r, val_match_approx (D.get r a) rs#r.
-
-Lemma regs_match_approx_top:
-  forall rs, regs_match_approx D.top rs.
-Proof.
-  intros. red; intros. simpl. rewrite PTree.gempty. 
-  unfold Approx.top, val_match_approx. auto.
-Qed.
-
-Lemma val_match_approx_increasing:
-  forall a1 a2 v,
-  Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v.
-Proof.
-  assert (A: forall v, v = Val.zero_ext 8 v -> v = Val.zero_ext 16 v).
-    intros. rewrite H.
-    destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
-  assert (B: forall v, v = Val.sign_ext 8 v -> v = Val.sign_ext 16 v).
-    intros. rewrite H.
-    destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.sign_ext_widen. compute; auto. split. omega. compute; auto.
-  assert (C: forall v, v = Val.zero_ext 8 v -> v = Val.sign_ext 16 v).
-    intros. rewrite H.
-    destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto.
-  intros. destruct a1; destruct a2; simpl in *; intuition; auto.
-Qed.
-
-Lemma regs_match_approx_increasing:
-  forall a1 a2 rs,
-  D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs.
-Proof.
-  unfold D.ge, regs_match_approx. intros.
-  apply val_match_approx_increasing with (D.get r a2); auto.
-Qed.
-
-Lemma regs_match_approx_update:
-  forall ra rs a v r,
-  val_match_approx a v ->
-  regs_match_approx ra rs ->
-  regs_match_approx (D.set r a ra) (rs#r <- v).
-Proof.
-  intros; red; intros. rewrite Regmap.gsspec. 
-  case (peq r0 r); intro.
-  subst r0. rewrite D.gss. auto.
-  rewrite D.gso; auto. 
-Qed.
-
-Lemma approx_regs_val_list:
-  forall ra rs rl,
-  regs_match_approx ra rs ->
-  list_forall2 val_match_approx (approx_regs ra rl) rs##rl.
-Proof.
-  induction rl; simpl; intros.
-  constructor.
-  constructor. apply H. auto.
-Qed.
-
-Lemma analyze_correct:
-  forall f pc rs pc' i,
-  f.(fn_code)!pc = Some i ->
-  In pc' (successors_instr i) ->
-  regs_match_approx (transfer f pc (analyze f)!!pc) rs ->
-  regs_match_approx (analyze f)!!pc' rs.
-Proof.
-  intros until i. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
-                      ((fn_entrypoint f, D.top) :: nil)).
-  intros approxs; intros.
-  apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
-  eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
-  auto.
-  intros. rewrite PMap.gi. apply regs_match_approx_top. 
-Qed.
-
-Lemma analyze_correct_start:
-  forall f rs,
-  regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs.
-Proof.
-  intros. unfold analyze. 
-  caseEq (DS.fixpoint (successors f) (transfer f)
-                      ((fn_entrypoint f, D.top) :: nil)).
-  intros approxs; intros.
-  apply regs_match_approx_increasing with D.top.
-  eapply DS.fixpoint_entry; eauto. auto with coqlib.
-  apply regs_match_approx_top. 
-  intros. rewrite PMap.gi. apply regs_match_approx_top.
-Qed.
-
-Lemma approx_bitwise_correct:
-  forall (sem_op: int -> int -> int) a1 n1 a2 n2,
-  (forall a b c, sem_op (Int.and a c) (Int.and b c) = Int.and (sem_op a b) c) ->
-  val_match_approx a1 (Vint n1) -> val_match_approx a2 (Vint n2) ->
-  val_match_approx (approx_bitwise_op a1 a2) (Vint (sem_op n1 n2)).
-Proof.
-  intros.
-  assert (forall N, 0 < N < Z_of_nat Int.wordsize ->
-    sem_op (Int.zero_ext N n1) (Int.zero_ext N n2) =
-    Int.zero_ext N (sem_op (Int.zero_ext N n1) (Int.zero_ext N n2))).
-  intros. repeat rewrite Int.zero_ext_and; auto. rewrite H. 
-  rewrite Int.and_assoc. rewrite Int.and_idem. auto.
-  unfold approx_bitwise_op. 
-  caseEq (Approx.bge Int8u a1 && Approx.bge Int8u a2); intro EQ1.
-  destruct (andb_prop _ _ EQ1).
-  assert (V1: val_match_approx Int8u (Vint n1)).
-    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
-  assert (V2: val_match_approx Int8u (Vint n2)).
-    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
-  simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto.
-  caseEq (Approx.bge Int16u a1 && Approx.bge Int16u a2); intro EQ2.
-  destruct (andb_prop _ _ EQ2).
-  assert (V1: val_match_approx Int16u (Vint n1)).
-    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
-  assert (V2: val_match_approx Int16u (Vint n2)).
-    eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto.
-  simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto.
-  exact I.
-Qed.
-
-Lemma approx_operation_correct:
-  forall app rs (ge: genv) sp op args m v,
-  regs_match_approx app rs ->
-  eval_operation ge sp op rs##args m = Some v ->
-  val_match_approx (approx_operation op (approx_regs app args)) v.
-Proof.
-  intros. destruct op; simpl; try (exact I). 
-(* move *)
-  destruct args; try (exact I). destruct args; try (exact I). 
-  simpl. simpl in H0. inv H0. apply H. 
-(* const int *)
-  destruct args; simpl in H0; inv H0.
-  destruct (Int.eq_dec i (Int.zero_ext 7 i)). red; simpl.
-    split.
-    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
-    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
-  destruct (Int.eq_dec i (Int.zero_ext 8 i)). red; simpl; congruence.
-  destruct (Int.eq_dec i (Int.sign_ext 8 i)). red; simpl; congruence.
-  destruct (Int.eq_dec i (Int.zero_ext 15 i)). red; simpl.
-    split.
-    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
-    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
-  destruct (Int.eq_dec i (Int.zero_ext 16 i)). red; simpl; congruence.
-  destruct (Int.eq_dec i (Int.sign_ext 16 i)). red; simpl; congruence.
-  exact I.
-(* const float *)
-  destruct args; simpl in H0; inv H0. 
-  destruct (Float.eq_dec f (Float.singleoffloat f)). red; simpl; congruence.
-  exact I.
-(* cast8signed *)
-  destruct args; simpl in H0; try congruence.
-  destruct args; simpl in H0; try congruence.
-  inv H0. destruct (rs#p); simpl; auto.
-  decEq. symmetry. apply Int.sign_ext_idem. compute; auto.
-(* cast8unsigned *)
-  destruct args; simpl in H0; try congruence.
-  destruct args; simpl in H0; try congruence.
-  inv H0. destruct (rs#p); simpl; auto.
-  decEq. symmetry. apply Int.zero_ext_idem. compute; auto.
-(* cast16signed *)
-  destruct args; simpl in H0; try congruence.
-  destruct args; simpl in H0; try congruence.
-  inv H0. destruct (rs#p); simpl; auto.
-  decEq. symmetry. apply Int.sign_ext_idem. compute; auto.
-(* cast16unsigned *)
-  destruct args; simpl in H0; try congruence.
-  destruct args; simpl in H0; try congruence.
-  inv H0. destruct (rs#p); simpl; auto.
-  decEq. symmetry. apply Int.zero_ext_idem. compute; auto.
-(* and *)
-  destruct args; try (exact I).
-  destruct args; try (exact I).
-  destruct args; try (exact I).
-  generalize (H p) (H p0). simpl in *. FuncInv. subst. 
-  apply approx_bitwise_correct; auto.
-  intros. repeat rewrite Int.and_assoc. decEq. 
-  rewrite (Int.and_commut b c). rewrite <- Int.and_assoc. rewrite Int.and_idem. auto.
-(* or *)
-  destruct args; try (exact I).
-  destruct args; try (exact I).
-  destruct args; try (exact I).
-  generalize (H p) (H p0). simpl in *. FuncInv. subst. 
-  apply approx_bitwise_correct; auto.
-  intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). 
-  rewrite <- Int.and_or_distrib. apply Int.and_commut.
-(* xor *)
-  destruct args; try (exact I).
-  destruct args; try (exact I).
-  destruct args; try (exact I).
-  generalize (H p) (H p0). simpl in *. FuncInv. subst. 
-  apply approx_bitwise_correct; auto.
-  intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). 
-  rewrite <- Int.and_xor_distrib. apply Int.and_commut.
-(* singleoffloat *)
-  destruct args; simpl in H0; try congruence.
-  destruct args; simpl in H0; try congruence.
-  inv H0. destruct (rs#p); simpl; auto.
-  decEq. rewrite Float.singleoffloat_idem; auto.
-(* comparison *)
-  simpl in H0. destruct (eval_condition c rs##args); try discriminate.
-  destruct b; inv H0; compute; auto. 
-Qed.
-
-Lemma approx_of_chunk_correct:
-  forall chunk m a v,
-  Mem.loadv chunk m a = Some v ->
-  val_match_approx (approx_of_chunk chunk) v.
-Proof.
-  intros. destruct a; simpl in H; try discriminate.
-  exploit Mem.load_cast; eauto. 
-  destruct chunk; intros; simpl; auto.
-Qed.
-
-End ANALYSIS.
-
-(** * Correctness of the code transformation *)
-
-Section PRESERVATION.
-
-Variable prog: program.
-Let tprog := transf_program prog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Lemma symbols_preserved:
-  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program. 
-  apply Genv.find_symbol_transf.
-Qed.
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program. 
-  apply Genv.find_var_info_transf.
-Qed.
-
-Lemma functions_translated:
-  forall (v: val) (f: fundef),
-  Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef f).
-Proof.  
-  intros.
-  exact (Genv.find_funct_transf transf_fundef _ _ H).
-Qed.
-
-Lemma function_ptr_translated:
-  forall (b: block) (f: fundef),
-  Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef f).
-Proof.  
-  intros. 
-  exact (Genv.find_funct_ptr_transf transf_fundef _ _ H).
-Qed.
-
-Lemma sig_function_translated:
-  forall f,
-  funsig (transf_fundef f) = funsig f.
-Proof.
-  intros. destruct f; reflexivity.
-Qed.
-
-Lemma find_function_translated:
-  forall ros rs fd,
-  find_function ge ros rs = Some fd ->
-  find_function tge ros rs = Some (transf_fundef fd).
-Proof.
-  intros. destruct ros; simpl in *. 
-  apply functions_translated; auto. 
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence.
-  apply function_ptr_translated; auto.
-Qed.
-
-(** Correctness of [transf_operation]. *)
-
-Lemma transf_operation_correct:
-  forall (ge: genv) app rs sp op args m v,
-  regs_match_approx app rs ->
-  eval_operation ge sp op rs##args m = Some v ->
-  eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args m = Some v.
-Proof.
-  intros until v. intro RMA.
-  assert (A: forall a r, Approx.bge a (approx_reg app r) = true -> val_match_approx a rs#r).
-    intros. eapply val_match_approx_increasing. apply Approx.bge_correct; eauto. apply RMA.
-Opaque Approx.bge.
-  destruct op; simpl; auto.
-(* cast8signed *)
-  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
-  intros EQ; inv EQ.
-  caseEq (Approx.bge Int8s (approx_reg app p)); intros.
-  exploit A; eauto. unfold val_match_approx. simpl. congruence.
-  auto.
-(* cast8unsigned *)
-  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
-  intros EQ; inv EQ.
-  caseEq (Approx.bge Int8u (approx_reg app p)); intros.
-  exploit A; eauto. unfold val_match_approx. simpl. congruence.
-  auto.
-(* cast8signed *)
-  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
-  intros EQ; inv EQ.
-  caseEq (Approx.bge Int16s (approx_reg app p)); intros.
-  exploit A; eauto. unfold val_match_approx. simpl. congruence.
-  auto.
-(* cast8unsigned *)
-  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
-  intros EQ; inv EQ.
-  caseEq (Approx.bge Int16u (approx_reg app p)); intros.
-  exploit A; eauto. unfold val_match_approx. simpl. congruence.
-  auto.
-(* singleoffloat *)
-  destruct args; simpl; try congruence. destruct args; simpl; try congruence. 
-  intros EQ; inv EQ.
-  caseEq (Approx.bge Single (approx_reg app p)); intros.
-  exploit A; eauto. unfold val_match_approx. simpl. congruence.
-  auto.
-Qed.
-
-(** Matching between states. *)
-
-Inductive match_stackframes: stackframe -> stackframe -> Prop :=
-   match_stackframe_intro:
-      forall res sp pc rs f,
-      (forall v, regs_match_approx (analyze f)!!pc (rs#res <- v)) ->
-    match_stackframes
-        (Stackframe res f sp pc rs)
-        (Stackframe res (transf_function f) sp pc rs).
-
-Inductive match_states: state -> state -> Prop :=
-  | match_states_intro:
-      forall s sp pc rs m f s'
-           (MATCH: regs_match_approx (analyze f)!!pc rs)
-           (STACKS: list_forall2 match_stackframes s s'),
-      match_states (State s f sp pc rs m)
-                   (State s' (transf_function f) sp pc rs m)
-  | match_states_call:
-      forall s f args m s',
-      list_forall2 match_stackframes s s' ->
-      match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args m)
-  | match_states_return:
-      forall s s' v m,
-      list_forall2 match_stackframes s s' ->
-      match_states (Returnstate s v m)
-                   (Returnstate s' v m).
-
-Ltac TransfInstr :=
-  match goal with
-  | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ =>
-      cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr));
-      [ simpl transf_instr
-      | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; 
-        unfold option_map; rewrite H1; reflexivity ]
-  end.
-
-(** The proof of semantic preservation follows from the lock-step simulation lemma below. *)
-
-Lemma transf_step_correct:
-  forall s1 t s2,
-  step ge s1 t s2 ->
-  forall s1' (MS: match_states s1 s1'),
-  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
-Proof.
-  induction 1; intros; inv MS.
-
-  (* Inop *)
-  econstructor; split. 
-  TransfInstr; intro. eapply exec_Inop; eauto.
-  econstructor; eauto.
-  eapply analyze_correct with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. auto.
-
-  (* Iop *)
-  exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
-  TransfInstr; intro. eapply exec_Iop; eauto.
-  apply transf_operation_correct; auto.
-  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
-  econstructor; eauto.
-  eapply analyze_correct with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. apply regs_match_approx_update; auto. 
-  eapply approx_operation_correct; eauto. 
-
-  (* Iload *)
-  econstructor; split. 
-  TransfInstr; intro. eapply exec_Iload with (a := a). eauto. 
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eauto.
-  econstructor; eauto.
-  eapply analyze_correct with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. apply regs_match_approx_update; auto.
-  eapply approx_of_chunk_correct; eauto. 
-
-  (* Istore *)
-  econstructor; split. 
-  TransfInstr; intro. eapply exec_Istore with (a := a). eauto.
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eauto.
-  econstructor; eauto.
-  eapply analyze_correct with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. auto.
-
-  (* Icall *)
-  TransfInstr; intro.
-  econstructor; split.
-  eapply exec_Icall. eauto. apply find_function_translated; eauto.
-  apply sig_function_translated; auto.
-  constructor; auto. constructor; auto.
-  econstructor; eauto. 
-  intros. eapply analyze_correct; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  apply regs_match_approx_update; auto. exact I.
-
-  (* Itailcall *)
-  TransfInstr; intro.
-  econstructor; split.
-  eapply exec_Itailcall. eauto. apply find_function_translated; eauto.
-  apply sig_function_translated; auto.
-  simpl; eauto. 
-  constructor; auto.
-
-  (* Ibuiltin *)
-  TransfInstr. intro.
-  exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split.
-  eapply exec_Ibuiltin; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact varinfo_preserved.
-  econstructor; eauto. 
-  eapply analyze_correct; eauto. simpl; auto. 
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. exact I.
-
-  (* Icond, true *)
-  exists (State s' (transf_function f) sp ifso rs m); split. 
-  TransfInstr. intro.
-  eapply exec_Icond_true; eauto.
-  econstructor; eauto.
-  eapply analyze_correct; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Icond, false *)
-  exists (State s' (transf_function f) sp ifnot rs m); split. 
-  TransfInstr. intro.
-  eapply exec_Icond_false; eauto.
-  econstructor; eauto.
-  eapply analyze_correct; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Ijumptable *)
-  exists (State s' (transf_function f) sp pc' rs m); split.
-  TransfInstr. intro.
-  eapply exec_Ijumptable; eauto.
-  constructor; auto.
-  eapply analyze_correct; eauto.
-  simpl. eapply list_nth_z_in; eauto.
-  unfold transfer; rewrite  H; auto.
-
-  (* Ireturn *)
-  exists (Returnstate s' (regmap_optget or Vundef rs) m'); split.
-  eapply exec_Ireturn; eauto. TransfInstr; auto.
-  constructor; auto.
-
-  (* internal function *)
-  simpl. unfold transf_function.
-  econstructor; split.
-  eapply exec_function_internal; simpl; eauto.
-  simpl. econstructor; eauto.
-  apply analyze_correct_start; auto.
-
-  (* external function *)
-  simpl. econstructor; split.
-  eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact varinfo_preserved.
-  constructor; auto.
-
-  (* return *)
-  inv H3. inv H1. 
-  econstructor; split.
-  eapply exec_return; eauto. 
-  econstructor; eauto. 
-Qed.
-
-Lemma transf_initial_states:
-  forall st1, initial_state prog st1 ->
-  exists st2, initial_state tprog st2 /\ match_states st1 st2.
-Proof.
-  intros. inversion H.
-  exploit function_ptr_translated; eauto. intro FIND.
-  exists (Callstate nil (transf_fundef f) nil m0); split.
-  econstructor; eauto.
-  apply Genv.init_mem_transf; auto.
-  replace (prog_main tprog) with (prog_main prog).
-  rewrite symbols_preserved. eauto.
-  reflexivity.
-  rewrite <- H3. apply sig_function_translated.
-  constructor. constructor.
-Qed.
-
-Lemma transf_final_states:
-  forall st1 st2 r, 
-  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
-Proof.
-  intros. inv H0. inv H. inv H4. constructor. 
-Qed.
-
-(** The preservation of the observable behavior of the program then
-  follows. *)
-
-Theorem transf_program_correct:
-  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
-Proof.
-  eapply forward_simulation_step.
-  eexact symbols_preserved.
-  eexact transf_initial_states.
-  eexact transf_final_states.
-  exact transf_step_correct. 
-Qed.
-
-End PRESERVATION.
-
-
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 45efdf9..c9ee5b5 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -216,93 +216,53 @@ Definition eval_constant (sp: val) (cst: constant) : option val :=
   | Ointconst n => Some (Vint n)
   | Ofloatconst n => Some (Vfloat n)
   | Oaddrsymbol s ofs =>
-      match Genv.find_symbol ge s with
-      | None => None
-      | Some b => Some (Vptr b ofs)
-      end
-  | Oaddrstack ofs =>
-      match sp with
-      | Vptr b n => Some (Vptr b (Int.add n ofs))
-      | _ => None
-      end
+      Some(match Genv.find_symbol ge s with
+           | None => Vundef
+           | Some b => Vptr b ofs end)
+  | Oaddrstack ofs => Some (Val.add sp (Vint ofs))
   end.
 
 Definition eval_unop (op: unary_operation) (arg: val) : option val :=
-  match op, arg with
-  | Ocast8unsigned, _ => Some (Val.zero_ext 8 arg)
-  | Ocast8signed, _ => Some (Val.sign_ext 8 arg)
-  | Ocast16unsigned, _ => Some (Val.zero_ext 16 arg)
-  | Ocast16signed, _ => Some (Val.sign_ext 16 arg)
-  | Onegint, Vint n1 => Some (Vint (Int.neg n1))
-  | Onotbool, Vint n1 => Some (Val.of_bool (Int.eq n1 Int.zero))
-  | Onotbool, Vptr b1 n1 => Some Vfalse
-  | Onotint, Vint n1 => Some (Vint (Int.not n1))
-  | Onegf, Vfloat f1 => Some (Vfloat (Float.neg f1))
-  | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1))
-  | Osingleoffloat, _ => Some (Val.singleoffloat arg)
-  | Ointoffloat, Vfloat f1 => option_map Vint (Float.intoffloat f1)
-  | Ointuoffloat, Vfloat f1 => option_map Vint (Float.intuoffloat f1)
-  | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1))
-  | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1))
-  | _, _ => None
+  match op with
+  | Ocast8unsigned => Some (Val.zero_ext 8 arg)
+  | Ocast8signed => Some (Val.sign_ext 8 arg)
+  | Ocast16unsigned => Some (Val.zero_ext 16 arg)
+  | Ocast16signed => Some (Val.sign_ext 16 arg)
+  | Onegint => Some (Val.negint arg)
+  | Onotbool => Some (Val.notbool arg)
+  | Onotint => Some (Val.notint arg)
+  | Onegf => Some (Val.negf arg)
+  | Oabsf => Some (Val.absf arg)
+  | Osingleoffloat => Some (Val.singleoffloat arg)
+  | Ointoffloat => Val.intoffloat arg
+  | Ointuoffloat => Val.intuoffloat arg
+  | Ofloatofint => Val.floatofint arg
+  | Ofloatofintu => Val.floatofintu arg
   end.
 
-Definition eval_compare_mismatch (c: comparison) : option val :=
-  match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end.
-
-Definition eval_compare_null (c: comparison) (n: int) : option val :=
-  if Int.eq n Int.zero then eval_compare_mismatch c else None.
-
 Definition eval_binop
             (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
-  match op, arg1, arg2 with
-  | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
-  | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1))
-  | Oadd, Vptr b1 n1, Vint n2 => Some (Vptr b1 (Int.add n1 n2))
-  | Osub, Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
-  | Osub, Vptr b1 n1, Vint n2 => Some (Vptr b1 (Int.sub n1 n2))
-  | Osub, Vptr b1 n1, Vptr b2 n2 =>
-      if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None
-  | Omul, Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
-  | Odiv, Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2))
-  | Odivu, Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
-  | Omod, Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
-  | Omodu, Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
-  | Oand, Vint n1, Vint n2 => Some (Vint (Int.and n1 n2))
-  | Oor, Vint n1, Vint n2 => Some (Vint (Int.or n1 n2))
-  | Oxor, Vint n1, Vint n2 => Some (Vint (Int.xor n1 n2))
-  | Oshl, Vint n1, Vint n2 =>
-      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None
-  | Oshr, Vint n1, Vint n2 =>
-      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
-  | Oshru, Vint n1, Vint n2 =>
-      if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
-   | Oaddf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.add f1 f2))
-  | Osubf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.sub f1 f2))
-  | Omulf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
-  | Odivf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.div f1 f2))
-  | Ocmp c, Vint n1, Vint n2 =>
-      Some (Val.of_bool(Int.cmp c n1 n2))
-  | Ocmpu c, Vint n1, Vint n2 =>
-      Some (Val.of_bool(Int.cmpu c n1 n2))
-  | Ocmpu c, Vptr b1 n1, Vptr b2 n2 =>
-      if Mem.valid_pointer m b1 (Int.unsigned n1)
-      && Mem.valid_pointer m b2 (Int.unsigned n2) then
-        if eq_block b1 b2
-        then Some(Val.of_bool(Int.cmpu c n1 n2))
-        else eval_compare_mismatch c
-      else None
-  | Ocmpu c, Vptr b1 n1, Vint n2 =>
-      eval_compare_null c n2
-  | Ocmpu c, Vint n1, Vptr b2 n2 =>
-      eval_compare_null c n1
-  | Ocmpf c, Vfloat f1, Vfloat f2 =>
-      Some (Val.of_bool (Float.cmp c f1 f2))
-  | _, _, _ => None
+  match op with
+  | Oadd => Some (Val.add arg1 arg2)
+  | Osub => Some (Val.sub arg1 arg2)
+  | Omul => Some (Val.mul arg1 arg2)
+  | Odiv => Val.divs arg1 arg2
+  | Odivu => Val.divu arg1 arg2
+  | Omod => Val.mods arg1 arg2
+  | Omodu => Val.modu arg1 arg2
+  | Oand => Some (Val.and arg1 arg2)
+  | Oor => Some (Val.or arg1 arg2)
+  | Oxor => Some (Val.xor arg1 arg2)
+  | Oshl => Some (Val.shl arg1 arg2)
+  | Oshr => Some (Val.shr arg1 arg2)
+  | Oshru => Some (Val.shru arg1 arg2)
+  | Oaddf => Some (Val.addf arg1 arg2)
+  | Osubf => Some (Val.subf arg1 arg2)
+  | Omulf => Some (Val.mulf arg1 arg2)
+  | Odivf => Some (Val.divf arg1 arg2)
+  | Ocmp c => Some (Val.cmp c arg1 arg2)
+  | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2)
+  | Ocmpf c => Some (Val.cmpf c arg1 arg2)
   end.
 
 (** Evaluation of an expression: [eval_expr ge sp e m a v]
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 39568a3..4c303ac 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -50,14 +50,16 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     apply Float.eq_dec.
     apply Int.eq_dec.
     apply ident_eq.
+    apply Int.eq_dec.
   Qed.
   Definition beq (x y: t) := if eq_dec x y then true else false.
   Lemma beq_correct: forall x y, beq x y = true -> x = y.
   Proof.
     unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
   Qed.
-  Definition ge (x y: t) : Prop :=
-    x = Unknown \/ y = Novalue \/ x = y.
+
+  Definition ge (x y: t) : Prop := x = Unknown \/ y = Novalue \/ x = y.
+
   Lemma ge_refl: forall x y, eq x y -> ge x y.
   Proof.
     unfold eq, ge; tauto.
@@ -165,7 +167,7 @@ Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
   match ros with
   | inl r =>
       match D.get r app with
-      | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
+      | G symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
       | _ => ros
       end
   | inr s => ros
@@ -179,17 +181,19 @@ Definition transf_instr (app: D.t) (instr: instruction) :=
           Iop (Ointconst n) nil res s
       | F n =>
           Iop (Ofloatconst n) nil res s
-      | S symb ofs =>
+      | G symb ofs =>
           Iop (Oaddrsymbol symb ofs) nil res s
+      | S ofs =>
+          Iop (Oaddrstack ofs) nil res s
       | _ =>
-          let (op', args') := op_strength_reduction (approx_reg app) op args in
+          let (op', args') := op_strength_reduction op args (approx_regs app args) in
           Iop op' args' res s
       end
   | Iload chunk addr args dst s =>
-      let (addr', args') := addr_strength_reduction (approx_reg app) addr args in
+      let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
       Iload chunk addr' args' dst s      
   | Istore chunk addr args src s =>
-      let (addr', args') := addr_strength_reduction (approx_reg app) addr args in
+      let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
       Istore chunk addr' args' src s      
   | Icall sig ros args res s =>
       Icall sig (transf_ros app ros) args res s
@@ -200,17 +204,17 @@ Definition transf_instr (app: D.t) (instr: instruction) :=
       | Some b =>
           if b then Inop s1 else Inop s2
       | None =>
-          let (cond', args') := cond_strength_reduction (approx_reg app) cond args in
+          let (cond', args') := cond_strength_reduction cond args (approx_regs app args) in
           Icond cond' args' s1 s2
       end
   | Ijumptable arg tbl =>
-      match intval (approx_reg app) arg with
-      | Some n =>
+      match approx_reg app arg with
+      | I n =>
           match list_nth_z tbl (Int.unsigned n) with
           | Some s => Inop s
           | None => instr
           end
-      | None => instr
+      | _ => instr
       end
   | _ =>
       instr
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 058d68e..7ac4339 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -36,9 +36,10 @@ Require Import ConstpropOpproof.
 Section ANALYSIS.
 
 Variable ge: genv.
+Variable sp: val.
 
 Definition regs_match_approx (a: D.t) (rs: regset) : Prop :=
-  forall r, val_match_approx ge (D.get r a) rs#r.
+  forall r, val_match_approx ge sp (D.get r a) rs#r.
 
 Lemma regs_match_approx_top:
   forall rs, regs_match_approx D.top rs.
@@ -49,7 +50,7 @@ Qed.
 
 Lemma val_match_approx_increasing:
   forall a1 a2 v,
-  Approx.ge a1 a2 -> val_match_approx ge a2 v -> val_match_approx ge a1 v.
+  Approx.ge a1 a2 -> val_match_approx ge sp a2 v -> val_match_approx ge sp a1 v.
 Proof.
   intros until v.
   intros [A|[B|C]].
@@ -68,7 +69,7 @@ Qed.
 
 Lemma regs_match_approx_update:
   forall ra rs a v r,
-  val_match_approx ge a v ->
+  val_match_approx ge sp a v ->
   regs_match_approx ra rs ->
   regs_match_approx (D.set r a ra) (rs#r <- v).
 Proof.
@@ -81,14 +82,13 @@ Qed.
 Lemma approx_regs_val_list:
   forall ra rs rl,
   regs_match_approx ra rs ->
-  val_list_match_approx ge (approx_regs ra rl) rs##rl.
+  val_list_match_approx ge sp (approx_regs ra rl) rs##rl.
 Proof.
   induction rl; simpl; intros.
   constructor.
   constructor. apply H. auto.
 Qed.
 
-
 (** The correctness of the static analysis follows from the results
   of module [ConstpropOpproof] and the fact that the result of
   the static analysis is a solution of the forward dataflow inequations. *)
@@ -178,26 +178,56 @@ Proof.
   intros. destruct f; reflexivity.
 Qed.
 
+Definition regs_lessdef (rs1 rs2: regset) : Prop :=
+  forall r, Val.lessdef (rs1#r) (rs2#r).
+
+Lemma regs_lessdef_regs:
+  forall rs1 rs2, regs_lessdef rs1 rs2 ->
+  forall rl, Val.lessdef_list rs1##rl rs2##rl.
+Proof.
+  induction rl; constructor; auto.
+Qed.
+
+Lemma set_reg_lessdef:
+  forall r v1 v2 rs1 rs2,
+  Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2).
+Proof.
+  intros; red; intros. repeat rewrite Regmap.gsspec. 
+  destruct (peq r0 r); auto.
+Qed.
+
+Lemma init_regs_lessdef:
+  forall rl vl1 vl2,
+  Val.lessdef_list vl1 vl2 ->
+  regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl).
+Proof.
+  induction rl; simpl; intros.
+  red; intros. rewrite Regmap.gi. auto.
+  inv H. red; intros. rewrite Regmap.gi. auto.
+  apply set_reg_lessdef; auto.
+Qed.
+
 Lemma transf_ros_correct:
-  forall ros rs f approx,
-  regs_match_approx ge approx rs ->
+  forall sp ros rs rs' f approx,
+  regs_match_approx ge sp approx rs ->
   find_function ge ros rs = Some f ->
-  find_function tge (transf_ros approx ros) rs = Some (transf_fundef f).
+  regs_lessdef rs rs' ->
+  find_function tge (transf_ros approx ros) rs' = Some (transf_fundef f).
 Proof.
-  intros until approx; intro MATCH.
-  destruct ros; simpl.
-  intro.
-  exploit functions_translated; eauto. intro FIND.  
-  caseEq (D.get r approx); intros; auto.
-  generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto.
-  generalize (MATCH r). rewrite H0. intros [b [A B]].
-  rewrite <- symbols_preserved in A.
-  rewrite B in FIND. rewrite H1 in FIND. 
-  rewrite Genv.find_funct_find_funct_ptr in FIND.
-  simpl. rewrite A. auto.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
-  intro. apply function_ptr_translated. auto.
-  congruence.
+  intros. destruct ros; simpl in *.
+  generalize (H r); intro MATCH. generalize (H1 r); intro LD.
+  destruct (rs#r); simpl in H0; try discriminate.
+  destruct (Int.eq_dec i Int.zero); try discriminate.
+  inv LD. 
+  assert (find_function tge (inl _ r) rs' = Some (transf_fundef f)).
+    simpl. rewrite <- H4. simpl. rewrite dec_eq_true. apply function_ptr_translated. auto.
+  destruct (D.get r approx); auto.
+  predSpec Int.eq Int.eq_spec i0 Int.zero; intros; auto.
+  simpl in *. unfold symbol_address in MATCH. rewrite symbols_preserved.
+  destruct (Genv.find_symbol ge i); try discriminate. 
+  inv MATCH. apply function_ptr_translated; auto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try discriminate.
+  apply function_ptr_translated; auto.
 Qed.
 
 (** The proof of semantic preservation is a simulation argument
@@ -227,29 +257,37 @@ Qed.
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
    match_stackframe_intro:
-      forall res sp pc rs f,
-      (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) ->
+      forall res sp pc rs f rs',
+      regs_lessdef rs rs' ->
+      (forall v, regs_match_approx ge sp (analyze f)!!pc (rs#res <- v)) ->
     match_stackframes
         (Stackframe res f sp pc rs)
-        (Stackframe res (transf_function f) sp pc rs).
+        (Stackframe res (transf_function f) sp pc rs').
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
-      forall s sp pc rs m f s'
-           (MATCH: regs_match_approx ge (analyze f)!!pc rs)
-           (STACKS: list_forall2 match_stackframes s s'),
+      forall s sp pc rs m f s' rs' m'
+           (MATCH: regs_match_approx ge sp (analyze f)!!pc rs)
+           (STACKS: list_forall2 match_stackframes s s')
+           (REGS: regs_lessdef rs rs')
+           (MEM: Mem.extends m m'),
       match_states (State s f sp pc rs m)
-                   (State s' (transf_function f) sp pc rs m)
+                   (State s' (transf_function f) sp pc rs' m')
   | match_states_call:
-      forall s f args m s',
-      list_forall2 match_stackframes s s' ->
+      forall s f args m s' args' m'
+           (STACKS: list_forall2 match_stackframes s s')
+           (ARGS: Val.lessdef_list args args')
+           (MEM: Mem.extends m m'),
       match_states (Callstate s f args m)
-                   (Callstate s' (transf_fundef f) args m)
+                   (Callstate s' (transf_fundef f) args' m')
   | match_states_return:
-      forall s s' v m,
+      forall s v m s' v' m'
+           (STACKS: list_forall2 match_stackframes s s')
+           (RES: Val.lessdef v v')
+           (MEM: Mem.extends m m'),
       list_forall2 match_stackframes s s' ->
       match_states (Returnstate s v m)
-                   (Returnstate s' v m).
+                   (Returnstate s' v' m').
 
 Ltac TransfInstr :=
   match goal with
@@ -272,7 +310,7 @@ Proof.
   induction 1; intros; inv MS.
 
   (* Inop *)
-  exists (State s' (transf_function f) sp pc' rs m); split.
+  exists (State s' (transf_function f) sp pc' rs' m'); split.
   TransfInstr; intro. eapply exec_Inop; eauto.
   econstructor; eauto.
   eapply analyze_correct_1 with (pc := pc); eauto.
@@ -280,58 +318,78 @@ Proof.
   unfold transfer; rewrite H. auto.
 
   (* Iop *)
-  exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split.
-  TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args);
-  intros op' args' OSR.
-  assert (eval_operation tge sp op' rs##args' m = Some v).
-    rewrite (eval_operation_preserved _ _ symbols_preserved). 
-    generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs m
-                  MATCH op args v).
-    rewrite OSR; simpl. auto.
-  generalize (eval_static_operation_correct ge op sp
-               (approx_regs (analyze f)!!pc args) rs##args m v
-               (approx_regs_val_list _ _ _ args MATCH) H0).
-  case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros;
-  simpl in H2;
-  eapply exec_Iop; eauto; simpl.
-  congruence.
-  congruence.
-  elim H2; intros b [A B]. rewrite symbols_preserved. 
-  rewrite A; rewrite B; auto.
-  econstructor; eauto. 
-  eapply analyze_correct_1 with (pc := pc); eauto.
-  simpl; auto.
-  unfold transfer; rewrite H. 
-  apply regs_match_approx_update; auto. 
-  eapply eval_static_operation_correct; eauto.
-  apply approx_regs_val_list; auto.
+  assert (MATCH': regs_match_approx ge sp (analyze f) # pc' rs # res <- v).
+    eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto.
+    unfold transfer; rewrite H. 
+    apply regs_match_approx_update; auto. 
+    eapply eval_static_operation_correct; eauto.
+    apply approx_regs_val_list; auto.
+  TransfInstr.
+  exploit eval_static_operation_correct; eauto. eapply approx_regs_val_list; eauto. intros VM.
+  destruct (eval_static_operation op (approx_regs (analyze f) # pc args)); intros; simpl in VM.
+  (* Novalue *)
+  contradiction.
+  (* Unknown *)
+  exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. 
+  destruct (op_strength_reduction op args (approx_regs (analyze f) # pc args)) as [op' args'].
+  intros [v' [EV' LD']].
+  assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v'').
+    eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto.
+  destruct EV'' as [v'' [EV'' LD'']].
+  exists (State s' (transf_function f) sp pc' (rs'#res <- v'') m'); split.
+  econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved.
+  econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
+  (* I i *)
+  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vint i)) m'); split.
+  econstructor; eauto.
+  econstructor; eauto. apply set_reg_lessdef; auto.
+  (* F *)
+  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vfloat f0)) m'); split.
+  econstructor; eauto.
+  econstructor; eauto. apply set_reg_lessdef; auto.
+  (* G *)
+  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (symbol_address tge i i0)) m'); split.
+  econstructor; eauto.
+  econstructor; eauto. apply set_reg_lessdef; auto.
+  unfold symbol_address. rewrite symbols_preserved; auto. 
+  (* S *)
+  subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Val.add sp (Vint i))) m'); split.
+  econstructor; eauto.
+  econstructor; eauto. apply set_reg_lessdef; auto.
 
   (* Iload *)
-  caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
-  intros addr' args' ASR.
-  assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved _ _ symbols_preserved). 
-    generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
-                  MATCH addr args).
-    rewrite ASR; simpl. congruence. 
-  TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split.
+  TransfInstr. 
+  generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs
+                  MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)).
+  destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args'].
+  intros P Q. rewrite H0 in P.
+  assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
+    eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto.
+  destruct ADDR' as [a' [A B]].
+  assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
+    rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  exploit Mem.loadv_extends; eauto. intros [v' [D E]].
+  exists (State s' (transf_function f) sp pc' (rs'#dst <- v') m'); split.
   eapply exec_Iload; eauto.
   econstructor; eauto. 
   eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
+  apply set_reg_lessdef; auto. 
 
   (* Istore *)
-  caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args);
-  intros addr' args' ASR.
-  assert (eval_addressing tge sp addr' rs##args' = Some a).
-    rewrite (eval_addressing_preserved _ _ symbols_preserved). 
-    generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs
-                  MATCH addr args).
-    rewrite ASR; simpl. congruence. 
-  TransfInstr. rewrite ASR. intro.
-  exists (State s' (transf_function f) sp pc' rs m'); split.
+  TransfInstr.
+  generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs
+                  MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)).
+  destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args'].
+  intros P Q. rewrite H0 in P.
+  assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a').
+    eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto.
+  destruct ADDR' as [a' [A B]].
+  assert (C: eval_addressing tge sp addr' rs'##args' = Some a').
+    rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
+  exploit Mem.storev_extends; eauto. intros [m2' [D E]].
+  exists (State s' (transf_function f) sp pc' rs' m2'); split.
   eapply exec_Istore; eauto.
   econstructor; eauto. 
   eapply analyze_correct_1; eauto. simpl; auto. 
@@ -347,17 +405,22 @@ Proof.
   intros. eapply analyze_correct_1; eauto. simpl; auto.
   unfold transfer; rewrite H.
   apply regs_match_approx_update; auto. simpl. auto.
+  apply regs_lessdef_regs; auto. 
 
   (* Itailcall *)
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   exploit transf_ros_correct; eauto. intros FIND'.
   TransfInstr; intro.
   econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
-  constructor; auto. 
+  constructor; auto. apply regs_lessdef_regs; auto. 
 
   (* Ibuiltin *)
+  exploit external_call_mem_extends; eauto. 
+  instantiate (1 := rs'##args). apply regs_lessdef_regs; auto.
+  intros [v' [m2' [A [B [C D]]]]].
   TransfInstr. intro.
-  exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split.
+  exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split.
   eapply exec_Ibuiltin; eauto.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
@@ -365,72 +428,61 @@ Proof.
   eapply analyze_correct_1; eauto. simpl; auto. 
   unfold transfer; rewrite H. 
   apply regs_match_approx_update; auto. simpl; auto.
-
-  (* Icond, true *)
-  exists (State s' (transf_function f) sp ifso rs m); split. 
-  caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
-  intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' m = Some true).
-    generalize (cond_strength_reduction_correct
-                  ge (approx_reg (analyze f)!!pc) rs m MATCH cond args).
-    rewrite CSR.  intro. congruence.
-  TransfInstr. rewrite CSR. 
-  caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
-  intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ m _
-               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
-  replace b with true. intro; eapply exec_Inop; eauto. congruence.
-  intros. eapply exec_Icond_true; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
-
-  (* Icond, false *)
-  exists (State s' (transf_function f) sp ifnot rs m); split. 
-  caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args);
-  intros cond' args' CSR.
-  assert (eval_condition cond' rs##args' m = Some false).
-    generalize (cond_strength_reduction_correct
-                  ge (approx_reg (analyze f)!!pc) rs m MATCH cond args).
-    rewrite CSR.  intro. congruence.
-  TransfInstr. rewrite CSR. 
-  caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)).
-  intros b ESC. 
-  generalize (eval_static_condition_correct ge cond _ _ m _
-               (approx_regs_val_list _ _ _ args MATCH) ESC); intro.
-  replace b with false. intro; eapply exec_Inop; eauto. congruence.
-  intros. eapply exec_Icond_false; eauto.
-  econstructor; eauto.
-  eapply analyze_correct_1; eauto.
-  simpl; auto.
-  unfold transfer; rewrite H; auto.
+  apply set_reg_lessdef; auto.
+
+  (* Icond *)
+  TransfInstr. 
+  generalize (cond_strength_reduction_correct ge sp (analyze f)#pc rs m
+                    MATCH cond args (approx_regs (analyze f) # pc args) (refl_equal _)).
+  destruct (cond_strength_reduction cond args (approx_regs (analyze f) # pc args)) as [cond' args'].
+  intros EV1. 
+  exists (State s' (transf_function f) sp (if b then ifso else ifnot) rs' m'); split. 
+  destruct (eval_static_condition cond (approx_regs (analyze f) # pc args)) as []_eqn.
+  assert (eval_condition cond rs ## args m = Some b0).
+    eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto.
+  assert (b = b0) by congruence. subst b0.
+  destruct b; eapply exec_Inop; eauto. 
+  eapply exec_Icond; eauto.
+  eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence.
+  econstructor; eauto. 
+  eapply analyze_correct_1; eauto. destruct b; simpl; auto. 
+  unfold transfer; rewrite H. auto. 
 
   (* Ijumptable *)
-  exists (State s' (transf_function f) sp pc' rs m); split.
-  caseEq (intval (approx_reg (analyze f)!!pc) arg); intros.
-  exploit intval_correct; eauto. eexact MATCH. intro VRS.
-  eapply exec_Inop; eauto. TransfInstr. rewrite H2. 
-  replace i with n by congruence. rewrite H1. auto.
-  eapply exec_Ijumptable; eauto. TransfInstr. rewrite H2. auto.
-  constructor; auto.
+  assert (A: (fn_code (transf_function f))!pc = Some(Ijumptable arg tbl)
+             \/ (fn_code (transf_function f))!pc = Some(Inop pc')).
+  TransfInstr. destruct (approx_reg (analyze f) # pc arg) as []_eqn; auto.
+  generalize (MATCH arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. 
+  simpl. intro EQ; inv EQ. rewrite H1. auto.
+  assert (B: rs'#arg = Vint n).
+  generalize (REGS arg); intro LD; inv LD; congruence.
+  exists (State s' (transf_function f) sp pc' rs' m'); split.
+  destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. 
+  econstructor; eauto.
   eapply analyze_correct_1; eauto.
   simpl. eapply list_nth_z_in; eauto.
   unfold transfer; rewrite  H; auto.
 
   (* Ireturn *)
-  exists (Returnstate s' (regmap_optget or Vundef rs) m'); split.
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
+  exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
   constructor; auto.
+  destruct or; simpl; auto. 
 
   (* internal function *)
+  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
+  intros [m2' [A B]].
   simpl. unfold transf_function.
   econstructor; split.
   eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
   apply analyze_correct_3; auto.
+  apply init_regs_lessdef; auto.
 
   (* external function *)
+  exploit external_call_mem_extends; eauto. 
+  intros [v' [m2' [A [B [C D]]]]].
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto.
@@ -441,7 +493,7 @@ Proof.
   inv H3. inv H1. 
   econstructor; split.
   eapply exec_return; eauto. 
-  econstructor; eauto. 
+  econstructor; eauto. apply set_reg_lessdef; auto. 
 Qed.
 
 Lemma transf_initial_states:
@@ -457,14 +509,14 @@ Proof.
   rewrite symbols_preserved. eauto.
   reflexivity.
   rewrite <- H3. apply sig_function_translated.
-  constructor. constructor.
+  constructor. constructor. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H4. constructor. 
+  intros. inv H0. inv H. inv STACKS. inv RES. constructor. 
 Qed.
 
 (** The preservation of the observable behavior of the program then
diff --git a/backend/LTL.v b/backend/LTL.v
index 5ed0a8f..422b0e0 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -207,18 +207,13 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge (map rs args) m t v m' ->
       step (State s f sp pc rs m)
          t (State s f sp pc' (Locmap.set res v rs) m')
-  | exec_Lcond_true:
-      forall s f sp pc rs m cond args ifso ifnot,
+  | exec_Lcond:
+      forall s f sp pc rs m cond args ifso ifnot b pc',
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) m = Some true ->
+      eval_condition cond (map rs args) m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
       step (State s f sp pc rs m)
-        E0 (State s f sp ifso (undef_temps rs) m)
-  | exec_Lcond_false:
-      forall s f sp pc rs m cond args ifso ifnot,
-      (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
-      eval_condition cond (map rs args) m = Some false ->
-      step (State s f sp pc rs m)
-        E0 (State s f sp ifnot (undef_temps rs) m)
+        E0 (State s f sp pc' (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp pc rs m arg tbl n pc',
       (fn_code f)!pc = Some(Ljumptable arg tbl) ->
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 2f96a09..50db0c6 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -629,12 +629,14 @@ Proof.
   traceEq.
   econstructor; eauto.
 
-  (* Lcond true *)
+  (* Lcond *)
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
+  destruct b.
+  (* true *)
   assert (REACH': (reachable f)!!ifso = true).
   eapply reachable_successors; eauto. simpl; auto.
-  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  exploit find_label_lin_succ; eauto. inv WTI; eauto. intros [c'' AT'].
   destruct (starts_with ifso c').
   econstructor; split.
   eapply plus_left'.  
@@ -648,10 +650,7 @@ Proof.
   econstructor; split.
   apply plus_one. eapply exec_Lcond_true; eauto.
   econstructor; eauto.
-
-  (* Lcond false *)
-  destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
-  simpl in EQ. subst c.
+  (* false *)
   assert (REACH': (reachable f)!!ifnot = true).
   eapply reachable_successors; eauto. simpl; auto.
   exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
diff --git a/backend/RTL.v b/backend/RTL.v
index 10d4a3f..6a20941 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -255,18 +255,13 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge rs##args m t v m' ->
       step (State s f sp pc rs m)
          t (State s f sp pc' (rs#res <- v) m')
-  | exec_Icond_true:
-      forall s f sp pc rs m cond args ifso ifnot,
+  | exec_Icond:
+      forall s f sp pc rs m cond args ifso ifnot b pc',
       (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args m = Some true ->
+      eval_condition cond rs##args m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
       step (State s f sp pc rs m)
-        E0 (State s f sp ifso rs m)
-  | exec_Icond_false:
-      forall s f sp pc rs m cond args ifso ifnot,
-      (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
-      eval_condition cond rs##args m = Some false ->
-      step (State s f sp pc rs m)
-        E0 (State s f sp ifnot rs m)
+        E0 (State s f sp pc' rs m)
   | exec_Ijumptable:
       forall s f sp pc rs m arg tbl n pc',
       (fn_code f)!pc = Some(Ijumptable arg tbl) ->
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 55cdd6b..c5182db 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -427,22 +427,22 @@ Proof.
 (* ifeq *)
   caseEq (Int.eq i key); intro EQ; rewrite EQ in H5.
   inv H5. exists nfound; exists rs; intuition.
-  apply star_one. eapply exec_Icond_true; eauto. 
-  simpl. rewrite H2. congruence.
+  apply star_one. eapply exec_Icond with (b := true); eauto. 
+  simpl. rewrite H2. simpl. congruence.
   exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
   exists nd1; exists rs1; intuition.
-  eapply star_step. eapply exec_Icond_false; eauto. 
-  simpl. rewrite H2. congruence. eexact EX. traceEq.
+  eapply star_step. eapply exec_Icond with (b := false); eauto. 
+  simpl. rewrite H2. simpl. congruence. eexact EX. traceEq.
 (* iflt *)
   caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5.
   exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
   exists nd1; exists rs1; intuition.
-  eapply star_step. eapply exec_Icond_true; eauto. 
-  simpl. rewrite H2. congruence. eexact EX. traceEq.
+  eapply star_step. eapply exec_Icond with (b := true); eauto. 
+  simpl. rewrite H2. simpl. congruence. eexact EX. traceEq.
   exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
   exists nd1; exists rs1; intuition.
-  eapply star_step. eapply exec_Icond_false; eauto. 
-  simpl. rewrite H2. congruence. eexact EX. traceEq.
+  eapply star_step. eapply exec_Icond with (b := false); eauto. 
+  simpl. rewrite H2. simpl. congruence. eexact EX. traceEq.
 (* jumptable *)
   set (rs1 := rs#rt <- (Vint(Int.sub i ofs))).
   assert (ME1: match_env map e nil rs1).
@@ -451,21 +451,21 @@ Proof.
     eapply exec_Iop; eauto. 
     predSpec Int.eq Int.eq_spec ofs Int.zero; simpl.
     rewrite H10. rewrite Int.sub_zero_l. congruence.
-    rewrite H6. rewrite <- Int.sub_add_opp. auto. 
+    rewrite H6. simpl. rewrite <- Int.sub_add_opp. auto. 
   caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9.
   exploit H5; eauto. intros [nd [A B]].
   exists nd; exists rs1; intuition. 
   eapply star_step. eexact EX1.
-  eapply star_step. eapply exec_Icond_true; eauto. 
-  simpl. unfold rs1. rewrite Regmap.gss. congruence. 
+  eapply star_step. eapply exec_Icond with (b := true); eauto. 
+  simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. 
   apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss. 
   reflexivity. traceEq.
   exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto.
   intros [nd [rs' [EX [NTH ME]]]].
   exists nd; exists rs'; intuition.
   eapply star_step. eexact EX1.
-  eapply star_step. eapply exec_Icond_false; eauto. 
-  simpl. unfold rs1. rewrite Regmap.gss. congruence.
+  eapply star_step. eapply exec_Icond with (b := false); eauto. 
+  simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence.
   eexact EX. reflexivity. traceEq.
 Qed.
 
@@ -739,11 +739,8 @@ Proof.
   exists rs1.
 (* Exec *)
   split. eapply star_right. eexact EX1. 
-  destruct b.
-  eapply exec_Icond_true; eauto. 
-  rewrite RES1. assumption.
-  eapply exec_Icond_false; eauto. 
-  rewrite RES1. assumption.
+  eapply exec_Icond with (b := b); eauto. 
+  rewrite RES1. auto.
   traceEq.
 (* Match-env *)
   split. assumption.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 02359b9..65506c8 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -565,7 +565,6 @@ Proof.
   rewrite H6. eapply external_call_well_typed; eauto. 
   (* Icond *)
   econstructor; eauto.
-  econstructor; eauto.
   (* Ijumptable *)
   econstructor; eauto.
   (* Ireturn *)
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 6ee9263..75c7dad 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -1154,7 +1154,7 @@ Proof.
   eapply star_right. eauto. 
   eapply exec_Lstore with (a := ta); eauto.
     simpl reglist. rewrite G. unfold ls3. rewrite Locmap.gss. simpl. 
-    destruct ta; simpl in Y; try discriminate. rewrite Int.add_zero. auto.
+    destruct ta; simpl in Y; try discriminate. simpl; rewrite Int.add_zero; auto.
   reflexivity. reflexivity. traceEq. 
   econstructor; eauto with coqlib.
   apply agree_undef_temps2. apply agree_exten with ls; auto.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d6c850a..54d59b1 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -147,8 +147,9 @@ Proof.
 
   inv H0. simpl in H7.
   assert (eval_condition c vl m = Some b).
-    destruct (eval_condition c vl m); try discriminate.
+    destruct (eval_condition c vl m).
     destruct b0; inv H7; inversion H1; congruence.
+    inv H7. inv H1.
   assert (eval_condexpr ge sp e m le (CEcond c e0) b).
     eapply eval_CEcond; eauto.
   destruct e0; auto. destruct e1; auto.
@@ -204,7 +205,7 @@ Lemma eval_sel_unop:
   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 e m le (sel_unop op a1) v.
+  exists v', eval_expr ge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   apply eval_cast8unsigned; auto.
@@ -212,19 +213,15 @@ Proof.
   apply eval_cast16unsigned; auto.
   apply eval_cast16signed; auto.
   apply eval_negint; auto.
-  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro.
-  change true with (negb false). eapply eval_notbool; eauto. subst i; constructor.
-  change false with (negb true). eapply eval_notbool; eauto. constructor; auto.
-  change Vfalse with (Val.of_bool (negb true)).
-  eapply eval_notbool; eauto. constructor.
+  apply eval_notbool; auto.
   apply eval_notint; auto.
   apply eval_negf; auto.
   apply eval_absf; auto.
   apply eval_singleoffloat; auto.
-  remember (Float.intoffloat f) as oi; destruct oi; inv H0. eapply eval_intoffloat; eauto.
-  remember (Float.intuoffloat f) as oi; destruct oi; inv H0. eapply eval_intuoffloat; eauto.
-  apply eval_floatofint; auto.
-  apply eval_floatofintu; auto.
+  eapply eval_intoffloat; eauto.
+  eapply eval_intuoffloat; eauto.
+  eapply eval_floatofint; eauto.
+  eapply eval_floatofintu; eauto.
 Qed.
 
 Lemma eval_sel_binop:
@@ -232,48 +229,29 @@ Lemma eval_sel_binop:
   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.
+  exists v', eval_expr ge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   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.
-  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_mul; auto.
+  eapply eval_divs; eauto.
+  eapply eval_divu; eauto.
+  eapply eval_mods; eauto.
+  eapply eval_modu; eauto.
   apply eval_and; auto.
   apply eval_or; auto.
   apply eval_xor; auto.
-  caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1.
   apply eval_shl; auto.
-  caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1.
   apply eval_shr; auto.
-  caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1.
   apply eval_shru; auto.
   apply eval_addf; auto.
   apply eval_subf; auto.
   apply eval_mulf; auto.
   apply eval_divf; auto.
   apply eval_comp; auto.
-  eapply eval_compu_int; eauto.
-  eapply eval_compu_int_ptr; eauto.
-  eapply eval_compu_ptr_int; eauto.
-  destruct (Mem.valid_pointer m b (Int.unsigned i) &&
-            Mem.valid_pointer m b0 (Int.unsigned i0)) as [] _eqn; try congruence.
-  destruct (eq_block b b0); inv H1.
-  eapply eval_compu_ptr_ptr; eauto.
-  eapply eval_compu_ptr_ptr_2; eauto.
-  eapply eval_compf; eauto.
+  apply eval_compu; auto.
+  apply eval_compf; auto.
 Qed.
 
 End CMCONSTR.
@@ -303,11 +281,46 @@ Proof.
   exploit expr_is_addrof_ident_correct; eauto. intro EQ; subst a.
   inv H1. inv H4. 
   destruct (Genv.find_symbol ge i); try congruence.
-  inv H3. rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. 
+  rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. 
   destruct fd; try congruence. 
   destruct (ef_inline e0); congruence.
 Qed.
 
+(** Compatibility of evaluation functions with the "less defined than" relation. *)
+
+Ltac TrivialExists :=
+  match goal with
+  | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto
+  | _ => idtac
+  end.
+
+Lemma eval_unop_lessdef:
+  forall op v1 v1' v,
+  eval_unop op v1 = Some v -> Val.lessdef v1 v1' ->
+  exists v', eval_unop op v1' = Some v' /\ Val.lessdef v v'.
+Proof.
+  intros until v; intros EV LD. inv LD. 
+  exists v; auto.
+  destruct op; simpl in *; inv EV; TrivialExists.
+Qed.
+
+Lemma eval_binop_lessdef:
+  forall op v1 v1' v2 v2' v m m',
+  eval_binop op v1 v2 m = Some v -> 
+  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' ->
+  exists v', eval_binop op v1' v2' m' = Some v' /\ Val.lessdef v v'.
+Proof.
+  intros until m'; intros EV LD1 LD2 ME.
+  assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v').
+  inv LD1. inv LD2. exists v; auto. 
+  destruct op; destruct v1'; simpl in *; inv EV; TrivialExists.
+  destruct op; simpl in *; inv EV; TrivialExists.
+  destruct op; try (exact H). 
+  simpl in *. TrivialExists. inv EV. apply Val.of_optbool_lessdef. 
+  intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto.
+  intros; eapply Mem.valid_pointer_extends; eauto.
+Qed.
+
 (** * Semantic preservation for instruction selection. *)
 
 Section PRESERVATION.
@@ -318,7 +331,7 @@ Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 (** Relationship between the global environments for the original
-  CminorSel program and the generated RTL program. *)
+  Cminor program and the generated CminorSel program. *)
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -327,15 +340,6 @@ Proof.
   apply Genv.find_symbol_transf.
 Qed.
 
-Lemma functions_translated:
-  forall (v: val) (f: Cminor.fundef),
-  Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (sel_fundef ge f).
-Proof.  
-  intros.
-  exact (Genv.find_funct_transf (sel_fundef ge) _ _ H).
-Qed.
-
 Lemma function_ptr_translated:
   forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
@@ -345,6 +349,17 @@ Proof.
   exact (Genv.find_funct_ptr_transf (sel_fundef ge) _ _ H).
 Qed.
 
+Lemma functions_translated:
+  forall (v v': val) (f: Cminor.fundef),
+  Genv.find_funct ge v = Some f ->
+  Val.lessdef v v' ->
+  Genv.find_funct tge v' = Some (sel_fundef ge f).
+Proof.  
+  intros. inv H0.
+  exact (Genv.find_funct_transf (sel_fundef ge) _ _ H).
+  simpl in H. discriminate.
+Qed.
+
 Lemma sig_function_translated:
   forall f,
   funsig (sel_fundef ge f) = Cminor.funsig f.
@@ -359,113 +374,189 @@ Proof.
   apply Genv.find_var_info_transf.
 Qed.
 
+(** Relationship between the local environments. *)
+
+Definition env_lessdef (e1 e2: env) : Prop :=
+  forall id v1, e1!id = Some v1 -> exists v2, e2!id = Some v2 /\ Val.lessdef v1 v2.
+
+Lemma set_var_lessdef:
+  forall e1 e2 id v1 v2,
+  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
+  env_lessdef (PTree.set id v1 e1) (PTree.set id v2 e2).
+Proof.
+  intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id).
+  exists v2; split; congruence.
+  auto.
+Qed.
+
+Lemma set_params_lessdef:
+  forall il vl1 vl2, 
+  Val.lessdef_list vl1 vl2 ->
+  env_lessdef (set_params vl1 il) (set_params vl2 il).
+Proof.
+  induction il; simpl; intros.
+  red; intros. rewrite PTree.gempty in H0; congruence.
+  inv H; apply set_var_lessdef; auto.
+Qed.
+
+Lemma set_locals_lessdef:
+  forall e1 e2, env_lessdef e1 e2 ->
+  forall il, env_lessdef (set_locals il e1) (set_locals il e2).
+Proof.
+  induction il; simpl. auto. apply set_var_lessdef; auto.
+Qed.
+
 (** Semantic preservation for expressions. *)
 
 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.
+  forall e' le m',
+  env_lessdef e e' -> Mem.extends m m' ->
+  exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'.
 Proof.
   induction 1; intros; simpl.
   (* Evar *)
-  constructor; auto.
+  exploit H0; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto.
   (* Econst *)
-  destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]).
-  rewrite symbols_preserved. auto.
+  destruct cst; simpl in *; inv H. 
+  exists (Vint i); split; auto. econstructor. constructor. auto. 
+  exists (Vfloat f); split; auto. econstructor. constructor. auto.
+  rewrite <- symbols_preserved. fold (symbol_address tge i i0). apply eval_addrsymbol.
+  apply eval_addrstack.
   (* Eunop *)
-  eapply eval_sel_unop; eauto.
+  exploit IHeval_expr; eauto. intros [v1' [A B]].
+  exploit eval_unop_lessdef; eauto. intros [v' [C D]].
+  exploit eval_sel_unop; eauto. intros [v'' [E F]].
+  exists v''; split; eauto. eapply Val.lessdef_trans; eauto. 
   (* Ebinop *)
-  eapply eval_sel_binop; eauto.
+  exploit IHeval_expr1; eauto. intros [v1' [A B]].
+  exploit IHeval_expr2; eauto. intros [v2' [C D]].
+  exploit eval_binop_lessdef; eauto. intros [v' [E F]].
+  exploit eval_sel_binop. eexact A. eexact C. eauto. intros [v'' [P Q]].
+  exists v''; split; eauto. eapply Val.lessdef_trans; eauto. 
   (* Eload *)
-  eapply eval_load; eauto.
+  exploit IHeval_expr; eauto. intros [vaddr' [A B]].
+  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
+  exists v'; split; auto. eapply eval_load; eauto.
   (* Econdition *)
+  exploit IHeval_expr1; eauto. intros [v1' [A B]].
+  exploit IHeval_expr2; eauto. intros [v2' [C D]].
+  replace (sel_expr (if b1 then a2 else a3)) with (if b1 then sel_expr a2 else sel_expr a3) in C.
+  assert (Val.bool_of_val v1' b1). inv B. auto. inv H0.
+  exists v2'; split; auto. 
   econstructor; eauto. eapply eval_condition_of_expr; eauto. 
   destruct b1; auto.
 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.
+  forall e' le m',
+  env_lessdef e e' -> Mem.extends m m' ->
+  exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'.
 Proof.
-  induction 1; intros; simpl; constructor; auto with evalexpr.
+  induction 1; intros; simpl. 
+  exists (@nil val); split; auto. constructor.
+  exploit sel_expr_correct; eauto. intros [v1' [A B]].
+  exploit IHeval_exprlist; eauto. intros [vl' [C D]].
+  exists (v1' :: vl'); split; auto. constructor; eauto.
 Qed.
 
-Hint Resolve sel_exprlist_correct: evalexpr.
-
-(** Semantic preservation for terminating function calls and statements. *)
-
-Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont :=
-  match k with
-  | Cminor.Kstop => Kstop
-  | Cminor.Kseq s1 k1 => Kseq (sel_stmt ge s1) (sel_cont k1)
-  | Cminor.Kblock k1 => Kblock (sel_cont k1)
-  | Cminor.Kcall id f sp e k1 =>
-      Kcall id (sel_function ge f) sp e (sel_cont k1)
-  end.
+(** Semantic preservation for functions and statements. *)
+
+Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
+  | match_cont_stop:
+      match_cont Cminor.Kstop Kstop
+  | match_cont_seq: forall s k k',
+      match_cont k k' ->
+      match_cont (Cminor.Kseq s k) (Kseq (sel_stmt ge s) k')
+  | match_cont_block: forall k k',
+      match_cont k k' ->
+      match_cont (Cminor.Kblock k) (Kblock k')
+  | match_cont_call: forall id f sp e k e' k',
+      match_cont k k' -> env_lessdef e e' ->
+      match_cont (Cminor.Kcall id f sp e k) (Kcall id (sel_function ge f) sp e' k').
 
 Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
-  | match_state: forall f s k s' k' sp e m,
+  | match_state: forall f s k s' k' sp e m e' m',
       s' = sel_stmt ge s ->
-      k' = sel_cont k ->
+      match_cont k k' ->
+      env_lessdef e e' ->
+      Mem.extends m m' ->
       match_states
         (Cminor.State f s k sp e m)
-        (State (sel_function ge f) s' k' sp e m)
-  | match_callstate: forall f args k k' m,
-      k' = sel_cont k ->
+        (State (sel_function ge f) s' k' sp e' m')
+  | match_callstate: forall f args args' k k' m m',
+      match_cont k k' ->
+      Val.lessdef_list args args' ->
+      Mem.extends m m' ->
       match_states
         (Cminor.Callstate f args k m)
-        (Callstate (sel_fundef ge f) args k' m)
-  | match_returnstate: forall v k k' m,
-      k' = sel_cont k ->
+        (Callstate (sel_fundef ge f) args' k' m')
+  | match_returnstate: forall v v' k k' m m',
+      match_cont k k' ->
+      Val.lessdef v v' ->
+      Mem.extends m m' ->
       match_states
         (Cminor.Returnstate v k m)
-        (Returnstate v k' m)
-  | match_builtin_1: forall ef args optid f sp e k m al k',
-      k' = sel_cont k ->
-      eval_exprlist tge sp e m nil al args ->
+        (Returnstate v' k' m')
+  | match_builtin_1: forall ef args args' optid f sp e k m al e' k' m',
+      match_cont k k' ->
+      Val.lessdef_list args args' ->
+      env_lessdef e e' ->
+      Mem.extends m m' ->
+      eval_exprlist tge sp e' m' nil al args' ->
       match_states
         (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
-        (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e m)
-  | match_builtin_2: forall v optid f sp e k m k',
-      k' = sel_cont k ->
+        (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e' m')
+  | match_builtin_2: forall v v' optid f sp e k m e' m' k',
+      match_cont k k' ->
+      Val.lessdef v v' ->
+      env_lessdef e e' ->
+      Mem.extends m m' ->
       match_states
         (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
-        (State (sel_function ge f) Sskip k' sp (set_optvar optid v e) m).
+        (State (sel_function ge f) Sskip k' sp (set_optvar optid v' e') m').
 
 Remark call_cont_commut:
-  forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k).
+  forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k').
 Proof.
-  induction k; simpl; auto.
+  induction 1; simpl; auto. constructor. constructor; auto.
 Qed.
 
 Remark find_label_commut:
-  forall lbl s k,
-  find_label lbl (sel_stmt ge s) (sel_cont k) =
-  option_map (fun sk => (sel_stmt ge (fst sk), sel_cont (snd sk)))
-             (Cminor.find_label lbl s k).
+  forall lbl s k k',
+  match_cont k k' ->
+  match Cminor.find_label lbl s k, find_label lbl (sel_stmt ge s) k' with
+  | None, None => True
+  | Some(s1, k1), Some(s1', k1') => s1' = sel_stmt ge s1 /\ match_cont k1 k1'
+  | _, _ => False
+  end.
 Proof.
   induction s; intros; simpl; auto.
-  unfold store. destruct (addressing m (sel_expr e)); auto.
-  destruct (expr_is_addrof_builtin ge e); auto.
-  change (Kseq (sel_stmt ge s2) (sel_cont k))
-    with (sel_cont (Cminor.Kseq s2 k)).
-  rewrite IHs1. rewrite IHs2. 
-  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto.
-  rewrite IHs1. rewrite IHs2. 
-  destruct (Cminor.find_label lbl s1 k); auto.
-  change (Kseq (Sloop (sel_stmt ge s)) (sel_cont k))
-    with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)).
-  auto.
-  change (Kblock (sel_cont k))
-    with (sel_cont (Cminor.Kblock k)).
-  auto.
-  destruct o; auto.
-  destruct (ident_eq lbl l); auto.
+(* store *)
+  unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
+(* call *)
+  destruct (expr_is_addrof_builtin ge e); simpl; auto.
+(* seq *)
+  exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. 
+  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
+  destruct (find_label lbl (sel_stmt ge s1) (Kseq (sel_stmt ge s2) k')) as [[sy ky] | ];
+  intuition. apply IHs2; auto.
+(* ifthenelse *)
+  exploit (IHs1 k); eauto. 
+  destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
+  destruct (find_label lbl (sel_stmt ge s1) k') as [[sy ky] | ];
+  intuition. apply IHs2; auto.
+(* loop *)
+  apply IHs. constructor; auto.
+(* block *)
+  apply IHs. constructor; auto.
+(* return *)
+  destruct o; simpl; auto. 
+(* label *)
+  destruct (ident_eq lbl l). auto. apply IHs; auto.
 Qed.
 
 Definition measure (s: Cminor.state) : nat :=
@@ -481,66 +572,125 @@ Lemma sel_step_correct:
   (exists T2, step tge T1 t T2 /\ match_states S2 T2)
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
 Proof.
-  induction 1; intros T1 ME; inv ME; simpl;
-  try (left; econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail).
-
+  induction 1; intros T1 ME; inv ME; simpl.
+  (* skip seq *)
+  inv H7. left; econstructor; split. econstructor. constructor; auto.
+  (* skip block *)
+  inv H7. left; econstructor; split. econstructor. constructor; auto.
   (* skip call *)
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   left; econstructor; split. 
-  econstructor. destruct k; simpl in H; simpl; auto. 
+  econstructor. inv H10; simpl in H; simpl; auto. 
   rewrite <- H0; reflexivity.
-  simpl. eauto. 
+  eauto. 
   constructor; auto.
+  (* assign *)
+  exploit sel_expr_correct; eauto. intros [v' [A B]].
+  left; econstructor; split.
+  econstructor; eauto.
+  constructor; auto. apply set_var_lessdef; auto.
   (* store *)
+  exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]].
+  exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]].
+  exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
   left; econstructor; split.
-  eapply eval_store; eauto with evalexpr.
+  eapply eval_store; eauto.
   constructor; auto.
   (* Scall *)
-  case_eq (expr_is_addrof_builtin ge a).
+  exploit sel_expr_correct; eauto. intros [vf' [A B]].
+  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
+  destruct (expr_is_addrof_builtin ge a) as [ef|]_eqn.
   (* Scall turned into Sbuiltin *)
-  intros ef EQ. exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd.
+  exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd.
   right; split. omega. split. auto. 
-  econstructor; eauto with evalexpr.
+  econstructor; eauto.
   (* Scall preserved *)
-  intro EQ. left; econstructor; split.
-  econstructor; eauto with evalexpr.
-  apply functions_translated; eauto. 
+  left; econstructor; split.
+  econstructor; eauto.
+  eapply functions_translated; eauto. 
   apply sig_function_translated.
-  constructor; auto.
+  constructor; auto. constructor; auto.
   (* Stailcall *)
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
+  exploit sel_expr_correct; eauto. intros [vf' [A B]].
+  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
   left; econstructor; split.
-  econstructor; eauto with evalexpr.
-  apply functions_translated; eauto. 
+  econstructor; eauto.
+  eapply functions_translated; eauto. 
   apply sig_function_translated.
-  constructor; auto. apply call_cont_commut.
+  constructor; auto. apply call_cont_commut; auto.
+  (* Seq *)
+  left; econstructor; split. constructor. constructor; auto. constructor; auto.
   (* Sifthenelse *)
-  left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) (sel_cont k) sp e m); split.
-  constructor. eapply eval_condition_of_expr; eauto with evalexpr.
+  exploit sel_expr_correct; eauto. intros [v' [A B]].
+  assert (Val.bool_of_val v' b). inv B. auto. inv H0.
+  left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) k' sp e' m'); split.
+  constructor. eapply eval_condition_of_expr; eauto.
   constructor; auto. destruct b; auto.
+  (* Sloop *)
+  left; econstructor; split. constructor. constructor; auto. constructor; auto.
+  (* Sblock *)
+  left; econstructor; split. constructor. constructor; auto. constructor; auto.
+  (* Sexit seq *)
+  inv H7. left; econstructor; split. constructor. constructor; auto.
+  (* Sexit0 block *)
+  inv H7. left; econstructor; split. constructor. constructor; auto.
+  (* SexitS block *)
+  inv H7. left; econstructor; split. constructor. constructor; auto.
+  (* Sswitch *)
+  exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
+  left; econstructor; split. econstructor; eauto. constructor; auto.
   (* Sreturn None *)
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   left; econstructor; split. 
   econstructor. simpl; eauto. 
-  constructor; auto. apply call_cont_commut.
+  constructor; auto. apply call_cont_commut; auto.
   (* Sreturn Some *)
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
+  exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split. 
-  econstructor. simpl. eauto with evalexpr. simpl; eauto.
-  constructor; auto. apply call_cont_commut.
+  econstructor; eauto.
+  constructor; auto. apply call_cont_commut; auto.
+  (* Slabel *)
+  left; econstructor; split. constructor. constructor; auto.
   (* Sgoto *)
+  exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)).
+    apply call_cont_commut; eauto.
+  rewrite H. 
+  destruct (find_label lbl (sel_stmt ge (Cminor.fn_body f)) (call_cont k'0))
+  as [[s'' k'']|]_eqn; intros; try contradiction.
+  destruct H0. 
   left; econstructor; split.
-  econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
-  rewrite H. simpl. reflexivity. 
+  econstructor; eauto. 
   constructor; auto.
+  (* internal function *)
+  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  intros [m2' [A B]].
+  left; econstructor; split.
+  econstructor; eauto.
+  constructor; auto. apply set_locals_lessdef. apply set_params_lessdef; auto.
   (* external call *)
+  exploit external_call_mem_extends; eauto. 
+  intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
   econstructor. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
   (* external call turned into a Sbuiltin *)
+  exploit external_call_mem_extends; eauto. 
+  intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
   econstructor. eauto. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
+  (* return *)
+  inv H2. 
+  left; econstructor; split. 
+  econstructor. 
+  constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
   (* return of an external call turned into a Sbuiltin *)
-  right; split. omega. split. auto. constructor; auto.
+  right; split. omega. split. auto. constructor; auto. 
+  destruct optid; simpl; auto. apply set_var_lessdef; auto.
 Qed.
 
 Lemma sel_initial_states:
@@ -554,14 +704,14 @@ Proof.
   simpl. fold tge. rewrite symbols_preserved. eexact H0.
   apply function_ptr_translated. eauto. 
   rewrite <- H2. apply sig_function_translated; auto.
-  constructor; auto.
+  constructor; auto. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma sel_final_states:
   forall S R r,
   match_states S R -> Cminor.final_state S r -> final_state R r.
 Proof.
-  intros. inv H0. inv H. simpl. constructor.
+  intros. inv H0. inv H. inv H3. inv H5. constructor.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index f3dd9ed..02a6ca9 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -508,17 +508,10 @@ Proof.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto. apply regset_set; auto.
 
-(* cond true *)
+(* cond *)
   TransfInstr. 
-  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split.
-  eapply exec_Icond_true; eauto.
-  apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto.
-  constructor; auto. 
-
-(* cond false *)
-  TransfInstr. 
-  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifnot rs' m'); split.
-  eapply exec_Icond_false; eauto.
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split.
+  eapply exec_Icond; eauto.
   apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto.
   constructor; auto. 
 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 8ff7347..d589260 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -319,14 +319,9 @@ Proof.
   (* cond *)
   generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.
-  eapply exec_Lcond_true; eauto.
+  eapply exec_Lcond; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
-  econstructor; eauto.
-  generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
-  left; econstructor; split.
-  eapply exec_Lcond_false; eauto.
-  rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
-  econstructor; eauto.
+  destruct b; econstructor; eauto.
   (* jumptable *)
   generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
   left; econstructor; split.