diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-20 10:17:46 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-20 10:17:46 +0200 |
| commit | a9c90fe3354f65340283dc79431bc6915ed1ad90 (patch) | |
| tree | b23f9d32f7b2d33c2eec38e56556bacc7f7e6b0b /scheduling/BTL_Scheduler.v | |
| parent | f59ff208a301bf3f04aab350d9f0b3b217ddeac3 (diff) | |
| download | compcert-kvx-a9c90fe3354f65340283dc79431bc6915ed1ad90.tar.gz compcert-kvx-a9c90fe3354f65340283dc79431bc6915ed1ad90.zip | |
proof for symbolic simu, need to finish equiv_inputs
Diffstat (limited to 'scheduling/BTL_Scheduler.v')
| -rw-r--r-- | scheduling/BTL_Scheduler.v | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 63114125..e7d2b37f 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -92,16 +92,16 @@ Qed. Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x, check_symbolic_simu_rec f1 f2 lpc = OK x -> - forall pc ib1, (fn_code f1)!pc = Some ib1 -> + forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc -> exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). Proof. -Admitted. - (* - induction lpc; simpl; intros f1 f2 x X pc ib1 PC; try (inv X; fail). - destruct ((fn_code f1) ! pc), ((fn_code f2) ! pc); inv X. - eapply IHlpc; eauto. + induction lpc; simpl; intros f1 f2 x X pc ib1 (PC & HIN); try contradiction. + destruct HIN; subst. + - rewrite PC in X; destruct ((fn_code f2)!pc); monadInv X. + exists i; split; auto. destruct x0. eapply simu_check_correct; eauto. + - destruct ((fn_code f1)!a), ((fn_code f2)!a); monadInv X. + eapply IHlpc; eauto. Qed. - *) Lemma check_symbolic_simu_correct x f1 f2: check_symbolic_simu f1 f2 = OK x -> @@ -109,7 +109,8 @@ Lemma check_symbolic_simu_correct x f1 f2: exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2). Proof. unfold check_symbolic_simu; intros X pc ib1 PC. - eapply check_symbolic_simu_rec_correct; eauto. + eapply check_symbolic_simu_rec_correct; intuition eauto. + apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto. Qed. Definition transf_function (f: BTL.function) := |