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

1 files changed, 460 insertions, 676 deletions

diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 82bca26..f14b6a9 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -44,8 +44,6 @@ Variable m: mem.
 
 Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.
 
-Ltac TrivialOp cstr := unfold cstr; intros; EvalOp.
-
 Ltac InvEval1 :=
   match goal with
   | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] =>
@@ -78,6 +76,12 @@ Ltac InvEval2 :=
 
 Ltac InvEval := InvEval1; InvEval2; InvEval2.
 
+Ltac TrivialExists :=
+  match goal with
+  | [ |- exists v, _ /\ Val.lessdef ?a v ] => exists a; split; [EvalOp | auto]
+  end.
+
+
 (** * Correctness of the smart constructors *)
 
 (** We now show that the code generated by "smart constructor" functions
@@ -100,66 +104,70 @@ Ltac InvEval := InvEval1; InvEval2; InvEval2.
   by the smart constructor.
 *)
 
+Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=
+  forall le a x,
+  eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v.
+
+Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop :=
+  forall le a x b y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.
+
 Theorem eval_addrsymbol:
-  forall le id ofs b,
-  Genv.find_symbol ge id = Some b ->
-  eval_expr ge sp e m le (addrsymbol id ofs) (Vptr b ofs).
+  forall le id ofs,
+  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v.
 Proof.
-  intros. unfold addrsymbol. econstructor. constructor. 
-  simpl. rewrite H. auto.
+  intros. unfold addrsymbol. econstructor; split. 
+  EvalOp. simpl; eauto. 
+  auto.
 Qed.
 
 Theorem eval_addrstack:
-  forall le ofs b n,
-  sp = Vptr b n ->
-  eval_expr ge sp e m le (addrstack ofs) (Vptr b (Int.add n ofs)).
+  forall le ofs,
+  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v.
 Proof.
-  intros. unfold addrstack. econstructor. constructor. 
-  simpl. unfold offset_sp. rewrite H. auto.
+  intros. unfold addrstack. econstructor; split.
+  EvalOp. simpl; eauto. 
+  auto.
 Qed.
 
-Lemma eval_notbool_base:
-  forall le a v b,
-  eval_expr ge sp e m le a v ->
-  Val.bool_of_val v b ->
-  eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)).
-Proof. 
-  TrivialOp notbool_base. simpl. 
-  inv H0. 
-  rewrite Int.eq_false; auto.
-  rewrite Int.eq_true; auto.
-  reflexivity.
+Theorem eval_notint: unary_constructor_sound notint Val.notint.
+Proof.
+  unfold notint; red; intros. TrivialExists. 
 Qed.
 
-Hint Resolve Val.bool_of_true_val Val.bool_of_false_val
-             Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof.
-
-Theorem eval_notbool:
-  forall le a v b,
-  eval_expr ge sp e m le a v ->
-  Val.bool_of_val v b ->
-  eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)).
+Theorem eval_notbool: unary_constructor_sound notbool Val.notbool.
 Proof.
-  induction a; simpl; intros; try (eapply eval_notbool_base; eauto).
-  destruct o; try (eapply eval_notbool_base; eauto).
-
-  destruct e0. InvEval. 
-  inv H0. rewrite Int.eq_false; auto. 
-  simpl; eauto with evalexpr.
-  rewrite Int.eq_true; simpl; eauto with evalexpr.
-  eapply eval_notbool_base; eauto.
+  assert (DFL: 
+    forall le a x,
+    eval_expr ge sp e m le a x ->
+     exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Ceq Int.zero)) (a ::: Enil)) v
+           /\ Val.lessdef (Val.notbool x) v).
+  intros. TrivialExists. simpl. destruct x; simpl; auto.
 
-  inv H. eapply eval_Eop; eauto.
-  simpl. assert (eval_condition c vl m = Some b).
-  generalize H6. simpl. 
-  case (eval_condition c vl); intros.
-  destruct b0; inv H1; inversion H0; auto; congruence.
-  congruence.
-  rewrite (Op.eval_negate_condition _ _ _ H). 
-  destruct b; reflexivity.
+  red. induction a; simpl; intros; eauto. destruct o; eauto.
+(* intconst *)
+  destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
+(* cmp *)
+  inv H. simpl in H5.
+  destruct (eval_condition c vl m) as []_eqn. 
+  TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto.
+  inv H5. simpl. 
+  destruct (eval_condition (negate_condition c) vl m) as []_eqn.
+  destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto.
+  exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto.
+(* condition *)
+  inv H. destruct v1.
+  exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
+  exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
+Qed.
 
-  inv H. eapply eval_Econdition; eauto. 
-  destruct v1; eauto.
+Lemma shift_symbol_address:
+  forall id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
+Proof.
+  intros. unfold symbol_address. destruct (Genv.find_symbol); auto. 
 Qed.
 
 Lemma eval_offset_addressing:
@@ -168,322 +176,247 @@ Lemma eval_offset_addressing:
   eval_addressing ge sp (offset_addressing addr n) args = Some (Val.add v (Vint n)).
 Proof.
   intros. destruct addr; simpl in *; FuncInv; subst; simpl.
-  rewrite Int.add_assoc. auto.
-  rewrite Int.add_assoc. auto.
-  rewrite <- Int.add_assoc. auto.
-  rewrite <- Int.add_assoc. auto.
-  rewrite <- Int.add_assoc. auto.
-  rewrite <- Int.add_assoc. auto.
-  rewrite <- Int.add_assoc. decEq. decEq. repeat rewrite Int.add_assoc. auto.
-  decEq. decEq. repeat rewrite Int.add_assoc. auto.
-  destruct (Genv.find_symbol ge i); inv H. auto. 
-  destruct (Genv.find_symbol ge i); inv H. simpl. 
-  repeat rewrite Int.add_assoc. decEq. decEq. decEq. apply Int.add_commut.
-  destruct (Genv.find_symbol ge i0); inv H. simpl.
-  repeat rewrite Int.add_assoc. decEq. decEq. decEq. apply Int.add_commut.
-  unfold offset_sp in *. destruct sp; inv H. simpl. rewrite Int.add_assoc. auto.
+  rewrite Val.add_assoc. auto. 
+  repeat rewrite Val.add_assoc. auto.
+  rewrite Val.add_assoc. auto.
+  repeat rewrite Val.add_assoc. auto.
+  rewrite shift_symbol_address. auto. 
+  rewrite shift_symbol_address. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
+  rewrite shift_symbol_address. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
+  rewrite Val.add_assoc. auto.
 Qed.
 
 Theorem eval_addimm:
-  forall le n a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)).
-Proof.
-  unfold addimm; intros until x.
-  generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro.
-  subst n. rewrite Int.add_zero. auto.
-  case (addimm_match a); intros; InvEval.
-  EvalOp. simpl. rewrite Int.add_commut. auto.
-  inv H0. EvalOp. simpl. rewrite (eval_offset_addressing _ _ _ _ H6). auto. 
-  EvalOp. 
-Qed. 
-
-Theorem eval_addimm_ptr:
-  forall le n a b ofs,
-  eval_expr ge sp e m le a (Vptr b ofs) ->
-  eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)).
-Proof.
-  unfold addimm; intros until ofs.
-  generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro.
-  subst n. rewrite Int.add_zero. auto.
-  case (addimm_match a); intros; InvEval.
-  inv H0. EvalOp. simpl. rewrite (eval_offset_addressing _ _ _ _ H6). auto. 
-  EvalOp. 
-Qed.
-
-Theorem eval_add:
-  forall le a b x y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (add a b) (Vint (Int.add x y)).
-Proof.
-  intros until y.
+  forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
+Proof.
+  red; unfold addimm; intros until x.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  subst n. intros. exists x; split; auto. 
+  destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
+  case (addimm_match a); intros; InvEval; simpl.
+  TrivialExists; simpl. rewrite Int.add_commut. auto.
+  inv H0. simpl in H6. TrivialExists. simpl. eapply eval_offset_addressing; eauto.
+  TrivialExists. 
+Qed.
+
+Theorem eval_add: binary_constructor_sound add Val.add.
+Proof.
+  red; intros until y.
   unfold add; case (add_match a b); intros; InvEval.
-  rewrite Int.add_commut. apply eval_addimm. auto.
-  apply eval_addimm. auto.
-  subst. EvalOp. simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut.
-  subst. EvalOp. simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut.
-  subst. EvalOp. simpl. decEq. decEq.
-    rewrite Int.add_permut. rewrite Int.add_assoc. decEq. apply Int.add_permut.
-  destruct (Genv.find_symbol ge id); inv H0.
-  destruct (Genv.find_symbol ge id); inv H0.
-  destruct (Genv.find_symbol ge id); inv H0.
-  destruct (Genv.find_symbol ge id); inv H0.
-  subst. EvalOp. simpl. rewrite Int.add_commut. auto.
-  subst. EvalOp. 
-  subst. EvalOp. simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  subst. EvalOp. simpl. decEq. decEq. apply Int.add_assoc.
-  EvalOp. simpl.  rewrite Int.add_zero. auto.
-Qed.
-
-Theorem eval_add_ptr:
-  forall le a b p x y,
-  eval_expr ge sp e m le a (Vptr p x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)).
-Proof.
-  intros until y. unfold add; case (add_match a b); intros; InvEval.
-  apply eval_addimm_ptr; auto.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut.
-  destruct (Genv.find_symbol ge id); inv H0.
-  subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. 
-  decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. 
-  decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  subst. EvalOp.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. auto.
-  EvalOp; simpl. rewrite Int.add_zero. auto.
-Qed.
-
-Theorem eval_add_ptr_2:
-  forall le a b x p y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vptr p y) ->
-  eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)).
-Proof.
-  intros until y. unfold add; case (add_match a b); intros; InvEval.
-  apply eval_addimm_ptr; auto.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq.
-    rewrite (Int.add_commut n1 n2). apply Int.add_permut.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. 
-    rewrite (Int.add_commut n1 n2). apply Int.add_permut.
-  subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. 
-  decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  destruct (Genv.find_symbol ge id); inv H0. 
-  subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. 
-  decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  subst. EvalOp. 
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. auto.
-  subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  EvalOp; simpl. rewrite Int.add_zero. auto.
-Qed.
-
-Theorem eval_sub:
-  forall le a b x y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)).
-Proof.
-  intros until y.
-  unfold sub; case (sub_match a b); intros; InvEval.
-  rewrite Int.sub_add_opp. 
-    apply eval_addimm. assumption.
-  replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)).
-    apply eval_addimm. EvalOp.
-    subst x; subst y.
-    repeat rewrite Int.sub_add_opp.
-    repeat rewrite Int.add_assoc. decEq. 
-    rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr.
-  replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
-    apply eval_addimm. EvalOp.
-    subst x. rewrite Int.sub_add_l. auto.
-  replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
-    apply eval_addimm. EvalOp.
-    subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. 
-  EvalOp.
-Qed.
-
-Theorem eval_sub_ptr_int:
-  forall le a b p x y,
-  eval_expr ge sp e m le a (Vptr p x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)).
-Proof.
-  intros until y.
+  rewrite Val.add_commut. apply eval_addimm; auto.
+  apply eval_addimm; auto.
+  subst. TrivialExists. simpl. rewrite Val.add_permut_4. auto.
+  subst. TrivialExists. simpl. rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto.
+  subst. TrivialExists. simpl. rewrite Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto.
+  subst. TrivialExists. simpl. rewrite shift_symbol_address. 
+    rewrite Val.add_commut. rewrite Val.add_assoc. decEq. decEq. apply Val.add_commut.
+  subst. TrivialExists. simpl. rewrite shift_symbol_address. rewrite Val.add_assoc.
+    decEq; decEq. apply Val.add_commut.
+  subst. TrivialExists. simpl. rewrite shift_symbol_address. rewrite Val.add_commut. 
+    rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
+  subst. TrivialExists. simpl. rewrite shift_symbol_address.
+    rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
+  subst. TrivialExists. simpl. rewrite Val.add_permut. rewrite Val.add_assoc.
+    decEq; decEq. apply Val.add_commut.
+  subst. TrivialExists.
+  subst. TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
+  subst. TrivialExists. simpl. rewrite Val.add_assoc; auto.
+  TrivialExists. simpl. destruct x; destruct y; simpl; auto; rewrite Int.add_zero; auto.
+Qed.
+
+Theorem eval_sub: binary_constructor_sound sub Val.sub.
+Proof.
+  red; intros until y.
   unfold sub; case (sub_match a b); intros; InvEval.
-  rewrite Int.sub_add_opp. 
-    apply eval_addimm_ptr. assumption.
-  subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)).
-    apply eval_addimm_ptr. EvalOp.
-    subst x; subst y.
-    repeat rewrite Int.sub_add_opp.
-    repeat rewrite Int.add_assoc. decEq. 
-    rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr.
-  subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
-    apply eval_addimm_ptr. EvalOp.
-    subst x. rewrite Int.sub_add_l. auto.
-  replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
-    apply eval_addimm_ptr. EvalOp.
-    subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. 
-  EvalOp.
-Qed.
-
-Theorem eval_sub_ptr_ptr:
-  forall le a b p x y,
-  eval_expr ge sp e m le a (Vptr p x) ->
-  eval_expr ge sp e m le b (Vptr p y) ->
-  eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)).
-Proof.
-  intros until y.
-  unfold sub; case (sub_match a b); intros; InvEval.
-  replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)).
-    apply eval_addimm. EvalOp. 
-    simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto.
-    subst x; subst y.
-    repeat rewrite Int.sub_add_opp.
-    repeat rewrite Int.add_assoc. decEq. 
-    rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr.
-  subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1).
-    apply eval_addimm. EvalOp.
-    simpl. unfold eq_block. rewrite zeq_true. auto.
-    subst x. rewrite Int.sub_add_l. auto.
-  subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)).
-    apply eval_addimm. EvalOp.
-    simpl. unfold eq_block. rewrite zeq_true. auto.
-    subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. 
-  EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto.
+  rewrite Val.sub_add_opp. apply eval_addimm; auto.
+  subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. 
+    rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
+    apply eval_addimm; EvalOp.
+  subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
+  subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
+  TrivialExists.
+Qed.
+
+Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
+Proof.
+  red; intros. unfold negint. TrivialExists.
 Qed.
 
 Theorem eval_shlimm:
-  forall le a n x,
-  eval_expr ge sp e m le a (Vint x) ->
-  Int.ltu n Int.iwordsize = true ->
-  eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)).
-Proof.
-  intros until x; unfold shlimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero).
-  intros. subst n. rewrite Int.shl_zero. auto.
-  case (shlimm_match a); intros. 
-  InvEval. EvalOp. 
-  case_eq (Int.ltu (Int.add n n1) Int.iwordsize); intros.
-  InvEval. revert H8. case_eq (Int.ltu n1 Int.iwordsize); intros; inv H8.
-  EvalOp. simpl. rewrite H2. rewrite Int.shl_shl; auto; rewrite Int.add_commut; auto.
-  EvalOp. simpl. rewrite H1; auto.
-  InvEval. subst. 
-  destruct (shift_is_scale n). 
-  EvalOp. simpl. decEq. decEq.
-  rewrite (Int.shl_mul (Int.add i n1)); auto. rewrite (Int.shl_mul n1); auto.
-  rewrite Int.mul_add_distr_l. auto.
-  EvalOp. constructor. EvalOp. simpl. eauto. constructor. simpl. rewrite H1. auto.
+  forall n, unary_constructor_sound (fun a => shlimm a n)
+                                    (fun x => Val.shl x (Vint n)).
+Proof.
+  red; intros until x.  unfold shlimm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
+  destruct (shlimm_match a); intros; InvEval.
+  exists (Vint (Int.shl n1 n)); split. EvalOp. 
+  simpl. destruct (Int.ltu n Int.iwordsize); auto.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
+  subst. destruct v1; simpl; auto. 
+  rewrite Heqb.
+  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
+  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto.
+  rewrite Int.add_commut. rewrite Int.shl_shl; auto. rewrite Int.add_commut; auto.
+  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
+  simpl. auto.
+  subst. destruct (shift_is_scale n).
+  econstructor; split. EvalOp. simpl. eauto.
+  destruct v1; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. 
+  rewrite Int.shl_mul. rewrite Int.mul_add_distr_l. rewrite (Int.shl_mul n1). auto.
+  TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. auto. 
   destruct (shift_is_scale n).
-  EvalOp. simpl. decEq. decEq.
-  rewrite Int.add_zero. symmetry. apply Int.shl_mul. 
-  EvalOp. simpl. rewrite H1; auto.
+  econstructor; split. EvalOp. simpl. eauto. 
+  destruct x; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. 
+  rewrite Int.add_zero. rewrite Int.shl_mul. auto. 
+  TrivialExists.
 Qed.
 
 Theorem eval_shruimm:
-  forall le a n x,
-  eval_expr ge sp e m le a (Vint x) ->
-  Int.ltu n Int.iwordsize = true ->
-  eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)).
-Proof.
-  intros until x; unfold shruimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero).
-  intros. subst n. rewrite Int.shru_zero. auto.
-  case (shruimm_match a); intros. 
-  InvEval. EvalOp. 
-  case_eq (Int.ltu (Int.add n n1) Int.iwordsize); intros.
-  InvEval. revert H8. case_eq (Int.ltu n1 Int.iwordsize); intros; inv H8.
-  EvalOp. simpl. rewrite H2. rewrite Int.shru_shru; auto; rewrite Int.add_commut; auto.
-  EvalOp. simpl. rewrite H1; auto. 
-  EvalOp. simpl. rewrite H1; auto.
+  forall n, unary_constructor_sound (fun a => shruimm a n)
+                                    (fun x => Val.shru x (Vint n)).
+Proof.
+  red; intros until x.  unfold shruimm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
+  destruct (shruimm_match a); intros; InvEval.
+  exists (Vint (Int.shru n1 n)); split. EvalOp. 
+  simpl. destruct (Int.ltu n Int.iwordsize); auto.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
+  subst. destruct v1; simpl; auto. 
+  rewrite Heqb.
+  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
+  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto.
+  rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
+  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
+  simpl. auto.
+  TrivialExists.
 Qed.
 
 Theorem eval_shrimm:
-  forall le a n x,
-  eval_expr ge sp e m le a (Vint x) ->
-  Int.ltu n Int.iwordsize = true ->
-  eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)).
-Proof.
-  intros until x; unfold shrimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero).
-  intros. subst n. rewrite Int.shr_zero. auto.
-  case (shrimm_match a); intros. 
-  InvEval. EvalOp. 
-  case_eq (Int.ltu (Int.add n n1) Int.iwordsize); intros.
-  InvEval. revert H8. case_eq (Int.ltu n1 Int.iwordsize); intros; inv H8.
-  EvalOp. simpl. rewrite H2. rewrite Int.shr_shr; auto; rewrite Int.add_commut; auto.
-  EvalOp. simpl. rewrite H1; auto. 
-  EvalOp. simpl. rewrite H1; auto.
+  forall n, unary_constructor_sound (fun a => shrimm a n)
+                                    (fun x => Val.shr x (Vint n)).
+Proof.
+  red; intros until x.  unfold shrimm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
+  destruct (shrimm_match a); intros; InvEval.
+  exists (Vint (Int.shr n1 n)); split. EvalOp. 
+  simpl. destruct (Int.ltu n Int.iwordsize); auto.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
+  subst. destruct v1; simpl; auto. 
+  rewrite Heqb.
+  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
+  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto.
+  rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto.
+  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
+  simpl. auto.
+  TrivialExists.
 Qed.
 
 Lemma eval_mulimm_base:
-  forall le a n x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)).
+  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
 Proof.
-  intros; unfold mulimm_base.
+  intros; red; intros; unfold mulimm_base. 
   generalize (Int.one_bits_decomp n). 
   generalize (Int.one_bits_range n).
   destruct (Int.one_bits n).
-  intros. EvalOp. 
+  intros. TrivialExists. 
   destruct l.
   intros. rewrite H1. simpl. 
-  rewrite Int.add_zero. rewrite <- Int.shl_mul.
-  apply eval_shlimm. auto. auto with coqlib. 
+  rewrite Int.add_zero.
+  replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul.
+  apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib.
   destruct l.
-  intros. apply eval_Elet with (Vint x). auto.
-  rewrite H1. simpl. rewrite Int.add_zero. 
-  rewrite Int.mul_add_distr_r.
-  apply eval_add. 
-  rewrite <- Int.shl_mul. apply eval_shlimm. constructor. auto. auto with coqlib.
-  rewrite <- Int.shl_mul. apply eval_shlimm. constructor. auto. auto with coqlib.
-  intros. EvalOp. 
+  intros. rewrite H1. simpl.
+  exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
+  exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
+  exploit eval_add. eexact A1. eexact A2. intros [v3 [A3 B3]].
+  exists v3; split. econstructor; eauto. 
+  rewrite Int.add_zero.
+  replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one i0)))
+     with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint i0))).
+  rewrite Val.mul_add_distr_r.
+  repeat rewrite Val.shl_mul. 
+  apply Val.lessdef_trans with (Val.add v1 v2); auto. apply Val.add_lessdef; auto. 
+  simpl. repeat rewrite H0; auto with coqlib. 
+  intros. TrivialExists. 
 Qed.
 
 Theorem eval_mulimm:
-  forall le a n x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)).
-Proof.
-  intros until x; unfold mulimm.
-  generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
-  subst n. rewrite Int.mul_zero. intros. EvalOp. 
-  generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro.
-  subst n. rewrite Int.mul_one. auto.
+  forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)).
+Proof.
+  intros; red; intros until x; unfold mulimm.
+  predSpec Int.eq Int.eq_spec n Int.zero. 
+  intros. exists (Vint Int.zero); split. EvalOp. 
+  destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto.
+  predSpec Int.eq Int.eq_spec n Int.one.
+  intros. exists x; split; auto.
+  destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto.
   case (mulimm_match a); intros; InvEval.
-  EvalOp. rewrite Int.mul_commut. reflexivity.
-  subst. rewrite Int.mul_add_distr_l. 
-  rewrite (Int.mul_commut n n2). apply eval_addimm. apply eval_mulimm_base. auto.
-  apply eval_mulimm_base. assumption.
+  TrivialExists. simpl. rewrite Int.mul_commut; auto.
+  subst. rewrite Val.mul_add_distr_l. 
+  exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]].
+  exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]].
+  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. 
+  rewrite Val.mul_commut; auto.
+  apply eval_mulimm_base; auto.
 Qed.
 
-Theorem eval_mul:
-  forall le a b x y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)).
+Theorem eval_mul: binary_constructor_sound mul Val.mul.
 Proof.
-  intros until y.
+  red; intros until y.
   unfold mul; case (mul_match a b); intros; InvEval.
-  rewrite Int.mul_commut. apply eval_mulimm. auto. 
+  rewrite Val.mul_commut. apply eval_mulimm. auto. 
   apply eval_mulimm. auto.
-  EvalOp.
+  TrivialExists.
 Qed.
 
-Lemma eval_orimm:
-  forall le n a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (orimm n a) (Vint (Int.or x n)).
+Theorem eval_andimm:
+  forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
 Proof.
-  intros. unfold orimm. 
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. rewrite Int.or_zero. auto.
+  intros; red; intros until x. unfold andimm.
+  predSpec Int.eq Int.eq_spec n Int.zero. 
+  intros. exists (Vint Int.zero); split. EvalOp. 
+  destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto.
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  intros. exists x; split; auto.
+  destruct x; simpl; auto. subst n. rewrite Int.and_mone. auto.
+  case (andimm_match a); intros; InvEval.
+  TrivialExists. simpl. rewrite Int.and_commut; auto.
+  subst. TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto.
+  subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. 
+  rewrite Int.and_commut. auto. compute; auto.
+  subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. 
+  rewrite Int.and_commut. auto. compute; auto.
+  TrivialExists.
+Qed.
+
+Theorem eval_and: binary_constructor_sound and Val.and.
+Proof.
+  red; intros until y; unfold and; case (and_match a b); intros; InvEval.
+  rewrite Val.and_commut. apply eval_andimm; auto.
+  apply eval_andimm; auto.
+  TrivialExists.
+Qed.
+
+Theorem eval_orimm:
+  forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)).
+Proof.
+  intros; red; intros until x. unfold orimm.
+  predSpec Int.eq Int.eq_spec n Int.zero. 
+  intros. exists x; split. auto.  
+  destruct x; simpl; auto. subst n. rewrite Int.or_zero. auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
-  subst n. rewrite Int.or_mone. EvalOp.
-  EvalOp.
+  intros. exists (Vint Int.mone); split. EvalOp.
+  destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto.
+  destruct (orimm_match a); intros; InvEval.
+  TrivialExists. simpl. rewrite Int.or_commut; auto.
+  subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. 
+  TrivialExists.
 Qed.
 
 Remark eval_same_expr:
@@ -501,432 +434,283 @@ Proof.
   discriminate.
 Qed.
 
-Theorem eval_or:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).
-Proof.
-  intros until y; unfold or; case (or_match a b); intros; InvEval.
-
-  rewrite Int.or_commut. apply eval_orimm; auto.
-  apply eval_orimm; auto.
-
-  revert H7; case_eq (Int.ltu n1 Int.iwordsize); intros; inv H7.
-  revert H6; case_eq (Int.ltu n2 Int.iwordsize); intros; inv H6.
-  caseEq (Int.eq (Int.add n1 n2) Int.iwordsize
-          && same_expr_pure t1 t2); intro.
-  destruct (andb_prop _ _ H1).
-  generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H4; intros.
-  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2.
-  EvalOp. simpl. rewrite H0. rewrite <- Int.or_ror; auto.
-  EvalOp. econstructor. EvalOp. simpl. rewrite H; eauto.
-  econstructor. EvalOp. simpl. rewrite H0; eauto. constructor.
-  simpl. auto.
-
-  revert H7; case_eq (Int.ltu n2 Int.iwordsize); intros; inv H7.
-  revert H6; case_eq (Int.ltu n1 Int.iwordsize); intros; inv H6.
-  caseEq (Int.eq (Int.add n1 n2) Int.iwordsize
-          && same_expr_pure t1 t2); intro.
-  destruct (andb_prop _ _ H1).
-  generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H4; intros.
-  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2.
-  EvalOp. simpl. rewrite H. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
-  EvalOp. econstructor. EvalOp. simpl. rewrite H; eauto.
-  econstructor. EvalOp. simpl. rewrite H0; eauto. constructor.
-  simpl. auto.
+Lemma eval_or: binary_constructor_sound or Val.or.
+Proof.
+  red; intros until y; unfold or; case (or_match a b); intros.
+(* intconst *)
+  InvEval. rewrite Val.or_commut. apply eval_orimm; auto. 
+  InvEval. apply eval_orimm; auto.
+(* shlimm - shruimm *)
+  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn.
+  destruct (andb_prop _ _ Heqb0). 
+  generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ.
+  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
+  exists (Val.ror v0 (Vint n2)); split. EvalOp.
+  destruct v0; simpl; auto. 
+  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto.
+  destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto.
+  simpl. rewrite <- Int.or_ror; auto.
+  TrivialExists. 
+(* shruimm - shlimm *) 
+  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn.
+  destruct (andb_prop _ _ Heqb0). 
+  generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ.
+  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
+  exists (Val.ror v1 (Vint n2)); split. EvalOp.
+  destruct v1; simpl; auto. 
+  destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto.
+  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto.
+  simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
+  TrivialExists. 
+(* default *)
+  TrivialExists.
+Qed.
+
+Theorem eval_xorimm:
+  forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Vint n)).
+Proof.
+  intros; red; intros until x. unfold xorimm.
+  predSpec Int.eq Int.eq_spec n Int.zero. 
+  intros. exists x; split. auto.  
+  destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto.
+  destruct (xorimm_match a); intros; InvEval.
+  TrivialExists. simpl. rewrite Int.xor_commut; auto.
+  subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. 
+  TrivialExists.
+Qed.
+
+Theorem eval_xor: binary_constructor_sound xor Val.xor.
+Proof.
+  red; intros until y; unfold xor; case (xor_match a b); intros; InvEval.
+  rewrite Val.xor_commut. apply eval_xorimm; auto.
+  apply eval_xorimm; auto.
+  TrivialExists.
+Qed.
 
-  EvalOp.
+Theorem eval_divs:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.divs x y = Some z ->
+  exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+Proof.
+  intros. unfold divs. exists z; split. EvalOp. auto.
 Qed.
 
-Lemma eval_andimm:
-  forall le n a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).
+Theorem eval_divu:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.divu x y = Some z ->
+  exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold andimm. 
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. rewrite Int.and_zero. EvalOp.
-  predSpec Int.eq Int.eq_spec n Int.mone.
-  subst n. rewrite Int.and_mone. auto.
-  EvalOp.
+  intros. unfold divu. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_and:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (and a b) (Vint (Int.and x y)).
+Theorem eval_mods:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.mods x y = Some z ->
+  exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
 Proof.
-  intros until y; unfold and. case (mul_match a b); intros.
-  InvEval. rewrite Int.and_commut. apply eval_andimm; auto.
-  InvEval. apply eval_andimm; auto.
-  EvalOp.
+  intros. unfold mods. exists z; split. EvalOp. auto.
 Qed.
 
-Lemma eval_xorimm:
-  forall le n a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (xorimm n a) (Vint (Int.xor x n)).
+Theorem eval_modu:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.modu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold xorimm. 
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. rewrite Int.xor_zero. auto.
-  EvalOp.
+  intros. unfold modu. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_xor:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)).
+Theorem eval_shl: binary_constructor_sound shl Val.shl.
 Proof.
-  intros until y; unfold xor. case (mul_match a b); intros.
-  InvEval. rewrite Int.xor_commut. apply eval_xorimm; auto.
-  InvEval. apply eval_xorimm; auto.
-  EvalOp.
+  red; intros until y; unfold shl; case (shl_match b); intros.
+  InvEval. apply eval_shlimm; auto.
+  TrivialExists. 
 Qed.
 
-Theorem eval_divu:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  y <> Int.zero ->
-  eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)).
+Theorem eval_shr: binary_constructor_sound shr Val.shr.
 Proof.
-  intros; unfold divu; EvalOp.
-  simpl. rewrite Int.eq_false; auto. 
+  red; intros until y; unfold shr; case (shr_match b); intros.
+  InvEval. apply eval_shrimm; auto.
+  TrivialExists. 
 Qed.
 
-Theorem eval_modu:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  y <> Int.zero ->
-  eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)).
+Theorem eval_shru: binary_constructor_sound shru Val.shru.
 Proof.
-  intros; unfold modu; EvalOp.
-  simpl. rewrite Int.eq_false; auto. 
+  red; intros until y; unfold shru; case (shru_match b); intros.
+  InvEval. apply eval_shruimm; auto.
+  TrivialExists. 
 Qed.
 
-Theorem eval_divs:
-  forall le a b x y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  y <> Int.zero ->
-  eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)).
+Theorem eval_negf: unary_constructor_sound negf Val.negf.
 Proof.
-  TrivialOp divs. simpl. 
-  predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto.
+  red; intros. TrivialExists. 
 Qed.
 
-Theorem eval_mods:
-  forall le a b x y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  y <> Int.zero ->
-  eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)).
+Theorem eval_absf: unary_constructor_sound absf Val.absf.
 Proof.
-  TrivialOp mods. simpl. 
-  predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto.
+  red; intros. TrivialExists. 
 Qed.
 
-Theorem eval_shl:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  Int.ltu y Int.iwordsize = true ->
-  eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)).
+Theorem eval_addf: binary_constructor_sound addf Val.addf.
 Proof.
-  intros until y; unfold shl; case (shift_match b); intros.
-  InvEval. apply eval_shlimm; auto.
-  EvalOp. simpl. rewrite H1. auto.
+  red; intros; TrivialExists.
+Qed.
+ 
+Theorem eval_subf: binary_constructor_sound subf Val.subf.
+Proof.
+  red; intros; TrivialExists.
 Qed.
 
-Theorem eval_shru:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  Int.ltu y Int.iwordsize = true ->
-  eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)).
+Theorem eval_mulf: binary_constructor_sound mulf Val.mulf.
 Proof.
-  intros until y; unfold shru; case (shift_match b); intros.
-  InvEval. apply eval_shruimm; auto.
-  EvalOp. simpl. rewrite H1. auto.
+  red; intros; TrivialExists.
 Qed.
 
-Theorem eval_shr:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  Int.ltu y Int.iwordsize = true ->
-  eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)).
+Theorem eval_divf: binary_constructor_sound divf Val.divf.
 Proof.
-  intros until y; unfold shr; case (shift_match b); intros.
-  InvEval. apply eval_shrimm; auto.
-  EvalOp. simpl. rewrite H1. auto.
+  red; intros; TrivialExists.
 Qed.
 
 Theorem eval_comp:
-  forall le c a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x y)).
-Proof.
-  intros until y.
-  unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
-Qed.
-
-Theorem eval_compu_int:
-  forall le c a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
-Proof.
-  intros until y.
-  unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
-Qed.
-
-Remark eval_compare_null_transf:
-  forall c x v,
-  Cminor.eval_compare_null c x = Some v ->
-  match eval_compare_null c x with
-  | Some true => Some Vtrue
-  | Some false => Some Vfalse
-  | None => None (A:=val)
-  end = Some v.
-Proof.
-  unfold Cminor.eval_compare_null, eval_compare_null; intros.
-  destruct (Int.eq x Int.zero); try discriminate. 
-  destruct c; try discriminate; auto.
-Qed.
-
-Theorem eval_compu_ptr_int:
-  forall le c a x1 x2 b y v,
-  eval_expr ge sp e m le a (Vptr x1 x2) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  Cminor.eval_compare_null c y = Some v ->
-  eval_expr ge sp e m le (compu c a b) v.
-Proof.
-  intros until v.
-  unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. apply eval_compare_null_transf; auto.
-  EvalOp. simpl. apply eval_compare_null_transf; auto.
-Qed.
-
-Remark eval_compare_null_swap:
-  forall c x,
-  Cminor.eval_compare_null (swap_comparison c) x = 
-  Cminor.eval_compare_null c x.
-Proof.
-  intros. unfold Cminor.eval_compare_null. 
-  destruct (Int.eq x Int.zero). destruct c; auto. auto.
-Qed.
-
-Theorem eval_compu_int_ptr:
-  forall le c a x b y1 y2 v,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vptr y1 y2) ->
-  Cminor.eval_compare_null c x = Some v ->
-  eval_expr ge sp e m le (compu c a b) v.
-Proof.
-  intros until v.
-  unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. apply eval_compare_null_transf. 
-  rewrite eval_compare_null_swap; auto.
-  EvalOp. simpl. apply eval_compare_null_transf. auto.
-Qed.
-
-Theorem eval_compu_ptr_ptr:
-  forall le c a x1 x2 b y1 y2,
-  eval_expr ge sp e m le a (Vptr x1 x2) ->
-  eval_expr ge sp e m le b (Vptr y1 y2) ->
-  Mem.valid_pointer m x1 (Int.unsigned x2)
-  && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
-  x1 = y1 ->
-  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)).
-Proof.
-  intros until y2.
-  unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. 
-  destruct (Int.cmpu c x2 y2); reflexivity.
-Qed.
-
-Theorem eval_compu_ptr_ptr_2:
-  forall le c a x1 x2 b y1 y2 v,
-  eval_expr ge sp e m le a (Vptr x1 x2) ->
-  eval_expr ge sp e m le b (Vptr y1 y2) ->
-  Mem.valid_pointer m x1 (Int.unsigned x2)
-  && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
-  x1 <> y1 ->
-  Cminor.eval_compare_mismatch c = Some v ->
-  eval_expr ge sp e m le (compu c a b) v.
-Proof.
-  intros until y2.
-  unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto.
-  destruct c; simpl in H3; inv H3; auto.
+  forall c, binary_constructor_sound (comp c) (Val.cmp c).
+Proof.
+  intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval.
+  TrivialExists. simpl. rewrite Val.swap_cmp_bool. auto.
+  TrivialExists.
+  TrivialExists.
 Qed.
 
-Theorem eval_compf:
-  forall le c a x b y,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le b (Vfloat y) ->
-  eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)).
+Theorem eval_compu:
+  forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
 Proof.
-  intros. unfold compf. EvalOp. simpl. 
-  destruct (Float.cmp c x y); reflexivity.
+  intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
+  TrivialExists. simpl. rewrite Val.swap_cmpu_bool. auto.
+  TrivialExists.
+  TrivialExists.
 Qed.
 
-Theorem eval_cast8signed:
-  forall le a v,
-  eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v).
-Proof. intros; unfold cast8signed; EvalOp. Qed.
-
-Theorem eval_cast8unsigned:
-  forall le a v,
-  eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v).
-Proof. intros; unfold cast8unsigned; EvalOp. Qed.
-
-Theorem eval_cast16signed:
-  forall le a v,
-  eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v).
-Proof. intros; unfold cast16signed; EvalOp. Qed.
+Theorem eval_compf:
+  forall c, binary_constructor_sound (compf c) (Val.cmpf c).
+Proof.
+  intros; red; intros. unfold compf. TrivialExists.
+Qed.
 
-Theorem eval_cast16unsigned:
-  forall le a v,
-  eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v).
-Proof. intros; unfold cast16unsigned; EvalOp. Qed.
 
-Theorem eval_singleoffloat:
-  forall le a v,
-  eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v).
-Proof. intros; unfold singleoffloat; EvalOp. Qed.
+Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
+Proof.
+  red; intros. unfold cast8signed. TrivialExists.
+Qed.
 
-Theorem eval_notint:
-  forall le a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (notint a) (Vint (Int.xor x Int.mone)).
-Proof. intros; unfold notint; EvalOp. Qed.
+Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
+Proof.
+  red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval.
+  subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. 
+  rewrite Int.and_commut. TrivialExists. compute; auto.
+  TrivialExists.
+Qed.
 
-Theorem eval_negint:
-  forall le a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (negint a) (Vint (Int.neg x)).
-Proof. intros; unfold negint; EvalOp. Qed.
+Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
+Proof.
+  red; intros. unfold cast16signed. TrivialExists.
+Qed.
 
-Theorem eval_negf:
-  forall le a x,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)).
-Proof. intros; unfold negf; EvalOp. Qed.
+Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
+Proof.
+  red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
+  subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. 
+  rewrite Int.and_commut. TrivialExists. compute; auto.
+  TrivialExists.
+Qed.
 
-Theorem eval_absf:
-  forall le a x,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)).
-Proof. intros; unfold absf; EvalOp. Qed.
+Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
+Proof.
+  red; intros. unfold singleoffloat. TrivialExists.
+Qed.
 
 Theorem eval_intoffloat:
-  forall le a x n,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  Float.intoffloat x = Some n ->
-  eval_expr ge sp e m le (intoffloat a) (Vint n).
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.intoffloat x = Some y ->
+  exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intoffloat; EvalOp.
-  simpl. rewrite H0. auto.
+  intros; unfold intoffloat. TrivialExists. 
 Qed.
 
 Theorem eval_floatofint:
-  forall le a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)).
-Proof. intros; unfold floatofint; EvalOp. Qed.
-
-Theorem eval_addf:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le b (Vfloat y) ->
-  eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)).
-Proof. intros; unfold addf; EvalOp. Qed.
-
-Theorem eval_subf:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le b (Vfloat y) ->
-  eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)).
-Proof. intros; unfold subf; EvalOp. Qed.
-
-Theorem eval_mulf:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le b (Vfloat y) ->
-  eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)).
-Proof. intros; unfold mulf; EvalOp. Qed.
-
-Theorem eval_divf:
-  forall le a x b y,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  eval_expr ge sp e m le b (Vfloat y) ->
-  eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)).
-Proof. intros; unfold divf; EvalOp. Qed.
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.floatofint x = Some y ->
+  exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold floatofint. TrivialExists. 
+Qed.
 
 Theorem eval_intuoffloat:
-  forall le a x n,
-  eval_expr ge sp e m le a (Vfloat x) ->
-  Float.intuoffloat x = Some n ->
-  eval_expr ge sp e m le (intuoffloat a) (Vint n).
-Proof.
-  intros. unfold intuoffloat. 
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.intuoffloat x = Some y ->
+  exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
+Proof.
+  intros. destruct x; simpl in H0; try discriminate. 
+  destruct (Float.intuoffloat f) as [n|]_eqn; simpl in H0; inv H0.
+  exists (Vint n); split; auto.
+  unfold intuoffloat. 
   econstructor. eauto. 
   set (im := Int.repr Int.half_modulus).
   set (fm := Float.floatofintu im).
-  assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)).
+  assert (eval_expr ge sp e m (Vfloat f :: le) (Eletvar O) (Vfloat f)).
     constructor. auto. 
-  apply eval_Econdition with (v1 := Float.cmp Clt x fm).
+  apply eval_Econdition with (v1 := Float.cmp Clt f fm).
   econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
-  caseEq (Float.cmp Clt x fm); intros.
+  destruct (Float.cmp Clt f fm) as []_eqn.
   exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
   exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
   replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
-  apply eval_addimm. eapply eval_intoffloat; eauto.
-  apply eval_subf; auto. EvalOp.
+  exploit (eval_addimm Float.ox8000_0000 (Vfloat f :: le)
+     (intoffloat
+        (subf (Eletvar 0)
+           (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)))).
+  unfold intoffloat, subf. 
+  EvalOp. constructor. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
+  simpl. eauto. constructor. simpl. rewrite EQ. simpl; eauto. 
+  intros [v [A B]]. simpl in B. inv B. auto.
   rewrite Int.sub_add_opp. rewrite Int.add_assoc. apply Int.add_zero. 
 Qed.
 
 Theorem eval_floatofintu:
-  forall le a x,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)).
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.floatofintu x = Some y ->
+  exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
 Proof.
-  intros. unfold floatofintu. 
+  intros. destruct x; simpl in H0; try discriminate. inv H0.
+  exists (Vfloat (Float.floatofintu i)); split; auto.
   econstructor. eauto. 
   set (fm := Float.floatofintu Float.ox8000_0000).
-  assert (eval_expr ge sp e m (Vint x :: le) (Eletvar O) (Vint x)).
+  assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)).
     constructor. auto. 
-  apply eval_Econdition with (v1 := Int.ltu x Float.ox8000_0000).
+  apply eval_Econdition with (v1 := Int.ltu i Float.ox8000_0000).
   econstructor. constructor. eauto. constructor.
   simpl. auto.
-  caseEq (Int.ltu x Float.ox8000_0000); intros.
+  destruct (Int.ltu i Float.ox8000_0000) as []_eqn.
   rewrite Float.floatofintu_floatofint_1; auto.
-  apply eval_floatofint; auto.
-  rewrite Float.floatofintu_floatofint_2; auto.
-  fold fm. apply eval_addf. apply eval_floatofint. 
-  rewrite Int.sub_add_opp. apply eval_addimm; auto.
-  EvalOp.
+  unfold floatofint. EvalOp. 
+  exploit (eval_addimm (Int.neg Float.ox8000_0000) (Vint i :: le) (Eletvar 0)); eauto.
+  simpl. intros [v [A B]]. inv B. 
+  unfold addf. EvalOp. 
+  constructor. unfold floatofint. EvalOp. simpl; eauto. 
+  constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. 
+  fold fm. rewrite Float.floatofintu_floatofint_2; auto.
+  rewrite Int.sub_add_opp. auto.
 Qed.
 
 Theorem eval_addressing: