diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-31 18:56:14 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-31 18:56:14 +0100 |
| commit | b6adc00a4726538ce80a00ddff1c9b65edd1b0d8 (patch) | |
| tree | 77d65a8136b57672b566b070f2f00a372f320647 | |
| parent | 44cbc6d5ec1afd92203c202054dbaf9e4083aa9f (diff) | |
| download | compcert-kvx-b6adc00a4726538ce80a00ddff1c9b65edd1b0d8.tar.gz compcert-kvx-b6adc00a4726538ce80a00ddff1c9b65edd1b0d8.zip | |
Décomposition de transf_find_bblock en lemmes
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index e66f862f..c95a8917 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -467,6 +467,23 @@ Proof. intros. inv H0. inv H. econstructor; eauto.
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).
+Proof.
+Admitted.
+
+Lemma transf_blocks_verified:
+ forall c tc ofs bb c',
+ transf_blocks c = OK tc ->
+ code_tail (Ptrofs.unsigned ofs) c (bb::c') ->
+ exists lbb,
+ verified_schedule bb = OK lbb
+ /\ exists tc', code_tail (Ptrofs.unsigned ofs) tc (lbb ++ tc').
+Proof.
+Admitted.
+
Lemma transf_find_bblock:
forall ofs f bb tf,
find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
@@ -475,7 +492,11 @@ Lemma transf_find_bblock: verified_schedule bb = OK lbb
/\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c).
Proof.
-Admitted.
+ intros.
+ monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
+ monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL).
+ eapply transf_blocks_verified; eauto.
+Qed.
Lemma transf_exec_bblock:
forall f tf bb rs m,
|