diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-25 11:25:16 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-25 11:25:16 +0100 |
| commit | 0e2080919f53ff40276c6aa1f253a591a89ec917 (patch) | |
| tree | 4a449ec738c35f48ac3a3372cd08b8ea50c5f2f4 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | e83e59892faf15d4d150761de75633a3624b2126 (diff) | |
| download | compcert-kvx-0e2080919f53ff40276c6aa1f253a591a89ec917.tar.gz compcert-kvx-0e2080919f53ff40276c6aa1f253a591a89ec917.zip | |
Progrès dans PostpassSchedulingproof
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 52 |
1 files changed, 46 insertions, 6 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index fe3c07eb..56662a0a 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -92,6 +92,8 @@ Axiom verified_schedule_correct: concat_all lbb = OK tbb
/\ bblock_equiv ge f bb tbb.
+Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
+
Remark builtin_body_nil:
forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
Proof.
@@ -100,11 +102,6 @@ Proof. eapply H1; eauto.
Qed.
-Lemma verified_schedule_single_inst:
- forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
-Proof.
-Admitted.
-
Lemma verified_schedule_builtin_idem:
forall bb ef args res lbb,
exit bb = Some (PExpand (Pbuiltin ef args res)) ->
@@ -117,6 +114,45 @@ Proof. - unfold size. rewrite H. rewrite H1. simpl. auto.
Qed.
+Lemma concat2_noexit:
+ forall a b bb,
+ concat2 a b = OK bb ->
+ exit a = None.
+Proof.
+ intros. destruct a as [hd bdy ex WF]; simpl in *.
+ destruct ex as [e|]; simpl in *; auto.
+ unfold concat2 in H. simpl in H. discriminate.
+Qed.
+
+Lemma concat2_decomp:
+ forall a b bb,
+ concat2 a b = OK bb ->
+ body bb = body a ++ body b
+ /\ exit bb = exit b.
+Proof.
+ intros. exploit concat2_noexit; eauto. intros.
+ destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *.
+ subst exa.
+ unfold concat2 in H; simpl in H.
+ destruct hdb.
+Admitted.
+
+Lemma concat2_straight:
+ forall a b bb rs m rs'' m'' f ge,
+ concat2 a b = OK bb ->
+ exec_bblock ge f bb rs m = Next rs'' m'' ->
+ exists rs' m',
+ exec_bblock ge f a rs m = Next rs' m'
+ /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
+ /\ exec_bblock ge f b rs' m' = Next rs'' m''.
+Proof.
+ intros.
+
+
+ apply concat2_noexit in H. destruct a as [hd bdy ex WF]. simpl in *. subst ex.
+ repeat eexists. unfold exec_bblock. simpl.
+Admitted.
+
Lemma concat_exec_bblock_nonil (ge: Genv.t fundef unit) (f: function) :
forall a bb rs m lbb rs'' m'',
lbb <> nil ->
@@ -128,9 +164,13 @@ Lemma concat_exec_bblock_nonil (ge: Genv.t fundef unit) (f: function) : /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
/\ exec_bblock ge f bb' rs' m' = Next rs'' m''.
Proof.
-
+ intros until m''. intros Hnonil CONC EXEB.
+ simpl in CONC.
+ destruct lbb as [|b lbb]; try contradiction. clear Hnonil.
+ monadInv CONC. exists x.
Admitted.
+
Lemma concat_all_size :
forall a lbb bb bb',
concat_all (a :: lbb) = OK bb ->
|