Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed

1 files changed, 0 insertions, 1093 deletions

diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
deleted file mode 100644
index ce80fc57..00000000
--- a/riscV/SelectOpproof.v
+++ /dev/null
@@ -1,1093 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*           Prashanth Mundkur, SRI International                      *)
-(*                                                                     *)
-(*  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.     *)
-(*                                                                     *)
-(*  The contributions by Prashanth Mundkur are reused and adapted      *)
-(*  under the terms of a Contributor License Agreement between         *)
-(*  SRI International and INRIA.                                       *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Correctness of instruction selection for operators *)
-
-Require Import Coqlib Zbits.
-Require Import AST Integers Floats.
-Require Import Values Memory Builtins Globalenvs.
-Require Import Cminor Op CminorSel.
-Require Import SelectOp.
-Require Import OpHelpers.
-Require Import OpHelpersproof.
-Require Import Lia.
-
-Local Open Scope cminorsel_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.
-
-(** 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:
-  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.
-    destruct Archi.ptr64; auto. rewrite Ptrofs.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.
-      destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto.
-    + econstructor; split. EvalOp. simpl; eauto. 
-      destruct sp; simpl; auto. destruct Archi.ptr64; auto. 
-      rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut m0). auto.
-    + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
-    + TrivialExists.
-Qed.
-
-Theorem eval_add: binary_constructor_sound add Val.add.
-Proof.
-  red; intros until y.
-  unfold add; case (add_match a b); intros; InvEval.
-  - rewrite 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.
-    destruct Archi.ptr64 eqn:SF; auto. 
-    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. 
-    rewrite (Ptrofs.add_commut (Ptrofs.of_int n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
-  - subst. econstructor; split.
-    EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
-    destruct sp; simpl; auto.
-    destruct v1; simpl; auto.
-    destruct Archi.ptr64 eqn:SF; auto. 
-    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
-    rewrite Ptrofs.add_commut. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; 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.
-  - 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.
-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; simpl.
-  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.
-  - 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; simpl.
-  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.
-  - 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. auto.
-  - 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. auto.
-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 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 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.
-  - TrivialExists.
-Qed.
-
-Theorem eval_and: binary_constructor_sound and Val.and.
-Proof.
-  red; intros until y; unfold and; case (and_match a b); intros; InvEval.
-  - rewrite Val.and_commut. apply eval_andimm; auto.
-  - apply eval_andimm; auto.
-  - TrivialExists.
-Qed.
-
-Theorem eval_orimm:
-  forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)).
-Proof.
-  intros; red; intros until x. unfold orimm.
-
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  intros. 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.
-  - TrivialExists.
-Qed.
-
-Theorem eval_or: binary_constructor_sound or Val.or.
-Proof.
-  red; intros until y; unfold or; case (or_match a b); intros; InvEval.
-  - rewrite Val.or_commut. apply eval_orimm; auto.
-  - apply eval_orimm; 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.
-
-  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.
-
-  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 H0, 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.
-  unfold notint; red; intros. rewrite Val.not_xor. apply eval_xorimm; auto.
-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. exists z; split. EvalOp.
-  2: apply Val.lessdef_refl.
-  cbn.
-  rewrite H1.
-  cbn.
-  trivial.
-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. exists z; split. EvalOp.
-  2: apply Val.lessdef_refl.
-  cbn.
-  rewrite H1.
-  cbn.
-  trivial.
-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. exists z; split. EvalOp.
-  2: apply Val.lessdef_refl.
-  cbn.
-  rewrite H1.
-  cbn.
-  trivial.
-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. exists z; split. EvalOp.
-  2: apply Val.lessdef_refl.
-  cbn.
-  rewrite H1.
-  cbn.
-  trivial.
-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.
-  cbn.
-  rewrite H0.
-  cbn.
-  reflexivity.
-  apply Val.lessdef_refl.
-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. omega.
-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. omega.
-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.
-  cbn. 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.
-  cbn. 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 until y; unfold floatofintu. case (floatofintu_match a); intros.
-  InvEval. simpl in H0. TrivialExists.
-  TrivialExists.
-  cbn. rewrite H0. 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 until y; unfold floatofint. case (floatofint_match a); intros.
-  InvEval. simpl in H0. TrivialExists.
-  TrivialExists.
-  cbn. rewrite H0. 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.
-  cbn. 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.
-  cbn. 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.
-  cbn. 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.
-  cbn. 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.
-
-Lemma mod_small_negative:
-  forall a modulus,
-    modulus > 0 -> -modulus < a < 0 -> a mod modulus = a + modulus.
-Proof.
-  intros.
-  replace (a mod modulus) with ((a + modulus) mod modulus).
-  apply Z.mod_small.
-  lia.
-  rewrite <- Zplus_mod_idemp_r.
-  rewrite Z.mod_same by lia.
-  rewrite Z.add_0_r.
-  reflexivity.
-Qed.
-
-Remark normalize_low_long: forall
-  (PTR64 : Archi.ptr64 = true) v1,
-    Val.loword (Val.normalize (Val.longofint v1) Tlong) = Val.normalize v1 Tint.
-Proof.
-  intros.
-  destruct v1; cbn; try rewrite PTR64; trivial.
-  f_equal.
-  unfold Int64.loword.
-  unfold Int.signed.
-  destruct zlt.
-  { rewrite Int64.int_unsigned_repr.
-    apply Int.repr_unsigned.
-  }
-  pose proof (Int.unsigned_range i).
-  rewrite Int64.unsigned_repr_eq.
-  replace ((Int.unsigned i - Int.modulus) mod Int64.modulus)
-    with (Int64.modulus + Int.unsigned i - Int.modulus).
-  {
-    rewrite <- (Int.repr_unsigned i) at 2.
-    apply Int.eqm_samerepr.
-    unfold Int.eqm, eqmod.
-    change Int.modulus with 4294967296 in *.
-    change Int64.modulus with 18446744073709551616 in *.
-    exists 4294967295.
-    lia.
-  }
-  { rewrite mod_small_negative.
-    lia.
-    constructor.
-    constructor.
-    change Int.modulus with 4294967296 in *.
-    change Int.half_modulus with 2147483648 in *.
-    change Int64.modulus with 18446744073709551616 in *.
-    lia.
-    lia.
-  }
-Qed.
-
-Lemma same_expr_pure_correct:
-  forall le a1 a2 v1 v2
-    (PURE : same_expr_pure a1 a2 = true)
-    (EVAL1 : eval_expr ge sp e m le a1 v1)
-    (EVAL2 : eval_expr ge sp e m le a2 v2),
-    v1 = v2.
-Proof.
-  intros.
-  destruct a1; destruct a2; cbn in *; try discriminate.
-  inv EVAL1. inv EVAL2.
-  destruct (ident_eq i i0); congruence.
-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.
-  pose proof (same_expr_pure_correct le a1 a2 v1 v2) as PURE.
-  destruct (same_expr_pure a1 a2).
-  { rewrite <- PURE by auto.
-    inv H.
-    exists v1. split. assumption.
-    unfold Val.select.
-    destruct b; apply Val.lessdef_normalize.
-  }
-  clear PURE.
-  destruct Archi.ptr64 eqn:PTR64.
-  2: discriminate.
-  destruct ty; cbn in *; try discriminate.
-  - (* Tint *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
-      * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
-        
-  - (* Tfloat *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true.
-        apply ExtValues.float_bits_normalize.
-      * rewrite ExtValues.select01_long_false.
-        apply ExtValues.float_bits_normalize.
-
-  - (* Tlong *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true. reflexivity.
-      * rewrite ExtValues.select01_long_false. reflexivity.
-
-  - (* Tsingle *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true.
-        rewrite normalize_low_long by assumption.
-        apply ExtValues.single_bits_normalize.
-      * rewrite ExtValues.select01_long_false.
-        rewrite normalize_low_long by assumption.
-        apply ExtValues.single_bits_normalize.
-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 (Archi.pic_code tt).
-  + 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. destruct Archi.ptr64 eqn:SF; inv H. 
-    simpl. auto.
-  - exists (v1 :: nil); split. eauto with evalexpr. simpl.
-    destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
-    simpl. auto.
-  - 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.
-  rewrite SF; auto.
-+ constructor; auto.
-- constructor; auto.
-Qed.
-
-(* floating-point division without HELPERS *)
-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.
-  TrivialExists.
-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.
-  TrivialExists.
-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.
-  destruct bf; intros until le; intro Heval.
-  all: try (inversion Heval; subst a; clear Heval;
-       exists v; split; trivial;
-       repeat (try econstructor; try eassumption)).
-Qed.
-
-End CMCONSTR.