diff options
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index ee3ed358..622992e5 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. @@ -1186,7 +1187,7 @@ 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. rewrite sel_builtin_nolabel; auto. @@ -1195,12 +1196,12 @@ Proof. (* builtin *) 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. @@ -1209,19 +1210,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 := |