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

2 files changed, 106 insertions, 38 deletions

diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 1483a5d7..e8e6fcc5 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -21,30 +21,60 @@ Axiom schedule: bblock -> list bblock.
 
 Extract Constant schedule => "PostpassSchedulingOracle.schedule".
 
-(* TODO - implement the verificator *)
-Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
+(* TODO: refactorisation.
 
-Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
-  match lbb with
-  | nil => OK nil
-  | (cons bb lbb) =>
-      do tlbb <- transf_blocks lbb;
-      do tbb <- verified_schedule bb;
-      OK (tbb ++ tlbb)
-  end.
+... concat2 ...
 
-Definition transl_function (f: function) : res function :=
-  do lb <- transf_blocks (fn_blocks f); 
-  OK (mkfunction (fn_sig f) lb).
-
-Definition transf_function (f: function) : res function :=
-  do tf <- transl_function f;
-  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
-  then Error (msg "code size exceeded")
-  else OK tf.
-
-Definition transf_fundef (f: fundef) : res fundef :=
-  transf_partial_fundef transf_function f.
-
-Definition transf_program (p: program) : res program :=
+Fixpoint concat_all (lbb: list bblock) : res bblock :=

+  match lbb with

+  | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")

+  | bb::nil => OK bb

+  | bb::lbb =>

+      do bb' <- concat_all lbb;

+      concat2 bb bb'

+  end.

+

+Axiom test_equiv_bblock: bblock -> bblock -> bool.

+

+Axiom test_equiv_bblock_correct:

+  forall ge f bb tbb,

+  test_equiv bb tbb = true ->

+  bblock_equiv ge f bb tbb.

+

+Definition verified_schedule (bb : bblock) : res (list bblock) := 

+  DO lbb <- (schedule bb) ;

+  DO tbb <- (concat lbb) ;

+  DO res <- test_equiv_bblock bb tbb ;

+  if res 

+  then OK lbb

+  else Error (msg "blah").

+

+*)

+

+(* TODO - implement the verificator *)

+Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).

+

+Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=

+  match lbb with

+  | nil => OK nil

+  | (cons bb lbb) =>

+      do tlbb <- transf_blocks lbb;

+      do tbb <- verified_schedule bb;

+      OK (tbb ++ tlbb)

+  end.

+

+Definition transl_function (f: function) : res function :=

+  do lb <- transf_blocks (fn_blocks f); 

+  OK (mkfunction (fn_sig f) lb).

+

+Definition transf_function (f: function) : res function :=

+  do tf <- transl_function f;

+  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))

+  then Error (msg "code size exceeded")

+  else OK tf.

+

+Definition transf_fundef (f: fundef) : res fundef :=

+  transf_partial_fundef transf_function f.

+

+Definition transf_program (p: program) : res program :=

   transform_partial_program transf_fundef p.
\ No newline at end of file
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 35936303..c95a8917 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -50,7 +50,14 @@ Proof.
   - intros. rewrite <- app_comm_cons. discriminate.

 Qed.

 

+Definition check_size bb :=

+  if zlt Ptrofs.max_unsigned (size bb)

+    then Error (msg "PostpassSchedulingproof.check_size")

+  else OK tt.

+

 Program Definition concat2 (bb bb': bblock) : res bblock :=

+  do ch <- check_size bb;

+  do ch' <- check_size bb';

   match (exit bb) with

   | None => 

       match (header bb') with

@@ -78,6 +85,18 @@ Next Obligation.
     apply (H ef args res). contradict H1. auto.

 Qed.

 

+Lemma concat2_zlt_size:

+  forall a b bb,

+  concat2 a b = OK bb ->

+     size a <= Ptrofs.max_unsigned

+  /\ size b <= Ptrofs.max_unsigned.

+Proof.

+  intros. monadInv H.

+  split.

+  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.

+  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.

+Qed.

+

 Fixpoint concat_all (lbb: list bblock) : res bblock :=

   match lbb with

   | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")

@@ -123,7 +142,7 @@ Lemma concat2_noexit:
 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.

+  unfold concat2 in H. simpl in H. monadInv H.

 Qed.

 

 Lemma concat2_decomp:

@@ -139,10 +158,10 @@ Proof.
   destruct hdb.

   - destruct exb.

     + destruct c.

-      * destruct i. discriminate.

+      * destruct i. monadInv H.

       * monadInv H. split; auto.

     + monadInv H. split; auto.

-  - discriminate.

+  - monadInv H.

 Qed.

 

 Lemma exec_body_app:

@@ -287,7 +306,6 @@ Qed.
 

 Lemma concat2_straight:

   forall a b bb rs m rs'' m'' f ge,

-  size a <= Ptrofs.max_unsigned -> size b <= Ptrofs.max_unsigned ->

   concat2 a b = OK bb ->

   exec_bblock ge f bb rs m = Next rs'' m'' ->

   exists rs' m',

@@ -295,7 +313,8 @@ Lemma concat2_straight:
     /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))

     /\ exec_bblock ge f b rs' m' = Next rs'' m''.

 Proof.

-  intros until ge. intros LTA LTB CONC2 EXEB.

+  intros until ge. intros CONC2 EXEB.

+  exploit concat2_zlt_size; eauto. intros (LTA & LTB).

   exploit concat2_noexit; eauto. intros EXA.

   exploit concat2_decomp; eauto. intros. inv H.

   unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.

@@ -315,8 +334,6 @@ Proof.
     exploit AB.size_positive. instantiate (1 := b). intro. omega.

 Qed.

 

-Axiom TODO: False.

-

 Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :

   forall a bb rs m lbb rs'' m'', 

   lbb <> nil ->

@@ -331,20 +348,20 @@ Proof.
   intros until m''. intros Hnonil CONC EXEB.

   simpl in CONC.

   destruct lbb as [|b lbb]; try contradiction. clear Hnonil.

-  monadInv CONC. exploit concat2_straight; eauto. 1-2: destruct TODO. intros (rs' & m' & EXEB1 & PCeq & EXEB2).

+  monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2).

   exists x. repeat econstructor. all: eauto.

-Admitted.

+Qed.

 

 Lemma concat2_size:

   forall a b bb, concat2 a b = OK bb -> size bb = size a + size b.

 Proof.

   intros. unfold concat2 in H.

   destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.

-  destruct exa; try discriminate. destruct hdb; try discriminate. destruct exb; try discriminate.

+  destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2).

   - destruct c.

-    + destruct i; try discriminate.

-    + inv H. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.

-  - inv H. unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.

+    + destruct i; try (monadInv EQ2).

+    + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.

+  - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.

 Qed.

 

 Lemma concat_all_size :

@@ -450,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 ->

@@ -458,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,