diff options
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 1240 |
1 files changed, 1240 insertions, 0 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v new file mode 100644 index 0000000..e41765a --- /dev/null +++ b/backend/Selectionproof.v @@ -0,0 +1,1240 @@ +(** Correctness of instruction selection *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Cminor. +Require Import Op. +Require Import CminorSel. +Require Import Selection. + +Open Local Scope selection_scope. + +Section CMCONSTR. + +Variable ge: 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 *) + +(** 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. + +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 m1 = 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) m2 = 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) m3 = 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. + +(** * Correctness of the smart constructors *) + +(** We now show that the code generated by "smart constructor" functions + such as [Selection.notint] behaves as expected. Continuing the + [notint] example, we show that if the expression [e] + evaluates to some integer value [Vint n], then [Selection.notint e] + evaluates to a value [Vint (Int.not n)] which is indeed the integer + negation of the value of [e]. + + All proofs follow a common pattern: +- Reasoning by case over the result of the classification functions + (such as [add_match] for integer addition), gathering additional + information on the shape of the argument expressions in the non-default + cases. +- Inversion of the evaluations of the arguments, exploiting the additional + information thus gathered. +- Equational reasoning over the arithmetic operations performed, + using the lemmas from the [Int] and [Float] modules. +- Construction of an evaluation derivation for the expression returned + by the smart constructor. +*) + +Lemma 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. + +Lemma 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 m2); 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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 m, + y <> Int.zero -> + eval_operation ge sp divop (Vint x :: Vint y :: nil) m = + 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +Lemma 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. + +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 (Ccompimm 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. + +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. + +Lemma 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. + +Lemma 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. + +(** * Correctness of instruction selection for operators *) + +(** We now prove a semantic preservation result for the [sel_unop] + and [sel_binop] selection functions. The proof exploits + the results of the previous section. *) + +Lemma eval_sel_unop: + forall sp le e m op a1 t m1 v1 v, + eval_expr ge sp le e m a1 t m1 v1 -> + eval_unop op v1 = Some v -> + eval_expr ge sp le e m (sel_unop op a1) t m1 v. +Proof. + destruct op; simpl; intros; FuncInv; try subst v. + apply eval_cast8unsigned; auto. + apply eval_cast8signed; auto. + apply eval_cast16unsigned; auto. + apply eval_cast16signed; auto. + EvalOp. + generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro. + change true with (negb false). eapply eval_notbool; eauto. subst i; constructor. + change false with (negb true). eapply eval_notbool; eauto. constructor; auto. + change Vfalse with (Val.of_bool (negb true)). + eapply eval_notbool; eauto. constructor. + apply eval_notint; auto. + EvalOp. + EvalOp. + apply eval_singleoffloat; auto. + EvalOp. + EvalOp. + EvalOp. +Qed. + +Lemma eval_sel_binop: + forall sp le e m op a1 a2 t1 m1 v1 t2 m2 v2 v, + eval_expr ge sp le e m a1 t1 m1 v1 -> + eval_expr ge sp le e m1 a2 t2 m2 v2 -> + eval_binop op v1 v2 m2 = Some v -> + eval_expr ge sp le e m (sel_binop op a1 a2) (t1 ** t2) m2 v. +Proof. + destruct op; simpl; intros; FuncInv; try subst v. + eapply eval_add; eauto. + eapply eval_add_ptr_2; eauto. + eapply eval_add_ptr; eauto. + eapply eval_sub; eauto. + eapply eval_sub_ptr_int; eauto. + destruct (eq_block b b0); inv H1. + eapply eval_sub_ptr_ptr; eauto. + eapply eval_mul; eauto. + generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. + eapply eval_divs; eauto. + generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. + eapply eval_divu; eauto. + generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. + eapply eval_mods; eauto. + generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. + eapply eval_modu; eauto. + eapply eval_and; eauto. + eapply eval_or; eauto. + EvalOp. + caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. + eapply eval_shl; eauto. + EvalOp. + caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. + eapply eval_shru; eauto. + eapply eval_addf; eauto. + eapply eval_subf; eauto. + EvalOp. + EvalOp. + EvalOp. simpl. destruct (Int.cmp c i i0); auto. + EvalOp. simpl. generalize H1; unfold eval_compare_null, Cminor.eval_compare_null. + destruct (Int.eq i Int.zero). destruct c; intro EQ; inv EQ; auto. + auto. + EvalOp. simpl. generalize H1; unfold eval_compare_null, Cminor.eval_compare_null. + destruct (Int.eq i0 Int.zero). destruct c; intro EQ; inv EQ; auto. + auto. + EvalOp. simpl. + destruct (valid_pointer m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)). + destruct (eq_block b b0); inv H1. + destruct (Int.cmp c i i0); auto. + auto. + EvalOp. simpl. destruct (Int.cmpu c i i0); auto. + EvalOp. simpl. destruct (Float.cmp c f f0); auto. +Qed. + +End CMCONSTR. + +(** * Semantic preservation for instruction selection. *) + +Section PRESERVATION. + +Variable prog: Cminor.program. +Let tprog := sel_program prog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +(** Relationship between the global environments for the original + CminorSel program and the generated RTL program. *) + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, sel_program. + apply Genv.find_symbol_transf. +Qed. + +Lemma functions_translated: + forall (v: val) (f: Cminor.fundef), + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (sel_fundef f). +Proof. + intros. + exact (Genv.find_funct_transf sel_fundef H). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: Cminor.fundef), + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (sel_fundef f). +Proof. + intros. + exact (Genv.find_funct_ptr_transf sel_fundef H). +Qed. + +Lemma sig_function_translated: + forall f, + funsig (sel_fundef f) = Cminor.funsig f. +Proof. + intros. destruct f; reflexivity. +Qed. + +(** This is the main semantic preservation theorem: + instruction selection preserves the semantics of function invocations. + The proof is an induction over the Cminor evaluation derivation. *) + +Lemma sel_function_correct: + forall m fd vargs t m' vres, + Cminor.eval_funcall ge m fd vargs t m' vres -> + CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres. +Proof. + apply (Cminor.eval_funcall_ind4 ge + (fun sp le e m a t m' v => eval_expr tge sp le e m (sel_expr a) t m' v) + (fun sp le e m a t m' v => eval_exprlist tge sp le e m (sel_exprlist a) t m' v) + (fun m fd vargs t m' vres => eval_funcall tge m (sel_fundef fd) vargs t m' vres) + (fun sp e m s t e' m' out => exec_stmt tge sp e m (sel_stmt s) t e' m' out)); + intros; simpl. + (* Evar *) + constructor; auto. + (* Econst *) + destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]). + rewrite symbols_preserved. auto. + (* Eunop *) + eapply eval_sel_unop; eauto. + (* Ebinop *) + subst t. eapply eval_sel_binop; eauto. + (* Eload *) + eapply eval_load; eauto. + (* Estore *) + subst t. eapply eval_store; eauto. + (* Ecall *) + econstructor; eauto. apply functions_translated; auto. + rewrite <- H4. apply sig_function_translated. + (* Econdition *) + econstructor; eauto. eapply eval_condition_of_expr; eauto. + destruct b1; auto. + (* Elet *) + econstructor; eauto. + (* Eletvar *) + constructor; auto. + (* Ealloc *) + econstructor; eauto. + (* Enil *) + constructor. + (* Econs *) + econstructor; eauto. + (* Internal function *) + econstructor; eauto. + (* External function *) + econstructor; eauto. + (* Sskip *) + constructor. + (* Sexpr *) + econstructor; eauto. + (* Sassign *) + econstructor; eauto. + (* Sifthenelse *) + econstructor; eauto. eapply eval_condition_of_expr; eauto. + destruct b1; auto. + (* Sseq *) + eapply exec_Sseq_continue; eauto. + eapply exec_Sseq_stop; eauto. + (* Sloop *) + eapply exec_Sloop_loop; eauto. + eapply exec_Sloop_stop; eauto. + (* Sblock *) + econstructor; eauto. + (* Sexit *) + constructor. + (* Sswitch *) + econstructor; eauto. + (* Sreturn *) + constructor. + econstructor; eauto. + (* Stailcall *) + econstructor; eauto. apply functions_translated; auto. + rewrite <- H4. apply sig_function_translated. +Qed. + +End PRESERVATION. + +(** As a corollary, instruction selection preserves the observable + behaviour of programs. *) + +Theorem sel_program_correct: + forall prog t r, + Cminor.exec_program prog t r -> + CminorSel.exec_program (sel_program prog) t r. +Proof. + intros. + destruct H as [b [f [m [FINDS [FINDF [SIG EXEC]]]]]]. + exists b; exists (sel_fundef f); exists m. + split. simpl. rewrite <- FINDS. apply symbols_preserved. + split. apply function_ptr_translated. auto. + split. rewrite <- SIG. apply sig_function_translated. + replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). + apply sel_function_correct; auto. + symmetry. unfold sel_program. apply Genv.init_mem_transf. +Qed. |