From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selectionproof.v | 1398 ---------------------------------------------- 1 file changed, 1398 deletions(-) delete mode 100644 backend/Selectionproof.v (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v deleted file mode 100644 index 6d62979..0000000 --- a/backend/Selectionproof.v +++ /dev/null @@ -1,1398 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 *) - -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 Smallstep. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. -Require Import Selection. - -Open Local Scope selection_scope. - -Section CMCONSTR. - -Variable ge: genv. -Variable sp: val. -Variable e: env. -Variable m: mem. - -(** * 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. - -Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition - eval_Elet eval_Eletvar - eval_CEtrue eval_CEfalse eval_CEcond - eval_CEcondition eval_Enil eval_Econs: evalexpr. - -Lemma eval_lift_expr: - forall w le a v, - eval_expr ge sp e m le a v -> - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v. -Proof. - intro w. - apply (eval_expr_ind3 ge sp e m - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v) - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp e m le' (lift_condexpr p a) v) - (fun le al vl => - forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp e m le' (lift_exprlist p al) 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. - - 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 le a v w, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m (w::le) (lift a) 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. - -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 [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. -*) - -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.not x)). -Proof. - unfold notint; intros until x; case (notint_match a); intros; InvEval. - EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - 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. - simpl. rewrite Int.or_idem. 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 m = Some b). - generalize H6. simpl. - case (eval_condition c vl m); 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. - -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. - destruct (Genv.find_symbol ge s); discriminate. - destruct sp; simpl in H1; discriminate. - subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. -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; EvalOp; simpl. - destruct (Genv.find_symbol ge s). - rewrite Int.add_commut. congruence. - discriminate. - destruct sp; simpl in H1; try discriminate. - inv H1. simpl. decEq. decEq. - rewrite Int.add_assoc. decEq. apply Int.add_commut. - subst. rewrite (Int.add_commut n m0). rewrite Int.add_assoc. auto. -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. - replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). - apply eval_addimm. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - 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. - apply eval_addimm. auto. - 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 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. - replace (Int.add x y) 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. apply Int.add_permut. - 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. - apply eval_addimm_ptr. auto. - 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 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. - replace (Int.add y x) 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. - rewrite (Int.add_commut n1 n2). apply Int.add_permut. - 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. - 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 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. - -Lemma eval_rolm: - forall le a amount mask x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (rolm a amount mask) (Vint (Int.rolm x amount mask)). -Proof. - intros until x. unfold rolm; case (rolm_match a); intros; InvEval. - eauto with evalexpr. - case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)). - 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. econstructor. EvalOp. simpl. rewrite H. reflexivity. constructor. auto. - EvalOp. -Qed. - -Theorem eval_shlimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp e m le (shlimm a n) (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 le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp e m le (shruimm a n) (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 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). - 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 (Vint x). 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. - 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. - intro. eapply eval_Elet; eauto with evalexpr. - 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. - 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 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. - -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. - -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 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 (mod_aux divop a b) - (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. - apply H. assumption. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. - simpl; reflexivity. apply eval_Enil. - reflexivity. -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. - 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 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 (Eop Odivu (a ::: b ::: Enil)) (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 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 until y. - unfold divu; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y). - intros. rewrite (Int.divu_pow2 x y i H0). - apply eval_shruimm. auto. - apply Int.is_power2_range with y. auto. - intros. apply eval_divu_base. auto. EvalOp. auto. - eapply eval_divu_base; eauto. -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 until y; unfold modu; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y). - intros. rewrite (Int.modu_and x y i H0). - rewrite <- Int.rolm_zero. apply eval_rolm. auto. - intro. rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. - auto. EvalOp. auto. auto. - rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. auto. auto. auto. auto. -Qed. - -Theorem 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. case (Int.is_rlw_mask n). - rewrite <- Int.rolm_zero. apply eval_rolm; 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. - apply eval_andimm; auto. - 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. - -Lemma 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. - caseEq (Int.eq amount1 amount2 - && Int.is_rlw_mask (Int.or mask1 mask2) - && same_expr_pure t1 t2); intro. - destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4). - generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2. - exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. - simpl. EvalOp. simpl. rewrite Int.or_rolm. auto. - simpl. apply eval_Eop with (Vint x :: Vint y :: nil). - econstructor. EvalOp. simpl. congruence. - econstructor. EvalOp. simpl. congruence. constructor. auto. - EvalOp. -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.repr 32) = 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.repr 32) = 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_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 until y; unfold addf. - destruct (use_fused_mul tt). - case (addf_match a b); intros; InvEval. - EvalOp. simpl. congruence. - EvalOp. simpl. rewrite Float.addf_commut. congruence. - EvalOp. - intros. 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 until y; unfold subf. - destruct (use_fused_mul tt). - case (subf_match a b); intros. - InvEval. EvalOp. simpl. congruence. - EvalOp. - intros. EvalOp. -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 until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. compute; auto. - 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 until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. compute; auto. - 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 until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. compute; auto. - 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 until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. compute; auto. - 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 until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - EvalOp. -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. - -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) -> - (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = 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. destruct (Int.eq y Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; auto. - EvalOp. simpl. destruct (Int.eq y Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; 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) -> - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = 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. destruct (Int.eq x Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; auto. - EvalOp. simpl. destruct (Int.eq x Int.zero); try discriminate. - unfold Cminor.eval_compare_mismatch in H1. unfold eval_compare_mismatch. - destruct c; try discriminate; 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) -> - valid_pointer m x1 (Int.signed x2) && - valid_pointer m y1 (Int.signed y2) = true -> - 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. rewrite H1. 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) -> - valid_pointer m x1 (Int.signed x2) && - valid_pointer m y1 (Int.signed y2) = true -> - 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 H1. rewrite dec_eq_false; auto. - destruct c; simpl in H3; inv H3; 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. - -Lemma negate_condexpr_correct: - forall le a b, - eval_condexpr ge sp e m le a b -> - eval_condexpr ge sp e m le (negate_condexpr a) (negb b). -Proof. - induction 1; simpl. - constructor. - constructor. - econstructor. eauto. apply eval_negate_condition. auto. - econstructor. eauto. destruct vb1; auto. -Qed. - -Scheme expr_ind2 := Induction for expr Sort Prop - with exprlist_ind2 := Induction for exprlist Sort Prop. - -Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop := - match el with - | Enil => True - | Econs e el' => P e /\ forall_exprlist P el' - end. - -Lemma expr_induction_principle: - forall (P: expr -> Prop), - (forall i : ident, P (Evar i)) -> - (forall (o : operation) (e : exprlist), - forall_exprlist P e -> P (Eop o e)) -> - (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist), - forall_exprlist P e -> P (Eload m a e)) -> - (forall (c : condexpr) (e : expr), - P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) -> - (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) -> - (forall n : nat, P (Eletvar n)) -> - forall e : expr, P e. -Proof. - intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto. - simpl. auto. - intros. simpl. auto. -Qed. - -Lemma eval_base_condition_of_expr: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le - (CEcond (Ccompimm Cne Int.zero) (a ::: Enil)) - b. -Proof. - intros. - eapply eval_CEcond. eauto with evalexpr. - inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. -Qed. - -Lemma is_compare_neq_zero_correct: - forall c v b, - is_compare_neq_zero c = true -> - eval_condition c (v :: nil) m = Some b -> - Val.bool_of_val v b. -Proof. - intros. - destruct c; simpl in H; try discriminate; - destruct c; simpl in H; try discriminate; - generalize (Int.eq_spec i Int.zero); rewrite H; intro; subst i. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. constructor. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. -Qed. - -Lemma is_compare_eq_zero_correct: - forall c v b, - is_compare_eq_zero c = true -> - eval_condition c (v :: nil) m = Some b -> - Val.bool_of_val v (negb b). -Proof. - intros. apply is_compare_neq_zero_correct with (negate_condition c). - destruct c; simpl in H; simpl; try discriminate; - destruct c; simpl; try discriminate; auto. - apply eval_negate_condition; auto. -Qed. - -Lemma eval_condition_of_expr: - forall a le v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le (condexpr_of_expr a) b. -Proof. - intro a0; pattern a0. - apply expr_induction_principle; simpl; intros; - try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct e0. InvEval. - inversion H1. - rewrite Int.eq_false; auto. constructor. - subst i; rewrite Int.eq_true. constructor. - eapply eval_base_condition_of_expr; eauto. - - inv H0. simpl in H7. - assert (eval_condition c vl m = Some b). - destruct (eval_condition c vl m); try discriminate. - destruct b0; inv H7; inversion H1; congruence. - assert (eval_condexpr ge sp e m le (CEcond c e0) b). - eapply eval_CEcond; eauto. - destruct e0; auto. destruct e1; auto. - simpl in H. destruct H. - inv H5. inv H11. - - case_eq (is_compare_neq_zero c); intros. - eapply H; eauto. - apply is_compare_neq_zero_correct with c; auto. - - case_eq (is_compare_eq_zero c); intros. - replace b with (negb (negb b)). apply negate_condexpr_correct. - eapply H; eauto. - apply is_compare_eq_zero_correct with c; auto. - apply negb_involutive. - - auto. - - inv H1. destruct v1; eauto with evalexpr. -Qed. - -Lemma eval_addressing: - forall le a v b ofs, - eval_expr ge sp e m le a v -> - v = Vptr b ofs -> - match addressing a with (mode, args) => - exists vl, - eval_exprlist ge sp e m le args vl /\ - eval_addressing ge sp mode vl = Some v - end. -Proof. - intros until v. unfold addressing; case (addressing_match a); intros; InvEval. - exists (@nil val). split. eauto with evalexpr. simpl. auto. - exists (@nil val). split. eauto with evalexpr. simpl. auto. - destruct (Genv.find_symbol ge s); congruence. - exists (Vint i0 :: nil). split. eauto with evalexpr. - simpl. destruct (Genv.find_symbol ge s). congruence. discriminate. - exists (Vptr b0 i :: nil). split. eauto with evalexpr. - simpl. congruence. - exists (Vint i :: Vptr b0 i0 :: nil). - split. eauto with evalexpr. simpl. - 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 le a v chunk v', - eval_expr ge sp e m le a v -> - Mem.loadv chunk m v = Some v' -> - eval_expr ge sp e m le (load chunk a) 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 chunk a1 a2 v1 v2 f k m', - eval_expr ge sp e m nil a1 v1 -> - eval_expr ge sp e m nil a2 v2 -> - Mem.storev chunk m v1 v2 = Some m' -> - step ge (State f (store chunk a1 a2) k sp e m) - E0 (State f Sskip k sp e m'). -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 step_store; 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 le op a1 v1 v, - eval_expr ge sp e m le a1 v1 -> - eval_unop op v1 = Some v -> - eval_expr ge sp e m le (sel_unop op a1) 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. - EvalOp. -Qed. - -Lemma eval_sel_binop: - forall le op a1 a2 v1 v2 v, - eval_expr ge sp e m le a1 v1 -> - eval_expr ge sp e m le a2 v2 -> - eval_binop op v1 v2 m = Some v -> - eval_expr ge sp e m le (sel_binop op a1 a2) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_add_ptr_2; auto. - apply eval_add_ptr; auto. - apply eval_sub; auto. - apply eval_sub_ptr_int; auto. - destruct (eq_block b b0); inv H1. - eapply eval_sub_ptr_ptr; eauto. - apply eval_mul; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divs; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divu; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_mods; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - EvalOp. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shl; auto. - EvalOp. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shru; auto. - apply eval_addf; auto. - apply eval_subf; auto. - EvalOp. - EvalOp. - apply eval_comp_int; auto. - eapply eval_comp_int_ptr; eauto. - eapply eval_comp_ptr_int; eauto. - generalize H1; clear H1. - case_eq (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)); intros. - destruct (eq_block b b0); inv H2. - eapply eval_comp_ptr_ptr; eauto. - eapply eval_comp_ptr_ptr_2; eauto. - discriminate. - eapply eval_compu; eauto. - eapply eval_compf; eauto. -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. - -(** Semantic preservation for expressions. *) - -Lemma sel_expr_correct: - forall sp e m a v, - Cminor.eval_expr ge sp e m a v -> - forall le, - eval_expr tge sp e m le (sel_expr a) v. -Proof. - induction 1; 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 *) - eapply eval_sel_binop; eauto. - (* Eload *) - eapply eval_load; eauto. - (* Econdition *) - econstructor; eauto. eapply eval_condition_of_expr; eauto. - destruct b1; auto. -Qed. - -Hint Resolve sel_expr_correct: evalexpr. - -Lemma sel_exprlist_correct: - forall sp e m a v, - Cminor.eval_exprlist ge sp e m a v -> - forall le, - eval_exprlist tge sp e m le (sel_exprlist a) v. -Proof. - induction 1; intros; simpl; constructor; auto with evalexpr. -Qed. - -Hint Resolve sel_exprlist_correct: evalexpr. - -(** Semantic preservation for terminating function calls and statements. *) - -Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := - match k with - | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1) - | Cminor.Kblock k1 => Kblock (sel_cont k1) - | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function f) sp e (sel_cont k1) - end. - -Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f s k s' k' sp e m, - s' = sel_stmt s -> - k' = sel_cont k -> - match_states - (Cminor.State f s k sp e m) - (State (sel_function f) s' k' sp e m) - | match_callstate: forall f args k k' m, - k' = sel_cont k -> - match_states - (Cminor.Callstate f args k m) - (Callstate (sel_fundef f) args k' m) - | match_returnstate: forall v k k' m, - k' = sel_cont k -> - match_states - (Cminor.Returnstate v k m) - (Returnstate v k' m). - -Remark call_cont_commut: - forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). -Proof. - induction k; simpl; auto. -Qed. - -Remark find_label_commut: - forall lbl s k, - find_label lbl (sel_stmt s) (sel_cont k) = - option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk))) - (Cminor.find_label lbl s k). -Proof. - induction s; intros; simpl; auto. - unfold store. destruct (addressing (sel_expr e)); auto. - change (Kseq (sel_stmt s2) (sel_cont k)) - with (sel_cont (Cminor.Kseq s2 k)). - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt s)) (sel_cont k)) - with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). - auto. - change (Kblock (sel_cont k)) - with (sel_cont (Cminor.Kblock k)). - auto. - destruct o; auto. - destruct (ident_eq lbl l); auto. -Qed. - -Lemma sel_step_correct: - forall S1 t S2, Cminor.step ge S1 t S2 -> - forall T1, match_states S1 T1 -> - exists T2, step tge T1 t T2 /\ match_states S2 T2. -Proof. - induction 1; intros T1 ME; inv ME; simpl; - try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). - - (* skip call *) - econstructor; split. - econstructor. destruct k; simpl in H; simpl; auto. - rewrite <- H0; reflexivity. - constructor; auto. - (* assign *) - exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split. - constructor. auto with evalexpr. - constructor; auto. - (* store *) - econstructor; split. - eapply eval_store; eauto with evalexpr. - constructor; auto. - (* Scall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. - (* Stailcall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. apply call_cont_commut. - (* Salloc *) - exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id (Vptr b Int.zero) e) m'); split. - econstructor; eauto with evalexpr. - constructor; auto. - (* Sifthenelse *) - exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. - constructor. eapply eval_condition_of_expr; eauto with evalexpr. - constructor; auto. destruct b; auto. - (* Sreturn None *) - econstructor; split. - econstructor. rewrite <- H; reflexivity. - constructor; auto. apply call_cont_commut. - (* Sreturn Some *) - econstructor; split. - econstructor. simpl. auto. eauto with evalexpr. - constructor; auto. apply call_cont_commut. - (* Sgoto *) - econstructor; split. - econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. - rewrite H. simpl. reflexivity. - constructor; auto. -Qed. - -Lemma sel_initial_states: - forall S, Cminor.initial_state prog S -> - exists R, initial_state tprog R /\ match_states S R. -Proof. - induction 1. - econstructor; split. - econstructor. - simpl. fold tge. rewrite symbols_preserved. eexact H. - apply function_ptr_translated. eauto. - rewrite <- H1. apply sig_function_translated; auto. - unfold tprog, sel_program. rewrite Genv.init_mem_transf. - constructor; auto. -Qed. - -Lemma sel_final_states: - forall S R r, - match_states S R -> Cminor.final_state S r -> final_state R r. -Proof. - intros. inv H0. inv H. simpl. constructor. -Qed. - -Theorem transf_program_correct: - forall (beh: program_behavior), - Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. -Proof. - unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_step_preservation; eauto. - eexact sel_initial_states. - eexact sel_final_states. - exact sel_step_correct. -Qed. - -End PRESERVATION. -- cgit v1.2.3