From cd69b24565713610d0ea5a613f4871af6e18e9d4 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 5 Mar 2019 10:48:03 +0100 Subject: No more axiom remaining in PostpassScheduling.v (but still a couple remaining in Asmblockdeps) --- mppa_k1c/PostpassScheduling.v | 98 ++++++++++++++++++++++++++++--------------- 1 file changed, 65 insertions(+), 33 deletions(-) (limited to 'mppa_k1c/PostpassScheduling.v') diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index fa0ebfe6..0c1cf605 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -33,13 +33,6 @@ Definition exec := exec_bblock. Definition bblock_equivb' := bblock_equivb. -Lemma bblock_equivb'_refl (ge: Genv.t fundef unit) (fn: function): forall tbb, bblock_equivb' tbb tbb = true. -Proof. - intros. rewrite bblock_equiv'_eq. apply bblock_equiv'_refl. - Unshelve. (* FIXME - problem of Genv and function *) - constructor; auto. -Qed. - Lemma trans_equiv_stuck: forall b1 b2 ge fn rs m, bblock_equiv' (P.Genv ge fn) (trans_block b1) (trans_block b2) -> @@ -54,7 +47,6 @@ Proof. reflexivity. eassumption. eassumption. Qed. - Lemma bblock_equiv'_comm: forall ge fn b1 b2, bblock_equiv' (P.Genv ge fn) b1 b2 <-> bblock_equiv' (P.Genv ge fn) b2 b1. @@ -270,13 +262,6 @@ Definition verify_schedule (bb bb' : bblock) : res unit := | false => Error (msg "PostpassScheduling.verify_schedule") end. -Lemma verify_schedule_refl (ge: Genv.t fundef unit) (fn: function): - forall bb, verify_schedule bb bb = OK tt. -Proof. - intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity. all: auto. -Qed. - - Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size"). @@ -397,7 +382,7 @@ Qed. Definition do_schedule (bb: bblock) : list bblock := if (Z.eqb (size bb) 1) then bb::nil else schedule bb. -Definition verified_schedule (bb : bblock) : res (list bblock) := +Definition verified_schedule_nob (bb : bblock) : res (list bblock) := let bb' := no_header bb in let lbb := do_schedule bb' in do tbb <- concat_all lbb; @@ -405,22 +390,48 @@ Definition verified_schedule (bb : bblock) : res (list bblock) := do schedcheck <- verify_schedule bb' tbb; stick_header_code (header bb) lbb. -Lemma verified_schedule_size: - forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb. +Lemma verified_schedule_nob_size: + forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb. Proof. intros. monadInv H. erewrite <- stick_header_code_size; eauto. apply verify_size_size. destruct x0; try discriminate. assumption. Qed. -Lemma verified_schedule_single_inst (ge: Genv.t fundef unit) (fn: function): - forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil). +Lemma verified_schedule_nob_no_header_in_middle: + forall lbb bb, + verified_schedule_nob bb = OK lbb -> + Forall (fun b => header b = nil) (tail lbb). Proof. - intros. unfold verified_schedule. - unfold do_schedule. rewrite no_header_size. rewrite H. simpl. - unfold verify_size. simpl. rewrite no_header_size. rewrite Z.add_0_r. cutrewrite (size bb =? size bb = true). rewrite verify_schedule_refl. simpl. - apply stick_header_code_no_header. all: auto. - rewrite H. reflexivity. + intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto. + eapply concat_all_no_header_in_middle. eassumption. +Qed. + +Lemma verified_schedule_nob_header: + forall bb tbb lbb, + verified_schedule_nob bb = OK (tbb :: lbb) -> + header bb = header tbb + /\ Forall (fun b => header b = nil) lbb. +Proof. + intros. split. + - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3. + simpl. reflexivity. + - apply verified_schedule_nob_no_header_in_middle in H. assumption. +Qed. + + +Definition verified_schedule (bb : bblock) : res (list bblock) := + match exit bb with + | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *) + | _ => verified_schedule_nob bb + end. + +Lemma verified_schedule_size: + forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb. +Proof. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + all: try (apply verified_schedule_nob_size; auto; fail). + destruct i. inv H. simpl. omega. Qed. Lemma verified_schedule_no_header_in_middle: @@ -428,8 +439,9 @@ Lemma verified_schedule_no_header_in_middle: verified_schedule bb = OK lbb -> Forall (fun b => header b = nil) (tail lbb). Proof. - intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto. - eapply concat_all_no_header_in_middle. eassumption. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail). + destruct i. inv H. simpl. auto. Qed. Lemma verified_schedule_header: @@ -438,15 +450,15 @@ Lemma verified_schedule_header: header bb = header tbb /\ Forall (fun b => header b = nil) lbb. Proof. - intros. split. - - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3. - simpl. reflexivity. - - apply verified_schedule_no_header_in_middle in H. assumption. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + all: try (eapply verified_schedule_nob_header; eauto; fail). + destruct i. inv H. split; simpl; auto. Qed. -Theorem verified_schedule_correct: + +Lemma verified_schedule_nob_correct: forall ge f bb lbb, - verified_schedule bb = OK lbb -> + verified_schedule_nob bb = OK lbb -> exists tbb, concat_all lbb = OK tbb /\ bblock_equiv ge f bb tbb. @@ -460,6 +472,26 @@ Proof. destruct (bblock_equivb _ _); auto; try discriminate. Qed. +Theorem verified_schedule_correct: + forall ge f bb lbb, + verified_schedule bb = OK lbb -> + exists tbb, + concat_all lbb = OK tbb + /\ bblock_equiv ge f bb tbb. +Proof. + intros. unfold verified_schedule in H. destruct (exit bb). destruct c. + all: try (eapply verified_schedule_nob_correct; eauto; fail). + destruct i. inv H. eexists. split; simpl; auto. constructor; auto. +Qed. + +Lemma verified_schedule_builtin_idem: + forall bb ef args res lbb, + exit bb = Some (PExpand (Pbuiltin ef args res)) -> + verified_schedule bb = OK lbb -> + lbb = bb :: nil. +Proof. + intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity. +Qed. Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) := -- cgit