diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-01 14:58:59 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-01 14:58:59 +0100 |
| commit | c3034c18bff34350a7c0d386cd01651622912eb6 (patch) | |
| tree | 125a62e7a82cb78c6196646a3fcbb8dc96043184 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 8ae9063a94fbf3756bb2b1d596f35b81e3e608eb (diff) | |
| download | compcert-kvx-c3034c18bff34350a7c0d386cd01651622912eb6.tar.gz compcert-kvx-c3034c18bff34350a7c0d386cd01651622912eb6.zip | |
Proof of transf_blocks_verified
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 55 |
1 files changed, 46 insertions, 9 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index c95a8917..a1d7b977 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -113,6 +113,11 @@ Axiom verified_schedule_correct: concat_all lbb = OK tbb
/\ bblock_equiv ge f bb tbb.
+Axiom verified_schedule_size:
+ forall bb lbb,
+ verified_schedule bb = OK lbb ->
+ size bb = size_blocks lbb.
+
Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
Remark builtin_body_nil:
@@ -468,21 +473,53 @@ Proof. Qed.
Lemma tail_find_bblock:
- forall f ofs bb,
- find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
- exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks f) (bb::c).
+ forall lbb pos bb,
+ find_bblock pos lbb = Some bb ->
+ exists c, code_tail pos lbb (bb::c).
Proof.
-Admitted.
+ induction lbb.
+ - intros. simpl in H. inv H.
+ - intros. simpl in H.
+ destruct (zlt pos 0); try (inv H; fail).
+ destruct (zeq pos 0).
+ + inv H. exists lbb. constructor; auto.
+ + apply IHlbb in H. destruct H as (c & TAIL). exists c.
+ cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto.
+ omega.
+Qed.
+
+Lemma code_tail_head_app:
+ forall l pos c1 c2,
+ code_tail pos c1 c2 ->
+ code_tail (pos + size_blocks l) (l++c1) c2.
+Proof.
+ induction l.
+ - intros. simpl. rewrite Z.add_0_r. auto.
+ - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption.
+Qed.
Lemma transf_blocks_verified:
- forall c tc ofs bb c',
+ forall c tc pos bb c',
transf_blocks c = OK tc ->
- code_tail (Ptrofs.unsigned ofs) c (bb::c') ->
+ code_tail pos c (bb::c') ->
exists lbb,
verified_schedule bb = OK lbb
- /\ exists tc', code_tail (Ptrofs.unsigned ofs) tc (lbb ++ tc').
-Proof.
-Admitted.
+ /\ exists tc', code_tail pos tc (lbb ++ tc').
+Proof.
+ induction c; intros.
+ - simpl in H. inv H. inv H0.
+ - inv H0.
+ + monadInv H. exists (schedule bb).
+ split; simpl; auto. eexists; eauto. econstructor; eauto.
+ + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.
+ exploit IHc; eauto.
+ intros (lbb & TRANS & tc' & TAIL).
+ monadInv TRANS.
+ repeat eexists; eauto.
+ erewrite verified_schedule_size; eauto.
+ apply code_tail_head_app.
+ eauto.
+Qed.
Lemma transf_find_bblock:
forall ofs f bb tf,
|