Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass

1 files changed, 137 insertions, 10 deletions

diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index c95a8917..ad423fb0 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -113,8 +113,18 @@ 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).

 

+Axiom verified_schedule_header:

+  forall bb tbb lbb,

+  verified_schedule bb = OK (tbb :: lbb) ->

+  header bb = header tbb.

+

 Remark builtin_body_nil:

   forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.

 Proof.

@@ -468,21 +478,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,

@@ -498,12 +540,97 @@ Proof.
   eapply transf_blocks_verified; eauto.

 Qed.

 

+Lemma transf_exec_body:

+  forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.

+Proof.

+Admitted.

+

+Lemma symbol_address_preserved:

+  forall l, Genv.symbol_address ge l Ptrofs.zero = Genv.symbol_address tge l Ptrofs.zero.

+Proof.

+  intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.

+Qed.

+

+Lemma head_tail {A: Type}:

+  forall (l: list A) hd, hd::l = hd :: (tail (hd::l)).

+Proof.

+  intros. simpl. auto.

+Qed.

+

+Lemma verified_schedule_not_empty:

+  forall bb lbb,

+  verified_schedule bb = OK lbb -> lbb <> nil.

+Proof.

+  intros. apply verified_schedule_size in H.

+  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.

+  destruct lbb; simpl in *; discriminate.

+Qed.

+

+Lemma verified_schedule_label:

+  forall bb tbb lbb l,

+  verified_schedule bb = OK (tbb :: lbb) ->

+  is_label l bb = is_label l tbb.

+Proof.

+Admitted.

+

+Lemma label_pos_head_app:

+  forall c bb lbb l tc,

+  verified_schedule bb = OK lbb ->

+  label_pos l 0 c = label_pos l 0 tc ->

+  label_pos l 0 (bb :: c) = label_pos l 0 (lbb ++ tc).

+Proof.

+  induction c.

+  - intros. simpl in H0. destruct lbb.

+    + apply verified_schedule_not_empty in H. contradiction.

+    + rewrite (head_tail lbb). simpl tl.

+      simpl. erewrite verified_schedule_label; eauto.

+      destruct (is_label l b) eqn:ISLBL; simpl; auto.

+      (* TODO - finish *)

+Admitted.

+

+

+Lemma label_pos_preserved:

+  forall c tc l,

+  transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.

+Proof.

+  induction c.

+  - intros. simpl in *. inv H. reflexivity.

+  - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ.

+    eapply label_pos_head_app; eauto.

+Qed.

+

+Lemma label_pos_preserved_blocks:

+  forall l f tf,

+  transf_function f = OK tf ->

+  label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).

+Proof.

+  intros. monadInv H. monadInv EQ.

+  destruct (zlt Ptrofs.max_unsigned _); try discriminate.

+  monadInv EQ0. simpl. eapply label_pos_preserved; eauto.

+Qed.

+

+Lemma transf_exec_control:

+  forall f tf ex rs m,

+  transf_function f = OK tf ->

+  exec_control ge f ex rs m = exec_control tge tf ex rs m.

+Proof.

+  intros. destruct ex; simpl; auto.

+  assert (ge = Genv.globalenv prog). auto.

+  assert (tge = Genv.globalenv tprog). auto.

+  pose symbol_address_preserved.

+  exploreInst; simpl; auto; try congruence.

+  - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.

+Admitted.

+

+

 Lemma transf_exec_bblock:

   forall f tf bb rs m,

   transf_function f = OK tf ->

   exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m.

 Proof.

-Admitted.

+  intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto.

+  eapply transf_exec_control; eauto.

+Qed.

 

 Lemma transf_step_simu:

   forall tf b lbb ofs c tbb rs m rs' m',