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

3 files changed, 828 insertions, 284 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index c293efb..3a8b857 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -20,12 +20,13 @@ Require Import Maps.
 Require Import Ordered.
 Require Import AST.
 Require Import Integers.
+Require Import Floats.
 Require Import Memdata.
 Require Import Csharpminor.
 Require Import Cminor.
 
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
 
 (** The main task in translating Csharpminor to Cminor is to explicitly
   stack-allocate local variables whose address is taken: these local
@@ -37,17 +38,17 @@ Open Local Scope error_monad_scope.
   taken in the Csharpminor code can be mapped to Cminor local
   variable, since the latter do not reside in memory.  
 
-  Another task performed during the translation to Cminor is the
-  insertion of truncation, zero- and sign-extension operations when
-  assigning to a Csharpminor local variable of ``small'' type
-  (e.g. [Mfloat32] or [Mint8signed]).  This is necessary to preserve
-  the ``normalize at assignment-time'' semantics of Clight and Csharpminor.
+  Another task performed during the translation to Cminor is to eliminate
+  redundant casts to small numerical types (8- and 16-bit integers,
+  single-precision floats).  
 
   Finally, the Clight-like [switch] construct of Csharpminor
   is transformed into the simpler, lower-level [switch] construct
   of Cminor.
 *)
 
+(** * Handling of variables *)
+
 Definition for_var (id: ident) : ident := xO id.
 Definition for_temp (id: ident) : ident := xI id.
 
@@ -69,41 +70,46 @@ Inductive var_info: Type :=
 
 Definition compilenv := PMap.t var_info.
 
-(*****
-(** [make_cast chunk e] returns a Cminor expression that normalizes
-  the value of Cminor expression [e] as prescribed by the memory chunk
-  [chunk].  For instance, 8-bit sign extension is performed if
-  [chunk] is [Mint8signed]. *)
-
-Definition make_cast (chunk: memory_chunk) (e: expr): expr :=
-  match chunk with
-  | Mint8signed => Eunop Ocast8signed e
-  | Mint8unsigned => Eunop Ocast8unsigned e
-  | Mint16signed => Eunop Ocast16signed e
-  | Mint16unsigned => Eunop Ocast16unsigned e
-  | Mint32 => e
-  | Mfloat32 => Eunop Osingleoffloat e
-  | Mfloat64 => e
-  end.
-**********)
+(** * Helper functions for code generation *)
 
 (** When the translation of an expression is stored in memory,
-  a cast at the toplevel of the expression can be redundant
+  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. *)
 
-Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
+Function uncast_int8 (e: expr) : expr :=
+  match e with
+  | Eunop (Ocast8unsigned|Ocast8signed|Ocast16unsigned|Ocast16signed) e1 =>
+      uncast_int8 e1
+  | Ebinop Oand e1 (Econst (Ointconst n)) =>
+      if Int.eq (Int.and n (Int.repr 255)) (Int.repr 255)
+      then uncast_int8 e1
+      else e
+  | _ => e
+  end.
+
+Function uncast_int16 (e: expr) : expr :=
   match e with
-  | Eunop Ocast8signed e1 =>
-      match chunk with Mint8signed => e1 | _ => e end
-  | Eunop Ocast8unsigned e1 =>
-      match chunk with Mint8unsigned => e1 | _ => e end
-  | Eunop Ocast16signed e1 =>
-      match chunk with Mint16signed => e1 | _ => e end
-  | Eunop Ocast16unsigned e1 =>
-      match chunk with Mint16unsigned => e1 | _ => e end
-  | Eunop Osingleoffloat e1 =>
-      match chunk with Mfloat32 => e1 | _ => e end
+  | Eunop (Ocast16unsigned|Ocast16signed) e1 =>
+      uncast_int16 e1
+  | Ebinop Oand e1 (Econst (Ointconst n)) =>
+      if Int.eq (Int.and n (Int.repr 65535)) (Int.repr 65535)
+      then uncast_int16 e1
+      else e
+  | _ => e
+  end.
+
+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.
 
@@ -116,16 +122,148 @@ Definition make_stackaddr (ofs: Z): expr :=
 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 *)
+  | 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
+  | 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
+  | Float32, Float32 => true
+  | _, _ => false
+  end.
+
+Definition lub (x y: approx) : approx :=
+  match x, y with
+  | 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
+  | Float32, Float32 => Float32
+  | _, _ => Any
+  end.
+
+Definition of_int (n: int) :=
+  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
+  | Mfloat32 => Float32
+  | Mfloat64 => Any
+  end.
+
+Definition unop (op: unary_operation) (a: approx) :=
+  match op with
+  | Ocast8unsigned => Int8u
+  | Ocast8signed => Int8s
+  | Ocast16unsigned => Int16u
+  | Ocast16signed => Int16s
+  | Osingleoffloat => Float32
+  | Onotbool => Int7
+  | _ => 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 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 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 _ => Int7
+  | Ocmpu _ => Int7
+  | Ocmpf _ => Int7
+  | _ => Any
+  end.
+
+End Approx.
+
+(** * Translation of expressions and statements. *)
+
 (** Generation of a Cminor expression for reading a Csharpminor variable. *)
 
-Definition var_get (cenv: compilenv) (id: ident): res expr :=
+Definition var_get (cenv: compilenv) (id: ident): res (expr * approx) :=
   match PMap.get id cenv with
   | Var_local chunk =>
-      OK(Evar (for_var id))
+      OK(Evar (for_var id), Approx.of_chunk chunk)
   | Var_stack_scalar chunk ofs =>
-      OK(Eload chunk (make_stackaddr ofs))
+      OK(Eload chunk (make_stackaddr ofs), Approx.of_chunk chunk)
   | Var_global_scalar chunk =>
-      OK(Eload chunk (make_globaladdr id))
+      OK(Eload chunk (make_globaladdr id), Approx.of_chunk chunk)
   | _ =>
       Error(msg "Cminorgen.var_get")
   end.
@@ -133,12 +271,12 @@ Definition var_get (cenv: compilenv) (id: ident): res expr :=
 (** Generation of a Cminor expression for taking the address of
   a Csharpminor variable. *)
 
-Definition var_addr (cenv: compilenv) (id: ident): res expr :=
+Definition var_addr (cenv: compilenv) (id: ident): res (expr * approx) :=
   match PMap.get id cenv with
   | Var_local chunk => Error(msg "Cminorgen.var_addr")
-  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs)
-  | Var_stack_array ofs => OK (make_stackaddr ofs)
-  | _ => OK (make_globaladdr id)
+  | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs, Any)
+  | Var_stack_array ofs => OK (make_stackaddr ofs, Any)
+  | _ => OK (make_globaladdr id, Any)
   end.
 
 (** Generation of a Cminor statement performing an assignment to
@@ -175,38 +313,46 @@ Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ) (k: stmt): res s
 
 (** Translation of constants. *)
 
-Definition transl_constant (cst: Csharpminor.constant): constant :=
+Definition transl_constant (cst: Csharpminor.constant): (constant * approx) :=
   match cst with
-  | Csharpminor.Ointconst n => Ointconst n
-  | Csharpminor.Ofloatconst n => Ofloatconst n
+  | Csharpminor.Ointconst n =>
+      (Ointconst n, Approx.of_int n)
+  | Csharpminor.Ofloatconst n =>
+      (Ofloatconst n, Approx.of_float n)
   end.
 
-(** Translation of expressions.  All the hard work is done by the
-  [make_*] and [var_*] functions defined above. *)
+(** 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. *)
 
 Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
-                     {struct e}: res expr :=
+                     {struct e}: res (expr * approx) :=
   match e with
-  | Csharpminor.Evar id => var_get cenv id
-  | Csharpminor.Etempvar id => OK (Evar (for_temp id))
-  | Csharpminor.Eaddrof id => var_addr cenv id
+  | Csharpminor.Evar id =>
+      var_get cenv id
+  | Csharpminor.Etempvar id =>
+      OK (Evar (for_temp id), Any)
+  | Csharpminor.Eaddrof id =>
+      var_addr cenv id
   | Csharpminor.Econst cst =>
-      OK (Econst (transl_constant cst))
+      let (tcst, a) := transl_constant cst in OK (Econst tcst, a)
   | Csharpminor.Eunop op e1 =>
-      do te1 <- transl_expr cenv e1;
-      OK (Eunop op te1)
+      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)
   | Csharpminor.Ebinop op e1 e2 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
-      OK (Ebinop op te1 te2)
+      do (te1, a1) <- transl_expr cenv e1;
+      do (te2, a2) <- transl_expr cenv e2;
+      OK (Ebinop op te1 te2, Approx.binop op a1 a2)
   | Csharpminor.Eload chunk e =>
-      do te <- transl_expr cenv e;
-      OK (Eload chunk te)
+      do (te, a) <- transl_expr cenv e;
+      OK (Eload chunk te, Approx.of_chunk chunk)
   | Csharpminor.Econdition e1 e2 e3 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
-      do te3 <- transl_expr cenv e3;
-      OK (Econdition te1 te2 te3)
+      do (te1, a1) <- transl_expr cenv e1;
+      do (te2, a2) <- transl_expr cenv e2;
+      do (te3, a3) <- transl_expr cenv e3;
+      OK (Econdition te1 te2 te3, Approx.lub a2 a3)
   end.
 
 Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
@@ -215,7 +361,7 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr)
   | nil =>
       OK nil
   | e1 :: e2 =>
-      do te1 <- transl_expr cenv e1;
+      do (te1, a1) <- transl_expr cenv e1;
       do te2 <- transl_exprlist cenv e2;
       OK (te1 :: te2)
   end.
@@ -261,12 +407,7 @@ Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env :=
   end.
 
 (** Translation of statements.  The nonobvious part is
-  the translation of [switch] statements, outlined above. 
-  Also note the additional type checks on arguments to calls and returns.
-  These checks should always succeed for C#minor code generated from
-  well-typed Clight code, but are necessary for the correctness proof
-  to go through.
-*)
+  the translation of [switch] statements, outlined above. *)
 
 Definition typ_of_opttyp (ot: option typ) :=
   match ot with None => Tint | Some t => t end.
@@ -278,17 +419,17 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv)
   | Csharpminor.Sskip =>
       OK Sskip
   | Csharpminor.Sassign id e =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       var_set cenv id te
   | Csharpminor.Sset id e =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       OK (Sassign (for_temp id) te)
   | Csharpminor.Sstore chunk e1 e2 =>
-      do te1 <- transl_expr cenv e1;
-      do te2 <- transl_expr cenv e2;
+      do (te1, a1) <- transl_expr cenv e1;
+      do (te2, a2) <- transl_expr cenv e2;
       OK (make_store chunk te1 te2)
   | Csharpminor.Scall optid sig e el =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
       OK (Scall (option_map for_temp optid) sig te tel)
   | Csharpminor.Sseq s1 s2 =>
@@ -296,7 +437,7 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv)
       do ts2 <- transl_stmt ret cenv xenv s2;
       OK (Sseq ts1 ts2)
   | Csharpminor.Sifthenelse e s1 s2 =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       do ts1 <- transl_stmt ret cenv xenv s1;
       do ts2 <- transl_stmt ret cenv xenv s2;
       OK (Sifthenelse te ts1 ts2)
@@ -311,12 +452,12 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv)
   | Csharpminor.Sswitch e ls =>
       let cases := switch_table ls O in
       let default := length cases in
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       transl_lblstmt ret cenv (switch_env ls xenv) ls (Sswitch te cases default)
   | Csharpminor.Sreturn None =>
       OK (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
-      do te <- transl_expr cenv e;
+      do (te, a) <- transl_expr cenv e;
       OK (Sreturn (Some te))
   | Csharpminor.Slabel lbl s =>
       do ts <- transl_stmt ret cenv xenv s; OK (Slabel lbl ts)
@@ -336,6 +477,8 @@ with transl_lblstmt (ret: option typ) (cenv: compilenv)
       transl_lblstmt ret cenv (List.tail xenv) ls' (Sseq (Sblock body) ts)
   end.
 
+(** * Stack layout *)
+
 (** Computation of the set of variables whose address is taken in
   a piece of Csharpminor code. *)
 
@@ -455,6 +598,8 @@ Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
   List.fold_left assign_global_variable 
                  p.(prog_vars) (PMap.init Var_global_array).
 
+(** * Translation of functions *)
+
 (** Function parameters whose address is taken must be stored in their
   stack slots at function entry.  (Cminor passes these parameters in
   local variables.) *)
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 10ffbe4..a6656e0 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1152,63 +1152,240 @@ Proof.
   intros. symmetry. eapply IMAGE; eauto. 
 Qed.
 
-(** * Correctness of Cminor construction functions *)
+(** * Properties of compile-time approximations of values *)
+
+Definition val_match_approx (a: approx) (v: val) : Prop :=
+  match a with
+  | 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 val_inject_val_of_bool:
-  forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
+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. 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. 
+  unfold Approx.bge in H; destruct a1; try discriminate; destruct a2; simpl in *; try discriminate; intuition; auto.
+Qed.
+
+Lemma approx_lub_ge_left:
+  forall x y, Approx.bge (Approx.lub x y) x = true.
+Proof.
+  destruct x; destruct y; auto. 
+Qed.
+
+Lemma approx_lub_ge_right:
+  forall x y, Approx.bge (Approx.lub x y) y = true.
+Proof.
+  destruct x; destruct y; auto. 
+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_ext 7 n)). 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 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. compute; auto. split. omega. compute; auto.
+    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
+  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.
-  intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor.
+  unfold Approx.of_float; intros. 
+  destruct (Float.eq_dec f (Float.singleoffloat f)); simpl; auto. congruence.
 Qed.
 
-Remark val_inject_eval_compare_mismatch:
-  forall f c v,  
-  eval_compare_mismatch c = Some v ->
-  val_inject f v v.
+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.
-  unfold eval_compare_mismatch; intros.
-  destruct c; inv H; unfold Vfalse, Vtrue; constructor.
+  intros. exploit Mem.load_cast; eauto. 
+  destruct chunk; intros; simpl; auto.
 Qed.
 
-Remark val_inject_eval_compare_null:
-  forall f i c v,  
-  eval_compare_null c i = Some v ->
-  val_inject f v v.
+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. compute; auto.
+  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto.
+  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto.
+  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto.
+  destruct v1; simpl; auto. destruct (Int.eq i Int.zero); auto.
+  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.
+  intros; unfold Approx.bitwise_and. 
+  destruct (Approx.bge Int8u a1) as []_eqn. simpl. apply Y; eauto. compute; auto.
+  destruct (Approx.bge Int8u a2) as []_eqn. simpl. apply X; eauto. compute; auto.
+  destruct (Approx.bge Int16u a1) as []_eqn. simpl. apply Y; eauto. compute; auto.
+  destruct (Approx.bge Int16u a2) as []_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 Int8u a1 && Approx.bge Int8u a2) as []_eqn.
+  destruct (andb_prop _ _ Heqb).
+  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) as []_eqn.
+  destruct (andb_prop _ _ Heqb0).
+  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 Int7 (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:
+  forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
 Proof.
-  unfold eval_compare_null. intros. destruct (Int.eq i Int.zero). 
-  eapply val_inject_eval_compare_mismatch; eauto. 
-  discriminate.
+  intros; destruct b; constructor.
 Qed.
 
-Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr.
+Remark val_inject_val_of_optbool:
+  forall f ob, val_inject f (Val.of_optbool ob) (Val.of_optbool ob).
+Proof.
+  intros; destruct ob; simpl. destruct b; constructor. constructor.
+Qed.
 
-Ltac TrivialOp :=
+Ltac TrivialExists :=
   match goal with
+  | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] =>
+      exists x; split; [auto | try(econstructor; eauto)]
   | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] =>
-      exists (Vint x); split;
-      [eauto with evalexpr | constructor]
+      exists (Vint x); split; [eauto with evalexpr | constructor]
   | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] =>
-      exists (Vfloat x); split;
-      [eauto with evalexpr | constructor]
-  | [ |- exists y, _ /\ val_inject _ (Val.of_bool ?x) _ ] =>
-      exists (Val.of_bool x); split;
-      [eauto with evalexpr | apply val_inject_val_of_bool]
-  | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] =>
-      exists x; split; [auto | econstructor; eauto]
+      exists (Vfloat x); split; [eauto with evalexpr | constructor]
   | _ => idtac
   end.
 
-(** Correctness of [transl_constant]. *)
-
-Lemma transl_constant_correct:
-  forall f sp cst v,
-  Csharpminor.eval_constant cst = Some v ->
-  exists tv,
-     eval_constant tge sp (transl_constant cst) = Some tv
-  /\ val_inject f v tv.
-Proof.
-  destruct cst; simpl; intros; inv H; TrivialOp.
-Qed.
-
 (** Compatibility of [eval_unop] with respect to [val_inject]. *)
 
 Lemma eval_unop_compat:
@@ -1220,104 +1397,96 @@ Lemma eval_unop_compat:
   /\ val_inject f v tv.
 Proof.
   destruct op; simpl; intros.
-  inv H; inv H0; simpl; TrivialOp.
-  inv H; inv H0; simpl; TrivialOp.
-  inv H; inv H0; simpl; TrivialOp.
-  inv H; inv H0; simpl; TrivialOp.
-  inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp.
-  inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp.
-  inv H0; inv H; TrivialOp.
-  inv H0; inv H; TrivialOp.
-  inv H0; inv H; TrivialOp.
-  inv H0; inv H; TrivialOp.
-  inv H0; inv H. destruct (Float.intoffloat f0); simpl in H1; inv H1. TrivialOp.
-  inv H0; inv H. destruct (Float.intuoffloat f0); simpl in H1; inv H1. TrivialOp.
-  inv H0; inv H; TrivialOp.
-  inv H0; inv H; TrivialOp.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists. apply val_inject_val_of_bool.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.intuoffloat f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
 Qed.
 
 (** Compatibility of [eval_binop] with respect to [val_inject]. *)
 
 Lemma eval_binop_compat:
   forall f op v1 tv1 v2 tv2 v m tm,
-  Csharpminor.eval_binop op v1 v2 m = Some v ->
+  eval_binop op v1 v2 m = Some v ->
   val_inject f v1 tv1 ->
   val_inject f v2 tv2 ->
   Mem.inject f m tm ->
   exists tv,
-     Cminor.eval_binop op tv1 tv2 tm = Some tv
+     eval_binop op tv1 tv2 tm = Some tv
   /\ val_inject f v tv.
 Proof.
   destruct op; simpl; intros.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H; inv H0; inv H1; TrivialExists.
     repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
     repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H; inv H0; inv H1; TrivialExists.
     apply Int.sub_add_l.
-    destruct (eq_block b1 b0); inv H4. 
-    assert (b3 = b2) by congruence. subst b3. 
-    unfold eq_block; rewrite zeq_true. TrivialOp.
-    replace delta0 with delta by congruence.
-    decEq. decEq. apply Int.sub_shifted.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.eq i0 Int.zero); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+    simpl. destruct (zeq b1 b0); auto.
+    subst b1. rewrite H in H0; inv H0. 
+    rewrite zeq_true. rewrite Int.sub_shifted. auto.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto.
+  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto.
+  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int.iwordsize); auto.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
 (* cmpu *)
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
-  exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
-  exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
-  (* cmpu ptr ptr *)
-  caseEq (Mem.valid_pointer m b1 (Int.unsigned ofs1) && Mem.valid_pointer m b0 (Int.unsigned ofs0)); 
-  intro EQ; rewrite EQ in H4; try discriminate.
-  elim (andb_prop _ _ EQ); intros.
-  exploit Mem.valid_pointer_inject_val. eauto. eexact H. econstructor; eauto. 
-  intros V1. rewrite V1.
-  exploit Mem.valid_pointer_inject_val. eauto. eexact H1. econstructor; eauto. 
-  intros V2. rewrite V2. simpl.
-  destruct (eq_block b1 b0); inv H4.
-  (* same blocks in source *)
-  assert (b3 = b2) by congruence. subst b3.
-  assert (delta0 = delta) by congruence. subst delta0.
-  exists (Val.of_bool (Int.cmpu c ofs1 ofs0)); split.
-  unfold eq_block; rewrite zeq_true; simpl.
-  decEq. decEq. rewrite Int.translate_cmpu. auto. 
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  eapply Mem.valid_pointer_inject_no_overflow; eauto.
-  apply val_inject_val_of_bool.
-  (* different blocks in source *)
-  simpl. exists v; split; [idtac | eapply val_inject_eval_compare_mismatch; eauto].
-  destruct (eq_block b2 b3); auto.
-  exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
-  congruence.
-  decEq. destruct c; simpl in H6; inv H6; unfold Int.cmpu.
-  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)).
-  congruence. auto.
-  predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)).
-  congruence. auto.
+  inv H; inv H0; inv H1; TrivialExists.
+    apply val_inject_val_of_optbool.
+    apply val_inject_val_of_optbool.
+    apply val_inject_val_of_optbool.
+Opaque Int.add.
+    unfold Val.cmpu. simpl. 
+    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) as []_eqn; simpl; auto.
+    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) as []_eqn; simpl; auto.
+    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto. 
+    intros V1. rewrite V1.
+    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
+    intros V2. rewrite V2. simpl.
+    destruct (zeq b1 b0).
+    (* same blocks *)
+    subst b1. rewrite H in H0; inv H0. rewrite zeq_true. 
+    rewrite Int.translate_cmpu. apply val_inject_val_of_optbool.
+    eapply Mem.valid_pointer_inject_no_overflow; eauto.
+    eapply Mem.valid_pointer_inject_no_overflow; eauto.
+    (* different source blocks *)
+    destruct (zeq b2 b3).
+    exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
+    congruence.
+    destruct c; simpl; auto. 
+    rewrite Int.eq_false. constructor. congruence.
+    rewrite Int.eq_false. constructor. congruence.
+    apply val_inject_val_of_optbool.
   (* cmpf *)
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
 Qed.
 
+(** * Correctness of Cminor construction functions *)
+
 Lemma make_stackaddr_correct:
   forall sp te tm ofs,
   eval_expr tge (Vptr sp Int.zero) te tm
@@ -1340,30 +1509,160 @@ Qed.
 
 (** Correctness of [make_store]. *)
 
+Inductive val_lessdef_upto (n: Z): val -> val -> Prop :=
+  | val_lessdef_upto_base:
+      forall v1 v2, Val.lessdef v1 v2 -> val_lessdef_upto n v1 v2
+  | val_lessdef_upto_int:
+      forall n1 n2, Int.zero_ext n n1 = Int.zero_ext n n2 -> val_lessdef_upto n (Vint n1) (Vint n2).
+
+Hint Resolve val_lessdef_upto_base.
+
+Remark val_lessdef_upto_zero_ext:
+  forall n n' v1 v2,
+  0 < n < Z_of_nat Int.wordsize -> n <= n' < Z_of_nat Int.wordsize ->
+  val_lessdef_upto n v1 v2 ->
+  val_lessdef_upto n (Val.zero_ext n' v1) v2.
+Proof.
+  intros. inv H1. inv H2. 
+  destruct v2; simpl; auto. 
+  apply val_lessdef_upto_int. apply Int.zero_ext_narrow; auto. 
+  simpl; auto.
+  apply val_lessdef_upto_int. rewrite <- H2. apply Int.zero_ext_narrow; auto.
+Qed.
+ 
+Remark val_lessdef_upto_sign_ext:
+  forall n n' v1 v2,
+  0 < n < Z_of_nat Int.wordsize -> n <= n' < Z_of_nat Int.wordsize ->
+  val_lessdef_upto n v1 v2 ->
+  val_lessdef_upto n (Val.sign_ext n' v1) v2.
+Proof.
+  intros. inv H1. inv H2. 
+  destruct v2; simpl; auto. 
+  apply val_lessdef_upto_int. apply Int.zero_sign_ext_narrow; auto. 
+  simpl; auto.
+  apply val_lessdef_upto_int. rewrite <- H2. apply Int.zero_sign_ext_narrow; auto.
+Qed.
+
+Remark val_lessdef_upto_and:
+  forall n v1 v2 m,
+  0 < n < Z_of_nat Int.wordsize ->
+  Int.eq (Int.and m (Int.repr (two_p n - 1))) (Int.repr (two_p n - 1)) = true ->
+  val_lessdef_upto n v1 v2 ->
+  val_lessdef_upto n (Val.and v1 (Vint m)) v2.
+Proof.
+  intros. set (p := Int.repr (two_p n - 1)) in *.
+  generalize (Int.eq_spec (Int.and m p) p). rewrite H0; intros.
+  inv H1. inv H3. 
+  destruct v2; simpl; auto. 
+  apply val_lessdef_upto_int. repeat rewrite Int.zero_ext_and; auto.
+  rewrite Int.and_assoc. congruence.
+  simpl; auto.
+  apply val_lessdef_upto_int. rewrite <- H3. repeat rewrite Int.zero_ext_and; auto.
+  rewrite Int.and_assoc. congruence.
+Qed.
+
+Lemma eval_uncast_int8:
+  forall sp te tm a x,
+  eval_expr tge sp te tm a x ->
+  exists v, eval_expr tge sp te tm (uncast_int8 a) v /\ val_lessdef_upto 8 x v.
+Proof.
+  intros until a. functional induction (uncast_int8 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. split. omega. compute; 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. split. omega. compute; 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. split. omega. compute; 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. split. omega. compute; auto.
+  (* and *)
+  inv H. inv H5. simpl in H0. inv H0. simpl in H6. inv H6. exploit IHe; eauto. intros [v [A B]].
+  exists v; split; auto. apply val_lessdef_upto_and; auto. compute; auto.
+  (* and 2 *)
+  exists x; split; auto.
+  (* default *)
+  exists x; split; auto.
+Qed.
+
+Lemma eval_uncast_int16:
+  forall sp te tm a x,
+  eval_expr tge sp te tm a x ->
+  exists v, eval_expr tge sp te tm (uncast_int16 a) v /\ val_lessdef_upto 16 x v.
+Proof.
+  intros until a. functional induction (uncast_int16 a); intros.
+  (* 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. split. omega. compute; 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. split. omega. compute; auto.
+  (* and *)
+  inv H. inv H5. simpl in H0. inv H0. simpl in H6. inv H6. exploit IHe; eauto. intros [v [A B]].
+  exists v; split; auto. apply val_lessdef_upto_and; auto. compute; auto.
+  (* and 2 *)
+  exists x; split; 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 n,
-      val_content_inject f Mint8signed (Vint (Int.sign_ext 8 n)) (Vint n)
+      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 n,
-      val_content_inject f Mint8unsigned (Vint (Int.zero_ext 8 n)) (Vint n)
+      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 n,
-      val_content_inject f Mint16signed (Vint (Int.sign_ext 16 n)) (Vint n)
+      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 n,
-      val_content_inject f Mint16unsigned (Vint (Int.zero_ext 16 n)) (Vint n)
-  | val_content_inject_32:
-      forall n,
-      val_content_inject f Mfloat32 (Vfloat (Float.singleoffloat n)) (Vfloat n)
+      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 ->
+      forall chunk v1 v2, val_inject f v1 v2 ->
       val_content_inject f chunk v1 v2.
 
 Hint Resolve val_content_inject_base.
 
-Lemma store_arg_content_inject:
+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 ->
@@ -1371,20 +1670,37 @@ Lemma store_arg_content_inject:
      eval_expr tge sp te tm (store_arg chunk a) vb
   /\ val_content_inject f chunk v vb.
 Proof.
-  intros. 
-  assert (exists vb,
-       eval_expr tge sp te tm a vb  
-    /\ val_content_inject f chunk v vb).
-  exists va; split. assumption. constructor. assumption.
-  destruct a; simpl store_arg; trivial;
-  destruct u; trivial;
-  destruct chunk; trivial;
-  inv H; simpl in H6; inv H6;
-  econstructor; (split; [eauto|idtac]);
-  destruct v1; simpl in H0; inv H0; constructor; constructor.
-Qed.
-
-Lemma storev_mapped_inject':
+  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_int8; 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. compute; auto.
+  (* int8unsigned *)
+  exploit eval_uncast_int8; eauto. intros [v' [A B]].
+  exists v'; split; auto.
+  inv B; auto. inv H0; auto. constructor. auto.
+  (* int16signed *)
+  exploit eval_uncast_int16; 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. compute; auto.
+  (* int16unsigned *)
+  exploit eval_uncast_int16; eauto. intros [v' [A B]].
+  exists v'; split; auto.
+  inv B; auto. inv H0; auto. constructor. auto.
+  (* int32 *)
+  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.
+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 ->
@@ -1400,11 +1716,11 @@ Proof.
   intros. rewrite <- H0. destruct a1; simpl; auto. 
   inv H2; (eapply Mem.storev_mapped_inject; [eauto|idtac|eauto|eauto]);
   auto; apply H3; intros.
-  apply Mem.store_int8_sign_ext.
-  apply Mem.store_int8_zero_ext.
-  apply Mem.store_int16_sign_ext.
-  apply Mem.store_int16_zero_ext.
-  apply Mem.store_float32_truncate.
+  rewrite <- Mem.store_int8_sign_ext. rewrite H4. apply Mem.store_int8_sign_ext.
+  rewrite <- Mem.store_int8_zero_ext. rewrite H4. apply Mem.store_int8_zero_ext.
+  rewrite <- Mem.store_int16_sign_ext. rewrite H4. apply Mem.store_int16_sign_ext.
+  rewrite <- Mem.store_int16_zero_ext. rewrite H4. apply Mem.store_int16_zero_ext.
+  rewrite <- Mem.store_float32_truncate. rewrite H4. apply Mem.store_float32_truncate.
 Qed.
 
 Lemma make_store_correct:
@@ -1422,36 +1738,87 @@ Lemma make_store_correct:
   /\ Mem.inject f m' tm'.
 Proof.
   intros. unfold make_store.
-  exploit store_arg_content_inject. eexact H0. eauto. 
+  exploit eval_store_arg. eexact H0. eauto. 
   intros [tv [EVAL VCINJ]].
-  exploit storev_mapped_inject'; eauto.
+  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_int8; eauto. intros [v1 [A B]].
+  exists (Val.zero_ext 8 v1); split. econstructor; eauto. 
+  inv B. apply Val.zero_ext_lessdef; auto. simpl. rewrite H0; auto. 
+(* cast8signed *)
+  exploit eval_uncast_int8; eauto. intros [v1 [A B]].
+  exists (Val.sign_ext 8 v1); split. econstructor; eauto. 
+  inv B. apply Val.sign_ext_lessdef; auto. simpl.
+  exploit Int.sign_ext_equal_if_zero_equal; eauto. compute; auto. intro EQ; rewrite EQ; auto.
+(* cast16unsigned *)
+  exploit eval_uncast_int16; eauto. intros [v1 [A B]].
+  exists (Val.zero_ext 16 v1); split. econstructor; eauto. 
+  inv B. apply Val.zero_ext_lessdef; auto. simpl. rewrite H0; auto. 
+(* cast16signed *)
+  exploit eval_uncast_int16; eauto. intros [v1 [A B]].
+  exists (Val.sign_ext 16 v1); split. econstructor; eauto. 
+  inv B. apply Val.sign_ext_lessdef; auto. simpl.
+  exploit Int.sign_ext_equal_if_zero_equal; eauto. compute; auto. intro EQ; rewrite EQ; auto.
+(* 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 accessors [var_get], [var_addr],
   and [var_set]. *)
 
 Lemma var_get_correct:
-  forall cenv id a f tf e le te sp lo hi m cs tm b chunk v,
-  var_get cenv id = OK a ->
+  forall cenv id a app f tf e le te sp lo hi m cs tm b chunk v,
+  var_get cenv id = OK (a, app) ->
   match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
   Mem.inject f m tm ->
   eval_var_ref ge e id b chunk ->
   Mem.load chunk m b 0 = Some v ->
   exists tv,
-    eval_expr tge (Vptr sp Int.zero) te tm a tv /\
-    val_inject f v tv.
+     eval_expr tge (Vptr sp Int.zero) te tm a tv
+  /\ val_inject f v tv
+  /\ val_match_approx app v.
 Proof.
   unfold var_get; intros.
   assert (match_var f id e m te sp cenv!!id). inv H0. inv MENV. auto.
   inv H4; rewrite <- H5 in H; inv H; inv H2; try congruence.
   (* var_local *)
+  rewrite H in H6; inv H6.
   exists v'; split.
   apply eval_Evar. auto.
-  congruence.
+  split. congruence. eapply approx_of_chunk_sound; eauto. 
   (* var_stack_scalar *)
   assert (b0 = b). congruence. subst b0.
   assert (chunk0 = chunk). congruence. subst chunk0.
@@ -1460,7 +1827,7 @@ Proof.
   intros [tv [LOAD INJ]].
   exists tv; split. 
   eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto.
-  auto.
+  split. auto. eapply approx_of_chunk_sound; eauto. 
   (* var_global_scalar *)
   simpl in *.
   exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
@@ -1472,17 +1839,18 @@ Proof.
   exists tv; split. 
   eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto.
   rewrite symbols_preserved; auto.
-  auto.
+  split. auto. eapply approx_of_chunk_sound; eauto. 
 Qed.
 
 Lemma var_addr_correct:
-  forall cenv id a f tf e le te sp lo hi m cs tm b,
+  forall cenv id a app f tf e le te sp lo hi m cs tm b,
   match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
-  var_addr cenv id = OK a ->
+  var_addr cenv id = OK (a, app) ->
   eval_var_addr ge e id b ->
   exists tv,
-    eval_expr tge (Vptr sp Int.zero) te tm a tv /\
-    val_inject f (Vptr b Int.zero) tv.
+     eval_expr tge (Vptr sp Int.zero) te tm a tv
+  /\ val_inject f (Vptr b Int.zero) tv
+  /\ val_match_approx app (Vptr b Int.zero).
 Proof.
   unfold var_addr; intros.
   assert (match_var f id e m te sp cenv!!id).
@@ -1490,20 +1858,21 @@ Proof.
   inv H2; rewrite <- H3 in H0; inv H0; inv H1; try congruence.
   (* var_stack_scalar *)
   exists (Vptr sp (Int.repr ofs)); split.
-  eapply make_stackaddr_correct. congruence. 
+  eapply make_stackaddr_correct.
+  split. congruence. exact I. 
   (* var_stack_array *)
   exists (Vptr sp (Int.repr ofs)); split.
-  eapply make_stackaddr_correct. congruence.
+  eapply make_stackaddr_correct. split. congruence. exact I. 
   (* var_global_scalar *)
   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.
-  econstructor; eauto. 
+  split. econstructor; eauto. exact I.
   (* var_global_array *)
   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.
-  econstructor; eauto. 
+  split. econstructor; eauto. exact I.
 Qed.
 
 Lemma var_set_correct:
@@ -2172,6 +2541,20 @@ Proof.
   intros. inv H0; inv H; constructor; auto.
 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.
+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.
+Qed.
+
 Lemma transl_expr_correct:
   forall f m tm cenv tf e le te sp lo hi cs
     (MINJ: Mem.inject f m tm)
@@ -2180,44 +2563,58 @@ Lemma transl_expr_correct:
              (Mem.nextblock m) (Mem.nextblock tm)),
   forall a v,
   Csharpminor.eval_expr ge e le m a v ->
-  forall ta
-    (TR: transl_expr cenv a = OK ta),
+  forall ta app
+    (TR: transl_expr cenv a = OK (ta, app)),
   exists tv,
      eval_expr tge (Vptr sp Int.zero) te tm ta tv
-  /\ val_inject f v tv.
+  /\ val_inject f v tv
+  /\ val_match_approx app v.
 Proof.
   induction 3; intros; simpl in TR; try (monadInv TR).
   (* Evar *)
   eapply var_get_correct; eauto.
   (* Etempvar *)
   inv MATCH. inv MENV. exploit me_temps0; eauto. intros [tv [A B]]. 
-  exists tv; split; auto. constructor; auto.
+  exists tv; split. constructor; auto. split. auto. exact I.
   (* Eaddrof *)
   eapply var_addr_correct; eauto.
   (* Econst *)
-  exploit transl_constant_correct; eauto. intros [tv [A B]].
+  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.
   (* Eunop *)
-  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
-  exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]].
-  exists tv; split. econstructor; eauto. auto.
+  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
+  unfold Csharpminor.eval_unop in H0. 
+  destruct (Approx.unop_is_redundant op x0) as []_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.
   (* Ebinop *)
-  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
-  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]].
+  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
+  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 [INJ2 APP2]]].
   exploit eval_binop_compat; eauto. intros [tv [EVAL INJ]].
-  exists tv; split. econstructor; eauto. auto.
+  exists tv; split. econstructor; eauto. split. auto. eapply approx_of_binop_sound; eauto.
   (* Eload *)
-  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit IHeval_expr; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
   exploit Mem.loadv_inject; eauto. intros [tv [LOAD INJ]].
-  exists tv; split. econstructor; eauto. auto.
+  exists tv; split. econstructor; eauto. split. auto.
+  destruct v1; simpl in H0; try discriminate. eapply approx_of_chunk_sound; eauto.
   (* Econdition *)
-  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
+  exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 [INJ1 APP1]]].
   assert (transl_expr cenv (if vb1 then b else c) =
-          OK (if vb1 then x0 else x1)).
+          OK ((if vb1 then x1 else x3), (if vb1 then x2 else x4))).
     destruct vb1; auto.
-  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]].
+  exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 [INJ2 APP2]]].
   exists tv2; split. eapply eval_Econdition; eauto.
-  eapply bool_of_val_inject; eauto. auto.
+  eapply bool_of_val_inject; eauto.
+  split. auto.
+  apply val_match_approx_increasing with (if vb1 then x2 else x4); auto.
+  destruct vb1. apply approx_lub_ge_left. apply approx_lub_ge_right. 
 Qed.
 
 Lemma transl_exprlist_correct:
@@ -2236,7 +2633,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]].
+  exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 [VINJ1 APP1]]].
   exploit IHeval_exprlist; eauto. intros [tv2 [EVAL2 VINJ2]].
   exists (tv1 :: tv2); split. constructor; auto. constructor; auto.
 Qed.
@@ -2669,7 +3066,7 @@ Proof.
 
 (* assign *)
   monadInv TR. 
-  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
   exploit var_set_correct; eauto. 
   intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]].
   left; econstructor; split.
@@ -2678,7 +3075,7 @@ Proof.
 
 (* set *)
   monadInv TR.
-  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
   econstructor; eauto. 
@@ -2687,9 +3084,9 @@ Proof.
 (* store *)
   monadInv TR.
   exploit transl_expr_correct. eauto. eauto. eexact H. eauto. 
-  intros [tv1 [EVAL1 VINJ1]].
+  intros [tv1 [EVAL1 [VINJ1 APP1]]].
   exploit transl_expr_correct. eauto. eauto. eexact H0. eauto. 
-  intros [tv2 [EVAL2 VINJ2]].
+  intros [tv2 [EVAL2 [VINJ2 APP2]]].
   exploit make_store_correct. eexact EVAL1. eexact EVAL2. eauto. eauto. auto. auto.
   intros [tm' [tv' [EXEC [STORE' MINJ']]]].
   left; econstructor; split.
@@ -2703,7 +3100,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]].
+  exploit transl_expr_correct; eauto. intros [tvf [EVAL1 [VINJ1 APP1]]].
   assert (tvf = vf).
     exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
     eapply val_inject_function_pointer; eauto.
@@ -2728,8 +3125,8 @@ Proof.
 
 (* ifthenelse *)
   monadInv TR.
-  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.
+  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.
   apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto.
   econstructor; eauto. destruct b; auto.
 
@@ -2781,7 +3178,7 @@ Proof.
 
 (* switch *)
   monadInv TR. left.
-  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
   inv VINJ.
   exploit switch_descent; eauto. intros [k1 [A B]].
   exploit switch_ascent; eauto. intros [k2 [C D]].
@@ -2805,7 +3202,7 @@ Proof.
 
 (* return some *)
   monadInv TR. left. 
-  exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
+  exploit transl_expr_correct; eauto. intros [tv [EVAL [VINJ APP]]].
   exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
   apply plus_one. eapply step_return_1. eauto. eauto. 
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index db5b7bc..0f7810d 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -441,11 +441,10 @@ Proof.
   exists (Vint n); split; auto.
   exists (Vptr b0 ofs); split; auto. constructor.
   exists (Vptr b0 ofs); split; auto. constructor.
-  rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero) as []_eqn. 
-  exists Vtrue; split. eapply eval_Ebinop; eauto with cshm. simpl. rewrite Heqb; auto.
-  constructor. apply Int.one_not_zero.
-  exists Vfalse; split. eapply eval_Ebinop; eauto with cshm. simpl. rewrite Heqb; auto.
-  constructor.
+  rewrite <- Float.cmp_ne_eq.
+  exists (Val.of_bool (Float.cmp Cne f Float.zero)); split.
+  econstructor; eauto with cshm. 
+  destruct (Float.cmp Cne f Float.zero); simpl; constructor. apply Int.one_not_zero.
 Qed.
 
 Lemma make_neg_correct:
@@ -607,15 +606,18 @@ Proof.
   inversion H8. eauto with cshm.
   (* pp ptr ptr *)
   inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
+  simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. auto.
   inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
+  simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9.
+  destruct cmp; simpl in *; inv H; auto.
   (* pp ptr int *)
   inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold eval_compare_null. rewrite H8. auto.
+  simpl. unfold Val.cmpu. simpl. rewrite H8.
+  destruct cmp; simpl in *; inv H; auto.
   (* pp int ptr *)
   inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold eval_compare_null. rewrite H8. auto.
+  simpl. unfold Val.cmpu. simpl. rewrite H8.
+  destruct cmp; simpl in *; inv H; auto.
   (* ff *)
   inversion H8. eauto with cshm.
   (* if *)