Merge of branch value-analysis.

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

3 files changed, 63 insertions, 825 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 36a62a8..79dd26f 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -205,7 +205,7 @@ Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block
                              : option (world * trace * mem) :=
   if block_is_volatile ge b then
     do id <- Genv.invert_symbol ge b;
-    do ev <- eventval_of_val v (type_of_chunk chunk);
+    do ev <- eventval_of_val (Val.load_result chunk v) (type_of_chunk chunk);
     do w' <- nextworld_vstore w chunk id ofs ev;
     Some(w', Event_vstore chunk id ofs ev :: nil, m)
   else
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 419ffff..3b902c5 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -55,220 +55,50 @@ Local Open Scope error_monad_scope.
 
 Definition compilenv := PTree.t Z.
 
-(** * Helper functions for code generation *)
-
-(** When the translation of an expression is stored in memory,
-  one or several casts at the toplevel of the expression can be redundant
-  with that implicitly performed by the memory store.
-  [store_arg] detects this case and strips away the redundant cast. *)
-
-Function uncast_int (m: int) (e: expr) {struct e} : expr :=
-  match e with
-  | Eunop (Ocast8unsigned|Ocast8signed) e1 =>
-      if Int.eq (Int.and (Int.repr 255) m) m then uncast_int m e1 else e
-  | Eunop (Ocast16unsigned|Ocast16signed) e1 =>
-      if Int.eq (Int.and (Int.repr 65535) m) m then uncast_int m e1 else e
-  | Ebinop Oand e1 (Econst (Ointconst n)) =>
-      if Int.eq (Int.and n m) m then uncast_int m e1 else e
-  | Ebinop Oshru e1 (Econst (Ointconst n)) =>
-      if Int.eq (Int.shru (Int.shl m n) n) m
-      then Ebinop Oshru (uncast_int (Int.shl m n) e1) (Econst (Ointconst n))
-      else e
-  | Ebinop Oshr e1 (Econst (Ointconst n)) =>
-      if Int.eq (Int.shru (Int.shl m n) n) m
-      then Ebinop Oshr (uncast_int (Int.shl m n) e1) (Econst (Ointconst n))
-      else e
-  | _ => e
-  end.
-
-Definition uncast_int8 (e: expr) : expr := uncast_int (Int.repr 255) e.
-
-Definition uncast_int16 (e: expr) : expr := uncast_int (Int.repr 65535) e.
-
-Function uncast_float32 (e: expr) : expr :=
-  match e with
-  | Eunop Osingleoffloat e1 => uncast_float32 e1
-  | _ => e
-  end.
-
-Function store_arg (chunk: memory_chunk) (e: expr) : expr :=
-  match chunk with
-  | Mint8signed | Mint8unsigned => uncast_int8 e
-  | Mint16signed | Mint16unsigned => uncast_int16 e
-  | Mfloat32 => uncast_float32 e
-  | _ => e
-  end.
-
-Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt :=
-  Sstore chunk e1 (store_arg chunk e2).
-
-Definition make_stackaddr (ofs: Z): expr :=
-  Econst (Oaddrstack (Int.repr ofs)).
-
-Definition make_globaladdr (id: ident): expr :=
-  Econst (Oaddrsymbol id Int.zero).
-
-Definition make_unop (op: unary_operation) (e: expr): expr :=
-  match op with
-  | Ocast8unsigned => Eunop Ocast8unsigned (uncast_int8 e)
-  | Ocast8signed => Eunop Ocast8signed (uncast_int8 e)
-  | Ocast16unsigned => Eunop Ocast16unsigned (uncast_int16 e)
-  | Ocast16signed => Eunop Ocast16signed (uncast_int16 e)
-  | Osingleoffloat => Eunop Osingleoffloat (uncast_float32 e)
-  | _ => Eunop op e
-  end.
-
-(** * Optimization of casts *)
-
-(** To remove redundant casts, we perform a modest static analysis
-  on the values of expressions, classifying them into the following
-  ranges. *)
-
-Inductive approx : Type :=
-  | Any                   (**r any value *)
-  | Int1                  (**r [0] or [1] *)
-  | Int7                  (**r [[0,127]] *)
-  | Int8s                 (**r [[-128,127]] *)
-  | Int8u                 (**r [[0,255]] *)
-  | Int15                 (**r [[0,32767]] *)
-  | Int16s                (**r [[-32768,32767]] *)
-  | Int16u                (**r [[0,65535]] *)
-  | Float32.               (**r single-precision float *)
-
-Module Approx.
-
-Definition bge (x y: approx) : bool :=
-  match x, y with
-  | Any, _ => true
-  | Int1, Int1 => true
-  | Int7, (Int1 | Int7) => true
-  | Int8s, (Int1 | Int7 | Int8s) => true
-  | Int8u, (Int1 | Int7 | Int8u) => true
-  | Int15, (Int1 | Int7 | Int8u | Int15) => true
-  | Int16s, (Int1 | Int7 | Int8s | Int8u | Int15 | Int16s) => true
-  | Int16u, (Int1 | Int7 | Int8u | Int15 | Int16u) => true
-  | Float32, Float32 => true
-  | _, _ => false
-  end.
-
-Definition of_int (n: int) :=
-  if Int.eq_dec n Int.zero || Int.eq_dec n Int.one then Int1
-  else 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 Any.
-
-Definition of_float (n: float) :=
-  if Float.eq_dec n (Float.singleoffloat n) then Float32 else Any.
-
-Definition of_chunk (chunk: memory_chunk) :=
-  match chunk with
-  | Mint8signed => Int8s
-  | Mint8unsigned => Int8u
-  | Mint16signed => Int16s
-  | Mint16unsigned => Int16u
-  | Mint32 => Any
-  | Mint64 => Any
-  | Mfloat32 => Float32
-  | Mfloat64 => Any
-  | Mfloat64al32 => Any
-  end.
-
-Definition unop (op: unary_operation) (a: approx) :=
-  match op with
-  | Ocast8unsigned => Int8u
-  | Ocast8signed => Int8s
-  | Ocast16unsigned => Int16u
-  | Ocast16signed => Int16s
-  | Osingleoffloat => Float32
-  | _ => Any
-  end.
-
-Definition unop_is_redundant (op: unary_operation) (a: approx) :=
-  match op with
-  | Ocast8unsigned => bge Int8u a
-  | Ocast8signed => bge Int8s a
-  | Ocast16unsigned => bge Int16u a
-  | Ocast16signed => bge Int16s a
-  | Osingleoffloat => bge Float32 a
-  | _ => false
-  end.
-
-Definition bitwise_and (a1 a2: approx) :=
-  if bge Int1 a1 || bge Int1 a2 then Int1
-  else if bge Int8u a1 || bge Int8u a2 then Int8u
-  else if bge Int16u a1 || bge Int16u a2 then Int16u
-  else Any.
-
-Definition bitwise_or (a1 a2: approx) :=
-  if bge Int1 a1 && bge Int1 a2 then Int1
-  else if bge Int8u a1 && bge Int8u a2 then Int8u
-  else if bge Int16u a1 && bge Int16u a2 then Int16u
-  else Any.
-
-Definition binop (op: binary_operation) (a1 a2: approx) :=
-  match op with
-  | Oand => bitwise_and a1 a2
-  | Oor | Oxor => bitwise_or a1 a2
-  | Ocmp _ => Int1
-  | Ocmpu _ => Int1
-  | Ocmpf _ => Int1
-  | _ => Any
-  end.
-
-End Approx.
-
-(** * Translation of expressions and statements. *)
-
 (** Generation of a Cminor expression for taking the address of
   a Csharpminor variable. *)
 
 Definition var_addr (cenv: compilenv) (id: ident): expr :=
   match PTree.get id cenv with
-  | Some ofs => make_stackaddr ofs
-  | None     => make_globaladdr id
+  | Some ofs => Econst (Oaddrstack (Int.repr ofs))
+  | None     => Econst (Oaddrsymbol id Int.zero)
   end.
 
+(** * Translation of expressions and statements. *)
+
 (** Translation of constants. *)
 
-Definition transl_constant (cst: Csharpminor.constant): (constant * approx) :=
+Definition transl_constant (cst: Csharpminor.constant): constant :=
   match cst with
   | Csharpminor.Ointconst n =>
-      (Ointconst n, Approx.of_int n)
+      Ointconst n
   | Csharpminor.Ofloatconst n =>
-      (Ofloatconst n, Approx.of_float n)
+      Ofloatconst n
   | Csharpminor.Olongconst n =>
-      (Olongconst n, Any)
+      Olongconst n
   end.
 
-(** Translation of expressions.  Return both a Cminor expression and
-  a compile-time approximation of the value of the original
-  C#minor expression, which is used to remove redundant casts. *)
+(** Translation of expressions.  *)
 
 Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
-                     {struct e}: res (expr * approx) :=
+                     {struct e}: res expr :=
   match e with
   | Csharpminor.Evar id =>
-      OK (Evar id, Any)
+      OK (Evar id)
   | Csharpminor.Eaddrof id =>
-      OK (var_addr cenv id, Any)
+      OK (var_addr cenv id)
   | Csharpminor.Econst cst =>
-      let (tcst, a) := transl_constant cst in OK (Econst tcst, a)
+      OK (Econst (transl_constant cst))
   | Csharpminor.Eunop op e1 =>
-      do (te1, a1)  <- transl_expr cenv e1;
-      if Approx.unop_is_redundant op a1
-      then OK (te1, a1)
-      else OK (make_unop op te1, Approx.unop op a1)
+      do te1  <- transl_expr cenv e1;
+      OK (Eunop op te1)
   | Csharpminor.Ebinop op e1 e2 =>
-      do (te1, a1) <- transl_expr cenv e1;
-      do (te2, a2) <- transl_expr cenv e2;
-      OK (Ebinop op te1 te2, Approx.binop op a1 a2)
+      do te1 <- transl_expr cenv e1;
+      do te2 <- transl_expr cenv e2;
+      OK (Ebinop op te1 te2)
   | Csharpminor.Eload chunk e =>
-      do (te, a) <- transl_expr cenv e;
-      OK (Eload chunk te, Approx.of_chunk chunk)
+      do te <- transl_expr cenv e;
+      OK (Eload chunk te)
   end.
 
 Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
@@ -277,7 +107,7 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
   | nil =>
       OK nil
   | e1 :: e2 =>
-      do (te1, a1) <- transl_expr cenv e1;
+      do te1 <- transl_expr cenv e1;
       do te2 <- transl_exprlist cenv e2;
       OK (te1 :: te2)
   end.
@@ -331,14 +161,14 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
   | Csharpminor.Sskip =>
       OK Sskip
   | Csharpminor.Sset id e =>
-      do (te, a) <- transl_expr cenv e;
+      do te <- transl_expr cenv e;
       OK (Sassign id te)
   | Csharpminor.Sstore chunk e1 e2 =>
-      do (te1, a1) <- transl_expr cenv e1;
-      do (te2, a2) <- transl_expr cenv e2;
-      OK (make_store chunk te1 te2)
+      do te1 <- transl_expr cenv e1;
+      do te2 <- transl_expr cenv e2;
+      OK (Sstore chunk te1 te2)
   | Csharpminor.Scall optid sig e el =>
-      do (te, a) <- transl_expr cenv e;
+      do te <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
       OK (Scall optid sig te tel)
   | Csharpminor.Sbuiltin optid ef el =>
@@ -349,7 +179,7 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
       do ts2 <- transl_stmt cenv xenv s2;
       OK (Sseq ts1 ts2)
   | Csharpminor.Sifthenelse e s1 s2 =>
-      do (te, a) <- transl_expr cenv e;
+      do te <- transl_expr cenv e;
       do ts1 <- transl_stmt cenv xenv s1;
       do ts2 <- transl_stmt cenv xenv s2;
       OK (Sifthenelse te ts1 ts2)
@@ -364,12 +194,12 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
   | Csharpminor.Sswitch e ls =>
       let cases := switch_table ls O in
       let default := length cases in
-      do (te, a) <- transl_expr cenv e;
+      do te <- transl_expr cenv e;
       transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default)
   | Csharpminor.Sreturn None =>
       OK (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
-      do (te, a) <- transl_expr cenv e;
+      do te <- transl_expr cenv e;
       OK (Sreturn (Some te))
   | Csharpminor.Slabel lbl s =>
       do ts <- transl_stmt cenv xenv s; OK (Slabel lbl ts)
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 672f804..78ec748 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1252,226 +1252,6 @@ Proof.
   eapply bind_parameters_agree; eauto. 
 Qed.
 
-(** * Properties of compile-time approximations of values *)
-
-Definition val_match_approx (a: approx) (v: val) : Prop :=
-  match a with
-  | Int1 => v = Val.zero_ext 1 v
-  | 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
-  | Float32 => v = Val.singleoffloat v
-  | Any => True
-  end.
-
-Remark undef_match_approx: forall a, val_match_approx a Vundef.
-Proof.
-  destruct a; simpl; auto.
-Qed.
-
-Lemma val_match_approx_increasing:
-  forall a1 a2 v,
-  Approx.bge a1 a2 = true -> 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. omega. 
-  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. omega.
-  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. omega.
-  assert (D: forall v, v = Val.zero_ext 1 v -> v = Val.zero_ext 8 v).
-    intros. rewrite H.
-    destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.zero_ext_widen. omega. 
-  assert (E: forall v, v = Val.zero_ext 1 v -> v = Val.sign_ext 8 v).
-    intros. rewrite H.
-    destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.sign_zero_ext_widen. omega.
-  intros. 
-  unfold Approx.bge in H; destruct a1; try discriminate; destruct a2; simpl in *; try discriminate; intuition.
-Qed.
-
-Lemma approx_of_int_sound:
-  forall n, val_match_approx (Approx.of_int n) (Vint n).
-Proof.
-  unfold Approx.of_int; intros.
-  destruct (Int.eq_dec n Int.zero); simpl. subst; auto. 
-  destruct (Int.eq_dec n Int.one); simpl. subst; auto. 
-  destruct (Int.eq_dec n (Int.zero_ext 7 n)). simpl.
-    split.
-    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. omega.
-    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. omega.
-  destruct (Int.eq_dec n (Int.zero_ext 8 n)). simpl; congruence.
-  destruct (Int.eq_dec n (Int.sign_ext 8 n)). simpl; congruence.
-  destruct (Int.eq_dec n (Int.zero_ext 15 n)). simpl.
-    split.
-    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. omega. 
-    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. omega. 
-  destruct (Int.eq_dec n (Int.zero_ext 16 n)). simpl; congruence.
-  destruct (Int.eq_dec n (Int.sign_ext 16 n)). simpl; congruence.
-  exact I.
-Qed.
-
-Lemma approx_of_float_sound:
-  forall f, val_match_approx (Approx.of_float f) (Vfloat f).
-Proof.
-  unfold Approx.of_float; intros. 
-  destruct (Float.eq_dec f (Float.singleoffloat f)); simpl; auto. congruence.
-Qed.
-
-Lemma approx_of_chunk_sound:
-  forall chunk m b ofs v,
-  Mem.load chunk m b ofs = Some v ->
-  val_match_approx (Approx.of_chunk chunk) v.
-Proof.
-  intros. exploit Mem.load_cast; eauto. 
-  destruct chunk; intros; simpl; auto.
-Qed.
-
-Lemma approx_of_unop_sound:
-  forall op v1 v a1,
-  eval_unop op v1 = Some v ->
-  val_match_approx a1 v1 ->
-  val_match_approx (Approx.unop op a1) v.
-Proof.
-  destruct op; simpl; intros; auto; inv H.
-  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. omega. 
-  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. omega. 
-  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. omega. 
-  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. omega. 
-  destruct v1; simpl; auto. rewrite Float.singleoffloat_idem; auto.
-Qed.
-
-Lemma approx_bitwise_and_sound:
-  forall a1 v1 a2 v2,
-  val_match_approx a1 v1 -> val_match_approx a2 v2 ->
-  val_match_approx (Approx.bitwise_and a1 a2) (Val.and v1 v2).
-Proof.
-  assert (X: forall v1 v2 N, 0 < N < Z_of_nat Int.wordsize ->
-            v2 = Val.zero_ext N v2 ->
-            Val.and v1 v2 = Val.zero_ext N (Val.and v1 v2)).
-    intros. rewrite Val.zero_ext_and in *; auto. 
-    rewrite Val.and_assoc. congruence. 
-  assert (Y: forall v1 v2 N, 0 < N < Z_of_nat Int.wordsize ->
-            v1 = Val.zero_ext N v1 ->
-            Val.and v1 v2 = Val.zero_ext N (Val.and v1 v2)).
-    intros. rewrite (Val.and_commut v1 v2). apply X; auto.
-  assert (P: forall a v, val_match_approx a v -> Approx.bge Int8u a = true ->
-               v = Val.zero_ext 8 v).
-    intros. apply (val_match_approx_increasing Int8u a v); auto.
-  assert (Q: forall a v, val_match_approx a v -> Approx.bge Int16u a = true ->
-               v = Val.zero_ext 16 v).
-    intros. apply (val_match_approx_increasing Int16u a v); auto.
-  assert (R: forall a v, val_match_approx a v -> Approx.bge Int1 a = true ->
-               v = Val.zero_ext 1 v).
-    intros. apply (val_match_approx_increasing Int1 a v); auto.
-
-  intros; unfold Approx.bitwise_and. 
-  destruct (Approx.bge Int1 a1) eqn:?. simpl. apply Y; eauto. compute; auto.
-  destruct (Approx.bge Int1 a2) eqn:?. simpl. apply X; eauto. compute; auto.
-  destruct (Approx.bge Int8u a1) eqn:?. simpl. apply Y; eauto. compute; auto.
-  destruct (Approx.bge Int8u a2) eqn:?. simpl. apply X; eauto. compute; auto.
-  destruct (Approx.bge Int16u a1) eqn:?. simpl. apply Y; eauto. compute; auto.
-  destruct (Approx.bge Int16u a2) eqn:?. simpl. apply X; eauto. compute; auto.
-  simpl; auto. 
-Qed.
-
-Lemma approx_bitwise_or_sound:
-  forall (sem_op: val -> val -> val) a1 v1 a2 v2,
-  (forall a b c, sem_op (Val.and a (Vint c)) (Val.and b (Vint c)) =
-                 Val.and (sem_op a b) (Vint c)) ->
-  val_match_approx a1 v1 -> val_match_approx a2 v2 ->
-  val_match_approx (Approx.bitwise_or a1 a2) (sem_op v1 v2).
-Proof.
-  intros.
-  assert (X: forall v v' N, 0 < N < Z_of_nat Int.wordsize ->
-            v = Val.zero_ext N v ->
-            v' = Val.zero_ext N v' ->
-            sem_op v v' = Val.zero_ext N (sem_op v v')).
-    intros. rewrite Val.zero_ext_and in *; auto.
-    rewrite H3; rewrite H4. rewrite H. rewrite Val.and_assoc.
-    simpl. rewrite Int.and_idem. auto.
-
-  unfold Approx.bitwise_or. 
-
-  destruct (Approx.bge Int1 a1 && Approx.bge Int1 a2) eqn:?.
-  destruct (andb_prop _ _ Heqb).
-  simpl. apply X. compute; auto. 
-  apply (val_match_approx_increasing Int1 a1 v1); auto.
-  apply (val_match_approx_increasing Int1 a2 v2); auto.
-
-  destruct (Approx.bge Int8u a1 && Approx.bge Int8u a2) eqn:?.
-  destruct (andb_prop _ _ Heqb0).
-  simpl. apply X. compute; auto. 
-  apply (val_match_approx_increasing Int8u a1 v1); auto.
-  apply (val_match_approx_increasing Int8u a2 v2); auto.
-
-  destruct (Approx.bge Int16u a1 && Approx.bge Int16u a2) eqn:?.
-  destruct (andb_prop _ _ Heqb1).
-  simpl. apply X. compute; auto. 
-  apply (val_match_approx_increasing Int16u a1 v1); auto.
-  apply (val_match_approx_increasing Int16u a2 v2); auto.
-
-  exact I.
-Qed.
-
-Lemma approx_of_binop_sound:
-  forall op v1 a1 v2 a2 m v,
-  eval_binop op v1 v2 m = Some v ->
-  val_match_approx a1 v1 -> val_match_approx a2 v2 ->
-  val_match_approx (Approx.binop op a1 a2) v.
-Proof.
-  assert (OB: forall ob, val_match_approx Int1 (Val.of_optbool ob)).
-    destruct ob; simpl. destruct b; auto. auto.
-  
-  destruct op; intros; simpl Approx.binop; simpl in H; try (exact I); inv H.
-  apply approx_bitwise_and_sound; auto.
-  apply approx_bitwise_or_sound; auto.
-    intros. destruct a; destruct b; simpl; auto.
-    rewrite (Int.and_commut i c); rewrite (Int.and_commut i0 c). 
-    rewrite <- Int.and_or_distrib. rewrite Int.and_commut. auto.
-  apply approx_bitwise_or_sound; auto.
-    intros. destruct a; destruct b; simpl; auto.
-    rewrite (Int.and_commut i c); rewrite (Int.and_commut i0 c). 
-    rewrite <- Int.and_xor_distrib. rewrite Int.and_commut. auto.
-  apply OB.
-  apply OB.
-  apply OB.
-Qed.
-
-Lemma approx_unop_is_redundant_sound:
-  forall op a v,
-  Approx.unop_is_redundant op a = true ->
-  val_match_approx a v ->
-  eval_unop op v = Some v.
-Proof.
-  unfold Approx.unop_is_redundant; intros; destruct op; try discriminate.
-(* cast8unsigned *)
-  assert (V: val_match_approx Int8u v) by (eapply val_match_approx_increasing; eauto).
-  simpl in *. congruence.
-(* cast8signed *)
-  assert (V: val_match_approx Int8s v) by (eapply val_match_approx_increasing; eauto).
-  simpl in *. congruence.
-(* cast16unsigned *)
-  assert (V: val_match_approx Int16u v) by (eapply val_match_approx_increasing; eauto).
-  simpl in *. congruence.
-(* cast16signed *)
-  assert (V: val_match_approx Int16s v) by (eapply val_match_approx_increasing; eauto).
-  simpl in *. congruence.
-(* singleoffloat *)
-  assert (V: val_match_approx Float32 v) by (eapply val_match_approx_increasing; eauto).
-  simpl in *. congruence.
-Qed.
-
 (** * Compatibility of evaluation functions with respect to memory injections. *)
 
 Remark val_inject_val_of_bool:
@@ -1622,363 +1402,6 @@ Qed.
 
 (** * Correctness of Cminor construction functions *)
 
-Lemma make_stackaddr_correct:
-  forall sp te tm ofs,
-  eval_expr tge (Vptr sp Int.zero) te tm
-            (make_stackaddr ofs) (Vptr sp (Int.repr ofs)).
-Proof.
-  intros; unfold make_stackaddr.
-  eapply eval_Econst. simpl. decEq. decEq.
-  rewrite Int.add_commut. apply Int.add_zero.
-Qed.
-
-Lemma make_globaladdr_correct:
-  forall sp te tm id b,
-  Genv.find_symbol tge id = Some b ->
-  eval_expr tge (Vptr sp Int.zero) te tm
-            (make_globaladdr id) (Vptr b Int.zero).
-Proof.
-  intros; unfold make_globaladdr.
-  eapply eval_Econst. simpl. rewrite H. auto.
-Qed.
-
-(** Correctness of [make_store]. *)
-
-Inductive val_lessdef_upto (m: int): val -> val -> Prop :=
-  | val_lessdef_upto_base:
-      forall v1 v2, Val.lessdef v1 v2 -> val_lessdef_upto m v1 v2
-  | val_lessdef_upto_int:
-      forall n1 n2, Int.and n1 m = Int.and n2 m -> val_lessdef_upto m (Vint n1) (Vint n2).
-
-Hint Resolve val_lessdef_upto_base.
-
-Remark val_lessdef_upto_and:
-  forall m v1 v2 p,
-  val_lessdef_upto m v1 v2 -> Int.and p m = m ->
-  val_lessdef_upto m (Val.and v1 (Vint p)) v2.
-Proof.
-  intros. inversion H; clear H.
-  inversion H1. destruct v2; simpl; auto. 
-  apply val_lessdef_upto_int. rewrite Int.and_assoc. congruence.
-  simpl. auto. 
-  simpl. apply val_lessdef_upto_int. rewrite Int.and_assoc. congruence. 
-Qed.
-
-Remark val_lessdef_upto_zero_ext:
-  forall m v1 v2 p,
-  val_lessdef_upto m v1 v2 -> Int.and (Int.repr (two_p p - 1)) m = m -> 0 < p < 32 ->
-  val_lessdef_upto m (Val.zero_ext p v1) v2.
-Proof.
-  intros. inversion H; clear H.
-  inversion H2. destruct v2; simpl; auto.
-  apply val_lessdef_upto_int. rewrite Int.zero_ext_and; auto. 
-  rewrite Int.and_assoc. rewrite H0. auto.
-  omega.
-  simpl; auto.
-  simpl. apply val_lessdef_upto_int. rewrite Int.zero_ext_and; auto.
-  rewrite Int.and_assoc. rewrite H0. auto. omega.
-Qed.
-
-Remark val_lessdef_upto_sign_ext:
-  forall m v1 v2 p,
-  val_lessdef_upto m v1 v2 -> Int.and (Int.repr (two_p p - 1)) m = m -> 0 < p < 32 ->
-  val_lessdef_upto m (Val.sign_ext p v1) v2.
-Proof.
-  intros.
-  assert (A: forall x, Int.and (Int.sign_ext p x) m = Int.and x m).
-    intros. transitivity (Int.and (Int.zero_ext p (Int.sign_ext p x)) m).
-    rewrite Int.zero_ext_and; auto. rewrite Int.and_assoc. congruence. omega.
-    rewrite Int.zero_ext_sign_ext.
-    rewrite Int.zero_ext_and; auto. rewrite Int.and_assoc. congruence. omega. omega.
-  inversion H; clear H.
-  inversion H2. destruct v2; simpl; auto.
-  apply val_lessdef_upto_int. auto. 
-  simpl; auto.
-  simpl. apply val_lessdef_upto_int. rewrite A. auto. 
-Qed.
-
-Remark val_lessdef_upto_shru:
-  forall m v1 v2 p,
-  val_lessdef_upto (Int.shl m p) v1 v2 -> Int.shru (Int.shl m p) p = m ->
-  val_lessdef_upto m (Val.shru v1 (Vint p)) (Val.shru v2 (Vint p)).
-Proof.
-  intros. inversion H; clear H.
-  inversion H1; simpl; auto.
-  simpl. destruct (Int.ltu p Int.iwordsize); auto. apply val_lessdef_upto_int.
-  rewrite <- H0. repeat rewrite Int.and_shru. congruence.
-Qed.
-
-Remark val_lessdef_upto_shr:
-  forall m v1 v2 p,
-  val_lessdef_upto (Int.shl m p) v1 v2 -> Int.shru (Int.shl m p) p = m ->
-  val_lessdef_upto m (Val.shr v1 (Vint p)) (Val.shr v2 (Vint p)).
-Proof.
-  intros. inversion H; clear H.
-  inversion H1; simpl; auto.
-  simpl. destruct (Int.ltu p Int.iwordsize); auto. apply val_lessdef_upto_int.
-  repeat rewrite Int.shr_and_shru_and; auto.
-  rewrite <- H0. repeat rewrite Int.and_shru. congruence.
-Qed.
-
-Lemma eval_uncast_int:
-  forall m sp te tm a x,
-  eval_expr tge sp te tm a x ->
-  exists v, eval_expr tge sp te tm (uncast_int m a) v /\ val_lessdef_upto m x v.
-Proof.
-  assert (EQ: forall p q, Int.eq p q = true -> p = q).
-    intros. generalize (Int.eq_spec p q). rewrite H; auto.   
-  intros until a. functional induction (uncast_int m a); intros.
-  (* cast8unsigned *)
-  inv H. simpl in H4; inv H4. exploit IHe; eauto. intros [v [A B]].
-  exists v; split; auto. apply val_lessdef_upto_zero_ext; auto. 
-  compute; auto.
-  exists x; auto. 
-  (* cast8signed *)
-  inv H. simpl in H4; inv H4. exploit IHe; eauto. intros [v [A B]].
-  exists v; split; auto. apply val_lessdef_upto_sign_ext; auto. 
-  compute; auto.
-  exists x; auto. 
-  (* cast16unsigned *)
-  inv H. simpl in H4; inv H4. exploit IHe; eauto. intros [v [A B]].
-  exists v; split; auto. apply val_lessdef_upto_zero_ext; auto. 
-  compute; auto.
-  exists x; auto. 
-  (* cast16signed *)
-  inv H. simpl in H4; inv H4. exploit IHe; eauto. intros [v [A B]].
-  exists v; split; auto. apply val_lessdef_upto_sign_ext; auto. 
-  compute; auto.
-  exists x; auto. 
-  (* and *)
-  inv H. simpl in H6; inv H6. inv H5. simpl in H0. inv H0.
-  exploit IHe; eauto. intros [v [A B]].
-  exists v; split; auto. apply val_lessdef_upto_and; auto.
-  exists x; auto.
-  (* shru *)
-  inv H. simpl in H6; inv H6. inv H5. simpl in H0. inv H0.
-  exploit IHe; eauto. intros [v [A B]].
-  exists (Val.shru v (Vint n)); split.
-  econstructor. eauto. econstructor. simpl; reflexivity. auto. 
-  apply val_lessdef_upto_shru; auto.
-  exists x; auto.
-  (* shr *)
-  inv H. simpl in H6; inv H6. inv H5. simpl in H0. inv H0.
-  exploit IHe; eauto. intros [v [A B]].
-  exists (Val.shr v (Vint n)); split.
-  econstructor. eauto. econstructor. simpl; reflexivity. auto. 
-  apply val_lessdef_upto_shr; auto.
-  exists x; auto.
-  (* default *)
-  exists x; split; auto.
-Qed.
-
-Inductive val_lessdef_upto_single: val -> val -> Prop :=
-  | val_lessdef_upto_single_base:
-      forall v1 v2, Val.lessdef v1 v2 -> val_lessdef_upto_single v1 v2
-  | val_lessdef_upto_single_float:
-      forall n1 n2, Float.singleoffloat n1 = Float.singleoffloat n2 -> val_lessdef_upto_single (Vfloat n1) (Vfloat n2).
-
-Hint Resolve val_lessdef_upto_single_base.
-
-Lemma eval_uncast_float32:
-  forall sp te tm a x,
-  eval_expr tge sp te tm a x ->
-  exists v, eval_expr tge sp te tm (uncast_float32 a) v /\ val_lessdef_upto_single x v.
-Proof.
-  intros until a. functional induction (uncast_float32 a); intros.
-  (* singleoffloat *)
-  inv H. simpl in H4; inv H4. exploit IHe; eauto. intros [v [A B]].
-  exists v; split; auto.
-  inv B. inv H. destruct v; simpl; auto. 
-  apply val_lessdef_upto_single_float. apply Float.singleoffloat_idem. 
-  simpl; auto.
-  apply val_lessdef_upto_single_float. rewrite H. apply Float.singleoffloat_idem.
-  (* default *)
-  exists x; auto.
-Qed.
-
-Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
-  | val_content_inject_8_signed:
-      forall n1 n2, Int.sign_ext 8 n1 = Int.sign_ext 8 n2 ->
-      val_content_inject f Mint8signed (Vint n1) (Vint n2)
-  | val_content_inject_8_unsigned:
-      forall n1 n2, Int.zero_ext 8 n1 = Int.zero_ext 8 n2 ->
-      val_content_inject f Mint8unsigned (Vint n1) (Vint n2)
-  | val_content_inject_16_signed:
-      forall n1 n2, Int.sign_ext 16 n1 = Int.sign_ext 16 n2 ->
-      val_content_inject f Mint16signed (Vint n1) (Vint n2)
-  | val_content_inject_16_unsigned:
-      forall n1 n2, Int.zero_ext 16 n1 = Int.zero_ext 16 n2 ->
-      val_content_inject f Mint16unsigned (Vint n1) (Vint n2)
-  | val_content_inject_single:
-      forall n1 n2, Float.singleoffloat n1 = Float.singleoffloat n2 ->
-      val_content_inject f Mfloat32 (Vfloat n1) (Vfloat n2)
-  | val_content_inject_base:
-      forall chunk v1 v2, val_inject f v1 v2 ->
-      val_content_inject f chunk v1 v2.
-
-Hint Resolve val_content_inject_base.
-
-Lemma eval_store_arg:
-  forall f sp te tm a v va chunk,
-  eval_expr tge sp te tm a va ->
-  val_inject f v va ->
-  exists vb,
-     eval_expr tge sp te tm (store_arg chunk a) vb
-  /\ val_content_inject f chunk v vb.
-Proof.
-  intros.
-  assert (DFL: forall v', Val.lessdef va v' -> val_content_inject f chunk v v').
-    intros. apply val_content_inject_base. inv H1. auto. inv H0. auto.
-  destruct chunk; simpl.
-  (* int8signed *)
-  exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v' [A B]].
-  exists v'; split; auto.
-  inv B; auto. inv H0; auto. constructor.
-  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
-  repeat rewrite Int.zero_ext_and; auto. omega. omega.
-  (* int8unsigned *)
-  exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v' [A B]].
-  exists v'; split; auto.
-  inv B; auto. inv H0; auto. constructor.
-  repeat rewrite Int.zero_ext_and; auto. omega. omega.
-  (* int16signed *)
-  exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v' [A B]].
-  exists v'; split; auto.
-  inv B; auto. inv H0; auto. constructor.
-  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
-  repeat rewrite Int.zero_ext_and; auto. omega. omega.
-  (* int16unsigned *)
-  exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v' [A B]].
-  exists v'; split; auto.
-  inv B; auto. inv H0; auto. constructor.
-  repeat rewrite Int.zero_ext_and; auto. omega. omega.
-  (* int32 *)
-  exists va; auto.
-  (* int64 *)
-  exists va; auto.
-  (* float32 *)
-  exploit eval_uncast_float32; eauto. intros [v' [A B]].
-  exists v'; split; auto.
-  inv B; auto. inv H0; auto. constructor. auto.
-  (* float64 *)
-  exists va; auto.
-  (* float64al32 *)
-  exists va; auto.
-Qed.
-
-Lemma storev_mapped_content_inject:
-  forall f chunk m1 a1 v1 n1 m2 a2 v2,
-  Mem.inject f m1 m2 ->
-  Mem.storev chunk m1 a1 v1 = Some n1 ->
-  val_inject f a1 a2 ->
-  val_content_inject f chunk v1 v2 ->
-  exists n2,
-    Mem.storev chunk m2 a2 v2 = Some n2 /\ Mem.inject f n1 n2.
-Proof.
-  intros.
-  assert (forall v1',
-    (forall b ofs, Mem.store chunk m1 b ofs v1 = Mem.store chunk m1 b ofs v1') ->
-    Mem.storev chunk m1 a1 v1' = Some n1).
-  intros. rewrite <- H0. destruct a1; simpl; auto. 
-  inv H2; eapply Mem.storev_mapped_inject;
-  try eapply H; try eapply H1; try apply H3; intros.
-  rewrite <- Mem.store_int8_sign_ext. rewrite H4. apply Mem.store_int8_sign_ext.
-  auto.
-  rewrite <- Mem.store_int8_zero_ext. rewrite H4. apply Mem.store_int8_zero_ext.
-  auto.
-  rewrite <- Mem.store_int16_sign_ext. rewrite H4. apply Mem.store_int16_sign_ext.
-  auto.
-  rewrite <- Mem.store_int16_zero_ext. rewrite H4. apply Mem.store_int16_zero_ext.
-  auto.
-  rewrite <- Mem.store_float32_truncate. rewrite H4. apply Mem.store_float32_truncate.
-  auto.
-  eauto.
-  auto.
-Qed.
-
-Lemma make_store_correct:
-  forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m' fn k,
-  eval_expr tge sp te tm addr tvaddr ->
-  eval_expr tge sp te tm rhs tvrhs ->
-  Mem.storev chunk m vaddr vrhs = Some m' ->
-  Mem.inject f m tm ->
-  val_inject f vaddr tvaddr ->
-  val_inject f vrhs tvrhs ->
-  exists tm', exists tvrhs',
-  step tge (State fn (make_store chunk addr rhs) k sp te tm)
-        E0 (State fn Sskip k sp te tm')
-  /\ Mem.storev chunk tm tvaddr tvrhs' = Some tm'
-  /\ Mem.inject f m' tm'.
-Proof.
-  intros. unfold make_store.
-  exploit eval_store_arg. eexact H0. eauto. 
-  intros [tv [EVAL VCINJ]].
-  exploit storev_mapped_content_inject; eauto.
-  intros [tm' [STORE MEMINJ]].
-  exists tm'; exists tv.
-  split. eapply step_store; eauto.
-  auto.
-Qed.
-
-(** Correctness of [make_unop]. *)
-
-Lemma eval_make_unop:
-  forall sp te tm a v op v',
-  eval_expr tge sp te tm a v ->
-  eval_unop op v = Some v' ->
-  exists v'', eval_expr tge sp te tm (make_unop op a) v'' /\ Val.lessdef v' v''.
-Proof.
-  intros; unfold make_unop. 
-  assert (DFL: exists v'', eval_expr tge sp te tm (Eunop op a) v'' /\ Val.lessdef v' v'').
-    exists v'; split. econstructor; eauto. auto.
-  destruct op; auto; simpl in H0; inv H0.
-(* cast8unsigned *)
-  exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v1 [A B]].
-  exists (Val.zero_ext 8 v1); split. econstructor; eauto. 
-  inv B. apply Val.zero_ext_lessdef; auto. simpl.
-  repeat rewrite Int.zero_ext_and; auto.
-  change (two_p 8 - 1) with 255. rewrite H0. auto.
-  omega. omega.
-(* cast8signed *)
-  exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v1 [A B]].
-  exists (Val.sign_ext 8 v1); split. econstructor; eauto. 
-  inv B. apply Val.sign_ext_lessdef; auto. simpl.
-  replace (Int.sign_ext 8 n2) with (Int.sign_ext 8 n1). auto.
-  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
-  repeat rewrite Int.zero_ext_and; auto. omega. omega.
-(* cast16unsigned *)
-  exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v1 [A B]].
-  exists (Val.zero_ext 16 v1); split. econstructor; eauto. 
-  inv B. apply Val.zero_ext_lessdef; auto. simpl.
-  repeat rewrite Int.zero_ext_and; auto.
-  change (two_p 16 - 1) with 65535. rewrite H0. auto.
-  omega. omega.
-(* cast16signed *)
-  exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v1 [A B]].
-  exists (Val.sign_ext 16 v1); split. econstructor; eauto. 
-  inv B. apply Val.sign_ext_lessdef; auto. simpl.
-  replace (Int.sign_ext 16 n2) with (Int.sign_ext 16 n1). auto.
-  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
-  repeat rewrite Int.zero_ext_and; auto. omega. omega.
-(* singleoffloat *)
-  exploit eval_uncast_float32; eauto. intros [v1 [A B]].
-  exists (Val.singleoffloat v1); split. econstructor; eauto. 
-  inv B. apply Val.singleoffloat_lessdef; auto. simpl. rewrite H0; auto.
-Qed.
-
-Lemma make_unop_correct:
-  forall f sp te tm a v op v' tv,
-  eval_expr tge sp te tm a tv ->
-  eval_unop op v = Some v' ->
-  val_inject f v tv ->
-  exists tv', eval_expr tge sp te tm (make_unop op a) tv' /\ val_inject f v' tv'.
-Proof.
-  intros. exploit eval_unop_compat; eauto. intros [tv' [A B]].
-  exploit eval_make_unop; eauto. intros [tv'' [C D]].
-  exists tv''; split; auto. 
-  inv D. auto. inv B. auto.
-Qed.
-
 (** Correctness of the variable accessor [var_addr] *)
 
 Lemma var_addr_correct:
@@ -1995,12 +1418,12 @@ Proof.
   inv H1; inv H0; try congruence.
   (* local *)
   exists (Vptr sp (Int.repr ofs)); split.
-  eapply make_stackaddr_correct.
+  constructor. simpl. rewrite Int.add_zero_l; auto. 
   congruence.
   (* global *)
   exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
   exists (Vptr b Int.zero); split.
-  eapply make_globaladdr_correct; eauto. rewrite symbols_preserved; auto.
+  constructor. simpl. rewrite symbols_preserved. rewrite H2. auto.
   econstructor; eauto.
 Qed.
 
@@ -2040,16 +1463,14 @@ Qed.
 Lemma transl_constant_correct:
   forall f sp cst v,
   Csharpminor.eval_constant cst = Some v ->
-  let (tcst, a) := transl_constant cst in
   exists tv,
-     eval_constant tge sp tcst = Some tv
-  /\ val_inject f v tv
-  /\ val_match_approx a v.
+     eval_constant tge sp (transl_constant cst) = Some tv
+  /\ val_inject f v tv.
 Proof.
   destruct cst; simpl; intros; inv H. 
-  exists (Vint i); intuition. apply approx_of_int_sound.
-  exists (Vfloat f0); intuition. apply approx_of_float_sound.
-  exists (Vlong i); intuition. 
+  exists (Vint i); auto.
+  exists (Vfloat f0); auto.
+  exists (Vlong i); auto.
 Qed.
 
 Lemma transl_expr_correct:
@@ -2060,46 +1481,34 @@ Lemma transl_expr_correct:
              (Mem.nextblock m) (Mem.nextblock tm)),
   forall a v,
   Csharpminor.eval_expr ge e le m a v ->
-  forall ta app
-    (TR: transl_expr cenv a = OK (ta, app)),
+  forall ta
+    (TR: transl_expr cenv a = OK ta),
   exists tv,
      eval_expr tge (Vptr sp Int.zero) te tm ta tv
-  /\ val_inject f v tv
-  /\ val_match_approx app v.
+  /\ val_inject f v tv.
 Proof.
   induction 3; intros; simpl in TR; try (monadInv TR).
   (* Etempvar *)
   inv MATCH. exploit MTMP; eauto. intros [tv [A B]]. 
-  exists tv; split. constructor; auto. split. auto. exact I.
+  exists tv; split. constructor; auto. auto.
   (* Eaddrof *)
-  exploit var_addr_correct; eauto. intros [tv [A B]].
-  exists tv; split. auto. split. auto. red. auto.
+  eapply var_addr_correct; eauto.
   (* Econst *)
-  exploit transl_constant_correct; eauto. 
-  destruct (transl_constant cst) as [tcst a]; inv TR.
-  intros [tv [A [B C]]].
-  exists tv; split. constructor; eauto. eauto.
+  exploit transl_constant_correct; eauto. intros [tv [A B]].
+  exists tv; split; eauto. constructor; eauto. 
   (* Eunop *)
-  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
-  unfold Csharpminor.eval_unop in H0. 
-  destruct (Approx.unop_is_redundant op x0) eqn:?; inv EQ0.
-  (* -- eliminated *)
-  exploit approx_unop_is_redundant_sound; eauto. intros. 
-  replace v with v1 by congruence.
-  exists tv1; auto.
-  (* -- preserved *)
-  exploit make_unop_correct; eauto. intros [tv [A B]].
-  exists tv; split. auto. split. auto. eapply approx_of_unop_sound; eauto.
+  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]].
+  exists tv; split; auto. econstructor; eauto.  
   (* Ebinop *)
-  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
-  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 [INJ2 APP2]]].
+  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]].
   exploit eval_binop_compat; eauto. intros [tv [EVAL INJ]].
-  exists tv; split. econstructor; eauto. split. auto. eapply approx_of_binop_sound; eauto.
+  exists tv; split. econstructor; eauto. auto.
   (* Eload *)
-  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
+  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
   exploit Mem.loadv_inject; eauto. intros [tv [LOAD INJ]].
-  exists tv; split. econstructor; eauto. split. auto.
-  destruct v1; simpl in H0; try discriminate. eapply approx_of_chunk_sound; eauto.
+  exists tv; split. econstructor; eauto. auto.
 Qed.
 
 Lemma transl_exprlist_correct:
@@ -2118,7 +1527,7 @@ Lemma transl_exprlist_correct:
 Proof.
   induction 3; intros; monadInv TR.
   exists (@nil val); split. constructor. constructor.
-  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 [VINJ1 APP1]]].
+  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]].
   exploit IHeval_exprlist; eauto. intros [tv2 [EVAL2 VINJ2]].
   exists (tv1 :: tv2); split. constructor; auto. constructor; auto.
 Qed.
@@ -2517,7 +1926,7 @@ Proof.
 
 (* set *)
   monadInv TR.
-  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
   econstructor; eauto. 
@@ -2526,13 +1935,12 @@ Proof.
 (* store *)
   monadInv TR.
   exploit transl_expr_correct. eauto. eauto. eexact H. eauto. 
-  intros [tv1 [EVAL1 [VINJ1 APP1]]].
+  intros [tv1 [EVAL1 VINJ1]].
   exploit transl_expr_correct. eauto. eauto. eexact H0. eauto. 
-  intros [tv2 [EVAL2 [VINJ2 APP2]]].
-  exploit make_store_correct. eexact EVAL1. eexact EVAL2. eauto. eauto. auto. auto.
-  intros [tm' [tv' [EXEC [STORE' MINJ']]]].
+  intros [tv2 [EVAL2 VINJ2]].
+  exploit Mem.storev_mapped_inject; eauto. intros [tm' [STORE' MINJ']]. 
   left; econstructor; split.
-  apply plus_one. eexact EXEC.
+  apply plus_one. econstructor; eauto. 
   econstructor; eauto.
   inv VINJ1; simpl in H1; try discriminate. unfold Mem.storev in STORE'.
   rewrite (Mem.nextblock_store _ _ _ _ _ _ H1).
@@ -2544,7 +1952,7 @@ Proof.
 (* call *)
   simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
   monadInv TR.
-  exploit transl_expr_correct; eauto. intros [tvf [EVAL1 [VINJ1 APP1]]].
+  exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
   assert (tvf = vf).
     exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
     eapply val_inject_function_pointer; eauto.
@@ -2596,8 +2004,8 @@ Opaque PTree.set.
 
 (* ifthenelse *)
   monadInv TR.
-  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
-  left; exists (State tfn (if b then x1 else x2) tk (Vptr sp Int.zero) te tm); split.
+  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
+  left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Int.zero) te tm); split.
   apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto.
   econstructor; eauto. destruct b; auto.
 
@@ -2649,7 +2057,7 @@ Opaque PTree.set.
 
 (* switch *)
   monadInv TR. left.
-  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   inv VINJ.
   exploit switch_descent; eauto. intros [k1 [A B]].
   exploit switch_ascent; eauto. intros [k2 [C D]].
@@ -2673,7 +2081,7 @@ Opaque PTree.set.
 
 (* return some *)
   monadInv TR. left. 
-  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
   apply plus_one. eapply step_return_1. eauto. eauto.