diff options
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 17 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpConfig.v | 4 |
2 files changed, 19 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c2477e66..80383c2f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1313,6 +1313,7 @@ Admitted. (* FIXME - à voir avec Sylvain *) Global Opaque bblock_eq_test. Hint Resolve bblock_eq_test_correct: wlp. + Inductive bblock_equiv' (bb bb': L.bblock) := | bblock_equiv_intro': (forall s, exec Ge bb s = exec Ge bb' s) -> @@ -1329,6 +1330,22 @@ Axiom bblock_equiv'_eq: forall b1 b2, bblock_equivb b1 b2 = true <-> bblock_equiv' b1 b2. (* FIXME - à voir avec Sylvain *) + +(* 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: Asmblock.bblock): bool := unsafe_coerce (bblock_eq_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. +Proof. + intros; unfold pure_bblock_eq_test. intros; eapply bblock_eq_test_correct; eauto. + apply unsafe_coerce_not_really_correct; eauto. +Qed. + + End SECT. Extract Constant bblock_equivb => "PostpassSchedulingOracle.bblock_equivb'". diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v index 55931e0f..3d807c4e 100644 --- a/mppa_k1c/abstractbb/Impure/ImpConfig.v +++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v @@ -19,7 +19,7 @@ Module Type ImpureView. *) -(* +(* *) Module UnsafeImpure. Parameter unsafe_coerce: forall {A}, t A -> A. @@ -27,7 +27,7 @@ Module Type ImpureView. Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=x -> mayRet k x. End UnsafeImpure. -*) +(* *) End ImpureView. |