AArch64 port

This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.

1 files changed, 1070 insertions, 0 deletions

diff --git a/aarch64/SelectOpproof.v b/aarch64/SelectOpproof.v
new file mode 100644
index 00000000..b78a5ed8
--- /dev/null
+++ b/aarch64/SelectOpproof.v
@@ -0,0 +1,1070 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*         Xavier Leroy, Collège de France and INRIA Paris             *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness of instruction selection for operators *)
+
+Require Import Coqlib Zbits.
+Require Import AST Integers Floats Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
+Require Import SelectOp.
+
+Local Open Scope cminorsel_scope.
+Local Transparent Archi.ptr64.
+
+(** * 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 := 
+  eauto with evalexpr;
+  match goal with
+  | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp|try reflexivity; auto]
+  | [ |- eval_exprlist _ _ _ _ _ _ _ ] => econstructor; EvalOp
+  | _ => idtac
+  end.
+
+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 ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+(** 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.
+
+(** ** Constants *)
+
+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. TrivialExists.
+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. TrivialExists.
+Qed.
+
+(** ** Addition, opposite, subtraction *)
+
+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.
++ subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
+Qed.
+
+Theorem eval_add: binary_constructor_sound add Val.add.
+Proof.
+  red; intros until y.
+  unfold add; case (add_match a b); intros; InvEval; subst.
+- rewrite Val.add_commut. apply eval_addimm; auto.
+- apply eval_addimm; auto.
+- 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.
+- 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.
+- rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
+- rewrite Val.add_commut. TrivialExists.
+- TrivialExists.
+- rewrite Val.add_commut. TrivialExists.
+- TrivialExists.
+- 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; subst.
+- TrivialExists.
+- TrivialExists.
+- 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; subst.
+- rewrite Val.sub_add_opp. apply eval_addimm; auto.
+- 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.
+- rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
+- rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
+- TrivialExists.
+- TrivialExists.
+- TrivialExists.
+Qed.
+
+(** ** Immediate shifts *)
+
+Remark eval_shlimm_base: forall le a n x,
+  eval_expr ge sp e m le a x ->
+  Int.ltu n Int.iwordsize = true ->
+  eval_expr ge sp e m le (shlimm_base a n) (Val.shl x (Vint n)).
+Proof.
+Local Opaque mk_amount32.
+  unfold shlimm_base; intros; EvalOp. simpl. rewrite mk_amount32_eq by auto. auto.
+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; [| destruct (Int.ltu n Int.iwordsize) eqn:L]; simpl.
+- intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
+- destruct (shlimm_match a); intros; InvEval; subst.
++ TrivialExists. simpl; rewrite L; auto.
++ destruct (Int.ltu (Int.add a n) Int.iwordsize) eqn:L2.
+* econstructor; split. eapply eval_shlimm_base; eauto.
+  destruct v1; simpl; auto. rewrite a32_range; simpl. rewrite L, L2. 
+  rewrite Int.shl_shl; auto using a32_range.
+* econstructor; split; [|eauto]. apply eval_shlimm_base; auto. EvalOp.
++ TrivialExists. simpl. rewrite mk_amount32_eq; auto.
++ TrivialExists. simpl. rewrite mk_amount32_eq; auto.
++ destruct (Int.ltu (Int.add a n) Int.iwordsize) eqn:L2.
+* TrivialExists. simpl. rewrite mk_amount32_eq by auto. 
+  destruct (Val.zero_ext s v1); simpl; auto.
+  rewrite a32_range; simpl; rewrite L, L2.
+  rewrite Int.shl_shl; auto using a32_range.
+* econstructor; split. eapply eval_shlimm_base; eauto. EvalOp; simpl; eauto. auto.
++ destruct (Int.ltu (Int.add a n) Int.iwordsize) eqn:L2.
+* TrivialExists. simpl. rewrite mk_amount32_eq by auto. 
+  destruct (Val.sign_ext s v1); simpl; auto.
+  rewrite a32_range; simpl; rewrite L, L2.
+  rewrite Int.shl_shl; auto using a32_range.
+* econstructor; split. eapply eval_shlimm_base; eauto. EvalOp; simpl; eauto. auto.
++ econstructor; eauto using eval_shlimm_base.
+- intros; TrivialExists.
+Qed.
+
+Remark eval_shruimm_base: forall le a n x,
+  eval_expr ge sp e m le a x ->
+  Int.ltu n Int.iwordsize = true ->
+  eval_expr ge sp e m le (shruimm_base a n) (Val.shru x (Vint n)).
+Proof.
+  unfold shruimm_base; intros; EvalOp. simpl. rewrite mk_amount32_eq by auto. auto.
+Qed.
+
+Remark sub_shift_amount:
+  forall y z,
+  Int.ltu y Int.iwordsize = true -> Int.ltu z Int.iwordsize = true -> Int.unsigned y <= Int.unsigned z ->
+  Int.ltu (Int.sub z y) Int.iwordsize = true.
+Proof.
+  intros. unfold Int.ltu; apply zlt_true. rewrite Int.unsigned_repr_wordsize.
+  apply Int.ltu_iwordsize_inv in H. apply Int.ltu_iwordsize_inv in H0.
+  unfold Int.sub; rewrite Int.unsigned_repr. omega.
+  generalize Int.wordsize_max_unsigned; omega.
+Qed.
+
+Theorem eval_shruimm:
+  forall n, unary_constructor_sound (fun a => shruimm a n)
+                                    (fun x => Val.shru x (Vint n)).
+Proof.
+Local Opaque Int.zwordsize.
+  red; intros until x; unfold shruimm.
+  predSpec Int.eq Int.eq_spec n Int.zero; [| destruct (Int.ltu n Int.iwordsize) eqn:L]; simpl.
+- intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
+- destruct (shruimm_match a); intros; InvEval; subst.
++ TrivialExists. simpl; rewrite L; auto.
++ destruct (Int.ltu n a) eqn:L2.
+* assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true).
+  { apply sub_shift_amount; auto using a32_range.
+    apply Int.ltu_inv in L2. omega. }
+  econstructor; split. EvalOp.
+  destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
+  simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto.
+* assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true).
+  { apply sub_shift_amount; auto using a32_range.
+    unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
+  econstructor; split. EvalOp.
+  destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
+  simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto.
++ destruct (Int.ltu (Int.add a n) Int.iwordsize) eqn:L2.
+* econstructor; split. eapply eval_shruimm_base; eauto.
+  destruct v1; simpl; auto. rewrite a32_range; simpl. rewrite L, L2. 
+  rewrite Int.shru_shru; auto using a32_range.
+* econstructor; split; [|eauto]. apply eval_shruimm_base; auto. EvalOp.
++ destruct (zlt (Int.unsigned n) s).
+* econstructor; split. EvalOp. rewrite mk_amount32_eq by auto.
+  destruct v1; simpl; auto. rewrite ! L; simpl.
+  set (s' := s - Int.unsigned n).
+  replace s with (s' + Int.unsigned n) by (unfold s'; omega).
+  rewrite Int.shru_zero_ext. auto. unfold s'; omega.
+* econstructor; split. EvalOp.
+  destruct v1; simpl; auto. rewrite ! L; simpl.
+  rewrite Int.shru_zero_ext_0 by omega. auto. 
++ econstructor; eauto using eval_shruimm_base.
+- intros; TrivialExists.
+Qed.
+
+Remark eval_shrimm_base: forall le a n x,
+  eval_expr ge sp e m le a x ->
+  Int.ltu n Int.iwordsize = true ->
+  eval_expr ge sp e m le (shrimm_base a n) (Val.shr x (Vint n)).
+Proof.
+  unfold shrimm_base; intros; EvalOp. simpl. rewrite mk_amount32_eq by auto. 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; [| destruct (Int.ltu n Int.iwordsize) eqn:L]; simpl.
+- intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
+- destruct (shrimm_match a); intros; InvEval; subst.
++ TrivialExists. simpl; rewrite L; auto.
++ destruct (Int.ltu n a) eqn:L2.
+* assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true).
+  { apply sub_shift_amount; auto using a32_range.
+    apply Int.ltu_inv in L2. omega. }
+  econstructor; split. EvalOp.
+  destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
+  simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto.
+* assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true).
+  { apply sub_shift_amount; auto using a32_range.
+    unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
+  econstructor; split. EvalOp.
+  destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
+  simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto.
++ destruct (Int.ltu (Int.add a n) Int.iwordsize) eqn:L2.
+* econstructor; split. eapply eval_shrimm_base; eauto.
+  destruct v1; simpl; auto. rewrite a32_range; simpl. rewrite L, L2. 
+  rewrite Int.shr_shr; auto using a32_range.
+* econstructor; split; [|eauto]. apply eval_shrimm_base; auto. EvalOp.
++ destruct (zlt (Int.unsigned n) s && zlt s Int.zwordsize) eqn:E.
+* InvBooleans. econstructor; split. EvalOp. rewrite mk_amount32_eq by auto.
+  destruct v1; simpl; auto. rewrite ! L; simpl.
+  set (s' := s - Int.unsigned n).
+  replace s with (s' + Int.unsigned n) by (unfold s'; omega).
+  rewrite Int.shr_sign_ext. auto. unfold s'; omega. unfold s'; omega.
+* econstructor; split; [|eauto]. apply eval_shrimm_base; auto. EvalOp.
++ econstructor; eauto using eval_shrimm_base. 
+- intros; TrivialExists.
+Qed.
+
+(** ** Multiplication *)
+
+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).
+  { rewrite Val.mul_commut; TrivialExists. } 
+  generalize (Int.one_bits_decomp n); generalize (Int.one_bits_range n);
+  destruct (Int.one_bits n) as [ | i [ | j []]]; intros P Q.
+- apply DFL.
+- replace (Val.mul x (Vint n)) with (Val.shl x (Vint i)).
+  apply eval_shlimm; auto.
+  simpl in Q. rewrite <- Val.shl_mul, Q, Int.add_zero. simpl. rewrite P by auto with coqlib. auto.
+- exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
+  exploit (eval_shlimm j (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.
+  simpl in Q. rewrite Q, Int.add_zero.
+  replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one j)))
+     with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint j))).
+  rewrite Val.mul_add_distr_r.
+  repeat rewrite Val.shl_mul. eapply Val.lessdef_trans; [|eauto]. apply Val.add_lessdef; auto.
+  simpl. repeat rewrite P by auto with coqlib. auto.
+- apply DFL.
+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; subst.
+- TrivialExists. simpl. rewrite Int.mul_commut; auto.
+- 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; subst.
+- rewrite Val.mul_commut. apply eval_mulimm; auto.
+- apply eval_mulimm; auto.
+- TrivialExists.
+Qed.
+
+Theorem eval_mulhs: binary_constructor_sound mulhs Val.mulhs.
+Proof.
+  unfold mulhs; red; intros. econstructor; split. EvalOp.
+  unfold eval_shiftl, eval_extend. rewrite ! mk_amount64_eq by auto.
+  destruct x; simpl; auto. destruct y; simpl; auto.
+  change (Int.ltu Int.zero Int64.iwordsize') with true; simpl.
+  rewrite ! Int64.shl'_zero.  
+  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 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.
+Qed.
+
+Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
+Proof.
+  unfold mulhu; red; intros. econstructor; split. EvalOp.
+  unfold eval_shiftl, eval_extend. rewrite ! mk_amount64_eq by auto.
+  destruct x; simpl; auto. destruct y; simpl; auto.
+  change (Int.ltu Int.zero Int64.iwordsize') with true; simpl.
+  rewrite ! Int64.shl'_zero.
+  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 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.
+Qed.
+
+(** Integer conversions *)
+
+Theorem eval_zero_ext:
+  forall sz, 0 <= sz -> unary_constructor_sound (zero_ext sz) (Val.zero_ext sz).
+Proof.
+  intros; red; intros until x; unfold zero_ext; case (zero_ext_match a); intros; InvEval; subst.
+- TrivialExists.
+- TrivialExists.
+- destruct (zlt (Int.unsigned a0) sz).
++ econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a32_range; simpl.
+  apply Val.lessdef_same. f_equal. rewrite Int.shl_zero_ext by omega. f_equal. omega.
++ TrivialExists.
+- TrivialExists.
+Qed.
+
+Theorem eval_sign_ext:
+  forall sz, 0 < sz -> unary_constructor_sound (sign_ext sz) (Val.sign_ext sz).
+Proof.
+  intros; red; intros until x; unfold sign_ext; case (sign_ext_match a); intros; InvEval; subst.
+- TrivialExists.
+- TrivialExists.
+- destruct (zlt (Int.unsigned a0) sz).
++ econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a32_range; simpl.
+  apply Val.lessdef_same. f_equal. rewrite Int.shl_sign_ext by omega. f_equal. omega.
++ TrivialExists.
+- TrivialExists.
+Qed.
+
+Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
+Proof.
+  apply eval_sign_ext; omega. 
+Qed.
+
+Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
+Proof.
+  apply eval_zero_ext; omega.
+Qed.
+
+Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
+Proof.
+  apply eval_sign_ext; omega. 
+Qed.
+
+Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
+Proof.
+  apply eval_zero_ext; omega.
+Qed.
+
+(** Bitwise not, and, or, xor *)
+
+Theorem eval_notint: unary_constructor_sound notint Val.notint.
+Proof.
+  assert (INV: forall v, Val.lessdef (Val.notint (Val.notint v)) v).
+  { destruct v; auto. simpl; rewrite Int.not_involutive; auto. } 
+  unfold notint; red; intros until x; case (notint_match a); intros; InvEval; subst.
+- TrivialExists.
+- TrivialExists.
+- exists v1; auto.
+- exists (eval_shift s v1 a0); split; auto. EvalOp.
+- econstructor; split. EvalOp. 
+  destruct v1; simpl; auto; destruct v0; simpl; auto.
+  rewrite Int.not_and_or_not, Int.not_involutive, Int.or_commut. auto.
+- econstructor; split. EvalOp. 
+  destruct v1; simpl; auto; destruct v0; simpl; auto.
+  rewrite Int.not_or_and_not, Int.not_involutive, Int.and_commut. auto.
+- econstructor; split. EvalOp. 
+  rewrite ! Val.not_xor, Val.xor_assoc; auto.
+- econstructor; split. EvalOp.
+  destruct v1; simpl; auto; destruct v0; simpl; auto.
+  unfold Int.not; rewrite ! Int.xor_assoc, Int.xor_idem, Int.xor_zero. auto.
+- TrivialExists.
+Qed.
+
+Lemma eval_andimm_base:
+  forall n, unary_constructor_sound (andimm_base n) (fun x => Val.and x (Vint n)).
+Proof.
+  intros; red; intros. unfold andimm_base.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  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.
+  exists x; split; auto.
+  subst. destruct x; simpl; auto. rewrite Int.and_mone; auto.
+  destruct (Z_is_power2m1 (Int.unsigned n)) as [s|] eqn:P.
+  assert (0 <= s) by (eapply Z_is_power2m1_nonneg; eauto).
+  rewrite <- (Int.repr_unsigned n), (Z_is_power2m1_sound _ _ P), <- Val.zero_ext_and by auto.
+  apply eval_zero_ext; auto.
+  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.
+  case (andimm_match a); intros; InvEval; subst.
+- rewrite Int.and_commut; TrivialExists.
+- rewrite Val.and_assoc, Int.and_commut. apply eval_andimm_base; auto.
+- destruct (zle 0 s).
++ rewrite Val.zero_ext_and, Val.and_assoc, Int.and_commut by auto. 
+  apply eval_andimm_base; auto.
++ apply eval_andimm_base. EvalOp.
+- apply eval_andimm_base; auto.
+Qed.
+
+Theorem eval_and: binary_constructor_sound and Val.and.
+Proof.
+  red; intros until y; unfold and; case (and_match a b); intros; InvEval; subst.
+- rewrite Val.and_commut; apply eval_andimm; auto.
+- apply eval_andimm; auto.
+- rewrite Val.and_commut; TrivialExists.
+- TrivialExists.
+- rewrite Val.and_commut; TrivialExists.
+- TrivialExists.
+- rewrite Val.and_commut; TrivialExists.
+- TrivialExists.
+- 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; subst.
+- rewrite Int.or_commut; TrivialExists.
+- rewrite Val.or_assoc, Int.or_commut; TrivialExists.
+- 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. destruct a1; try discriminate. destruct a2; try discriminate.
+  simpl in H; destruct (ident_eq i i0); inv H.
+  split. auto. inv H0; inv H1; congruence.
+Qed.
+
+Theorem eval_or: binary_constructor_sound or Val.or.
+Proof.
+  red; intros until y; unfold or; case (or_match a b); intros; InvEval; subst.
+- rewrite Val.or_commut. apply eval_orimm; auto.
+- apply eval_orimm; auto.
+- rewrite Val.or_commut; TrivialExists.
+- TrivialExists.
+- rewrite Val.or_commut; TrivialExists.
+- TrivialExists.
+- (* shl - shru *)
+  destruct (Int.eq (Int.add a1 a2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
++ InvBooleans. apply Int.same_if_eq in H.
+  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
+  econstructor; split. EvalOp.
+  destruct v0; simpl; auto. rewrite ! a32_range. simpl. rewrite <- Int.or_ror; auto using a32_range.
++ TrivialExists.
+- (* shru - shl *)
+  destruct (Int.eq (Int.add a2 a1) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
++ InvBooleans. apply Int.same_if_eq in H.
+  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
+  econstructor; split. EvalOp.
+  destruct v0; simpl; auto. rewrite ! a32_range. simpl.
+  rewrite Int.or_commut, <- Int.or_ror; auto using a32_range.
++ TrivialExists.
+- rewrite Val.or_commut; TrivialExists.
+- TrivialExists.
+- TrivialExists.
+Qed.
+
+Lemma eval_xorimm_base:
+  forall n, unary_constructor_sound (xorimm_base n) (fun x => Val.xor x (Vint n)).
+Proof.
+  intros; red; intros. unfold xorimm_base.
+  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. rewrite <- Val.not_xor. apply eval_notint; auto.
+  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.
+  destruct (xorimm_match a); intros; InvEval; subst.
+- rewrite Int.xor_commut; TrivialExists.
+- rewrite Val.xor_assoc; simpl. rewrite (Int.xor_commut n2). apply eval_xorimm_base; auto.
+- apply eval_xorimm_base; auto.
+Qed.
+
+Theorem eval_xor: binary_constructor_sound xor Val.xor.
+Proof.
+  red; intros until y; unfold xor; case (xor_match a b); intros; InvEval; subst.
+- rewrite Val.xor_commut; apply eval_xorimm; auto.
+- apply eval_xorimm; auto.
+- rewrite Val.xor_commut; TrivialExists.
+- TrivialExists.
+- rewrite Val.xor_commut; TrivialExists.
+- TrivialExists.
+- rewrite Val.xor_commut; TrivialExists.
+- TrivialExists.
+- TrivialExists.
+Qed.
+
+(** ** Integer division and modulus *)
+
+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; TrivialExists.
+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, mod_aux.
+  exploit Val.mods_divs; eauto. intros (q & A & B). subst z.
+  TrivialExists. repeat (econstructor; eauto with evalexpr). exact A.
+Qed.
+
+Theorem eval_divu_base:
+  forall le a x b 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; TrivialExists.
+Qed.
+
+Theorem eval_modu_base:
+  forall le a x b 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, mod_aux.
+  exploit Val.modu_divu; eauto. intros (q & A & B). subst z.
+  TrivialExists. repeat (econstructor; eauto with evalexpr). exact A.
+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.
+  change (Int.ltu Int.zero (Int.repr 31)) with true in H0; inv H0.
+  rewrite Int.shrx_zero by (compute; auto). auto.
+- TrivialExists.
+Qed.
+
+(** General shifts *)
+
+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.
+
+(** Floating-point operations *)
+
+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; InvEval; subst.
+- (* constant *)
+  rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
+- (* eq cmp *)
+  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 *)
+  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.
+- (* mask zero *)
+  predSpec Int.eq Int.eq_spec n2 Int.zero.
++ subst n2. econstructor; split. EvalOp. simpl. 
+  destruct v1; simpl; try (rewrite sem_undef; auto).
+  rewrite sem_eq. destruct (Int.eq (Int.and i m0) Int.zero); auto.
++ TrivialExists. simpl. rewrite sem_default. auto.
+- (* mask not zero *)
+  predSpec Int.eq Int.eq_spec n2 Int.zero.
++ subst n2. econstructor; split. EvalOp. simpl. 
+  destruct v1; simpl; try (rewrite sem_undef; auto).
+  rewrite sem_ne. destruct (Int.eq (Int.and i m0) Int.zero); auto.
++ TrivialExists. simpl. rewrite sem_default. 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; subst.
+- eapply eval_compimm_swap; eauto.
+  intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
+- eapply eval_compimm; eauto.
+- TrivialExists. simpl. rewrite Val.swap_cmp_bool. auto.
+- TrivialExists.
+- 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; subst.
+- eapply eval_compimm_swap; eauto.
+  intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
+- eapply eval_compimm; eauto.
+- TrivialExists. simpl. rewrite Val.swap_cmpu_bool. auto.
+- TrivialExists.
+- 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.
+
+(** Floating-point conversions *)
+
+Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
+Proof.
+  red; intros; TrivialExists.
+Qed.
+
+Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle.
+Proof.
+  red; intros; TrivialExists.
+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; TrivialExists.
+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 until y; unfold floatofint. case (floatofint_match a); intros; InvEval.
+- TrivialExists.
+- TrivialExists.
+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; TrivialExists.
+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 until y; unfold floatofintu. case (floatofintu_match a); intros; InvEval.
+- TrivialExists.
+- TrivialExists.
+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; TrivialExists.
+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 until y; unfold singleofint. case (singleofint_match a); intros; InvEval.
+- TrivialExists.
+- TrivialExists.
+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; TrivialExists.
+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 until y; unfold singleofintu. case (singleofintu_match a); intros; InvEval.
+- TrivialExists.
+- TrivialExists.
+Qed.
+
+(** Selection *)
+
+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.
+  destruct (match ty with Tint | Tlong | Tfloat | Tsingle => true | _ => false end); inv H.
+  rewrite <- H3; TrivialExists. 
+Qed.
+
+(** Addressing modes *)
+
+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.
+- econstructor; split. EvalOp. simpl; auto.
+- econstructor; split. EvalOp. simpl; auto.
+- econstructor; split. EvalOp. simpl. 
+  destruct v1; try discriminate. rewrite <- H; auto.
+- econstructor; split. EvalOp. simpl. congruence.
+- econstructor; split. EvalOp. simpl. congruence.
+- econstructor; split. EvalOp. simpl. congruence.
+- econstructor; split. EvalOp. simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero; auto.
+Qed.
+
+(** Builtins *)
+
+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.
+- constructor.
+- constructor.
+- constructor.
+- inv H. InvEval. simpl in H6. inv H6. constructor; auto.
+- subst v. repeat constructor; auto.
+- constructor; auto. 
+Qed.
+
+(** Platform-specific known builtins *)
+
+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.
+  intros. discriminate.
+Qed.
+
+End CMCONSTR.