diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-01 12:18:51 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-01 12:18:51 +0200 |
| commit | 9b74954477b9b1e5b75fbdd15215fc09941f72e4 (patch) | |
| tree | 5b6a338a681452bf5746535bbab81ec6de83db2e /scheduling/BTL_Livecheck.v | |
| parent | 84ddcd68504461bb2dee30ac38f0bb495b8aec38 (diff) | |
| download | compcert-kvx-9b74954477b9b1e5b75fbdd15215fc09941f72e4.tar.gz compcert-kvx-9b74954477b9b1e5b75fbdd15215fc09941f72e4.zip | |
Lemma liveness_checker_correct
Diffstat (limited to 'scheduling/BTL_Livecheck.v')
| -rw-r--r-- | scheduling/BTL_Livecheck.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 62833dc3..6015d91f 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -126,6 +126,18 @@ Definition liveness_checker (f: BTL.function): res unit := | false => Error (msg "BTL_Livecheck: liveness_checker failed") end. +Lemma liveness_checker_correct f n ibf: + liveness_checker f = OK tt -> + f.(fn_code)!n = Some ibf -> + iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt. +Proof. + unfold liveness_checker. + destruct list_iblock_checker eqn:EQL; try congruence. + intros _ P. exploit list_iblock_checker_correct; eauto. + - eapply PTree.elements_correct; eauto. + - simpl; auto. +Qed. + Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. (** TODO: adapt stuff RTLpathLivegenproof *) |