diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-25 15:29:33 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-25 15:29:33 +0100 |
| commit | 9980f1ae211b04f568147b3c58897a9a1a121703 (patch) | |
| tree | afb2aef00c4428bc9d964b18ba496ba93d5907a3 /mppa_k1c/lib | |
| parent | 7e08f7bba8c36ded9d5787dd588336449ef1e62f (diff) | |
| download | compcert-kvx-9980f1ae211b04f568147b3c58897a9a1a121703.tar.gz compcert-kvx-9980f1ae211b04f568147b3c58897a9a1a121703.zip | |
Plugged Asmblockdeps into PostpassScheduling
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 8c299f88..69234938 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -20,6 +20,12 @@ Module AB:=Asmblock. 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'. + Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. Proof. @@ -1096,4 +1102,4 @@ Proof. intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. Qed. -End MATCH_STACK.
\ No newline at end of file +End MATCH_STACK. |