diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 10:48:03 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 10:48:03 +0100 |
commit | cd69b24565713610d0ea5a613f4871af6e18e9d4 (patch) | |
tree | 83b17653996bdacfa64b529a542e8269d30461ac | |
parent | e9859d89510e6593c83f954b8b9580fff0dd51f4 (diff) | |
download | compcert-kvx-cd69b24565713610d0ea5a613f4871af6e18e9d4.tar.gz compcert-kvx-cd69b24565713610d0ea5a613f4871af6e18e9d4.zip |
No more axiom remaining in PostpassScheduling.v (but still a couple remaining in Asmblockdeps)
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 | ||||
-rw-r--r-- | mppa_k1c/PostpassScheduling.v | 98 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 12 |
3 files changed, 66 insertions, 46 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index bb800b99..4f10406f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1366,7 +1366,7 @@ Axiom bblock_equivb: L.bblock -> L.bblock -> bool. Axiom bblock_equiv'_eq: forall b1 b2, - bblock_equivb b1 b2 = true <-> bblock_equiv' b1 b2. (* FIXME - à voir avec Sylvain *) + bblock_equivb b1 b2 = true -> bblock_equiv' b1 b2. (* FIXME - à voir avec Sylvain *) (* Coerce bblock_eq_test into a pure function (this is a little unsafe like all oracles in CompCert). *) 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) := diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2ecb494d..f969e5b4 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -38,18 +38,6 @@ Proof. eapply H1; eauto. Qed. -Lemma verified_schedule_builtin_idem (ge: Genv.t fundef unit) (fn: function): - forall bb ef args res lbb, - exit bb = Some (PExpand (Pbuiltin ef args res)) -> - verified_schedule bb = OK lbb -> - lbb = bb :: nil. -Proof. - intros. exploit builtin_body_nil; eauto. intros. - rewrite verified_schedule_single_inst in H0; auto. - - inv H0. auto. - - unfold size. rewrite H. rewrite H1. simpl. auto. -Qed. - Lemma exec_body_app: forall l l' ge rs m rs'' m'', exec_body ge (l ++ l') rs m = Next rs'' m'' -> |