diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 08:37:05 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 08:37:05 +0200 |
commit | 579ce1d6d18371b753fff2dac7305e13b85b8cab (patch) | |
tree | 68879b84ccfabf0424178c4ad046ebd97461d8c2 /mppa_k1c/Asmblockdeps.v | |
parent | 3be0a8daa9ed0e787d1e4b26092aea4a496b88fd (diff) | |
download | compcert-kvx-579ce1d6d18371b753fff2dac7305e13b85b8cab.tar.gz compcert-kvx-579ce1d6d18371b753fff2dac7305e13b85b8cab.zip |
generalize bblock_equiv into bblock_simu
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 32 |
1 files changed, 16 insertions, 16 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. |