diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-24 12:00:58 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-24 12:00:58 +0100 |
| commit | e83e59892faf15d4d150761de75633a3624b2126 (patch) | |
| tree | e28b39945de14838e221514c2bfdb2677da61527 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 897d83b892df7f2e7a0a633ab7c22313c91c1bb9 (diff) | |
| download | compcert-kvx-e83e59892faf15d4d150761de75633a3624b2126.tar.gz compcert-kvx-e83e59892faf15d4d150761de75633a3624b2126.zip | |
Un peu d'avancement sur PostpassSchedulingproof
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 36 |
1 files changed, 27 insertions, 9 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 4205398a..fe3c07eb 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -41,11 +41,12 @@ Proof. - discriminate.
Qed.
-Lemma app_nonil2 {A: Type} : forall (l': list A) l, l' <> nil -> l ++ l' <> nil.
+Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil.
Proof.
- induction l'; try contradiction.
- intros. cutrewrite (l ++ a :: l' = (l ++ a :: nil) ++ l'). apply app_nonil.
-Admitted.
+ destruct l.
+ - intros. simpl; auto.
+ - intros. rewrite <- app_comm_cons. discriminate.
+Qed.
Program Definition concat2 (bb bb': bblock) : res bblock :=
match (exit bb) with
@@ -91,14 +92,31 @@ Axiom verified_schedule_correct: concat_all lbb = OK tbb
/\ bblock_equiv ge f bb tbb.
-Lemma verified_schedule_builtin_idem:
- forall bi ef args res lbb,
- exit bi = Some (PExpand (Pbuiltin ef args res)) ->
- verified_schedule bi = OK lbb ->
- lbb = bi :: nil.
+Remark builtin_body_nil:
+ forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
+Proof.
+ intros. destruct bb as [hd bdy ex WF]. simpl in *.
+ apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
+ 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)) ->
+ verified_schedule bb = OK lbb ->
+ lbb = bb :: nil.
+Proof.
+ intros. exploit builtin_body_nil; eauto. intros.
+ rewrite verified_schedule_single_inst in H0.
+ - inv H0. auto.
+ - unfold size. rewrite H. rewrite H1. simpl. auto.
+Qed.
+
Lemma concat_exec_bblock_nonil (ge: Genv.t fundef unit) (f: function) :
forall a bb rs m lbb rs'' m'',
lbb <> nil ->
|