diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 22:32:13 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 22:32:13 +0200 |
| commit | 0b99415251e56c64adb5caeec8f7c9c4f77ac926 (patch) | |
| tree | cfed8d56e859c4b1ebd51cecd0a257f9d4361704 /mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | |
| parent | e1ae915f648df0137d0f183f3b992583528184a7 (diff) | |
| download | compcert-kvx-0b99415251e56c64adb5caeec8f7c9c4f77ac926.tar.gz compcert-kvx-0b99415251e56c64adb5caeec8f7c9c4f77ac926.zip | |
generalize bblock_equiv into bblock_simu (abstract_bb)
Diffstat (limited to 'mppa_k1c/abstractbb/AbstractBasicBlocksDef.v')
| -rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index d1950209..618f3ebe 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -140,9 +140,9 @@ Proof. Qed. -(** A small theory of bblockram equality *) +(** A small theory of bblock equality *) -(* equalities on bblockram outputs *) +(* equalities on bblock outputs *) Definition res_eq (om1 om2: option mem): Prop := match om1 with | Some m1 => exists m2, om2 = Some m2 /\ forall x, m1 x = m2 x @@ -163,10 +163,10 @@ Proof. - intros; erewrite IHe, IHe0; auto. Qed. -Definition bblock_equiv (p1 p2: bblock): Prop - := forall m, res_eq (run p1 m) (run p2 m). +Definition bblock_simu (p1 p2: bblock): Prop + := forall m, (run p1 m) <> None -> res_eq (run p1 m) (run p2 m). -Lemma alt_inst_equiv_refl i old1 old2: +Lemma inst_equiv_refl i old1 old2: (forall x, old1 x = old2 x) -> forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (inst_run i m1 old1) (inst_run i m2 old2). @@ -178,10 +178,10 @@ Proof. unfold assign; intro y. destruct (R.eq_dec x y); auto. Qed. -Lemma alt_bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). +Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). Proof. induction p as [ | i p']; simpl; eauto. - intros m1 m2 H; lapply (alt_inst_equiv_refl i m1 m2); auto. + intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto. intros X; lapply (X m1 m2); auto; clear X. destruct (inst_run i m1 m1); simpl. - intros [m3 [H1 H2]]; rewrite H1; simpl; auto. @@ -205,11 +205,11 @@ Proof. - intro; subst; simpl; auto. Qed. -Lemma bblock_equiv_alt p1 p2: bblock_equiv p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p1 m1) (run p2 m2)). +Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)). Proof. - unfold bblock_equiv; intuition. - intros; eapply res_eq_trans. eapply alt_bblock_equiv_refl; eauto. - eauto. + unfold bblock_simu; intuition. + intros; eapply res_eq_trans. eauto. + eapply bblock_equiv_refl; eauto. Qed. |