Module SelectOpproof


Correctness of instruction selection for operators

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Open Local Scope cminorsel_scope.
Require Import NormaliseSpec.
Require Import ExprEval.
Require Import Memory.


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.



Correctness of the smart constructors


Section CMCONSTR.

Variable ge: genv.
Variable sp: expr_sym.
Variable e: env.
Variable m: mem.

We now show that the code generated by "smart constructor" functions such as SelectOp.notint behaves as expected. Continuing the notint example, we show that if the expression e evaluates to some integer value Vint n, then SelectOp.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:

Definition unary_constructor_sound (cstr: expr -> expr) (sem: expr_sym -> expr_sym) : Prop :=
  forall le a x
         (EXPR: 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: expr_sym -> expr_sym -> expr_sym) : Prop :=
  forall le a x b y
         (EXPR1: eval_expr ge sp e m le a x)
         (EXPR2: 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.

Ltac TrivialExists :=
  eexists; split; [repeat (econstructor; simpl; eauto)|eauto; try solve[constructor; simpl; auto]].

Theorem eval_addrsymbol:
  forall le id ofs b' o',
    Genv.symbol_address' ge id ofs = Some (Eval (Vptr b' o')) ->
    exists v,
      eval_expr ge sp e m le (addrsymbol id ofs) v/\
      same_eval v (Eval (Vptr b' o')).
Proof.
  intros.
  unfold addrsymbol.
  destr_cond_match. destr_cond_match.
  - apply Cop.int_eq_true in Heqb0 . subst; auto.
    eexists; split.
    econstructor; eauto.
    econstructor; eauto.
    simpl. unfold Genv.symbol_address' in *. des (Genv.find_symbol ge id).
    inv H. eauto.
    unfold Genv.symbol_address' in *. des (Genv.find_symbol ge id).
  - eexists; split.
    repeat (econstructor; simpl; eauto); simpl.
    unfold Genv.symbol_address' in *. des (Genv.find_symbol ge id).
    inv H. eauto.
    unfold Genv.symbol_address' in *. des (Genv.find_symbol ge id).
    inv H. red; intros; simpl.
    rewrite Int.add_zero; auto.
  - eexists; split.
    repeat (econstructor; simpl; eauto); simpl.
    rewrite H. eauto. reflexivity.
Qed.

Theorem eval_addrstack:
  forall le ofs,
  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ same_eval (Val.add sp (Eval (Vint ofs))) v.
Proof.
  intros. unfold addrstack. econstructor; split.
  EvalOp. simpl; eauto.
  reflexivity.
Qed.

Theorem eval_notint: unary_constructor_sound notint Val.notint.
Proof.
  unfold notint; red; intros until x.
  destr; InvEval.
  - TrivialExists.
  - TrivialExists. ld.
    unfold Int.not. subst. rewrite <- Int.xor_assoc; auto.
  - TrivialExists.
Qed.

Theorem eval_addimm:
  forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Eval (Vint n))).
Proof.
  red; unfold addimm; intros until x.
  intros.
  destr; InvEval; ld.
  - eexists; split; eauto.
    apply Cop.int_eq_true in Heqb. subst.
    ld; rewrite Int.add_zero; auto.
  - destr.
    + (eexists; split; [repeat econstructor; simpl; eauto|]).
      inv EXPR. simpl in *. des vl. inv H4.
      ld. rewrite Int.add_commut; auto.
    + inv EXPR. eapply eval_offset_addressing_total in H4; eauto.
      destruct H4 as [e0 [A B]].
      intros.
      TrivialExists.
      red; intros. rewrite B. constructor.
    + 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.
  - generalize (eval_addimm n1 le t2 y EXPR2).
    intros [v [A B]].
    eexists; split; eauto.
    red; intros; specialize (B alloc em); inv B; simpl; seval; try constructor.
    rewrite Int.add_commut. auto.
  - generalize (eval_addimm n2 le t1 x EXPR1).
    intros [v [A B]].
    eexists; split; eauto.
  - eexists; split; [repeat (econstructor; simpl; eauto)|].
    subst.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    rewrite Int.add_commut; sint.
  - eexists; split; [repeat (econstructor; simpl; eauto)|].
    subst.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    rewrite Int.add_commut; sint.
  - eexists; split; [repeat (econstructor; simpl; eauto)|].
    subst.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - unfold Genv.symbol_address' in *.
    des (Genv.find_symbol ge id). inv H0.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    unfold Genv.symbol_address'. rewrite Heqo. simpl. eauto.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - unfold Genv.symbol_address' in *.
    des (Genv.find_symbol ge id). inv H0.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    unfold Genv.symbol_address'. rewrite Heqo. simpl; eauto.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - unfold Genv.symbol_address' in *.
    des (Genv.find_symbol ge id). inv H0.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    unfold Genv.symbol_address'. rewrite Heqo. simpl; eauto.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - unfold Genv.symbol_address' in *.
    des (Genv.find_symbol ge id). inv H0.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    unfold Genv.symbol_address'. rewrite Heqo. simpl; eauto.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - subst.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - subst.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    constructor; simpl; eauto.
  - subst.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - subst.
    eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    red; intros; simpl; seval; try constructor;
    apply Val.lessdef_same; sint;
    repeat (rewrite Int.add_commut; sint).
  - eexists; split; [repeat (econstructor; simpl; eauto)|]; simpl.
    red; intros; simpl; seval; try constructor;
    rewrite Int.add_zero; constructor.
Qed.

Theorem eval_sub: binary_constructor_sound sub Val.sub.
Proof.
  red; intros until y.
  unfold sub; case (sub_match a b); intros; InvEval.
  - eapply eval_addimm in EXPR1; eauto.
    destruct EXPR1 as [v [A B]].
    eexists; split; eauto.
    revert B. eapply Val.lessdef_trans; eauto.
    red; intros; simpl; seval; try constructor.
    rewrite Int.sub_add_opp; auto.
  - subst.
    assert (eval_expr ge sp e m le (Eop Osub (t1 ::: t2 ::: Enil))
                      (Val.sub v1 v0)).
    EvalOp.
    exploit eval_addimm. eexact H.
    instantiate (1:=Int.sub n1 n2).
    intros [v [A B]].
    eexists; split; eauto.
    revert B; eapply Val.lessdef_trans; eauto.
    clear.
    red; intros; simpl; seval; try constructor.
    + apply Val.lessdef_same; sint.
      rewrite ! Int.sub_add_opp.
      rewrite Int.neg_add_distr. sint.
      rewrite Int.add_commut; sint.
  - subst.
    assert (eval_expr ge sp e m le (Eop Osub (t1 ::: t2 ::: Enil))
                      (Val.sub v1 y)).
    EvalOp.
    exploit eval_addimm. eexact H.
    instantiate (1:=n1).
    intros [v [A B]].
    eexists; split; eauto.
    revert B; eapply Val.lessdef_trans; eauto.
    clear.
    red; intros; simpl; seval; try constructor.
    + apply Val.lessdef_same; sint.
      rewrite ! Int.sub_add_opp.
      sint.
  - subst.
    assert (eval_expr ge sp e m le (Eop Osub (t1 ::: t2 ::: Enil))
                      (Val.sub x v1)).
    EvalOp.
    exploit eval_addimm. eexact H.
    instantiate (1:=Int.neg n2).
    intros [v [A B]].
    eexists; split; eauto.
    revert B; eapply Val.lessdef_trans; eauto.
    clear.
    red; intros; simpl; seval; try constructor.
    + apply Val.lessdef_same; sint.
      rewrite ! Int.sub_add_opp.
      sint.
      rewrite Int.neg_add_distr; sint.
  - eexists; split; [repeat (econstructor; simpl; eauto) | ].
    constructor.
Qed.

Theorem eval_negint: unary_constructor_sound negint Val.negint.
Proof.
  red; intros until x. unfold negint. case (negint_match a); intros; InvEval.
  - eexists; split; [repeat (econstructor; simpl; eauto)|eauto].
    constructor; simpl; auto.
  - eexists; split; [repeat (econstructor; simpl; eauto)|eauto].
Qed.

Theorem eval_shlimm:
  forall n, unary_constructor_sound (fun a => shlimm a n)
                                    (fun x => Val.shl x (Eval (Vint n))).
Proof.
  red; intros until x. unfold shlimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros; subst. exists x; split; auto.
    red; intros; simpl; seval; try constructor.
    rewrite Int.shl_zero; auto.
  - destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
    + destruct (shlimm_match a) eqn:?; intros; InvEval; try (TrivialExists; subst; reflexivity).
      * TrivialExists.
        red; intros; simpl; seval; try constructor.
        destr. constructor.
      * destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?; simpl;
        TrivialExists; subst;
        red; intros; simpl; seval; try constructor. rewrite Heqb.
        repeat destr; try constructor.
        rewrite Int.shl_shl; auto.
        rewrite Int.add_commut; auto.
        rewrite Int.add_commut; auto.
      * subst. destruct (shift_is_scale n); TrivialExists; try reflexivity.
        red; intros; simpl; seval; try constructor.
        destr.
        apply Val.lessdef_same; sint.
         rewrite Int.shl_mul. rewrite Int.mul_add_distr_l.
        rewrite (Int.shl_mul n1). auto.
      * destruct (shift_is_scale n); TrivialExists; try reflexivity.
        ld. destr.
        rewrite Int.add_zero. rewrite Int.shl_mul. auto.
    + intros. TrivialExists; reflexivity.
Qed.

Theorem eval_shruimm:
  forall n, unary_constructor_sound (fun a => shruimm a n)
                                    (fun x => Val.shru x (Eval (Vint n))).
Proof.
  red; intros until x. unfold shruimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros; subst. exists x; split; auto.
    ld. destr; try constructor.
    rewrite Int.shru_zero; auto.
  - destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl;
    destruct (shruimm_match a); intros; InvEval; try solve [TrivialExists].
    + TrivialExists. ld. destr. constructor.
    + destr.
      TrivialExists. ld. destr. destr. revert Heqv; destr. inv Heqv.
      rewrite Int.shru_shru; auto. apply Val.lessdef_same; sint.
      f_equal; sint. rewrite Int.add_commut; auto.
      TrivialExists. subst. ld.
    + subst. TrivialExists.
Qed.

Theorem eval_shrimm:
  forall n, unary_constructor_sound (fun a => shrimm a n)
                                    (fun x => Val.shr x (Eval (Vint n))).
Proof.
  red; intros until x. unfold shrimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros; subst. exists x; split; auto. ld.
    rewrite Int.shr_zero; auto.
  - destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl;
    destruct (shrimm_match a); intros; InvEval; try (TrivialExists; subst; reflexivity).
    + TrivialExists. ld. destr. constructor.
    + destr; TrivialExists; subst; ld. repeat destr; try constructor.
      rewrite Int.shr_shr; auto;
      rewrite Int.add_commut; auto.
    + subst. TrivialExists.
Qed.

Lemma eval_mulimm_base:
  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Eval (Vint n))).
Proof.
  intros; red; intros; unfold mulimm_base.
  generalize (Int.one_bits_decomp n).
  generalize (Int.one_bits_range n).
  destruct (Int.one_bits n).
  - intros. TrivialExists.
  - destruct l.
    + intros. rewrite H0. simpl.
      rewrite Int.add_zero.
      exploit eval_shlimm; eauto.
      intros [v [A B]].
      eexists; split; eauto.
      revert B; eapply Val.lessdef_trans; eauto.
      ld.
      rewrite <- Int.shl_mul.
      rewrite H; auto.
    + destruct l.
      * intros. rewrite H0. simpl.
        exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. auto. intros [v1 [A1 B1]].
        exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. auto.
        intros [v2 [A2 B2]].
        exploit eval_add. eexact A1. eexact A2.
        intros [v3 [A3 B3]].
        exists v3; split. econstructor; eauto.
        revert B3; eapply Val.lessdef_trans; eauto.
        rewrite Int.add_zero.
        unfold Val.add. ldt.
        clear - H. ld. rewrite ! H; auto. simpl.
        rewrite Int.mul_add_distr_r.
        rewrite <- ! Int.shl_mul. auto.
      * intros. TrivialExists.
Qed.



Theorem eval_mulimm:
  forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Eval (Vint n))).
Proof.
  intros; red; intros until x; unfold mulimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros. exists (Eval (Vint Int.zero)); split. EvalOp.
    subst. ld.
    rewrite Int.mul_zero. auto.
  - predSpec Int.eq Int.eq_spec n Int.one.
    + intros. exists x; split; auto.
      subst n. ld. rewrite Int.mul_one. auto.
    + case (mulimm_match a); intros; InvEval.
      * TrivialExists. ld. rewrite Int.mul_commut; auto.
      * subst.
        exploit eval_mulimm_base. eexact H5.
        intros [v' [A1 B1]].
        exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v').
        eauto.
        intros [v'' [A2 B2]].
        exists v''; split; auto.
        revert B2; eapply Val.lessdef_trans; auto.
        unfold Val.add. ldt.
        ld.
        rewrite Int.mul_add_distr_l. rewrite (Int.mul_commut n n2); 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.
  - exploit eval_mulimm. eauto. intros [v [A B]].
    eexists; split. eauto. ldt. ld.
    rewrite Int.mul_commut. auto.
  - apply eval_mulimm. eauto.
  - TrivialExists.
Qed.

Theorem eval_andimm:
  forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Eval (Vint n))).
Proof.
  intros; red; intros until x. unfold andimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros. TrivialExists. subst. ld.
    rewrite Int.and_zero. auto.
  - predSpec Int.eq Int.eq_spec n Int.mone.
    + intros. exists x; split; auto.
      subst n. ld. rewrite Int.and_mone. auto.
    + case (andimm_match a); intros; InvEval; try TrivialExists; ld.
      * rewrite Int.and_commut; auto.
      * rewrite Int.and_assoc. rewrite (Int.and_commut n). auto.
      * rewrite Int.zero_ext_and. rewrite Int.and_assoc.
        rewrite (Int.and_commut n). auto. omega.
      * rewrite Int.zero_ext_and by omega. rewrite Int.and_assoc.
        rewrite (Int.and_commut n). 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.
  - exploit eval_andimm. eauto. intros [v [A B]].
    eexists; split; eauto. ldt. ld. rewrite Int.and_commut. auto.
  - apply eval_andimm; auto.
  - TrivialExists.
Qed.

Theorem eval_orimm:
  forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Eval (Vint n))).
Proof.
  intros; red; intros until x. unfold orimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros. eexists; split; eauto. ld. rewrite Int.or_zero. auto.
  - predSpec Int.eq Int.eq_spec n Int.mone.
    + intros. exists (Eval (Vint Int.mone)); split. EvalOp.
      subst n. ld.
      rewrite Int.or_mone. auto.
    + destruct (orimm_match a); intros; InvEval.
      * TrivialExists. ld. rewrite Int.or_commut; auto.
      * subst. TrivialExists. ld. rewrite Int.or_assoc. rewrite (Int.or_commut n2).
        auto.
      * 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.

Remark int_add_sub_eq:
  forall x y z, Int.add x y = z -> Int.sub z x = y.
Proof.
  intros. subst z. rewrite Int.sub_add_l. rewrite Int.sub_idem. apply Int.add_zero_l.
Qed.

Lemma eval_or: binary_constructor_sound or Val.or.
Proof.
  red; intros until y; unfold or; case (or_match a b); intros.
  -
    InvEval. exploit eval_orimm. eauto.
    intros [v [A B]]. eexists; split; eauto. ldt. ld.
    rewrite Int.or_commut; auto.
  - InvEval. apply eval_orimm; auto.
  -
    predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
    + destruct (same_expr_pure t1 t2) eqn:?.
      * InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
        TrivialExists.
        ld. repeat destr; try constructor.
        rewrite <- Int.or_ror; auto.
      * InvEval. TrivialExists. subst. ld.
        erewrite ! int_add_sub_eq; eauto.
    + simpl. TrivialExists.
  -
    predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
    destruct (same_expr_pure t1 t2) eqn:?.
    + InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
      TrivialExists.
      ld. repeat destr; try constructor.
      rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
    + InvEval. TrivialExists. subst.
      erewrite int_add_sub_eq; eauto. ld; destr; try constructor.
      destr; try constructor.
      rewrite Int.or_commut; auto.
    + TrivialExists.
  -
    TrivialExists.
Qed.

Theorem eval_xorimm:
  forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Eval (Vint n))).
Proof.
  intros; red; intros until x. unfold xorimm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - intros. exists x; split. auto.
    subst n. ld. rewrite Int.xor_zero. auto.
  - destruct (xorimm_match a); intros; InvEval;
    TrivialExists; ld.
    + rewrite Int.xor_commut; auto.
    + rewrite Int.xor_assoc. rewrite (Int.xor_commut n); auto.
    + unfold Int.not. rewrite Int.xor_assoc. rewrite (Int.xor_commut n); 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.
  - exploit eval_xorimm. eauto.
    intros [v [A B]]. eexists; split; eauto.
    ldt. ld.
    rewrite Int.xor_commut; auto.
  - apply eval_xorimm; auto.
  - TrivialExists.
Qed.

Theorem eval_divs_base:
  binary_constructor_sound divs_base Val.divs.
Proof.
  red; intros. unfold divs_base.
  eexists; split. repeat (econstructor; simpl; eauto). auto.
Qed.

Theorem eval_divu_base:
  binary_constructor_sound divu_base Val.divu.
Proof.
  red; intros. unfold divu_base. eexists; split.
  repeat (econstructor; simpl; eauto). auto.
Qed.

Theorem eval_mods_base:
  binary_constructor_sound mods_base Val.mods.
Proof.
  red; intros. unfold mods_base. eexists; split.
  repeat (econstructor; simpl; eauto). auto.
Qed.


Theorem eval_modu_base:
  binary_constructor_sound modu_base Val.modu.
Proof.
  red; intros. unfold modu_base. eexists; split.
  repeat (econstructor; simpl; eauto). auto.
Qed.

Theorem eval_shrximm:
  forall n,
    unary_constructor_sound (fun x => shrximm x n) (fun x => Val.shrx x (Eval (Vint n))) .
Proof.
  red; intros. unfold shrximm.
  predSpec Int.eq Int.eq_spec n Int.zero.
  - subst n. exists x; split; auto.
    ld. destr; try constructor.
    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.
  - TrivialExists.
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 sg: se_signedness.
  Variable default: comparison -> int -> condition.
  Variable intsem: comparison -> int -> int -> bool.
  Variable sem: comparison -> expr_sym -> expr_sym -> expr_sym.

  Hypothesis sem_int:
    forall x y c,
      same_eval (sem c (Eval (Vint x)) (Eval (Vint y)))
                (Val.of_bool (intsem c x y)).
  
  Hypothesis sem_default:
    forall c x y ,
      same_eval (sem c x y) (Ebinop (OpCmp sg c) Tint Tint x y).

  Hypothesis default_eq:
    default = match sg with
                  SESigned => Ccompimm
                | SEUnsigned => Ccompuimm
              end.
  

  Lemma se_ld:
    forall v1 v2,
      same_eval v1 v2 ->
      Val.lessdef v1 v2.
Proof.
    intros v1 v2 A; red; intros.
    rewrite A; auto.
  Qed.
  
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 (Eval (Vint n2))) v.
Proof.
  intros until x.
  unfold compimm; des (compimm_match c a); intros.
  -
    InvEval. TrivialExists. apply se_ld. rewrite sem_int. destruct (intsem c n1 n2); simpl; reflexivity.
  -
    InvEval. inv H. simpl in H5.
    destruct (Int.eq_dec n2 Int.zero).
    + subst n2.
      generalize (eval_negate_condition c vl); rewrite H5; simpl.
      destr_cond_match; try intuition discriminate. intro A.
      TrivialExists. apply se_ld. rewrite A.
      rewrite sem_default; simpl; auto.
      red; simpl; auto.
      des sg; intros; simpl; seval;
      apply expr_no_ptr in Heqv; contradiction.
    + destr. subst.
      * TrivialExists.
        apply se_ld. rewrite sem_default.
        eapply eval_condition_cmp_one. eauto.
      * TrivialExists.
        red; intros; simpl; seval; auto;
        rewrite (sem_default Ceq x (Eval (Vint n2))) in Heqv;
        simpl in Heqv; revert Heqv; seval; des sg;
        eapply eval_condition_zero_one in Heqv; eauto;
        try des (Int.eq i0 n2); inv Heqv0;
        try des (Int.eq i n2); try constructor;
        try apply Cop.int_eq_true in Heqb; subst; try congruence.
  -
    InvEval. inv H. simpl in H5. inv H5.
    destruct (Int.eq_dec n2 Int.zero).
    + subst n2. TrivialExists.
      apply se_ld. rewrite sem_default.
      eapply eval_condition_cmp_zero; eauto.
    + destruct (Int.eq_dec n2 Int.one).
      * generalize (eval_negate_condition c vl); rewrite H0. subst n2.
        simpl. destr_cond_match; try intuition congruence. intro A.
        TrivialExists. red; intros; simpl.
        rewrite A.
        rewrite (sem_default Cne x (Eval (Vint Int.one))).
        simpl.
        des sg; seval; try constructor;
        des (Int.eq i Int.one); des (Int.eq i Int.zero);
        try apply Cop.int_eq_true in Heqb;
        try apply Cop.int_eq_true in Heqb0; subst; try congruence; auto;
        eapply eval_condition_zero_one in H0; eauto;
        destruct H0; subst; try rewrite Int.eq_true in *; try congruence.
      * TrivialExists.
        red; intros. rewrite (sem_default Cne x (Eval (Vint n2))).
        simpl.
        seval; des sg; try constructor;
        eapply eval_condition_zero_one in H0; eauto;
        destruct H0; subst;
        des (Int.eq Int.one n2); des (Int.eq Int.zero n2);
        try apply Cop.int_eq_true in Heqb;
        try apply Cop.int_eq_true in Heqb0; subst; try congruence; auto.
  -
    destruct (Int.eq_dec n2 Int.zero).
    + InvEval; subst.
      TrivialExists. apply se_ld. rewrite sem_default.
      red; simpl; auto.
      des sg; intros; simpl; seval.
    + des sg; eexists; split; repeat (econstructor; simpl; eauto);
      apply se_ld; auto; apply sem_default.
  -
    destruct (Int.eq_dec n2 Int.zero).
    + InvEval; subst.
      TrivialExists. apply se_ld. rewrite sem_default.
      red; simpl; auto. repeat destr.
      des sg; intros; simpl; seval; des (Int.eq (Int.and i n1) Int.zero).
    + inv H. inv H3. inv H6. des sg; eexists; split; repeat econstructor; simpl; eauto; apply se_ld; inv H5; apply sem_default.
  -
    des sg; eexists; split; repeat econstructor; simpl;eauto; apply se_ld; apply sem_default.
Qed.

Hypothesis sem_swap:
  forall c x y, same_eval (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 (Eval (Vint n2)) x) v.
Proof.
  intros. exploit eval_compimm. eauto.
  intros [v [A B]].
  eexists; split. eauto.
  ldt. red; intros.
  rewrite (sem_swap c x (Eval (Vint n2))).
  auto.
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 with (sg:=SESigned); eauto.
    + intros; red; simpl; auto. des (Int.cmp c0 x y0).
    + intros; red; simpl; intros; seval.
    + intros; red; simpl; intros; seval.
      rewrite Int.swap_cmp. auto.
  - eapply eval_compimm with (sg:=SESigned); eauto.
    + intros; red; simpl; auto. des (Int.cmp c0 x0 y).
    + intros; red; simpl; intros; seval.
  - TrivialExists.
Qed.

Theorem eval_compu:
  forall c, binary_constructor_sound (compu c) (Val.cmpu c).
Proof.
    intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
  - eapply eval_compimm_swap with SEUnsigned; eauto.
    + intros; red; simpl; auto. des (Int.cmpu c0 x y0).
    + intros; red; simpl; intros; seval.
    + intros; red; simpl; intros; seval.
      rewrite Int.swap_cmpu. auto.
  - eapply eval_compimm with SEUnsigned; eauto.
    + intros; red; simpl; auto. des (Int.cmpu c0 x0 y).
    + intros; red; simpl; intros; seval.
  - 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. destruct (cast8unsigned_match a); intros; InvEval.
  - TrivialExists.
  - subst.
    exploit eval_andimm. eauto.
    intros [v [A B]].
    eexists; split. eauto. ldt. ld.
    rewrite Int.zero_ext_and by omega. apply Val.lessdef_same; sint.
    rewrite Int.and_assoc; f_equal.
    rewrite Int.and_commut. auto.
  - TrivialExists.
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.
Qed.

Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
Proof.
  red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
  - TrivialExists.
  - subst.
    exploit eval_andimm. eauto.
    intros [v [A B]].
    eexists; split. eauto.
    ldt. ld.
    rewrite Int.zero_ext_and by omega. rewrite Int.and_assoc.
    rewrite (Int.and_commut n). auto.
  - TrivialExists.
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_intoffloat:
  unary_constructor_sound intoffloat Val.intoffloat.
Proof.
  red; intros; unfold intoffloat. TrivialExists.
Qed.

Theorem eval_floatofint:
  unary_constructor_sound floatofint Val.floatofint.
Proof.
  intros until x; unfold floatofint. case (floatofint_match a); intros; InvEval;
  TrivialExists.
Qed.







  
  


Theorem eval_intofsingle:
  unary_constructor_sound intofsingle Val.intofsingle.
Proof.
  intros; unfold intofsingle. TrivialExists.
Qed.

Theorem eval_singleofint:
  unary_constructor_sound singleofint Val.singleofint.
Proof.
  intros until x; unfold singleofint. case (singleofint_match a); intros; InvEval.
  TrivialExists. ld. unfold convert_t. simpl.
  rewrite Float32.of_int_double. auto.
  TrivialExists.
Qed.




Theorem eval_addressing:
  forall ge le chunk a v ,
    eval_expr ge sp e m le a v ->
    wt_expr v Tint ->
  match addressing chunk a with (mode, args) =>
    exists vl v',
    eval_exprlist ge sp e m le args vl /\
    Op.eval_addressing ge sp mode vl = Some v' /\ Val.lessdef v v'
  end.
Proof.
  intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
  - inv H. exists vl; exists v; repeat split; auto.
  - eexists; eexists; split.
    + constructor; eauto. econstructor.
    + subst; simpl. split; eauto.
      apply se_ld.
      red; simpl; intros.
      generalize (expr_type _ _ H0 cm em).
      seval.
      rewrite Int.add_zero; auto.
Qed.

End CMCONSTR.