Merge branch 'kvx-work' into mppa-RTLpathSE

Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand
framework

1 files changed, 1734 insertions, 0 deletions

diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
new file mode 100644
index 00000000..c23ed601
--- /dev/null
+++ b/kvx/SelectOpproof.v
@@ -0,0 +1,1734 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** Correctness of instruction selection for operators *)
+
+Require Import Builtins.
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import ExtValues.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Cminor.
+Require Import Op.
+Require Import CminorSel.
+Require Import Builtins1.
+Require Import SelectOp.
+Require Import Events.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
+Require Import DecBoolOps.
+
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
+
+(** * Useful lemmas and tactics *)
+
+(** The following are trivial lemmas and custom tactics that help
+  perform backward (inversion) and forward reasoning over the evaluation
+  of operator applications. *)
+
+Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.
+
+Ltac InvEval1 :=
+  match goal with
+  | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] =>
+      inv H; InvEval1
+  | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] =>
+      inv H; InvEval1
+  | _ =>
+      idtac
+  end.
+
+Ltac InvEval2 :=
+  match goal with
+  | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
+      simpl in H; inv H
+  | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
+      simpl in H; FuncInv
+  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
+      simpl in H; FuncInv
+  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
+      simpl in H; FuncInv
+  | _ =>
+      idtac
+  end.
+
+Ltac InvEval := 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 *)
+
+Section CMCONSTR.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+  
+(* Helper lemmas - from SplitLongproof.v *)
+
+Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto.
+Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
+
+Lemma eval_helper:
+  forall le id name sg args vargs vres,
+  eval_exprlist ge sp e m le args vargs ->
+  helper_declared prog id name sg  ->
+  external_implements name sg vargs vres ->
+  eval_expr ge sp e m le (Eexternal id sg args) vres.
+Proof.
+  intros.
+  red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q).
+  rewrite <- Genv.find_funct_ptr_iff in Q.
+  econstructor; eauto.
+Qed.
+
+Corollary eval_helper_1:
+  forall le id name sg arg1 varg1 vres,
+  eval_expr ge sp e m le arg1 varg1 ->
+  helper_declared prog id name sg  ->
+  external_implements name sg (varg1::nil) vres ->
+  eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres.
+Proof.
+  intros. eapply eval_helper; eauto. constructor; auto. constructor.
+Qed.
+
+Corollary eval_helper_2:
+  forall le id name sg arg1 arg2 varg1 varg2 vres,
+  eval_expr ge sp e m le arg1 varg1 ->
+  eval_expr ge sp e m le arg2 varg2 ->
+  helper_declared prog id name sg  ->
+  external_implements name sg (varg1::varg2::nil) vres ->
+  eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres.
+Proof.
+  intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor.
+Qed.
+
+(** We now show that the code generated by "smart constructor" functions
+  such as [Selection.notint] behaves as expected.  Continuing the
+  [notint] example, we show that if the expression [e]
+  evaluates to some integer value [Vint n], then [Selection.notint e]
+  evaluates to a value [Vint (Int.not n)] which is indeed the integer
+  negation of the value of [e].
+
+  All proofs follow a common pattern:
+- Reasoning by case over the result of the classification functions
+  (such as [add_match] for integer addition), gathering additional
+  information on the shape of the argument expressions in the non-default
+  cases.
+- Inversion of the evaluations of the arguments, exploiting the additional
+  information thus gathered.
+- Equational reasoning over the arithmetic operations performed,
+  using the lemmas from the [Int] and [Float] modules.
+- Construction of an evaluation derivation for the expression returned
+  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,
+  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
+Proof.
+  intros. unfold addrsymbol. econstructor; split.
+  EvalOp. simpl; eauto.
+  auto.
+Qed.
+
+Theorem eval_addrstack:
+  forall le ofs,
+  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v.
+Proof.
+  intros. unfold addrstack. econstructor; split.
+  EvalOp. simpl; eauto.
+  auto.
+Qed.
+
+Theorem eval_addimm_shlimm:
+  forall sh k2, unary_constructor_sound (addimm_shlimm sh k2) (fun x => ExtValues.addx sh x (Vint k2)).
+Proof.
+  red; unfold addimm_shlimm; intros.
+  destruct (Compopts.optim_addx tt).
+  {
+  destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT.
+  - TrivialExists. simpl.
+    f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e1.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e1.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e2.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e2.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e3.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e3.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e4.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e4.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    discriminate.
+  - unfold addx. rewrite Val.add_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+  }
+  { unfold addx. rewrite Val.add_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+    }
+Qed.
+
+Theorem eval_addimm:
+  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.
+  - case (addimm_match a); intros; InvEval; simpl.
+    + TrivialExists; simpl. rewrite Int.add_commut. auto.
+    + econstructor; split. EvalOp. simpl; eauto. 
+      unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto.
+    + econstructor; split. EvalOp. simpl; eauto. 
+      destruct sp; simpl; auto.
+    + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
+    + TrivialExists; simpl. subst x.
+      destruct v1; simpl; trivial.
+      destruct (Int.ltu _ _); simpl; trivial.
+      rewrite Int.add_assoc. rewrite Int.add_commut.
+      reflexivity.
+    + pose proof eval_addimm_shlimm as ADDX.
+      unfold unary_constructor_sound in ADDX.
+      unfold addx in ADDX.
+      rewrite Val.add_commut.
+      subst x.
+      apply ADDX; assumption.
+    + TrivialExists.
+Qed.
+
+Lemma eval_addx: forall n, binary_constructor_sound (add_shlimm n) (ExtValues.addx n).
+Proof.
+  red.
+  intros.
+  unfold add_shlimm.
+  destruct (Compopts.optim_addx tt).
+  {
+  destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT.
+  - TrivialExists.
+    simpl.
+    f_equal. f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      rewrite <- e1.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      rewrite <- e2.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      rewrite <- e3.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      rewrite <- e4.
+      apply Int.repr_unsigned. }
+    discriminate.
+  - TrivialExists;
+      repeat econstructor; eassumption.
+  }
+  { TrivialExists;
+      repeat econstructor; eassumption.
+  }
+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 Val.add_commut. apply eval_addimm; auto.
+  - apply eval_addimm; auto.
+  - subst.
+    replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
+       with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
+    apply eval_addimm. EvalOp.
+    repeat rewrite Val.add_assoc. decEq. apply Val.add_permut.
+  - subst. econstructor; split.
+    EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
+    rewrite Val.add_commut. destruct sp; simpl; auto.
+    destruct v1; simpl; auto.
+  - subst. econstructor; split.
+    EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
+    destruct sp; simpl; auto.
+    destruct v1; simpl; auto.
+  - subst.
+    replace (Val.add (Val.add v1 (Vint n1)) y)
+       with (Val.add (Val.add v1 y) (Vint n1)).
+    apply eval_addimm. EvalOp.
+    repeat rewrite Val.add_assoc. decEq. apply Val.add_commut.
+  - subst.
+    replace (Val.add x (Val.add v1 (Vint n2)))
+       with (Val.add (Val.add x v1) (Vint n2)).
+    apply eval_addimm. EvalOp.
+    repeat rewrite Val.add_assoc. reflexivity.
+  - (* Omadd *)
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
+  - (* Omadd rev *)
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
+    simpl. rewrite Val.add_commut. reflexivity.
+  - (* Omaddimm *)
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
+  - (* Omaddimm rev *)
+    subst. destruct (Compopts.optim_madd tt); TrivialExists;
+    repeat (eauto; econstructor; simpl).
+    simpl. rewrite Val.add_commut. reflexivity.
+    (* Oaddx *)
+  - subst. pose proof eval_addx as ADDX.
+    unfold binary_constructor_sound in ADDX.
+    rewrite Val.add_commut.
+    apply ADDX; assumption.
+    (* Oaddx *)
+  - subst. pose proof eval_addx as ADDX.
+    unfold binary_constructor_sound in ADDX.
+    apply ADDX; assumption.
+  - TrivialExists.
+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 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. simpl. subst. reflexivity.
+  - destruct (Compopts.optim_madd tt).
+    + TrivialExists. simpl. subst.
+      rewrite sub_add_neg.
+      rewrite neg_mul_distr_r.
+      unfold Val.neg.
+      reflexivity.
+    + TrivialExists. repeat (eauto; econstructor).
+      simpl. subst. reflexivity.
+  - TrivialExists.
+Qed.
+
+Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
+Proof.
+  red; intros until x. unfold negint. case (negint_match a); intros; InvEval.
+  TrivialExists.
+  TrivialExists.
+Qed.
+
+Theorem eval_shlimm:
+  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 (Int.ltu n Int.iwordsize) eqn:LT; simpl.
+  destruct (shlimm_match a); intros; InvEval.
+  - exists (Vint (Int.shl n1 n)); split. EvalOp.
+    simpl. rewrite LT. auto.
+  - destruct (Int.ltu (Int.add n n1) Int.iwordsize) 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) eqn:?; simpl; auto.
+      destruct (Int.ltu n Int.iwordsize) 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.
+  - TrivialExists.
+  - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
+    auto.
+Qed.
+
+Theorem eval_shruimm:
+  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 (Int.ltu n Int.iwordsize) eqn:LT.
+  destruct (shruimm_match a); intros; InvEval.
+  - exists (Vint (Int.shru n1 n)); split. EvalOp.
+    simpl. rewrite LT; auto.
+  - destruct (Int.ltu (Int.add n n1) Int.iwordsize) 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) eqn:?; simpl; auto.
+    rewrite LT. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
+    subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
+    simpl. auto.
+  - subst x.
+    simpl negb.
+    cbn iota.
+    destruct (is_bitfield _ _) eqn:BOUNDS.
+    + exists (extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+            (Z.sub
+               (Z.add
+                  (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                  Z.one) Int.zwordsize) v1).
+      split.
+      ++ EvalOp.
+      ++ unfold extfz.
+         rewrite BOUNDS.
+         destruct v1; try (simpl; apply Val.lessdef_undef).
+        replace (Z.sub Int.zwordsize
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+        replace (Z.sub Int.zwordsize
+             (Z.sub
+                (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
+                (Z.sub
+                   (Z.add
+                      (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                      Z.one) Int.zwordsize))) with (Int.unsigned n) by omega.
+        rewrite Int.repr_unsigned.
+        rewrite Int.repr_unsigned.
+        simpl.
+        destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial.
+        simpl.
+        destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial.
+    + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity.
+  - TrivialExists.
+  - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
+    auto.
+Qed.
+
+Theorem eval_shrimm:
+  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 (Int.ltu n Int.iwordsize) eqn:LT.
+  destruct (shrimm_match a); intros; InvEval.
+  - exists (Vint (Int.shr n1 n)); split. EvalOp.
+    simpl. rewrite LT; auto.
+  - destruct (Int.ltu (Int.add n n1) Int.iwordsize) 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) eqn:?; simpl; auto.
+    rewrite LT.
+    rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto.
+    subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
+    simpl. auto.
+  - subst x.
+    simpl negb.
+    cbn iota.
+    destruct (is_bitfield _ _) eqn:BOUNDS.
+    + exists (extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+            (Z.sub
+               (Z.add
+                  (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                  Z.one) Int.zwordsize) v1).
+      split.
+      ++ EvalOp.
+      ++ unfold extfs.
+         rewrite BOUNDS.
+         destruct v1; try (simpl; apply Val.lessdef_undef).
+        replace (Z.sub Int.zwordsize
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+        replace (Z.sub Int.zwordsize
+             (Z.sub
+                (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
+                (Z.sub
+                   (Z.add
+                      (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                      Z.one) Int.zwordsize))) with (Int.unsigned n) by omega.
+        rewrite Int.repr_unsigned.
+        rewrite Int.repr_unsigned.
+        simpl.
+        destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial.
+        simpl.
+        destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial.
+    + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity.
+  - TrivialExists.
+  - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
+    auto.
+Qed.
+
+Lemma eval_mulimm_base:
+  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
+Proof.
+  intros; red; intros; unfold mulimm_base.
+
+  assert (DFL: exists v, eval_expr ge sp e m le (Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)) v /\ Val.lessdef (Val.mul x (Vint n)) v).
+  TrivialExists. econstructor. EvalOp. simpl; eauto. econstructor. eauto. constructor.
+  rewrite Val.mul_commut. auto.
+
+  generalize (Int.one_bits_decomp n).
+  generalize (Int.one_bits_range n).
+  destruct (Int.one_bits n).
+  - intros. TrivialExists.
+  - destruct l.
+    + intros. rewrite H1. simpl.
+      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. 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 (x :: le)). eexact A1. eexact A2. intros [v [A B]].
+      exists v; 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. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto.
+      simpl. repeat rewrite H0; auto with coqlib.
+      intros. TrivialExists.
+Qed.
+
+Theorem eval_mulimm:
+  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.
+  - 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: binary_constructor_sound mul Val.mul.
+Proof.
+  red; intros until y.
+  unfold mul; case (mul_match a b); intros; InvEval.
+  rewrite Val.mul_commut. apply eval_mulimm. auto.
+  apply eval_mulimm. auto.
+  TrivialExists.
+Qed.
+
+Theorem eval_mulhs: binary_constructor_sound mulhs Val.mulhs.
+Proof.
+  red; intros. unfold mulhs; destruct Archi.ptr64 eqn:SF.
+- econstructor; split.
+  EvalOp. constructor. EvalOp. constructor. EvalOp. constructor. EvalOp. simpl; eauto. 
+  constructor. EvalOp. simpl; eauto. constructor. 
+  simpl; eauto. constructor. simpl; eauto. constructor. simpl; eauto.
+  destruct x; simpl; auto. destruct y; simpl; auto.
+  change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
+  apply Val.lessdef_same. f_equal. 
+  transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
+  unfold Int.mulhs; f_equal. rewrite Zbits.Zshiftr_div_two_p by omega. reflexivity.
+  apply Int.same_bits_eq; intros n N.
+  change Int.zwordsize with 32 in *.
+  assert (N1: 0 <= n < 64) by omega.
+  rewrite Int64.bits_loword by auto.
+  rewrite Int64.bits_shr' by auto.
+  change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
+  rewrite zlt_true by omega.
+  rewrite Int.testbit_repr by auto. 
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)).
+  rewrite Z.shiftr_spec by omega. auto.
+  apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
+  change Int64.zwordsize with 64; omega.
+- TrivialExists.
+Qed.
+
+Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
+Proof.
+  red; intros. unfold mulhu; destruct Archi.ptr64 eqn:SF.
+- econstructor; split.
+  EvalOp. constructor. EvalOp. constructor. EvalOp. constructor. EvalOp. simpl; eauto. 
+  constructor. EvalOp. simpl; eauto. constructor. 
+  simpl; eauto. constructor. simpl; eauto. constructor. simpl; eauto.
+  destruct x; simpl; auto. destruct y; simpl; auto.
+  change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
+  apply Val.lessdef_same. f_equal. 
+  transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
+  unfold Int.mulhu; f_equal. rewrite Zbits.Zshiftr_div_two_p by omega. reflexivity.
+  apply Int.same_bits_eq; intros n N.
+  change Int.zwordsize with 32 in *.
+  assert (N1: 0 <= n < 64) by omega.
+  rewrite Int64.bits_loword by auto.
+  rewrite Int64.bits_shru' by auto.
+  change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
+  rewrite zlt_true by omega.
+  rewrite Int.testbit_repr by auto. 
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)).
+  rewrite Z.shiftr_spec by omega. auto.
+  apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
+  change Int64.zwordsize with 64; omega.
+- TrivialExists.
+Qed.
+
+Theorem eval_andimm:
+  forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
+Proof.
+  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.
+  subst. destruct x; simpl; auto. rewrite Int.and_mone; auto.
+
+  case (andimm_match a); intros.
+  - InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
+  - InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
+  - InvEval. TrivialExists. simpl; congruence.
+  - 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.
+  - (*andn*) TrivialExists; simpl; congruence.
+  - (*andn reverse*) rewrite Val.and_commut. TrivialExists; simpl; congruence.
+  - 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. subst. exists x; split; auto.
+  destruct x; simpl; auto. rewrite Int.or_zero; auto.
+
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  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.
+  - InvEval. TrivialExists. simpl; congruence.
+  - TrivialExists.
+Qed.
+
+
+Remark eval_same_expr:
+  forall a1 a2 le v1 v2,
+  same_expr_pure a1 a2 = true ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  a1 = a2 /\ v1 = v2.
+Proof.
+  intros until v2.
+  destruct a1; simpl; try (intros; discriminate).
+  destruct a2; simpl; try (intros; discriminate).
+  case (ident_eq i i0); intros.
+  subst i0. inversion H0. inversion H1. split. auto. congruence.
+  discriminate.
+Qed.
+
+Lemma int_eq_commut: forall x y : int,
+    (Int.eq x y) = (Int.eq y x).
+Proof.
+  intros.
+  predSpec Int.eq Int.eq_spec x y;
+    predSpec Int.eq Int.eq_spec y x;
+    congruence.
+Qed.
+
+Theorem eval_or: binary_constructor_sound or Val.or.
+Proof.
+  unfold or; red; intros.
+  assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop Oor (a:::b:::Enil)) v /\ Val.lessdef (Val.or x y) v) by TrivialExists.
+  assert (ROR: forall v n1 n2,
+    Int.add n1 n2 = Int.iwordsize ->
+    Val.lessdef (Val.or (Val.shl v (Vint n1)) (Val.shru v (Vint n2)))
+                (Val.ror v (Vint n2))).
+  { intros. destruct v; simpl; auto.
+    destruct (Int.ltu n1 Int.iwordsize) eqn:N1; auto.
+    destruct (Int.ltu n2 Int.iwordsize) eqn:N2; auto.
+    simpl. rewrite <- Int.or_ror; auto. }
+  
+  destruct (or_match a b); InvEval.
+  
+  - rewrite Val.or_commut. apply eval_orimm; auto.
+  - apply eval_orimm; auto.
+  - predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize; auto.
+    destruct (same_expr_pure t1 t2) eqn:?; auto.
+    InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
+    exists (Val.ror v0 (Vint n2)); split. EvalOp. apply ROR; auto.
+  - predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize; auto.
+    destruct (same_expr_pure t1 t2) eqn:?; auto.
+    InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
+    exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto.
+  - (*orn*) TrivialExists; simpl; congruence.
+  - (*orn reversed*) rewrite Val.or_commut. TrivialExists; simpl; congruence.
+  - set (zstop := (int_highest_bit mask)).
+    set (zstart := (Int.unsigned start)).
+    destruct (is_bitfield _ _) eqn:Risbitfield.
+    + destruct (and_dec _ _) as [[Rmask Rnmask] | ].
+      * simpl in H6.
+        injection H6.
+        clear H6.
+        intro. subst y. subst x.
+        TrivialExists. simpl. f_equal.
+        unfold insf.
+        rewrite Risbitfield.
+        rewrite Rmask.
+        rewrite Rnmask.
+        simpl.
+        unfold bitfield_mask.
+        subst v0.
+        subst zstart.
+        rewrite Int.repr_unsigned.
+        reflexivity.
+      * apply DEFAULT.
+    + apply DEFAULT.
+  - set (zstop := (int_highest_bit mask)).
+    set (zstart := 0).
+    destruct (is_bitfield _ _) eqn:Risbitfield.
+    + destruct (and_dec _ _) as [[Rmask Rnmask] | ].
+      * subst y. subst x.
+        TrivialExists. simpl. f_equal.
+        unfold insf.
+        rewrite Risbitfield.
+        rewrite Rmask.
+        rewrite Rnmask.
+        simpl.
+        unfold bitfield_mask.
+        subst zstart.
+        rewrite (Val.or_commut (Val.and v1 _)).
+        rewrite (Val.or_commut (Val.and v1 _)).
+        destruct v0; simpl; trivial.
+        unfold Int.ltu, Int.iwordsize, Int.zwordsize.
+        rewrite Int.unsigned_repr.
+        ** rewrite Int.unsigned_repr.
+        *** simpl.
+            rewrite Int.shl_zero.
+            reflexivity.
+        *** simpl.
+            unfold Int.max_unsigned, Int.modulus.
+            simpl.
+            omega.
+        ** unfold Int.max_unsigned, Int.modulus.
+           simpl.
+           omega.
+      * apply DEFAULT.
+    + apply DEFAULT.
+  - apply DEFAULT.
+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.
+  - predSpec Int.eq Int.eq_spec n Int.mone.
+    -- subst n. intros. rewrite <- Val.not_xor. TrivialExists.
+    -- intros. destruct (xorimm_match a); intros; InvEval.
+       + TrivialExists. simpl. rewrite Int.xor_commut; auto.
+       + subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. 
+         predSpec Int.eq Int.eq_spec (Int.xor n2 n) Int.zero.
+         * exists v1; split; auto. destruct v1; simpl; auto. rewrite H1, Int.xor_zero; auto.  
+         * 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.
+
+Theorem eval_notint: unary_constructor_sound notint Val.notint.
+Proof.
+  assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v).
+    destruct v; simpl; auto. rewrite Int.not_involutive; auto.
+    unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - subst x. exists (Val.and v1 v0); split; trivial.
+      econstructor. constructor. eassumption. constructor.
+      eassumption. constructor. simpl. reflexivity.
+    - subst x. exists (Val.and v1 (Vint n)); split; trivial.
+      econstructor. constructor. eassumption. constructor.
+      simpl. reflexivity.
+    - subst x. exists (Val.or v1 v0); split; trivial.
+      econstructor. constructor. eassumption. constructor.
+      eassumption. constructor. simpl. reflexivity.
+    - subst x. exists (Val.or v1 (Vint n)); split; trivial.
+      econstructor. constructor. eassumption. constructor.
+      simpl. reflexivity.
+    - subst x. exists (Val.xor v1 v0); split; trivial.
+      econstructor. constructor. eassumption. constructor.
+      eassumption. constructor. simpl. reflexivity.
+    - subst x. exists (Val.xor v1 (Vint n)); split; trivial.
+      econstructor. constructor. eassumption. constructor.
+      simpl. reflexivity.
+    (* andn *)
+    - subst x. TrivialExists. simpl.
+      destruct v0; destruct v1; simpl; trivial.
+      f_equal. f_equal.
+      rewrite Int.not_and_or_not.
+      rewrite Int.not_involutive.
+      apply Int.or_commut.
+    - subst x. TrivialExists. simpl.
+      destruct v1; simpl; trivial.
+      f_equal. f_equal.
+      rewrite Int.not_and_or_not.
+      rewrite Int.not_involutive.
+      reflexivity.
+    (* orn *)
+    - subst x. TrivialExists. simpl.
+      destruct v0; destruct v1; simpl; trivial.
+      f_equal. f_equal.
+      rewrite Int.not_or_and_not.
+      rewrite Int.not_involutive.
+      apply Int.and_commut.
+    - subst x. TrivialExists. simpl.
+      destruct v1; simpl; trivial.
+      f_equal. f_equal.
+      rewrite Int.not_or_and_not.
+      rewrite Int.not_involutive.
+      reflexivity.
+    - subst x. exists v1; split; trivial.
+    - TrivialExists.
+    - TrivialExists.
+Qed.
+
+Theorem eval_divs_base:
+  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_base a b) v /\ Val.lessdef z v.
+Proof.
+  intros; unfold divs_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+Theorem eval_mods_base:
+  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_base a b) v /\ Val.lessdef z v.
+Proof.
+  intros; unfold mods_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+Theorem eval_divu_base:
+  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_base a b) v /\ Val.lessdef z v.
+Proof.
+  intros; unfold divu_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+(* For using 64-bit unsigned division for 32-bit
+
+  intros until z.
+  intros Hax Hby Hdiv. unfold divu_base.
+  pose proof (divu_is_divlu x y) as DIVU.
+  destruct (Val.divlu (Val.longofintu x) (Val.longofintu y))
+    as [ ql | ] eqn:Ediv.
+  { TrivialExists.
+    { econstructor. eapply eval_helper_2; eauto.
+      { econstructor. econstructor. eassumption.
+       constructor. simpl. reflexivity. }
+      { econstructor. econstructor. eassumption.
+        constructor. simpl. reflexivity. }
+      { DeclHelper. }
+      { UseHelper. }
+      constructor. }
+    simpl.
+    congruence.
+  }
+  congruence.
+Qed.
+ *)
+  
+Theorem eval_modu_base:
+  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_base a b) v /\ Val.lessdef z v.
+Proof.
+  intros; unfold modu_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+(* for using 64-bit unsigned modulo for 32-bit
+
+  intros until z.
+  intros Hax Hby Hmod. unfold modu_base.
+  pose proof (modu_is_modlu x y) as MODU.
+  destruct (Val.modlu (Val.longofintu x) (Val.longofintu y))
+    as [ ql | ] eqn:Emod.
+  { TrivialExists.
+    { econstructor. eapply eval_helper_2; eauto.
+      { econstructor. econstructor. eassumption.
+       constructor. simpl. reflexivity. }
+      { econstructor. econstructor. eassumption.
+        constructor. simpl. reflexivity. }
+      { DeclHelper. }
+      { UseHelper. }
+      constructor. }
+    simpl.
+    congruence.
+  }
+  congruence.
+Qed.
+ *)
+  
+Theorem eval_shrximm:
+  forall le a n x z,
+    eval_expr ge sp e m le a x ->
+    Val.shrx x (Vint n) = Some z ->
+    exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
+Proof.
+  intros. unfold shrximm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  subst n. exists x; split; auto.
+  destruct x; simpl in H0; try discriminate.
+  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
+  replace (Int.shrx i Int.zero) with i. auto.
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
+  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+  econstructor; split. EvalOp.
+  simpl. rewrite H0. simpl. reflexivity. auto.
+Qed.
+
+Theorem eval_shl: binary_constructor_sound shl Val.shl.
+Proof.
+  red; intros until y; unfold shl; case (shl_match b); intros.
+  InvEval. apply eval_shlimm; auto.
+  TrivialExists.
+Qed.
+
+Theorem eval_shr: binary_constructor_sound shr Val.shr.
+Proof.
+  red; intros until y; unfold shr; case (shr_match b); intros.
+  InvEval. apply eval_shrimm; auto.
+  TrivialExists.
+Qed.
+
+Theorem eval_shru: binary_constructor_sound shru Val.shru.
+Proof.
+  red; intros until y; unfold shru; case (shru_match b); intros.
+  InvEval. apply eval_shruimm; auto.
+  TrivialExists.
+Qed.
+
+Theorem eval_negf: unary_constructor_sound negf Val.negf.
+Proof.
+  red; intros. TrivialExists.
+Qed.
+
+Theorem eval_absf: unary_constructor_sound absf Val.absf.
+Proof.
+  red; intros. TrivialExists.
+Qed.
+
+Theorem eval_addf: binary_constructor_sound addf Val.addf.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_subf: binary_constructor_sound subf Val.subf.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_mulf: binary_constructor_sound mulf Val.mulf.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_negfs: unary_constructor_sound negfs Val.negfs.
+Proof.
+  red; intros. TrivialExists.
+Qed.
+
+Theorem eval_absfs: unary_constructor_sound absfs Val.absfs.
+Proof.
+  red; intros. TrivialExists.
+Qed.
+
+Theorem eval_addfs: binary_constructor_sound addfs Val.addfs.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_subfs: binary_constructor_sound subfs Val.subfs.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Section COMP_IMM.
+
+Variable default: comparison -> int -> condition.
+Variable intsem: comparison -> int -> int -> bool.
+Variable sem: comparison -> val -> val -> val.
+
+Hypothesis sem_int: forall c x y, sem c (Vint x) (Vint y) = Val.of_bool (intsem c x y).
+Hypothesis sem_undef: forall c v, sem c Vundef v = Vundef.
+Hypothesis sem_eq: forall x y, sem Ceq (Vint x) (Vint y) = Val.of_bool (Int.eq x y).
+Hypothesis sem_ne: forall x y, sem Cne (Vint x) (Vint y) = Val.of_bool (negb (Int.eq x y)).
+Hypothesis sem_default: forall c v n, sem c v (Vint n) = Val.of_optbool (eval_condition (default c n) (v :: nil) m).
+
+Lemma eval_compimm:
+  forall le c a n2 x,
+  eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (compimm default intsem c a n2) v
+         /\ Val.lessdef (sem c x (Vint n2)) v.
+Proof.
+  intros until x.
+  unfold compimm; case (compimm_match c a); intros.
+(* constant *)
+  - InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
+(* eq cmp *)
+  - InvEval. inv H. simpl in H5. inv H5.
+    destruct (Int.eq_dec n2 Int.zero).
+    + subst n2. TrivialExists.
+      simpl. rewrite eval_negate_condition.
+      destruct (eval_condition c0 vl m); simpl.
+      unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
+      rewrite sem_undef; auto.
+    + destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
+      simpl. destruct (eval_condition c0 vl m); simpl.
+      unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
+      rewrite sem_undef; auto.
+      exists (Vint Int.zero); split. EvalOp.
+      destruct (eval_condition c0 vl m); simpl.
+      unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto.
+      rewrite sem_undef; auto.
+(* ne cmp *)
+  - InvEval. inv H. simpl in H5. inv H5.
+    destruct (Int.eq_dec n2 Int.zero).
+    + subst n2. TrivialExists.
+      simpl. destruct (eval_condition c0 vl m); simpl.
+      unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
+      rewrite sem_undef; auto.
+    + destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
+      simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl.
+      unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
+      rewrite sem_undef; auto.
+      exists (Vint Int.one); split. EvalOp.
+      destruct (eval_condition c0 vl m); simpl.
+      unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto.
+      rewrite sem_undef; auto.
+(* default *)
+  - TrivialExists. simpl. rewrite sem_default. auto.
+Qed.
+
+Hypothesis sem_swap:
+  forall c x y, sem (swap_comparison c) x y = sem c y x.
+
+Lemma eval_compimm_swap:
+  forall le c a n2 x,
+  eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v
+         /\ Val.lessdef (sem c (Vint n2) x) v.
+Proof.
+  intros. rewrite <- sem_swap. eapply eval_compimm; eauto.
+Qed.
+
+End COMP_IMM.
+
+Theorem eval_comp:
+  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.
+  eapply eval_compimm_swap; eauto.
+  intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
+  eapply eval_compimm; eauto.
+  TrivialExists.
+Qed.
+
+Theorem eval_compu:
+  forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
+Proof.
+  intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
+  eapply eval_compimm_swap; eauto.
+  intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
+  eapply eval_compimm; eauto.
+  TrivialExists.
+Qed.
+
+Theorem eval_compf:
+  forall c, binary_constructor_sound (compf c) (Val.cmpf c).
+Proof.
+  intros; red; intros. unfold compf. TrivialExists.
+Qed.
+
+Theorem eval_compfs:
+  forall c, binary_constructor_sound (compfs c) (Val.cmpfs c).
+Proof.
+  intros; red; intros. unfold compfs. TrivialExists.
+Qed.
+
+Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
+Proof.
+  red; intros until x. unfold cast8signed. case (cast8signed_match a); intros; InvEval.
+  TrivialExists.
+  TrivialExists.
+Qed.
+
+Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
+Proof.
+  red; intros until x. unfold cast8unsigned.
+  rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate.
+Qed.
+
+Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
+Proof.
+  red; intros until x. unfold cast16signed. case (cast16signed_match a); intros; InvEval.
+  TrivialExists.
+  TrivialExists.
+Qed.
+
+Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
+Proof.
+  red; intros until x. unfold cast8unsigned.
+  rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate.
+Qed.
+
+Theorem eval_intoffloat:
+  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. TrivialExists.
+  simpl. rewrite H0. reflexivity.
+Qed.
+
+Theorem eval_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; unfold intuoffloat. TrivialExists.
+  simpl. rewrite H0. reflexivity.
+Qed.
+
+Theorem eval_floatofintu:
+  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 Val.floatofintu in *.
+  unfold floatofintu.
+  destruct (floatofintu_match a).
+  - InvEval.
+    TrivialExists.
+  - InvEval.
+    TrivialExists.
+    constructor. econstructor. constructor. eassumption. constructor.
+    simpl. f_equal. constructor.
+    simpl.
+    destruct x; simpl; trivial; try discriminate.
+    f_equal.
+    inv H0.
+    f_equal.
+    rewrite Float.of_intu_of_longu.
+    reflexivity.
+Qed.
+
+Theorem eval_floatofint:
+  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.
+  destruct (floatofint_match a).
+  - InvEval.
+    TrivialExists.
+  - InvEval.
+    TrivialExists.
+    constructor. econstructor. constructor. eassumption. constructor.
+    simpl. f_equal. constructor.
+    simpl.
+    destruct x; simpl; trivial; try discriminate.
+    f_equal.
+    inv H0.
+    f_equal.
+    rewrite Float.of_int_of_long.
+    reflexivity.
+Qed.
+
+Theorem eval_intofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.intofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold intofsingle. TrivialExists.
+  simpl. rewrite H0. reflexivity.
+Qed.
+
+Theorem eval_singleofint:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.singleofint x = Some y ->
+  exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold singleofint; TrivialExists.
+  simpl. rewrite H0. reflexivity.
+Qed.
+
+Theorem eval_intuofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.intuofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold intuofsingle. TrivialExists.
+  simpl. rewrite H0. reflexivity.
+Qed.
+
+Theorem eval_singleofintu:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.singleofintu x = Some y ->
+  exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold intuofsingle. TrivialExists.
+  simpl. rewrite H0. reflexivity.
+Qed.
+
+Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
+Proof.
+  red; intros. unfold singleoffloat. TrivialExists.
+Qed.
+
+Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle.
+Proof.
+  red; intros. unfold floatofsingle. TrivialExists.
+Qed.
+
+Theorem eval_addressing:
+  forall le chunk a v b ofs,
+  eval_expr ge sp e m le a v ->
+  v = Vptr b ofs ->
+  match addressing chunk a with (mode, args) =>
+    exists vl,
+    eval_exprlist ge sp e m le args vl /\
+    eval_addressing ge sp mode vl = Some v
+  end.
+Proof.
+  intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
+  - exists (@nil val);  split. eauto with evalexpr. simpl. auto.
+  - destruct (orb _ _).
+  + exists (Vptr b ofs0 :: nil); split.
+    constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence.
+  + exists (@nil val); split. constructor. simpl; auto.
+  - exists (v1 :: nil); split. eauto with evalexpr. simpl.
+    destruct v1; simpl in H; try discriminate.
+  - exists (v1 :: nil); split. eauto with evalexpr. simpl.
+    destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
+    simpl. auto.
+  - destruct (Compopts.optim_xsaddr tt).
+    + destruct (Z.eq_dec _ _).
+      * exists (v1 :: v2 :: nil); split.
+        repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence.
+      * exists (v1 :: v0 :: nil); split.
+        repeat (constructor; auto). econstructor.
+        repeat (constructor; auto). eassumption. simpl. congruence.
+        simpl. congruence.
+    + exists (v1 :: v0 :: nil); split.
+        repeat (constructor; auto). econstructor.
+        repeat (constructor; auto). eassumption. simpl. congruence.
+        simpl. congruence.
+  - unfold addxl in *.
+    destruct (Compopts.optim_xsaddr tt).
+    + unfold int_of_shift1_4 in *.
+      destruct (Z.eq_dec _ _).
+      * exists (v0 :: v1 :: nil); split.
+        repeat (constructor; auto). simpl.
+        congruence.
+      * eexists; split.
+        repeat (constructor; auto). eassumption.
+        econstructor.
+        repeat (constructor; auto). eassumption. simpl.
+        reflexivity.
+        simpl. congruence.
+    + eexists; split.
+        repeat (constructor; auto). eassumption.
+        econstructor.
+        repeat (constructor; auto). eassumption. simpl.
+        reflexivity.
+        simpl. unfold int_of_shift1_4 in *. congruence.
+  - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence.
+  - exists (v :: nil);  split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
+Qed.
+
+Theorem eval_builtin_arg:
+  forall a v,
+  eval_expr ge sp e m nil a v ->
+  CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v.
+Proof.
+  intros until v. unfold builtin_arg; case (builtin_arg_match a); intros.
+- InvEval. constructor.
+- InvEval. constructor.
+- InvEval. constructor.
+- InvEval. simpl in H5. inv H5. constructor.
+- InvEval. subst v. constructor; auto.
+- inv H. InvEval. simpl in H6; inv H6. constructor; auto.
+- destruct Archi.ptr64 eqn:SF.
++ constructor; auto.
++ InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vint n) else Val.add v1 (Vint n)).
+  repeat constructor; auto.
+  rewrite SF; auto.
+- destruct Archi.ptr64 eqn:SF.
++ InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vlong n) else Val.add v1 (Vlong n)).
+  repeat constructor; auto.
++ constructor; auto.
+- constructor; auto.
+Qed.
+
+(* ternary *)
+(* does not work due to possible nondeterminism
+Lemma cond_to_condition0_correct :
+  forall cond : condition,
+  forall al : exprlist,
+    match (cond_to_condition0 cond al) with
+    | None => True
+    | Some(cond0, e1) =>
+      forall le vl v1,
+      eval_expr ge sp e m le e1 v1 ->
+      eval_exprlist ge sp e m le al vl ->
+      (eval_condition0 cond0 v1 m) = (eval_condition cond vl m)
+    end.
+Proof.
+  intros.
+  unfold cond_to_condition0.
+  case (cond_to_condition0_match cond al); trivial.
+  {
+    intros.
+    destruct (Int.eq_dec _ _); trivial.
+    intros until v1.
+    intros He1 Hel.
+    InvEval.
+    simpl.
+    f_equal.
+    eapply eval_expr_determ. eassumption.
+  }
+Qed.
+*)
+
+Lemma eval_neg_condition0:
+  forall cond0: condition0,
+  forall v1: val,
+  forall m: mem,
+    (eval_condition0 (negate_condition0 cond0) v1 m) =
+    option_map negb (eval_condition0 cond0 v1 m).
+Proof.
+  intros.
+  destruct cond0; simpl;
+  try rewrite Val.negate_cmp_bool;
+  try rewrite Val.negate_cmpu_bool;
+  try rewrite Val.negate_cmpl_bool;
+  try rewrite Val.negate_cmplu_bool;
+  reflexivity.
+Qed.
+
+Lemma select_neg:
+  forall a b c,
+    Val.select (option_map negb a) b c =
+    Val.select a c b.
+Proof.
+  destruct a; simpl; trivial.
+  destruct b; simpl; trivial.
+Qed.
+
+Lemma eval_select0: 
+  forall le ty cond0 ac vc a1 v1 a2 v2,
+  eval_expr ge sp e m le ac vc ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  exists v, 
+     eval_expr ge sp e m le (select0 ty cond0 a1 a2 ac) v
+  /\ Val.lessdef (Val.select (eval_condition0 cond0 vc m) v1 v2 ty) v.
+Proof.
+  intros.
+  unfold select0.
+  destruct (select0_match ty cond0 a1 a2 ac).
+  all: InvEval; econstructor; split;
+    try  repeat (try econstructor; try eassumption).
+  all: rewrite eval_neg_condition0; rewrite select_neg; constructor.
+Qed.
+
+Lemma bool_cond0_ne:
+  forall ob : option bool,
+  forall m,
+    (eval_condition0 (Ccomp0 Cne) (Val.of_optbool ob) m) = ob.
+Proof.
+  destruct ob; simpl; trivial.
+  intro.
+  destruct b; reflexivity.
+Qed.
+
+Lemma eval_condition_ccomp_swap :
+  forall c x y m,
+    eval_condition (Ccomp (swap_comparison c)) (x :: y :: nil) m=
+    eval_condition (Ccomp c) (y :: x :: nil) m.
+Proof.
+  intros; unfold eval_condition;
+  apply Val.swap_cmp_bool.
+Qed.
+
+Lemma eval_condition_ccompu_swap :
+  forall c x y m,
+    eval_condition (Ccompu (swap_comparison c)) (x :: y :: nil) m=
+    eval_condition (Ccompu c) (y :: x :: nil) m.
+Proof.
+  intros; unfold eval_condition;
+  apply Val.swap_cmpu_bool.
+Qed.
+
+Lemma eval_condition_ccompl_swap :
+  forall c x y m,
+    eval_condition (Ccompl (swap_comparison c)) (x :: y :: nil) m=
+    eval_condition (Ccompl c) (y :: x :: nil) m.
+Proof.
+  intros; unfold eval_condition;
+  apply Val.swap_cmpl_bool.
+Qed.
+
+Lemma eval_condition_ccomplu_swap :
+  forall c x y m,
+    eval_condition (Ccomplu (swap_comparison c)) (x :: y :: nil) m=
+    eval_condition (Ccomplu c) (y :: x :: nil) m.
+Proof.
+  intros; unfold eval_condition;
+  apply Val.swap_cmplu_bool.
+Qed.
+
+Theorem eval_select: 
+  forall le ty cond al vl a1 v1 a2 v2 a b,
+  select ty cond al a1 a2 = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_condition cond vl m = Some b ->
+  exists v, 
+     eval_expr ge sp e m le a v
+  /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
+Proof.
+  unfold select.
+  intros until b.
+  intro Hop; injection Hop; clear Hop; intro; subst a.
+  intros HeL He1 He2 HeC.
+  unfold cond_to_condition0.
+  destruct (cond_to_condition0_match cond al).
+  {
+    InvEval.
+    rewrite <- HeC. 
+    destruct (Int.eq_dec x Int.zero).
+    { subst x.
+      simpl.
+      change (Val.cmp_bool c v0 (Vint Int.zero))
+        with (eval_condition0 (Ccomp0 c) v0 m).
+      eapply eval_select0; eassumption.
+    }
+    simpl.
+    erewrite <- (bool_cond0_ne (Val.cmp_bool c v0 (Vint x))).
+    eapply eval_select0; repeat (try econstructor; try eassumption).
+  }
+  {
+    InvEval.
+    rewrite <- HeC. 
+    destruct (Int.eq_dec x Int.zero).
+    { subst x.
+      simpl.
+      change (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint Int.zero))
+        with (eval_condition0 (Ccompu0 c) v0 m).
+      eapply eval_select0; eassumption.
+    }
+    simpl.
+    erewrite <- (bool_cond0_ne (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint x))).
+    eapply eval_select0; repeat (try econstructor; try eassumption).
+  }
+  {
+    InvEval.
+    rewrite <- HeC. 
+    destruct (Int64.eq_dec x Int64.zero).
+    { subst x.
+      simpl.
+      change (Val.cmpl_bool c v0 (Vlong Int64.zero))
+      with (eval_condition0 (Ccompl0 c) v0 m).
+      eapply eval_select0; eassumption.
+    }
+    simpl.
+    erewrite <- (bool_cond0_ne (Val.cmpl_bool c v0 (Vlong x))).
+    eapply eval_select0; repeat (try econstructor; try eassumption).
+  }
+  {
+    InvEval.
+    rewrite <- HeC. 
+    destruct (Int64.eq_dec x Int64.zero).
+    { subst x.
+      simpl.
+      change (Val.cmplu_bool  (Mem.valid_pointer m) c v0 (Vlong Int64.zero))
+      with (eval_condition0 (Ccomplu0 c) v0 m).
+      eapply eval_select0; eassumption.
+    }
+    simpl.
+    erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))).
+    eapply eval_select0; repeat (try econstructor; try eassumption).
+  }
+  erewrite <- (bool_cond0_ne (Some b)).
+  eapply eval_select0; repeat (try econstructor; try eassumption).
+  rewrite <- HeC.
+  simpl.
+  reflexivity.
+Qed.
+
+(* floating-point division *)
+Theorem eval_divf_base:
+  forall le a b x 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 (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+  intros; unfold divf_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+
+Lemma eval_divfs_base1:
+  forall le a b x 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 (divfs_base1 b) v /\ Val.lessdef (ExtValues.invfs y) v.
+Proof.
+  intros; unfold divfs_base1.
+  econstructor; split.
+  repeat (try econstructor; try eassumption).
+  trivial.
+Qed.
+
+Lemma eval_divfs_baseX:
+  forall le a b x 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 (divfs_baseX a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros; unfold divfs_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+Theorem eval_divfs_base:
+  forall le a b x 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 (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros; unfold divfs_base.
+  destruct (divfs_base_match _).
+  - destruct (Float32.eq_dec _ _).
+    + exists (Val.divfs x y).
+      split; trivial. repeat (try econstructor; try eassumption).
+      simpl. InvEval. reflexivity.
+    + apply eval_divfs_baseX; assumption.
+  - apply eval_divfs_baseX; assumption.
+Qed.
+
+(** Platform-specific known builtins *)
+
+Lemma eval_fma:
+  forall al a vl v le,
+  gen_fma al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem BI_fma vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  unfold gen_fma.
+  intros until le.
+  intro Heval.
+  destruct (gen_fma_match _) in *; try discriminate.
+  all: inversion Heval; subst a; clear Heval; intro; InvEval.
+  - subst v1.
+    TrivialExists.
+  destruct v0; simpl; trivial;
+    destruct v2; simpl; trivial;
+      destruct v3; simpl; trivial.
+  - intro Heval.
+  simpl in Heval.
+  inv Heval.
+  TrivialExists.
+  destruct v0; simpl; trivial;
+    destruct v1; simpl; trivial;
+      destruct v2; simpl; trivial.
+Qed.
+
+Lemma eval_fmaf:
+  forall al a vl v le,
+  gen_fmaf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem BI_fmaf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  unfold gen_fmaf.
+  intros until le.
+  intro Heval.
+  destruct (gen_fmaf_match _) in *; try discriminate.
+  all: inversion Heval; subst a; clear Heval; intro; InvEval.
+  - subst v1.
+    TrivialExists.
+  destruct v0; simpl; trivial;
+    destruct v2; simpl; trivial;
+      destruct v3; simpl; trivial.
+  - intro Heval.
+  simpl in Heval.
+  inv Heval.
+  TrivialExists.
+  destruct v0; simpl; trivial;
+    destruct v1; simpl; trivial;
+      destruct v2; simpl; trivial.
+Qed.
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  destruct bf; intros until le; intro Heval.
+  all: try (inversion Heval; subst a; clear Heval;
+       exists v; split; trivial;
+       repeat (try econstructor; try eassumption)).
+  - apply eval_fma; assumption.
+  - apply eval_fmaf; assumption.
+Qed.
+
+End CMCONSTR.