diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:15:15 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-07-30 11:15:15 +0200 |
| commit | 211382d21013c038c3c716454fcfa5a375dba8ba (patch) | |
| tree | 8eff5ce39ad3909c397ca157bc91e9b1e1cf3800 | |
| parent | 98c22a6f37c7230faf80b6366aaa1c2476f9e67c (diff) | |
| download | compcert-kvx-211382d21013c038c3c716454fcfa5a375dba8ba.tar.gz compcert-kvx-211382d21013c038c3c716454fcfa5a375dba8ba.zip | |
(#139) - Predicate is_concat
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 15 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
2 files changed, 9 insertions, 8 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 76757eba..8b6de1e2 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -208,7 +208,8 @@ Proof. + apply IHlbb in EQ. assumption. Qed. - +Inductive is_concat : bblock -> list bblock -> Prop := + | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb. Definition verify_schedule (bb bb' : bblock) : res unit := match bblock_simub bb bb' with @@ -466,14 +467,14 @@ Qed. Lemma verified_schedule_nob_correct: forall ge f bb lbb, verified_schedule_nob bb = OK lbb -> - exists tbb, - concat_all lbb = OK tbb + exists tbb, + is_concat tbb lbb /\ bblock_simu ge f bb tbb. Proof. intros. monadInv H. exploit stick_header_code_concat_all; eauto. intros (tbb & CONC & STH). - exists tbb. split; auto. + exists tbb. split; auto. constructor; auto. rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto. eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2. destruct (bblock_simub _ _); auto; try discriminate. @@ -482,13 +483,13 @@ Qed. Theorem verified_schedule_correct: forall ge f bb lbb, verified_schedule bb = OK lbb -> - exists tbb, - concat_all lbb = OK tbb + exists tbb, + is_concat tbb lbb /\ bblock_simu ge f bb tbb. Proof. intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (eapply verified_schedule_nob_correct; eauto; fail). - inv H. eexists. split; simpl; auto. constructor; auto. + inv H. eexists. split; simpl; auto. constructor; auto. simpl; auto. constructor; auto. Qed. Lemma verified_schedule_builtin_idem: diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 0edaf4e2..2207a2fa 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -736,7 +736,7 @@ Proof. induction 1; intros; inv MS. - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). + exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC. assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. |