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

4 files changed, 28 insertions, 29 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 7361ee81..c6207627 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1297,14 +1297,13 @@ Variable Ge: genv.
 
 Local Hint Resolve trans_state_match.
 
-Lemma bblock_equiv_reduce: 
+Lemma bblock_simu_reduce:
   forall p1 p2 ge fn,
   Ge = Genv ge fn ->
   L.bblock_equiv Ge (trans_block p1) (trans_block p2) ->
-  Asmblockgenproof0.bblock_equiv ge fn p1 p2.
+  Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
-  unfold bblock_equiv, res_eq; intros p1 p2 ge fn H1 H2; constructor.
-  intros rs m.
+  unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK.
   generalize (H2 (trans_state (State rs m))); clear H2.
   intro H2. 
   exploit (forward_simu Ge rs m p1 ge fn (trans_state (State rs m))); eauto.
@@ -1599,37 +1598,38 @@ Definition string_of_op (op: P.op): ?? pstring :=
   | Fail => RET (Str "Fail")
   end.
 
-Definition bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
+Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
   if verb then
     IDT.verb_bblock_eq_test string_of_name string_of_op (trans_block p1) (trans_block p2)
   else
     IDT.bblock_eq_test (trans_block p1) (trans_block p2).
 
-Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp.
+Local Hint Resolve IDT.bblock_eq_test_correct bblock_simu_reduce IDT.verb_bblock_eq_test_correct: wlp.
 
-Theorem bblock_eq_test_correct verb p1 p2 :
-  WHEN bblock_eq_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Ge = Genv ge fn -> Asmblockgenproof0.bblock_equiv ge fn p1 p2.
+Theorem bblock_simu_test_correct verb p1 p2 :
+  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Ge = Genv ge fn -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
   wlp_simplify.
 Qed.
-Hint Resolve bblock_eq_test_correct: wlp.
+Hint Resolve bblock_simu_test_correct: wlp.
 
 (* Coerce bblock_eq_test into a pure function (this is a little unsafe like all oracles in CompCert). *)
 
 Import UnsafeImpure.
 
-Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2).
+Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2).
 
-Theorem pure_bblock_eq_test_correct verb p1 p2:
-  forall ge fn, Ge = Genv ge fn ->
-   pure_bblock_eq_test verb p1 p2 = true -> Asmblockgenproof0.bblock_equiv ge fn p1 p2.
+Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: Ge = Genv ge fn -> pure_bblock_simu_test verb p1 p2 = true -> bblock_simu ge fn p1 p2.
 Proof.
-   intros; unfold pure_bblock_eq_test. intros; eapply bblock_eq_test_correct; eauto.
+   intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto.
    apply unsafe_coerce_not_really_correct; eauto.
 Qed.
 
-Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_eq_test true.
+Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true.
 
-Definition bblock_equiv_eq := pure_bblock_eq_test_correct true.
+Lemma bblock_simub_correct p1 p2 ge fn: Ge = Genv ge fn -> bblock_simub p1 p2 = true -> bblock_simu ge fn p1 p2.
+Proof.
+ eapply (pure_bblock_simu_test_correct true).
+Qed.
 
 End SECT_BBLOCK_EQUIV.
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index ecd40f5c..15cb4c48 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -211,7 +211,7 @@ Qed.
 
 
 Definition verify_schedule (bb bb' : bblock) : res unit :=
-  match (bblock_equivb bb bb') with
+  match bblock_simub bb bb' with
   | true => OK tt
   | false => Error (msg "PostpassScheduling.verify_schedule")
   end.
@@ -230,7 +230,7 @@ Lemma verify_schedule_no_header:
   forall bb bb',
   verify_schedule (no_header bb) bb' = verify_schedule bb bb'.
 Proof.
-  intros. unfold verify_schedule. unfold bblock_equivb. unfold pure_bblock_eq_test. unfold bblock_eq_test. rewrite trans_block_noheader_inv.
+  intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv.
   reflexivity.
 Qed.
 
@@ -240,7 +240,7 @@ Lemma stick_header_verify_schedule:
   stick_header hd bb' = hbb' ->
   verify_schedule bb bb' = verify_schedule bb hbb'.
 Proof.
-  intros. unfold verify_schedule. unfold bblock_equivb. unfold pure_bblock_eq_test. unfold bblock_eq_test.
+  intros. unfold verify_schedule. unfold bblock_simub, pure_bblock_simu_test, bblock_simu_test.
   rewrite <- H. rewrite trans_block_header_inv. reflexivity.
 Qed.
 
@@ -429,15 +429,15 @@ Lemma verified_schedule_nob_correct:
   verified_schedule_nob bb = OK lbb ->
   exists tbb, 
      concat_all lbb = OK tbb
-  /\ bblock_equiv ge f bb tbb.
+  /\ bblock_simu ge f bb tbb.
 Proof.
   intros. monadInv H.
   exploit stick_header_code_concat_all; eauto.
   intros (tbb & CONC & STH).
   exists tbb. split; auto.
   rewrite verify_schedule_no_header in EQ0. erewrite stick_header_verify_schedule in EQ0; eauto.
-  eapply bblock_equiv_eq; eauto. unfold verify_schedule in EQ0. unfold bblock_equivb in EQ0.
-  destruct (pure_bblock_eq_test true _ _); auto; try discriminate.
+  eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ0.
+  destruct (bblock_simub _ _); auto; try discriminate.
 Qed.
 
 Theorem verified_schedule_correct:
@@ -445,7 +445,7 @@ Theorem verified_schedule_correct:
   verified_schedule bb = OK lbb ->
   exists tbb, 
      concat_all lbb = OK tbb
-  /\ bblock_equiv ge f bb tbb.
+  /\ bblock_simu ge f bb tbb.
 Proof.
   intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
   all: try (eapply verified_schedule_nob_correct; eauto; fail).
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index f470ef8a..5d4fc881 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -741,7 +741,7 @@ Proof.
       eapply transf_function_no_overflow; eauto. 
 
     erewrite transf_exec_bblock in H2; eauto.
-    inv BBEQ. rewrite H3 in H2.
+    unfold bblock_simu in BBEQ. rewrite BBEQ in H2; try congruence.
     exists (State rs' m'). split; try (constructor; auto).
     eapply transf_step_simu; eauto.
 
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index a8da1cf1..e0780b9d 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -21,11 +21,10 @@ Module AB:=Asmvliw.
 
 Hint Extern 2 (_ <> _) => congruence: asmgen.
 
-Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
-  | bblock_equiv_intro:
-      (forall rs m,
-      exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) ->
-      bblock_equiv ge f bb bb'.
+Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
+  forall rs m,
+    exec_bblock ge f bb rs m <> Stuck ->
+    exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m.
 
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.