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

2 files changed, 80 insertions, 67 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index b608255f..6a23e08e 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1659,118 +1659,131 @@ Proof.
     (* Pcb *)
     + simpl in H0. destruct (cmp_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i.
         ++ unfold par_eval_branch in H0. destruct (Val.cmp_bool _ _ _) eqn:VALCMP; try discriminate. destruct b.
-          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate.
+          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate.
               inv H0. inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
                 rewrite CFB. Simpl. rewrite (H0 r).
-                unfold eval_branch_deps. Admitted. (* rewrite VALCMP.
-                unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity.
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
+                unfold goto_label_deps. rewrite LPOS.
+                unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
           +++ inv H0. inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
-                rewrite CFB. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
+                rewrite CFB. Simpl. rewrite (H0 r).
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
                 reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
         ++ unfold par_eval_branch in H0. destruct (Val.cmpl_bool _ _ _) eqn:VALCMP; try discriminate. destruct b.
-          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate.
+          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate.
               inv H0; inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
-                rewrite CFB. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
-                unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity.
+                rewrite CFB. Simpl. rewrite (H0 r).
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
+                unfold goto_label_deps. rewrite LPOS.
+                unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
           +++ inv H0. inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
                 rewrite CFB. Simpl. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
                 reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
       (* Pcbu *)
-    + destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i.
+    + simpl in H0. destruct (cmpu_for_btest _) eqn:CFB. destruct o; try discriminate. destruct i.
         ++ unfold par_eval_branch in H0. destruct (Val_cmpu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b.
-          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate.
+          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate.
               inv H0. inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
-                rewrite CFB. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
-                unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity.
+                rewrite CFB. Simpl. rewrite (H0 r).
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
+                unfold goto_label_deps. rewrite LPOS.
+                unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
           +++ inv H0. inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
-                rewrite CFB. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
+                rewrite CFB. Simpl. rewrite (H0 r).
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
                 reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
         ++ unfold par_eval_branch in H0. destruct (Val_cmplu_bool _ _ _) eqn:VALCMP; try discriminate. destruct b.
-          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (rsr PC) eqn:NB; try discriminate.
+          +++ unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ PC) eqn:NB; try discriminate.
               inv H0; inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
-                rewrite CFB. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
-                unfold goto_label_deps. rewrite LPOS. rewrite NB. reflexivity.
+                rewrite CFB. Simpl. rewrite (H0 r).
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
+                unfold goto_label_deps. rewrite LPOS.
+                unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
           +++ inv H0. inv MSR; inv MSW. eexists; split; try split.
               * simpl. rewrite (H0 PC).
                 rewrite CFB. Simpl. rewrite (H0 r).
-                unfold eval_branch_deps. rewrite VALCMP.
+                unfold eval_branch_deps. unfold par_nextblock in VALCMP. rewrite Pregmap.gso in VALCMP; try discriminate. rewrite VALCMP.
                 reflexivity.
               * Simpl.
-              * intros rr; destruct rr; Simpl.
-Qed. *)
-(* 
-Theorem forward_simu_par_nextblockge ge fn rsr rsw mr mw sr sw sz rs' ex rs'' m'':
-  Ge = Genv ge fn ->
-  match_states (State rsr mr) sr ->
-  match_states (State rsw mw) sw ->
-  par_nextblock (Ptrofs.repr sz) rsr rsw = rs' ->
-  parexec_control ge fn ex rsr rs' mw = Next rs'' m'' ->
-  exists s'',
-     macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s''
-  /\ match_states (State rs'' m'') s''. *)
+              * intros rr; destruct rr; unfold par_nextblock; Simpl.
+  - simpl in *. inv MSR. inv MSW. inv H0. eexists. split.
+    rewrite (H1 PC). simpl. reflexivity.
+    split. Simpl.
+    intros rr. destruct rr; unfold par_nextblock; Simpl.
+Qed.
 
 Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
 
+(* Lemma put in Parallelizability. 
+Lemma prun_iw_app_some:
+  forall c c' sr sw s' s'',
+  prun_iw Ge c sw sr = Some s' ->
+  prun_iw Ge c' s' sr = Some s'' ->
+  prun_iw Ge (c ++ c') sw sr = Some s''.
+Proof.
+  induction c.
+  - simpl. intros. congruence.
+  - intros. simpl in *. destruct (macro_prun _ _ _ _); auto. eapply IHc; eauto. discriminate.
+Qed.
+*)
+
 Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz rs' m':
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr mr = Next rs' m' ->
+  parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr rsw mr mw = Next rs' m' ->
   exists s',
-     prun_iw Ge (trans_block_aux bdy sz ex) sr sw = Some s'
+     prun_iw Ge (trans_block_aux bdy sz ex) sw sr = Some s'
   /\ match_states (State rs' m') s'.
 Proof.
   intros. unfold parexec_wio_bblock_aux in H2. unfold trans_block_aux.
   destruct (parexec_wio_body _ _ _ _ _ _) eqn:WIOB; try discriminate.
   exploit forward_simu_par_body. 4: eapply WIOB. all: eauto.
   intros (s' & RUNB & MS').
-  destruct ex.
-  - exploit forward_simu_par_control. 4: eapply H2. all: eauto.
-Admitted.
-
+  exploit forward_simu_par_control. 4: eapply H2. all: eauto.
+  intros (s'' & RUNCTL & MS'').
+  eexists. split.
+  erewrite prun_iw_app_Some; eauto. unfold prun_iw. rewrite RUNCTL. reflexivity. eassumption.
+Qed.
 
-Theorem forward_simu_par_wio_bblock ge fn rsr mr sr bdy1 bdy2 ex sz rs' m' rs2 m2:
+Theorem forward_simu_par_wio_bblock ge fn rsr rsw mr sr sw mw bdy1 bdy2 ex sz rs' m' rs2 m2:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
-  parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr mr = Next rs' m' ->
+  match_states (State rsw mw) sw ->
+  parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw = Next rs' m' ->
   parexec_wio_body ge bdy2 rsr rs' mr m' = Next rs2 m2 ->
   exists s2',
-     prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr = Some s2'
+     prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr = Some s2'
   /\ match_states (State rs2 m2) s2'.
 Proof.
-  intros; exploit forward_simu_par_wio_bblock_aux. 4: eauto. all: eauto.
-  intros (s1' & X1 & X2).
-  exploit (forward_simu_par_body bdy2). 4: eauto. all: eauto.
-  intros (s2' & X3 & X4).
-  eexists; split; eauto.
-  erewrite prun_iw_app_Some; eauto.
+  intros. exploit forward_simu_par_wio_bblock_aux. 4: eapply H2. all: eauto.
+  intros (s' & RUNAUX & MS').
+  exploit forward_simu_par_body. 4: eapply H3. all: eauto.
+  intros (s'' & RUNBDY2 & MS'').
+  eexists. split.
+  erewrite prun_iw_app_Some; eauto. eassumption.
 Qed.
 
 Lemma trans_body_perserves_permutation bdy1 bdy2:
@@ -1838,7 +1851,7 @@ Admitted.
 Lemma forward_simu_par_wio_stuck_bdy1 ge fn rs m s1' bdy1 sz ex:
   Ge = Genv ge fn ->
   match_states (State rs m) s1' ->
-  parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rs m = Stuck ->
+  parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rs rs m m = Stuck ->
   prun_iw Ge ((trans_block_aux bdy1 sz ex)) s1' s1' = None.
 Proof.
   unfold parexec_wio_bblock_aux, trans_block_aux; intros.
@@ -1854,7 +1867,7 @@ Qed.
 Lemma forward_simu_par_wio_stuck_bdy2 ge fn rs m s1' bdy1 bdy2 sz ex m' rs':
   Ge = Genv ge fn ->
   match_states (State rs m) s1' ->
-  parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rs m = Next rs' m' ->
+  parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rs rs m m = Next rs' m' ->
   parexec_wio_body ge bdy2 rs rs' m m' = Stuck ->
   prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) s1' s1'=None.
 Proof.
@@ -1877,7 +1890,7 @@ Proof.
   inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).
   exploit trans_block_perserves_permutation; eauto.
   intros Perm.
-  remember (parexec_wio_bblock_aux _ _ _ _ _ _ _) as pwb.
+  remember (parexec_wio_bblock_aux _ _ _ _ _ _ _ _ _) as pwb.
   destruct pwb; try congruence.
   exploit forward_simu_par_wio_bblock; eauto. intros (s2' & PIW & MS').
   unfold prun; simpl; eexists; split; eauto.
@@ -1894,7 +1907,7 @@ Proof.
   inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).
   exploit trans_block_perserves_permutation; eauto.
   intros Perm.
-  destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _) eqn:WIOEXIT.
+  destruct (parexec_wio_bblock_aux _ _ _ _ _ _ _ _) eqn:WIOEXIT.
   - econstructor; eauto. split. eapply forward_simu_par_wio_stuck_bdy2; eauto. auto.
   - clear WIO. econstructor; eauto. split; eauto.
     simpl; apply prun_iw_app_None; auto.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index d3349344..8407f28d 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -233,25 +233,25 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
   | Pbuiltin ef args res =>
       Stuck (**r treated specially below *)
   end
-  | None => Next rsw mw
+  | None => Next (rsw#PC <- (rsr#PC)) mw
 end.
 
 
-Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m: mem): outcome :=
-  match parexec_wio_body bdy rs rs m m with
+Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
+  match parexec_wio_body bdy rsr rsw mr mw with
   | Next rsw mw =>
-    let rs := par_nextblock size_b rs in 
+    let rsr := par_nextblock size_b rsr in 
     let rsw := par_nextblock size_b rsw in 
-    parexec_control f ext rs rsw mw
+    parexec_control f ext rsr rsw mw
   | Stuck => Stuck
   end.
 
 Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
-  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m.
+  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
 
 Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ 
-      o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with
+      o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs rs m m with
       | Next rsw mw => parexec_wio_body bdy2 rs rsw m mw
       | Stuck => Stuck
       end.