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

1 files changed, 110 insertions, 6 deletions

diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index fe3c07eb..ef9f5f0d 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -16,6 +16,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock.

 Require Import Asmblockgenproof0.

 Require Import PostpassScheduling.

+Require Import Asmblockgenproof.

 

 Local Open Scope error_monad_scope.

 

@@ -92,6 +93,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 +103,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 +115,108 @@ 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.

+  - destruct exb.

+    + destruct c.

+      * destruct i. discriminate.

+      * monadInv H. split; auto.

+    + monadInv H. split; auto.

+  - discriminate.

+Qed.

+

+Lemma exec_body_app:

+  forall l l' ge rs m rs'' m'',

+  exec_body ge (l ++ l') rs m = Next rs'' m'' ->

+  exists rs' m',

+       exec_body ge l rs m = Next rs' m'

+    /\ exec_body ge l' rs' m' = Next rs'' m''.

+Proof.

+  induction l.

+  - intros. simpl in H. repeat eexists. auto.

+  - intros. rewrite <- app_comm_cons in H. simpl in H.

+    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.

+    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).

+      repeat eexists. simpl. rewrite EXEBI. eauto. auto.

+    + discriminate.

+Qed.

+

+Lemma exec_body_pc:

+  forall l ge rs1 m1 rs2 m2,

+  exec_body ge l rs1 m1 = Next rs2 m2 ->

+  rs2 PC = rs1 PC.

+Proof.

+  induction l.

+  - intros. inv H. auto.

+  - intros until m2. intro EXEB.

+    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.

+    eapply IHl in H0. rewrite H0.

+    erewrite exec_basic_instr_pc; eauto.

+Qed.

+

+(* Lemma exec_basic_instr_pc_var:

+  forall ge i rs m rs' m' v,

+  exec_basic_instr ge i rs m = Next rs' m' ->

+  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.

+Proof.

+  intros. unfold exec_basic_instr in *. exploreInst.

+    - inv H. unfold exec_arith_instr. exploreInst. Search (_ # _ <- _).

+Qed.

+

+Lemma exec_body_pc_var:

+  forall l ge rs m rs' m' v,

+  exec_body ge l rs m = Next rs' m' ->

+  exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'.

+Proof.

+  induction l.

+  - intros. simpl. simpl in H. inv H. auto.

+  - intros. simpl in *.

+    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.

+    + 

+Qed. *)

+

+

+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.

+  exploit concat2_noexit; eauto. intros.

+  exploit concat2_decomp; eauto. intros. inv H2.

+(*   destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]. *)

+  unfold exec_bblock in H0. destruct (exec_body ge (body bb) rs m) eqn:EXEB.

+  - rewrite H3 in EXEB. apply exec_body_app in EXEB. destruct EXEB as (rs1 & m1 & EXEB1 & EXEB2).

+    repeat eexists.

+      unfold exec_bblock. rewrite EXEB1. rewrite H1. simpl. eauto.

+      exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H2. auto.

+      unfold exec_bblock.

+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 +228,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 ->