diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /backend/Cmconstrproof.v | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) | |
download | compcert-355b4abcee015c3fae9ac5653c25259e104a886c.tar.gz compcert-355b4abcee015c3fae9ac5653c25259e104a886c.zip |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Cmconstrproof.v')
-rw-r--r-- | backend/Cmconstrproof.v | 1207 |
1 files changed, 0 insertions, 1207 deletions
diff --git a/backend/Cmconstrproof.v b/backend/Cmconstrproof.v deleted file mode 100644 index 35b3d8a0..00000000 --- a/backend/Cmconstrproof.v +++ /dev/null @@ -1,1207 +0,0 @@ -(** Correctness of the Cminor smart constructors. This file states - evaluation rules for the smart constructors, for instance that [add - a b] evaluates to [Vint(Int.add i j)] if [a] evaluates to [Vint i] - and [b] to [Vint j]. It then proves that these rules are - admissible, that is, satisfied for all possible choices of [a] and - [b]. The Cminor producer can then use these evaluation rules - (theorems) to reason about the execution of terms produced by the - smart constructors. -*) - -Require Import Coqlib. -Require Import Compare_dec. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Mem. -Require Import Events. -Require Import Op. -Require Import Globalenvs. -Require Import Cminor. -Require Import Cmconstr. - -Section CMCONSTR. - -Variable ge: Cminor.genv. - -(** * Lifting of let-bound variables *) - -Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop := - | insert_lenv_0: - forall le v, - insert_lenv le O v (v :: le) - | insert_lenv_S: - forall le p w le' v, - insert_lenv le p w le' -> - insert_lenv (v :: le) (S p) w (v :: le'). - -Lemma insert_lenv_lookup1: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p > n)%nat -> - nth_error le' n = Some v. -Proof. - induction 1; intros. - omegaContradiction. - destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. -Qed. - -Lemma insert_lenv_lookup2: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p <= n)%nat -> - nth_error le' (S n) = Some v. -Proof. - induction 1; intros. - simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. -Qed. - -Scheme eval_expr_ind_3 := Minimality for eval_expr Sort Prop - with eval_condexpr_ind_3 := Minimality for eval_condexpr Sort Prop - with eval_exprlist_ind_3 := Minimality for eval_exprlist Sort Prop. - -Hint Resolve eval_Evar eval_Eop eval_Eload eval_Estore - eval_Ecall eval_Econdition eval_Ealloc - eval_Elet eval_Eletvar - eval_CEtrue eval_CEfalse eval_CEcond - eval_CEcondition eval_Enil eval_Econs: evalexpr. - -Lemma eval_list_one: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_exprlist ge sp le e m1 (a ::: Enil) t m2 (v :: nil). -Proof. - intros. econstructor. eauto. constructor. traceEq. -Qed. - -Lemma eval_list_two: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 t, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - t = t1 ** t2 -> - eval_exprlist ge sp le e m1 (a1 ::: a2 ::: Enil) t m3 (v1 :: v2 :: nil). -Proof. - intros. econstructor. eauto. econstructor. eauto. constructor. - reflexivity. traceEq. -Qed. - -Lemma eval_list_three: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 a3 t3 m4 v3 t, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - eval_expr ge sp le e m3 a3 t3 m4 v3 -> - t = t1 ** t2 ** t3 -> - eval_exprlist ge sp le e m1 (a1 ::: a2 ::: a3 ::: Enil) t m4 (v1 :: v2 :: v3 :: nil). -Proof. - intros. econstructor. eauto. econstructor. eauto. econstructor. eauto. constructor. - reflexivity. reflexivity. traceEq. -Qed. - -Hint Resolve eval_list_one eval_list_two eval_list_three: evalexpr. - -Lemma eval_lift_expr: - forall w sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - forall p le', insert_lenv le p w le' -> - eval_expr ge sp le' e m1 (lift_expr p a) t m2 v. -Proof. - intros w. - apply (eval_expr_ind_3 ge - (fun sp le e m1 a t m2 v => - forall p le', insert_lenv le p w le' -> - eval_expr ge sp le' e m1 (lift_expr p a) t m2 v) - (fun sp le e m1 a t m2 vb => - forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp le' e m1 (lift_condexpr p a) t m2 vb) - (fun sp le e m1 al t m2 vl => - forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp le' e m1 (lift_exprlist p al) t m2 vl)); - simpl; intros; eauto with evalexpr. - - destruct v1; eapply eval_Econdition; - eauto with evalexpr; simpl; eauto with evalexpr. - - eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. auto. - - case (le_gt_dec p n); intro. - apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. - apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. - - destruct vb1; eapply eval_CEcondition; - eauto with evalexpr; simpl; eauto with evalexpr. -Qed. - -Lemma eval_lift: - forall sp le e m1 a t m2 v w, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp (w::le) e m1 (lift a) t m2 v. -Proof. - intros. unfold lift. eapply eval_lift_expr. - eexact H. apply insert_lenv_0. -Qed. -Hint Resolve eval_lift: evalexpr. - -(** * Useful lemmas and tactics *) - -Ltac EvalOp := eapply eval_Eop; eauto with evalexpr. - -Ltac TrivialOp cstr := - unfold cstr; intros; EvalOp. - -(** The following are trivial lemmas and custom tactics that help - perform backward (inversion) and forward reasoning over the evaluation - of operator applications. *) - -Lemma inv_eval_Eop_0: - forall sp le e m1 op t m2 v, - eval_expr ge sp le e m1 (Eop op Enil) t m2 v -> - t = E0 /\ m2 = m1 /\ eval_operation ge sp op nil = Some v. -Proof. - intros. inversion H. inversion H6. - intuition. congruence. -Qed. - -Lemma inv_eval_Eop_1: - forall sp le e m1 op t a1 m2 v, - eval_expr ge sp le e m1 (Eop op (a1 ::: Enil)) t m2 v -> - exists v1, - eval_expr ge sp le e m1 a1 t m2 v1 /\ - eval_operation ge sp op (v1 :: nil) = Some v. -Proof. - intros. - inversion H. inversion H6. inversion H18. - subst. exists v1; intuition. rewrite E0_right. auto. -Qed. - -Lemma inv_eval_Eop_2: - forall sp le e m1 op a1 a2 t3 m3 v, - eval_expr ge sp le e m1 (Eop op (a1 ::: a2 ::: Enil)) t3 m3 v -> - exists t1, exists t2, exists m2, exists v1, exists v2, - eval_expr ge sp le e m1 a1 t1 m2 v1 /\ - eval_expr ge sp le e m2 a2 t2 m3 v2 /\ - t3 = t1 ** t2 /\ - eval_operation ge sp op (v1 :: v2 :: nil) = Some v. -Proof. - intros. - inversion H. subst. inversion H6. subst. inversion H8. subst. - inversion H11. subst. - exists t1; exists t0; exists m0; exists v0; exists v1. - intuition. traceEq. -Qed. - -Ltac SimplEval := - match goal with - | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op Enil) ?t ?m2 ?v) -> _] => - intro XX1; - generalize (inv_eval_Eop_0 sp le e m1 op t m2 v XX1); - clear XX1; - intros [XX1 [XX2 XX3]]; - subst t m2; simpl in XX3; - try (simplify_eq XX3; clear XX3; - let EQ := fresh "EQ" in (intro EQ; rewrite EQ)) - | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: Enil)) ?t ?m2 ?v) -> _] => - intro XX1; - generalize (inv_eval_Eop_1 sp le e m1 op t a1 m2 v XX1); - clear XX1; - let v1 := fresh "v" in let EV := fresh "EV" in - let EQ := fresh "EQ" in - (intros [v1 [EV EQ]]; simpl in EQ) - | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?t ?m2 ?v) -> _] => - intro XX1; - generalize (inv_eval_Eop_2 sp le e m1 op a1 a2 t m2 v XX1); - clear XX1; - let t1 := fresh "t" in let t2 := fresh "t" in - let m := fresh "m" in - let v1 := fresh "v" in let v2 := fresh "v" in - let EV1 := fresh "EV" in let EV2 := fresh "EV" in - let EQ := fresh "EQ" in let TR := fresh "TR" in - (intros [t1 [t2 [m [v1 [v2 [EV1 [EV2 [TR EQ]]]]]]]]; simpl in EQ) - | _ => idtac - end. - -Ltac InvEval H := - generalize H; SimplEval; clear H. - -(** ** Admissible evaluation rules for the smart constructors *) - -(** 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_negint: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (negint a) t m2 (Vint (Int.neg x)). -Proof. - TrivialOp negint. -Qed. - -Theorem eval_negfloat: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vfloat x) -> - eval_expr ge sp le e m1 (negfloat a) t m2 (Vfloat (Float.neg x)). -Proof. - TrivialOp negfloat. -Qed. - -Theorem eval_absfloat: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vfloat x) -> - eval_expr ge sp le e m1 (absfloat a) t m2 (Vfloat (Float.abs x)). -Proof. - TrivialOp absfloat. -Qed. - -Theorem eval_intoffloat: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vfloat x) -> - eval_expr ge sp le e m1 (intoffloat a) t m2 (Vint (Float.intoffloat x)). -Proof. - TrivialOp intoffloat. -Qed. - -Theorem eval_floatofint: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (floatofint a) t m2 (Vfloat (Float.floatofint x)). -Proof. - TrivialOp floatofint. -Qed. - -Theorem eval_floatofintu: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (floatofintu a) t m2 (Vfloat (Float.floatofintu x)). -Proof. - TrivialOp floatofintu. -Qed. - -Theorem eval_notint: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (notint a) t m2 (Vint (Int.not x)). -Proof. - unfold notint; intros until x; case (notint_match a); intros. - InvEval H. FuncInv. EvalOp. simpl. congruence. - InvEval H. FuncInv. EvalOp. simpl. congruence. - InvEval H. FuncInv. EvalOp. simpl. congruence. - eapply eval_Elet. eexact H. - eapply eval_Eop. - eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - apply eval_Enil. reflexivity. reflexivity. - simpl. rewrite Int.or_idem. auto. traceEq. -Qed. - -Lemma eval_notbool_base: - forall sp le e m1 a t m2 v b, - eval_expr ge sp le e m1 a t m2 v -> - Val.bool_of_val v b -> - eval_expr ge sp le e m1 (notbool_base a) t m2 (Val.of_bool (negb b)). -Proof. - TrivialOp notbool_base. simpl. - inversion 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 a sp le e m1 t m2 v b, - eval_expr ge sp le e m1 a t m2 v -> - Val.bool_of_val v b -> - eval_expr ge sp le e m1 (notbool a) t m2 (Val.of_bool (negb b)). -Proof. - assert (N1: forall v b, Val.is_false v -> Val.bool_of_val v b -> Val.is_true (Val.of_bool (negb b))). - intros. inversion H0; simpl; auto; subst v; simpl in H. - congruence. apply Int.one_not_zero. contradiction. - assert (N2: forall v b, Val.is_true v -> Val.bool_of_val v b -> Val.is_false (Val.of_bool (negb b))). - intros. inversion H0; simpl; auto; subst v; simpl in H. - congruence. - - induction a; simpl; intros; try (eapply eval_notbool_base; eauto). - destruct o; try (eapply eval_notbool_base; eauto). - - destruct e. InvEval H. injection XX3; clear XX3; intro; subst v. - inversion H0. rewrite Int.eq_false; auto. - simpl; eauto with evalexpr. - rewrite Int.eq_true; simpl; eauto with evalexpr. - eapply eval_notbool_base; eauto. - - inversion H. subst. - simpl in H11. eapply eval_Eop; eauto. - simpl. caseEq (eval_condition c vl); intros. - rewrite H1 in H11. - assert (b0 = b). - destruct b0; inversion H11; subst v; inversion H0; auto. - subst b0. rewrite (Op.eval_negate_condition _ _ H1). - destruct b; reflexivity. - rewrite H1 in H11; discriminate. - - inversion H; eauto 10 with evalexpr valboolof. - inversion H; eauto 10 with evalexpr valboolof. - - inversion H. subst. eapply eval_Econdition with (t2 := t8). eexact H34. - destruct v4; eauto. auto. -Qed. - -Theorem eval_addimm: - forall sp le e m1 n a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (addimm n a) t m2 (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 H0. EvalOp. simpl. rewrite Int.add_commut. auto. - InvEval H0. destruct (Genv.find_symbol ge s); discriminate. - InvEval H0. - destruct sp; simpl in XX3; discriminate. - InvEval H0. FuncInv. EvalOp. simpl. subst x. - rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. - EvalOp. -Qed. - -Theorem eval_addimm_ptr: - forall sp le e m1 n t a m2 b ofs, - eval_expr ge sp le e m1 a t m2 (Vptr b ofs) -> - eval_expr ge sp le e m1 (addimm n a) t m2 (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 H0. - InvEval H0. EvalOp. simpl. - destruct (Genv.find_symbol ge s). - rewrite Int.add_commut. congruence. - discriminate. - InvEval H0. destruct sp; simpl in XX3; try discriminate. - inversion XX3. EvalOp. simpl. decEq. decEq. - rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. FuncInv. subst b0; subst ofs. EvalOp. simpl. - rewrite (Int.add_commut n m). rewrite Int.add_assoc. auto. - EvalOp. -Qed. - -Theorem eval_add: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vint (Int.add x y)). -Proof. - intros until y. unfold add; case (add_match a b); intros. - InvEval H. rewrite Int.add_commut. apply eval_addimm. - rewrite E0_left; assumption. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)). - apply eval_addimm. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - InvEval H. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i y) n1). - apply eval_addimm. EvalOp. - subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. FuncInv. - apply eval_addimm. rewrite E0_right. auto. - InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add x i) n2). - apply eval_addimm. EvalOp. - subst y. rewrite Int.add_assoc. auto. - EvalOp. -Qed. - -Theorem eval_add_ptr: - forall sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add x y)). -Proof. - intros until y. unfold add; case (add_match a b); intros. - InvEval H. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - InvEval H. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i y) n1). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. apply eval_addimm_ptr. rewrite E0_right. auto. - InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add x i) n2). - apply eval_addimm_ptr. EvalOp. - subst y. rewrite Int.add_assoc. auto. - EvalOp. -Qed. - -Theorem eval_add_ptr_2: - forall sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vptr p y) -> - eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add y x)). -Proof. - intros until y. unfold add; case (add_match a b); intros. - InvEval H. - apply eval_addimm_ptr. rewrite E0_left. auto. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.add y x) with (Int.add (Int.add i0 i) (Int.add n1 n2)). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. - rewrite (Int.add_commut n1 n2). apply Int.add_permut. - InvEval H. FuncInv. - replace (Int.add y x) with (Int.add (Int.add y i) n1). - apply eval_addimm_ptr. EvalOp. - subst x. repeat rewrite Int.add_assoc. auto. - InvEval H0. - InvEval H0. FuncInv. - replace (Int.add y x) with (Int.add (Int.add i x) n2). - apply eval_addimm_ptr. EvalOp. subst b0; reflexivity. - subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - EvalOp. -Qed. - -Theorem eval_sub: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros. - InvEval H0. rewrite Int.sub_add_opp. - apply eval_addimm. rewrite E0_right. assumption. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub i i0) (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. - InvEval H. FuncInv. - 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. - InvEval H0. FuncInv. - 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 sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vptr p (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros. - InvEval H0. rewrite Int.sub_add_opp. - apply eval_addimm_ptr. rewrite E0_right. assumption. - InvEval H. FuncInv. InvEval H0. FuncInv. - subst b0. - replace (Int.sub x y) with (Int.add (Int.sub i i0) (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. - InvEval H. FuncInv. 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. - InvEval H0. FuncInv. - 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 sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vptr p y) -> - eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros. - InvEval H0. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub i i0) (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. - InvEval H. FuncInv. 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. - InvEval H0. FuncInv. 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. - -Lemma eval_rolm: - forall sp le e m1 a amount mask t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (rolm a amount mask) t m2 (Vint (Int.rolm x amount mask)). -Proof. - intros until x. unfold rolm; case (rolm_match a); intros. - InvEval H. eauto with evalexpr. - case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)). - InvEval H. FuncInv. EvalOp. simpl. subst x. - decEq. decEq. - replace (Int.and (Int.add amount1 amount) (Int.repr 31)) - with (Int.modu (Int.add amount1 amount) (Int.repr 32)). - symmetry. apply Int.rolm_rolm. - change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one). - apply Int.modu_and with (Int.repr 5). reflexivity. - EvalOp. - EvalOp. -Qed. - -Theorem eval_shlimm: - forall sp le e m1 a n t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shlimm a n) t m2 (Vint (Int.shl x n)). -Proof. - intros. unfold shlimm. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - subst n. rewrite Int.shl_zero. auto. - rewrite H0. - replace (Int.shl x n) with (Int.rolm x n (Int.shl Int.mone n)). - apply eval_rolm. auto. symmetry. apply Int.shl_rolm. exact H0. -Qed. - -Theorem eval_shruimm: - forall sp le e m1 a n t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shruimm a n) t m2 (Vint (Int.shru x n)). -Proof. - intros. unfold shruimm. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - subst n. rewrite Int.shru_zero. auto. - rewrite H0. - replace (Int.shru x n) with (Int.rolm x (Int.sub (Int.repr 32) n) (Int.shru Int.mone n)). - apply eval_rolm. auto. symmetry. apply Int.shru_rolm. exact H0. -Qed. - -Lemma eval_mulimm_base: - forall sp le e m1 a t n m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (mulimm_base n a) t m2 (Vint (Int.mul x n)). -Proof. - intros; unfold mulimm_base. - generalize (Int.one_bits_decomp n). - generalize (Int.one_bits_range n). - change (Z_of_nat wordsize) with 32. - 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 t m2 (Vint x) E0. auto. - rewrite H1. simpl. rewrite Int.add_zero. - rewrite Int.mul_add_distr_r. - rewrite <- Int.shl_mul. - rewrite <- Int.shl_mul. - EvalOp. eapply eval_Econs. - apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. - auto with coqlib. - eapply eval_Econs. - apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. - auto with coqlib. - auto with evalexpr. - reflexivity. traceEq. reflexivity. traceEq. - intros. EvalOp. -Qed. - -Theorem eval_mulimm: - forall sp le e m1 a n t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (mulimm n a) t m2 (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. - intro. eapply eval_Elet; eauto with evalexpr. traceEq. - 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 H1. EvalOp. rewrite Int.mul_commut. reflexivity. - InvEval H1. FuncInv. - replace (Int.mul x n) with (Int.add (Int.mul i n) (Int.mul n n2)). - apply eval_addimm. apply eval_mulimm_base. auto. - subst x. rewrite Int.mul_add_distr_l. decEq. apply Int.mul_commut. - apply eval_mulimm_base. assumption. -Qed. - -Theorem eval_mul: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (mul a b) (t1**t2) m3 (Vint (Int.mul x y)). -Proof. - intros until y. - unfold mul; case (mul_match a b); intros. - InvEval H. rewrite Int.mul_commut. apply eval_mulimm. - rewrite E0_left; auto. - InvEval H0. rewrite E0_right. apply eval_mulimm. auto. - EvalOp. -Qed. - -Theorem eval_divs: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - y <> Int.zero -> - eval_expr ge sp le e m1 (divs a b) (t1**t2) m3 (Vint (Int.divs x y)). -Proof. - TrivialOp divs. simpl. - predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. -Qed. - -Lemma eval_mod_aux: - forall divop semdivop, - (forall sp x y, - y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) = - Some (Vint (semdivop x y))) -> - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - y <> Int.zero -> - eval_expr ge sp le e m1 (mod_aux divop a b) (t1**t2) m3 - (Vint (Int.sub x (Int.mul (semdivop x y) y))). -Proof. - intros; unfold mod_aux. - eapply eval_Elet. eexact H0. eapply eval_Elet. - apply eval_lift. eexact H1. - eapply eval_Eop. eapply eval_Econs. - eapply eval_Eletvar. simpl; reflexivity. - eapply eval_Econs. eapply eval_Eop. - eapply eval_Econs. eapply eval_Eop. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. reflexivity. reflexivity. - apply H. assumption. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. reflexivity. reflexivity. - simpl; reflexivity. apply eval_Enil. - reflexivity. reflexivity. reflexivity. - reflexivity. traceEq. -Qed. - -Theorem eval_mods: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - y <> Int.zero -> - eval_expr ge sp le e m1 (mods a b) (t1**t2) m3 (Vint (Int.mods x y)). -Proof. - intros; unfold mods. - rewrite Int.mods_divs. - eapply eval_mod_aux; eauto. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. -Qed. - -Lemma eval_divu_base: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - y <> Int.zero -> - eval_expr ge sp le e m1 (Eop Odivu (a ::: b ::: Enil)) (t1**t2) m3 (Vint (Int.divu x y)). -Proof. - intros. EvalOp. simpl. - predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. -Qed. - -Theorem eval_divu: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - y <> Int.zero -> - eval_expr ge sp le e m1 (divu a b) (t1**t2) m3 (Vint (Int.divu x y)). -Proof. - intros until y. - unfold divu; case (divu_match b); intros. - InvEval H0. caseEq (Int.is_power2 y). - intros. rewrite (Int.divu_pow2 x y i H0). - apply eval_shruimm. rewrite E0_right. auto. - apply Int.is_power2_range with y. auto. - intros. subst n2. eapply eval_divu_base. eexact H. EvalOp. auto. - eapply eval_divu_base; eauto. -Qed. - -Theorem eval_modu: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - y <> Int.zero -> - eval_expr ge sp le e m1 (modu a b) (t1**t2) m3 (Vint (Int.modu x y)). -Proof. - intros until y; unfold modu; case (divu_match b); intros. - InvEval H0. caseEq (Int.is_power2 y). - intros. rewrite (Int.modu_and x y i H0). - rewrite <- Int.rolm_zero. apply eval_rolm. rewrite E0_right; auto. - intro. rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. - eexact H. EvalOp. auto. auto. - rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. - eexact H. eexact H0. auto. auto. -Qed. - -Theorem eval_andimm: - forall sp le e m1 n a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (andimm n a) t m2 (Vint (Int.and x n)). -Proof. - intros. unfold andimm. case (Int.is_rlw_mask n). - rewrite <- Int.rolm_zero. apply eval_rolm; auto. - EvalOp. -Qed. - -Theorem eval_and: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (and a b) (t1**t2) m3 (Vint (Int.and x y)). -Proof. - intros until y; unfold and; case (mul_match a b); intros. - InvEval H. rewrite Int.and_commut. - rewrite E0_left; apply eval_andimm; auto. - InvEval H0. rewrite E0_right; apply eval_andimm; auto. - EvalOp. -Qed. - -Remark eval_same_expr_pure: - forall a1 a2 sp le e m1 t1 m2 v1 t2 m3 v2, - same_expr_pure a1 a2 = true -> - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - t1 = E0 /\ t2 = E0 /\ a2 = a1 /\ v2 = v1 /\ m2 = m1. -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. - assert (v2 = v1). congruence. tauto. - discriminate. -Qed. - -Lemma eval_or: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (or a b) (t1**t2) m3 (Vint (Int.or x y)). -Proof. - intros until y; unfold or; case (or_match a b); intros. - generalize (Int.eq_spec amount1 amount2); case (Int.eq amount1 amount2); intro. - case (Int.is_rlw_mask (Int.or mask1 mask2)). - caseEq (same_expr_pure t0 t3); intro. - simpl. InvEval H. FuncInv. InvEval H0. FuncInv. - generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0). - intros [EQ1 [EQ2 [EQ3 [EQ4 EQ5]]]]. - injection EQ4; intro EQ7. subst. - EvalOp. simpl. rewrite Int.or_rolm. auto. - simpl. EvalOp. - simpl. EvalOp. - simpl. EvalOp. - EvalOp. -Qed. - -Theorem eval_xor: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (xor a b) (t1**t2) m3 (Vint (Int.xor x y)). -Proof. TrivialOp xor. Qed. - -Theorem eval_shl: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shl a b) (t1**t2) m3 (Vint (Int.shl x y)). -Proof. - intros until y; unfold shl; case (shift_match b); intros. - InvEval H0. rewrite E0_right. apply eval_shlimm; auto. - EvalOp. simpl. rewrite H1. auto. -Qed. - -Theorem eval_shr: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shr a b) (t1**t2) m3 (Vint (Int.shr x y)). -Proof. - TrivialOp shr. simpl. rewrite H1. auto. -Qed. - -Theorem eval_shru: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shru a b) (t1**t2) m3 (Vint (Int.shru x y)). -Proof. - intros until y; unfold shru; case (shift_match b); intros. - InvEval H0. rewrite E0_right; apply eval_shruimm; auto. - EvalOp. simpl. rewrite H1. auto. -Qed. - -Theorem eval_addf: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (addf a b) (t1**t2) m3 (Vfloat (Float.add x y)). -Proof. - intros until y; unfold addf; case (addf_match a b); intros. - InvEval H. FuncInv. EvalOp. - econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor. - traceEq. simpl. subst x. reflexivity. - InvEval H0. FuncInv. eapply eval_Elet. eexact H. EvalOp. - econstructor; eauto with evalexpr. - econstructor; eauto with evalexpr. - econstructor. apply eval_Eletvar. simpl; reflexivity. - constructor. reflexivity. traceEq. - subst y. rewrite Float.addf_commut. reflexivity. auto. - EvalOp. -Qed. - -Theorem eval_subf: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (subf a b) (t1**t2) m3 (Vfloat (Float.sub x y)). -Proof. - intros until y; unfold subf; case (subf_match a b); intros. - InvEval H. FuncInv. EvalOp. - econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor. - traceEq. subst x. reflexivity. - EvalOp. -Qed. - -Theorem eval_mulf: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (mulf a b) (t1**t2) m3 (Vfloat (Float.mul x y)). -Proof. TrivialOp mulf. Qed. - -Theorem eval_divf: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (divf a b) (t1**t2) m3 (Vfloat (Float.div x y)). -Proof. TrivialOp divf. Qed. - -Theorem eval_cast8signed: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast8signed a) t m2 (Val.cast8signed v). -Proof. - intros until v; unfold cast8signed; case (cast8signed_match a); intros. - replace (Val.cast8signed v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity. - EvalOp. -Qed. - -Theorem eval_cast8unsigned: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast8unsigned a) t m2 (Val.cast8unsigned v). -Proof. - intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros. - replace (Val.cast8unsigned v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity. - EvalOp. -Qed. - -Theorem eval_cast16signed: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast16signed a) t m2 (Val.cast16signed v). -Proof. - intros until v; unfold cast16signed; case (cast16signed_match a); intros. - replace (Val.cast16signed v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity. - EvalOp. -Qed. - -Theorem eval_cast16unsigned: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast16unsigned a) t m2 (Val.cast16unsigned v). -Proof. - intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros. - replace (Val.cast16unsigned v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity. - EvalOp. -Qed. - -Theorem eval_singleoffloat: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (singleoffloat a) t m2 (Val.singleoffloat v). -Proof. - intros until v; unfold singleoffloat; case (singleoffloat_match a); intros. - replace (Val.singleoffloat v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - EvalOp. -Qed. - -Theorem eval_cmp: - forall sp le c e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 (Val.of_bool (Int.cmp c x y)). -Proof. - TrivialOp cmp. - simpl. case (Int.cmp c x y); auto. -Qed. - -Theorem eval_cmp_null_r: - forall sp le c e m1 a t1 m2 p x b t2 m3 v, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint Int.zero) -> - (c = Ceq /\ v = Vfalse) \/ (c = Cne /\ v = Vtrue) -> - eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 v. -Proof. - TrivialOp cmp. - simpl. elim H1; intros [EQ1 EQ2]; subst c; subst v; reflexivity. -Qed. - -Theorem eval_cmp_null_l: - forall sp le c e m1 a t1 m2 p x b t2 m3 v, - eval_expr ge sp le e m1 a t1 m2 (Vint Int.zero) -> - eval_expr ge sp le e m2 b t2 m3 (Vptr p x) -> - (c = Ceq /\ v = Vfalse) \/ (c = Cne /\ v = Vtrue) -> - eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 v. -Proof. - TrivialOp cmp. - simpl. elim H1; intros [EQ1 EQ2]; subst c; subst v; reflexivity. -Qed. - -Theorem eval_cmp_ptr: - forall sp le c e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vptr p y) -> - eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 (Val.of_bool (Int.cmp c x y)). -Proof. - TrivialOp cmp. - simpl. unfold eq_block. rewrite zeq_true. - case (Int.cmp c x y); auto. -Qed. - -Theorem eval_cmpu: - forall sp le c e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (cmpu c a b) (t1**t2) m3 (Val.of_bool (Int.cmpu c x y)). -Proof. - TrivialOp cmpu. - simpl. case (Int.cmpu c x y); auto. -Qed. - -Theorem eval_cmpf: - forall sp le c e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (cmpf c a b) (t1**t2) m3 (Val.of_bool (Float.cmp c x y)). -Proof. - TrivialOp cmpf. - simpl. case (Float.cmp c x y); auto. -Qed. - -Lemma eval_base_condition_of_expr: - forall sp le a e m1 t m2 v (b: bool), - eval_expr ge sp le e m1 a t m2 v -> - Val.bool_of_val v b -> - eval_condexpr ge sp le e m1 - (CEcond (Ccompuimm Cne Int.zero) (a ::: Enil)) - t m2 b. -Proof. - intros. - eapply eval_CEcond. eauto with evalexpr. - inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. -Qed. - -Lemma eval_condition_of_expr: - forall a sp le e m1 t m2 v (b: bool), - eval_expr ge sp le e m1 a t m2 v -> - Val.bool_of_val v b -> - eval_condexpr ge sp le e m1 (condexpr_of_expr a) t m2 b. -Proof. - induction a; simpl; intros; - try (eapply eval_base_condition_of_expr; eauto; fail). - destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct e. InvEval H. inversion XX3; subst v. - inversion H0. - rewrite Int.eq_false; auto. constructor. - subst i; rewrite Int.eq_true. constructor. - eapply eval_base_condition_of_expr; eauto. - - inversion H. subst. eapply eval_CEcond; eauto. simpl in H11. - destruct (eval_condition c vl); try discriminate. - destruct b0; inversion H11; subst; inversion H0; congruence. - - inversion H. subst. - destruct v1; eauto with evalexpr. -Qed. - -Theorem eval_conditionalexpr_true: - forall sp le e m1 a1 t1 m2 v1 t2 a2 m3 v2 a3, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - Val.is_true v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - eval_expr ge sp le e m1 (conditionalexpr a1 a2 a3) (t1**t2) m3 v2. -Proof. - intros; unfold conditionalexpr. - apply eval_Econdition with t1 m2 true t2; auto. - eapply eval_condition_of_expr; eauto with valboolof. -Qed. - -Theorem eval_conditionalexpr_false: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 a3, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - Val.is_false v1 -> - eval_expr ge sp le e m2 a3 t2 m3 v2 -> - eval_expr ge sp le e m1 (conditionalexpr a1 a2 a3) (t1**t2) m3 v2. -Proof. - intros; unfold conditionalexpr. - apply eval_Econdition with t1 m2 false t2; auto. - eapply eval_condition_of_expr; eauto with valboolof. -Qed. - -Lemma eval_addressing: - forall sp le e m1 a t m2 v b ofs, - eval_expr ge sp le e m1 a t m2 v -> - v = Vptr b ofs -> - match addressing a with (mode, args) => - exists vl, - eval_exprlist ge sp le e m1 args t m2 vl /\ - eval_addressing ge sp mode vl = Some v - end. -Proof. - intros until v. unfold addressing; case (addressing_match a); intros. - InvEval H. exists (@nil val). split. eauto with evalexpr. - simpl. auto. - InvEval H. exists (@nil val). split. eauto with evalexpr. - simpl. auto. - InvEval H. InvEval EV. rewrite E0_left in TR. subst t1. FuncInv. - congruence. - destruct (Genv.find_symbol ge s); congruence. - exists (Vint i0 :: nil). split. eauto with evalexpr. - simpl. subst v. destruct (Genv.find_symbol ge s). congruence. - discriminate. - InvEval H. FuncInv. - congruence. - exists (Vptr b0 i :: nil). split. eauto with evalexpr. - simpl. congruence. - InvEval H. FuncInv. - congruence. - exists (Vint i :: Vptr b0 i0 :: nil). - split. eauto with evalexpr. simpl. - rewrite Int.add_commut. congruence. - exists (Vptr b0 i :: Vint i0 :: nil). - split. eauto with evalexpr. simpl. congruence. - exists (v :: nil). split. eauto with evalexpr. - subst v. simpl. rewrite Int.add_zero. auto. -Qed. - -Theorem eval_load: - forall sp le e m1 a t m2 v chunk v', - eval_expr ge sp le e m1 a t m2 v -> - Mem.loadv chunk m2 v = Some v' -> - eval_expr ge sp le e m1 (load chunk a) t m2 v'. -Proof. - intros. generalize H0; destruct v; simpl; intro; try discriminate. - unfold load. - generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). - destruct (addressing a). intros [vl [EV EQ]]. - eapply eval_Eload; eauto. -Qed. - -Theorem eval_store: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 chunk m4, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - Mem.storev chunk m3 v1 v2 = Some m4 -> - eval_expr ge sp le e m1 (store chunk a1 a2) (t1**t2) m4 v2. -Proof. - intros. generalize H1; destruct v1; simpl; intro; try discriminate. - unfold store. - generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). - destruct (addressing a1). intros [vl [EV EQ]]. - eapply eval_Estore; eauto. -Qed. - -Theorem exec_ifthenelse_true: - forall sp e m1 a t1 m2 v ifso ifnot t2 e3 m3 out, - eval_expr ge sp nil e m1 a t1 m2 v -> - Val.is_true v -> - exec_stmt ge sp e m2 ifso t2 e3 m3 out -> - exec_stmt ge sp e m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out. -Proof. - intros. unfold ifthenelse. - apply exec_Sifthenelse with t1 m2 true t2. - eapply eval_condition_of_expr; eauto with valboolof. - auto. auto. -Qed. - -Theorem exec_ifthenelse_false: - forall sp e m1 a t1 m2 v ifso ifnot t2 e3 m3 out, - eval_expr ge sp nil e m1 a t1 m2 v -> - Val.is_false v -> - exec_stmt ge sp e m2 ifnot t2 e3 m3 out -> - exec_stmt ge sp e m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out. -Proof. - intros. unfold ifthenelse. - apply exec_Sifthenelse with t1 m2 false t2. - eapply eval_condition_of_expr; eauto with valboolof. - auto. auto. -Qed. - -End CMCONSTR. - |