diff options
Diffstat (limited to 'ia32/SelectOpproof.v')
| -rw-r--r-- | ia32/SelectOpproof.v | 935 |
1 files changed, 935 insertions, 0 deletions
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v new file mode 100644 index 0000000..59fed01 --- /dev/null +++ b/ia32/SelectOpproof.v @@ -0,0 +1,935 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* 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. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Cminor. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +Section CMCONSTR. + +Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. + +(** * 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 TrivialOp cstr := unfold cstr; intros; EvalOp. + +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 *) + +(** 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: +- 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. +*) + +Theorem eval_addrsymbol: + forall le id ofs b, + Genv.find_symbol ge id = Some b -> + eval_expr ge sp e m le (addrsymbol id ofs) (Vptr b ofs). +Proof. + intros. unfold addrsymbol. econstructor. constructor. + simpl. rewrite H. auto. +Qed. + +Theorem eval_addrstack: + forall le ofs b n, + sp = Vptr b n -> + eval_expr ge sp e m le (addrstack ofs) (Vptr b (Int.add n ofs)). +Proof. + intros. unfold addrstack. econstructor. constructor. + simpl. unfold offset_sp. rewrite H. auto. +Qed. + +Lemma eval_notbool_base: + forall le a v b, + eval_expr ge sp e m le a v -> + Val.bool_of_val v b -> + eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)). +Proof. + TrivialOp notbool_base. simpl. + inv H0. + rewrite Int.eq_false; auto. + rewrite Int.eq_true; auto. + reflexivity. +Qed. + +Hint Resolve Val.bool_of_true_val Val.bool_of_false_val + Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof. + +Theorem eval_notbool: + forall le a v b, + eval_expr ge sp e m le a v -> + Val.bool_of_val v b -> + eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)). +Proof. + induction a; simpl; intros; try (eapply eval_notbool_base; eauto). + destruct o; try (eapply eval_notbool_base; eauto). + + destruct e0. InvEval. + inv H0. rewrite Int.eq_false; auto. + simpl; eauto with evalexpr. + rewrite Int.eq_true; simpl; eauto with evalexpr. + eapply eval_notbool_base; eauto. + + inv H. eapply eval_Eop; eauto. + simpl. assert (eval_condition c vl = Some b). + generalize H6. simpl. + case (eval_condition c vl); intros. + destruct b0; inv H1; inversion H0; auto; congruence. + congruence. + rewrite (Op.eval_negate_condition _ _ H). + destruct b; reflexivity. + + inv H. eapply eval_Econdition; eauto. + destruct v1; eauto. +Qed. + +Lemma eval_offset_addressing: + forall addr n args v, + eval_addressing ge sp addr args = Some v -> + eval_addressing ge sp (offset_addressing addr n) args = Some (Val.add v (Vint n)). +Proof. + intros. destruct addr; simpl in *; FuncInv; subst; simpl. + rewrite Int.add_assoc. auto. + rewrite Int.add_assoc. auto. + rewrite <- Int.add_assoc. auto. + rewrite <- Int.add_assoc. auto. + rewrite <- Int.add_assoc. auto. + rewrite <- Int.add_assoc. auto. + rewrite <- Int.add_assoc. decEq. decEq. repeat rewrite Int.add_assoc. auto. + decEq. decEq. repeat rewrite Int.add_assoc. auto. + destruct (Genv.find_symbol ge i); inv H. auto. + destruct (Genv.find_symbol ge i); inv H. simpl. + repeat rewrite Int.add_assoc. decEq. decEq. decEq. apply Int.add_commut. + destruct (Genv.find_symbol ge i0); inv H. simpl. + repeat rewrite Int.add_assoc. decEq. decEq. decEq. apply Int.add_commut. + unfold offset_sp in *. destruct sp; inv H. simpl. rewrite Int.add_assoc. auto. +Qed. + +Theorem eval_addimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)). +Proof. + unfold addimm; intros until x. + generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. + subst n. rewrite Int.add_zero. auto. + case (addimm_match a); intros; InvEval. + EvalOp. simpl. rewrite Int.add_commut. auto. + inv H0. EvalOp. simpl. rewrite (eval_offset_addressing _ _ _ _ H6). auto. + EvalOp. +Qed. + +Theorem eval_addimm_ptr: + forall le n a b ofs, + eval_expr ge sp e m le a (Vptr b ofs) -> + eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)). +Proof. + unfold addimm; intros until ofs. + generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. + subst n. rewrite Int.add_zero. auto. + case (addimm_match a); intros; InvEval. + inv H0. EvalOp. simpl. rewrite (eval_offset_addressing _ _ _ _ H6). auto. + EvalOp. +Qed. + +Theorem eval_add: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (add a b) (Vint (Int.add x y)). +Proof. + intros until y. + unfold add; case (add_match a b); intros; InvEval. + rewrite Int.add_commut. apply eval_addimm. auto. + apply eval_addimm. auto. + subst. EvalOp. simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. + subst. EvalOp. simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. + subst. EvalOp. simpl. decEq. decEq. + rewrite Int.add_permut. rewrite Int.add_assoc. decEq. apply Int.add_permut. + destruct (Genv.find_symbol ge id); inv H0. + destruct (Genv.find_symbol ge id); inv H0. + destruct (Genv.find_symbol ge id); inv H0. + destruct (Genv.find_symbol ge id); inv H0. + subst. EvalOp. simpl. rewrite Int.add_commut. auto. + subst. EvalOp. + subst. EvalOp. simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + subst. EvalOp. simpl. decEq. decEq. apply Int.add_assoc. + EvalOp. simpl. rewrite Int.add_zero. auto. +Qed. + +Theorem eval_add_ptr: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)). +Proof. + intros until y. unfold add; case (add_match a b); intros; InvEval. + apply eval_addimm_ptr; auto. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. + destruct (Genv.find_symbol ge id); inv H0. + subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. + decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut. + subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. + decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut. + subst. EvalOp. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. auto. + EvalOp; simpl. rewrite Int.add_zero. auto. +Qed. + +Theorem eval_add_ptr_2: + forall le a b x p y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vptr p y) -> + eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)). +Proof. + intros until y. unfold add; case (add_match a b); intros; InvEval. + apply eval_addimm_ptr; auto. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. + rewrite (Int.add_commut n1 n2). apply Int.add_permut. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. + rewrite (Int.add_commut n1 n2). apply Int.add_permut. + subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. + decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut. + destruct (Genv.find_symbol ge id); inv H0. + subst. EvalOp; simpl. destruct (Genv.find_symbol ge id); inv H0. + decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut. + subst. EvalOp. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. auto. + subst. EvalOp; simpl. decEq. decEq. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + EvalOp; simpl. rewrite Int.add_zero. auto. +Qed. + +Theorem eval_sub: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). +Proof. + intros until y. + unfold sub; case (sub_match a b); intros; InvEval. + rewrite Int.sub_add_opp. + apply eval_addimm. assumption. + replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). + apply eval_addimm. EvalOp. + subst x; subst y. + repeat rewrite Int.sub_add_opp. + repeat rewrite Int.add_assoc. decEq. + rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. + replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + apply eval_addimm. EvalOp. + subst x. rewrite Int.sub_add_l. auto. + replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + apply eval_addimm. EvalOp. + subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. + EvalOp. +Qed. + +Theorem eval_sub_ptr_int: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)). +Proof. + intros until y. + unfold sub; case (sub_match a b); intros; InvEval. + rewrite Int.sub_add_opp. + apply eval_addimm_ptr. assumption. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). + apply eval_addimm_ptr. EvalOp. + subst x; subst y. + repeat rewrite Int.sub_add_opp. + repeat rewrite Int.add_assoc. decEq. + rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + apply eval_addimm_ptr. EvalOp. + subst x. rewrite Int.sub_add_l. auto. + replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + apply eval_addimm_ptr. EvalOp. + subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. + EvalOp. +Qed. + +Theorem eval_sub_ptr_ptr: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vptr p y) -> + eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). +Proof. + intros until y. + unfold sub; case (sub_match a b); intros; InvEval. + replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). + apply eval_addimm. EvalOp. + simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto. + subst x; subst y. + repeat rewrite Int.sub_add_opp. + repeat rewrite Int.add_assoc. decEq. + rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + apply eval_addimm. EvalOp. + simpl. unfold eq_block. rewrite zeq_true. auto. + subst x. rewrite Int.sub_add_l. auto. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + apply eval_addimm. EvalOp. + simpl. unfold eq_block. rewrite zeq_true. auto. + subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. + EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto. +Qed. + +Theorem eval_shlimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + Int.ltu n Int.iwordsize = true -> + eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). +Proof. + intros until x; unfold shlimm. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero). + intros. subst n. rewrite Int.shl_zero. auto. + case (shlimm_match a); intros. + InvEval. EvalOp. + case_eq (Int.ltu (Int.add n n1) Int.iwordsize); intros. + InvEval. revert H8. case_eq (Int.ltu n1 Int.iwordsize); intros; inv H8. + EvalOp. simpl. rewrite H2. rewrite Int.shl_shl; auto; rewrite Int.add_commut; auto. + EvalOp. simpl. rewrite H1; auto. + InvEval. subst. + destruct (shift_is_scale n). + EvalOp. simpl. decEq. decEq. + rewrite (Int.shl_mul (Int.add i n1)); auto. rewrite (Int.shl_mul n1); auto. + rewrite Int.mul_add_distr_l. auto. + EvalOp. constructor. EvalOp. simpl. eauto. constructor. simpl. rewrite H1. auto. + destruct (shift_is_scale n). + EvalOp. simpl. decEq. decEq. + rewrite Int.add_zero. symmetry. apply Int.shl_mul. + EvalOp. simpl. rewrite H1; auto. +Qed. + +Theorem eval_shruimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + Int.ltu n Int.iwordsize = true -> + eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). +Proof. + intros until x; unfold shruimm. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero). + intros. subst n. rewrite Int.shru_zero. auto. + case (shruimm_match a); intros. + InvEval. EvalOp. + case_eq (Int.ltu (Int.add n n1) Int.iwordsize); intros. + InvEval. revert H8. case_eq (Int.ltu n1 Int.iwordsize); intros; inv H8. + EvalOp. simpl. rewrite H2. rewrite Int.shru_shru; auto; rewrite Int.add_commut; auto. + EvalOp. simpl. rewrite H1; auto. + EvalOp. simpl. rewrite H1; auto. +Qed. + +Theorem eval_shrimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + Int.ltu n Int.iwordsize = true -> + eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)). +Proof. + intros until x; unfold shrimm. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero). + intros. subst n. rewrite Int.shr_zero. auto. + case (shrimm_match a); intros. + InvEval. EvalOp. + case_eq (Int.ltu (Int.add n n1) Int.iwordsize); intros. + InvEval. revert H8. case_eq (Int.ltu n1 Int.iwordsize); intros; inv H8. + EvalOp. simpl. rewrite H2. rewrite Int.shr_shr; auto; rewrite Int.add_commut; auto. + EvalOp. simpl. rewrite H1; auto. + EvalOp. simpl. rewrite H1; auto. +Qed. + +Lemma eval_mulimm_base: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)). +Proof. + intros; unfold mulimm_base. + generalize (Int.one_bits_decomp n). + generalize (Int.one_bits_range n). + destruct (Int.one_bits n). + intros. EvalOp. + destruct l. + intros. rewrite H1. simpl. + rewrite Int.add_zero. rewrite <- Int.shl_mul. + apply eval_shlimm. auto. auto with coqlib. + destruct l. + intros. apply eval_Elet with (Vint x). auto. + rewrite H1. simpl. rewrite Int.add_zero. + rewrite Int.mul_add_distr_r. + apply eval_add. + rewrite <- Int.shl_mul. apply eval_shlimm. constructor. auto. auto with coqlib. + rewrite <- Int.shl_mul. apply eval_shlimm. constructor. auto. auto with coqlib. + intros. EvalOp. +Qed. + +Theorem eval_mulimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)). +Proof. + intros until x; unfold mulimm. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. + subst n. rewrite Int.mul_zero. intros. EvalOp. + generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro. + subst n. rewrite Int.mul_one. auto. + case (mulimm_match a); intros; InvEval. + EvalOp. rewrite Int.mul_commut. reflexivity. + subst. rewrite Int.mul_add_distr_l. + rewrite (Int.mul_commut n n2). apply eval_addimm. apply eval_mulimm_base. auto. + apply eval_mulimm_base. assumption. +Qed. + +Theorem eval_mul: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)). +Proof. + intros until y. + unfold mul; case (mul_match a b); intros; InvEval. + rewrite Int.mul_commut. apply eval_mulimm. auto. + apply eval_mulimm. auto. + EvalOp. +Qed. + +Lemma eval_orimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (orimm n a) (Vint (Int.or x n)). +Proof. + intros. unfold orimm. + predSpec Int.eq Int.eq_spec n Int.zero. + subst n. rewrite Int.or_zero. auto. + predSpec Int.eq Int.eq_spec n Int.mone. + subst n. rewrite Int.or_mone. EvalOp. + EvalOp. +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. + +Theorem eval_or: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (or a b) (Vint (Int.or x y)). +Proof. + intros until y; unfold or; case (or_match a b); intros; InvEval. + + rewrite Int.or_commut. apply eval_orimm; auto. + apply eval_orimm; auto. + + revert H7; case_eq (Int.ltu n1 Int.iwordsize); intros; inv H7. + revert H6; case_eq (Int.ltu n2 Int.iwordsize); intros; inv H6. + caseEq (Int.eq (Int.add n1 n2) Int.iwordsize + && same_expr_pure t1 t2); intro. + destruct (andb_prop _ _ H1). + generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H4; intros. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. + EvalOp. simpl. rewrite H0. rewrite <- Int.or_ror; auto. + EvalOp. econstructor. EvalOp. simpl. rewrite H; eauto. + econstructor. EvalOp. simpl. rewrite H0; eauto. constructor. + simpl. auto. + + revert H7; case_eq (Int.ltu n2 Int.iwordsize); intros; inv H7. + revert H6; case_eq (Int.ltu n1 Int.iwordsize); intros; inv H6. + caseEq (Int.eq (Int.add n1 n2) Int.iwordsize + && same_expr_pure t1 t2); intro. + destruct (andb_prop _ _ H1). + generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H4; intros. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. + EvalOp. simpl. rewrite H. rewrite Int.or_commut. rewrite <- Int.or_ror; auto. + EvalOp. econstructor. EvalOp. simpl. rewrite H; eauto. + econstructor. EvalOp. simpl. rewrite H0; eauto. constructor. + simpl. auto. + + EvalOp. +Qed. + +Lemma eval_andimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)). +Proof. + intros. unfold andimm. + predSpec Int.eq Int.eq_spec n Int.zero. + subst n. rewrite Int.and_zero. EvalOp. + predSpec Int.eq Int.eq_spec n Int.mone. + subst n. rewrite Int.and_mone. auto. + EvalOp. +Qed. + +Theorem eval_and: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (and a b) (Vint (Int.and x y)). +Proof. + intros until y; unfold and. case (mul_match a b); intros. + InvEval. rewrite Int.and_commut. apply eval_andimm; auto. + InvEval. apply eval_andimm; auto. + EvalOp. +Qed. + +Lemma eval_xorimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (xorimm n a) (Vint (Int.xor x n)). +Proof. + intros. unfold xorimm. + predSpec Int.eq Int.eq_spec n Int.zero. + subst n. rewrite Int.xor_zero. auto. + EvalOp. +Qed. + +Theorem eval_xor: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)). +Proof. + intros until y; unfold xor. case (mul_match a b); intros. + InvEval. rewrite Int.xor_commut. apply eval_xorimm; auto. + InvEval. apply eval_xorimm; auto. + EvalOp. +Qed. + +Theorem eval_divu: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)). +Proof. + intros; unfold divu; EvalOp. + simpl. rewrite Int.eq_false; auto. +Qed. + +Theorem eval_modu: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)). +Proof. + intros; unfold modu; EvalOp. + simpl. rewrite Int.eq_false; auto. +Qed. + +Theorem eval_divs: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)). +Proof. + TrivialOp divs. simpl. + predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. +Qed. + +Theorem eval_mods: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)). +Proof. + TrivialOp mods. simpl. + predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. +Qed. + +Theorem eval_shl: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y Int.iwordsize = true -> + eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). +Proof. + intros until y; unfold shl; case (shift_match b); intros. + InvEval. apply eval_shlimm; auto. + EvalOp. simpl. rewrite H1. auto. +Qed. + +Theorem eval_shru: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y Int.iwordsize = true -> + eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). +Proof. + intros until y; unfold shru; case (shift_match b); intros. + InvEval. apply eval_shruimm; auto. + EvalOp. simpl. rewrite H1. auto. +Qed. + +Theorem eval_shr: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y Int.iwordsize = true -> + eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). +Proof. + intros until y; unfold shr; case (shift_match b); intros. + InvEval. apply eval_shrimm; auto. + EvalOp. simpl. rewrite H1. auto. +Qed. + +Theorem eval_comp_int: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x y)). +Proof. + intros until y. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. +Qed. + +Remark eval_compare_null_transf: + forall c x v, + Cminor.eval_compare_null c x = Some v -> + match eval_compare_null c x with + | Some true => Some Vtrue + | Some false => Some Vfalse + | None => None (A:=val) + end = Some v. +Proof. + unfold Cminor.eval_compare_null, eval_compare_null; intros. + destruct (Int.eq x Int.zero); try discriminate. + destruct c; try discriminate; auto. +Qed. + +Theorem eval_comp_ptr_int: + forall le c a x1 x2 b y v, + eval_expr ge sp e m le a (Vptr x1 x2) -> + eval_expr ge sp e m le b (Vint y) -> + Cminor.eval_compare_null c y = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until v. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. apply eval_compare_null_transf; auto. + EvalOp. simpl. apply eval_compare_null_transf; auto. +Qed. + +Remark eval_compare_null_swap: + forall c x, + Cminor.eval_compare_null (swap_comparison c) x = + Cminor.eval_compare_null c x. +Proof. + intros. unfold Cminor.eval_compare_null. + destruct (Int.eq x Int.zero). destruct c; auto. auto. +Qed. + +Theorem eval_comp_int_ptr: + forall le c a x b y1 y2 v, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vptr y1 y2) -> + Cminor.eval_compare_null c x = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until v. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. apply eval_compare_null_transf. + rewrite eval_compare_null_swap; auto. + EvalOp. simpl. apply eval_compare_null_transf. auto. +Qed. + +Theorem eval_comp_ptr_ptr: + forall le c a x1 x2 b y1 y2, + eval_expr ge sp e m le a (Vptr x1 x2) -> + eval_expr ge sp e m le b (Vptr y1 y2) -> + x1 = y1 -> + eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). +Proof. + intros until y2. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. subst y1. rewrite dec_eq_true. + destruct (Int.cmp c x2 y2); reflexivity. +Qed. + +Theorem eval_comp_ptr_ptr_2: + forall le c a x1 x2 b y1 y2 v, + eval_expr ge sp e m le a (Vptr x1 x2) -> + eval_expr ge sp e m le b (Vptr y1 y2) -> + x1 <> y1 -> + Cminor.eval_compare_mismatch c = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until y2. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite dec_eq_false; auto. + destruct c; simpl in H2; inv H2; auto. +Qed. + +Theorem eval_compu: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). +Proof. + intros until y. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. +Qed. + +Theorem eval_compf: + forall le c a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)). +Proof. + intros. unfold compf. EvalOp. simpl. + destruct (Float.cmp c x y); reflexivity. +Qed. + +Theorem eval_cast8signed: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v). +Proof. intros; unfold cast8signed; EvalOp. Qed. + +Theorem eval_cast8unsigned: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v). +Proof. intros; unfold cast8unsigned; EvalOp. Qed. + +Theorem eval_cast16signed: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v). +Proof. intros; unfold cast16signed; EvalOp. Qed. + +Theorem eval_cast16unsigned: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v). +Proof. intros; unfold cast16unsigned; EvalOp. Qed. + +Theorem eval_singleoffloat: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). +Proof. intros; unfold singleoffloat; EvalOp. Qed. + +Theorem eval_notint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (notint a) (Vint (Int.xor x Int.mone)). +Proof. intros; unfold notint; EvalOp. Qed. + +Theorem eval_negint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (negint a) (Vint (Int.neg x)). +Proof. intros; unfold negint; EvalOp. Qed. + +Theorem eval_negf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)). +Proof. intros; unfold negf; EvalOp. Qed. + +Theorem eval_absf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)). +Proof. intros; unfold absf; EvalOp. Qed. + +Theorem eval_intoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)). +Proof. intros; unfold intoffloat; EvalOp. Qed. + +Theorem eval_floatofint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). +Proof. intros; unfold floatofint; EvalOp. Qed. + +Theorem eval_addf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)). +Proof. intros; unfold addf; EvalOp. Qed. + +Theorem eval_subf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)). +Proof. intros; unfold subf; EvalOp. Qed. + +Theorem eval_mulf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)). +Proof. intros; unfold mulf; EvalOp. Qed. + +Theorem eval_divf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)). +Proof. intros; unfold divf; EvalOp. Qed. + +Theorem eval_intuoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)). +Proof. + intros. unfold intuoffloat. + econstructor. eauto. + set (im := Int.repr Int.half_modulus). + set (fm := Float.floatofintu im). + assert (eval_expr ge sp e m (Vfloat x :: le) (Eletvar O) (Vfloat x)). + constructor. auto. + apply eval_Econdition with (v1 := Float.cmp Clt x fm). + econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. + simpl. auto. + caseEq (Float.cmp Clt x fm); intros. + rewrite Float.intuoffloat_intoffloat_1; auto. + EvalOp. + rewrite Float.intuoffloat_intoffloat_2; auto. + fold im. apply eval_addimm. apply eval_intoffloat. apply eval_subf; auto. EvalOp. +Qed. + +Theorem eval_floatofintu: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). +Proof. + intros. unfold floatofintu. + econstructor. eauto. + set (fm := Float.floatofintu Float.ox8000_0000). + assert (eval_expr ge sp e m (Vint x :: le) (Eletvar O) (Vint x)). + constructor. auto. + apply eval_Econdition with (v1 := Int.ltu x Float.ox8000_0000). + econstructor. constructor. eauto. constructor. + simpl. auto. + caseEq (Int.ltu x Float.ox8000_0000); intros. + rewrite Float.floatofintu_floatofint_1; auto. + apply eval_floatofint; auto. + rewrite Float.floatofintu_floatofint_2; auto. + fold fm. apply eval_addf. apply eval_floatofint. + rewrite Int.sub_add_opp. apply eval_addimm; auto. + EvalOp. +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. + inv H. exists vl; auto. + exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. +Qed. + +End CMCONSTR. |