diff options
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 120 |
1 files changed, 62 insertions, 58 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d66c7de8..fe286627 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -17,6 +17,7 @@ Require Import Coqlib Maps. Require Import AST Linking Errors Integers. Require Import Values Memory Builtins Events Globalenvs Smallstep. Require Import Switch Cminor Op CminorSel Cminortyping. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectDiv SplitLong SelectLong Selection. Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof. @@ -87,7 +88,7 @@ Lemma get_helpers_correct: forall p hf, get_helpers (prog_defmap p) = OK hf -> helper_functions_declared p hf. Proof. - intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. + intros. monadInv H. red; simpl. auto 22 using lookup_helper_correct. Qed. Theorem transf_program_match: @@ -107,7 +108,7 @@ Proof. { unfold helper_declared; intros. destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q). inv Q. inv H3. auto. } - red in H. decompose [Logic.and] H; clear H. red; auto 20. + red in H. decompose [Logic.and] H; clear H. red; auto 22. Qed. (** * Correctness of the instruction selection functions for expressions *) @@ -175,7 +176,7 @@ Proof. generalize (match_program_defmap _ _ _ _ _ TRANSF id). unfold Cminor.fundef; rewrite H; intros R; inv R. inv H2. destruct H4 as (cu & A & B). monadInv B. auto. } - unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20. + unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 22. Qed. Section CMCONSTR. @@ -195,12 +196,12 @@ Variable e: env. Variable m: mem. Lemma eval_condexpr_of_expr: - forall a le v b, + forall expected a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr tge sp e m le (condexpr_of_expr a) b. + eval_condexpr tge sp e m le (condexpr_of_expr a expected) b. Proof. - intros until a. functional induction (condexpr_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a expected); intros. (* compare *) inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. @@ -309,46 +310,47 @@ Lemma eval_sel_binop: exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_sub; auto. - apply eval_mul; auto. - eapply eval_divs; eauto. - eapply eval_divu; eauto. - eapply eval_mods; eauto. - eapply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - apply eval_xor; auto. - apply eval_shl; auto. - apply eval_shr; auto. - apply eval_shru; auto. - apply eval_addf; auto. - apply eval_subf; auto. - apply eval_mulf; auto. - apply eval_divf; auto. - apply eval_addfs; auto. - apply eval_subfs; auto. - apply eval_mulfs; auto. - apply eval_divfs; auto. - eapply eval_addl; eauto. - eapply eval_subl; eauto. - eapply eval_mull; eauto. - eapply eval_divls; eauto. - eapply eval_divlu; eauto. - eapply eval_modls; eauto. - eapply eval_modlu; eauto. - eapply eval_andl; eauto. - eapply eval_orl; eauto. - eapply eval_xorl; eauto. - eapply eval_shll; eauto. - eapply eval_shrl; eauto. - eapply eval_shrlu; eauto. - apply eval_comp; auto. - apply eval_compu; auto. - apply eval_compf; auto. - apply eval_compfs; auto. - exists v; split; auto. eapply eval_cmpl; eauto. - exists v; split; auto. eapply eval_cmplu; eauto. + - exists v1; split; trivial. apply Val.lessdef_normalize. + - apply eval_add; auto. + - apply eval_sub; auto. + - apply eval_mul; auto. + - eapply eval_divs; eauto. + - eapply eval_divu; eauto. + - eapply eval_mods; eauto. + - eapply eval_modu; eauto. + - apply eval_and; auto. + - apply eval_or; auto. + - apply eval_xor; auto. + - apply eval_shl; auto. + - apply eval_shr; auto. + - apply eval_shru; auto. + - apply eval_addf; auto. + - apply eval_subf; auto. + - apply eval_mulf; auto. + - apply eval_divf; auto. + - apply eval_addfs; auto. + - apply eval_subfs; auto. + - apply eval_mulfs; auto. + - apply eval_divfs; auto. + - eapply eval_addl; eauto. + - eapply eval_subl; eauto. + - eapply eval_mull; eauto. + - eapply eval_divls; eauto. + - eapply eval_divlu; eauto. + - eapply eval_modls; eauto. + - eapply eval_modlu; eauto. + - eapply eval_andl; eauto. + - eapply eval_orl; eauto. + - eapply eval_xorl; eauto. + - eapply eval_shll; eauto. + - eapply eval_shrl; eauto. + - eapply eval_shrlu; eauto. + - apply eval_comp; auto. + - apply eval_compu; auto. + - apply eval_compf; auto. + - apply eval_compfs; auto. + - exists v; split; auto. eapply eval_cmpl; eauto. + - exists v; split; auto. eapply eval_cmplu; eauto. Qed. Lemma eval_sel_select: @@ -781,6 +783,8 @@ Lemma sel_select_opt_correct: Cminor.eval_expr ge sp e m cond vcond -> Cminor.eval_expr ge sp e m a1 v1 -> Cminor.eval_expr ge sp e m a2 v2 -> + Val.has_type v1 ty -> + Val.has_type v2 ty -> Val.bool_of_val vcond b -> env_lessdef e e' -> Mem.extends m m' -> exists v', eval_expr tge sp e' m' le a v' /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'. @@ -790,7 +794,7 @@ Proof. exploit sel_expr_correct. eexact H0. eauto. eauto. intros (vcond' & EVC & LDC). exploit sel_expr_correct. eexact H1. eauto. eauto. intros (v1' & EV1 & LD1). exploit sel_expr_correct. eexact H2. eauto. eauto. intros (v2' & EV2 & LD2). - assert (Val.bool_of_val vcond' b) by (inv H3; inv LDC; constructor). + assert (Val.bool_of_val vcond' b) by (inv H5; inv LDC; constructor). exploit eval_condition_of_expr. eexact EVC. eauto. rewrite C. intros (vargs' & EVARGS & EVCOND). exploit eval_select; eauto. intros (v' & X & Y). exists v'; split; eauto. @@ -1194,21 +1198,21 @@ Remark find_label_commut: Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr e)); simpl; auto. +- unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. rewrite sel_builtin_nolabel; auto. (* tailcall *) - destruct (classify_call (prog_defmap cunit) e); simpl; auto. +- destruct (classify_call (prog_defmap cunit) e); simpl; auto. (* builtin *) - rewrite sel_builtin_nolabel; auto. +- rewrite sel_builtin_nolabel; auto. (* seq *) - exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. +- exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) - destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC. +- destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC. inv SE. exploit if_conversion_nolabel; eauto. intros (A & B & C). rewrite A, B, C. auto. monadInv SE; simpl. @@ -1217,19 +1221,19 @@ Proof. destruct (find_label lbl x k') as [[sy ky] | ]; intuition. apply IHs2; auto. (* loop *) - apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto. +- apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto. (* block *) - apply IHs. constructor; auto. auto. +- apply IHs. constructor; auto. auto. (* switch *) - destruct b. +- destruct b. destruct (validate_switch Int64.modulus n l (compile_switch Int64.modulus n l)); inv SE. simpl; auto. destruct (validate_switch Int.modulus n l (compile_switch Int.modulus n l)); inv SE. simpl; auto. (* return *) - destruct o; inv SE; simpl; auto. +- destruct o; inv SE; simpl; auto. (* label *) - destruct (ident_eq lbl l). auto. apply IHs; auto. +- destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. Definition measure (s: Cminor.state) : nat := |