diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-18 11:46:10 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-06-18 11:46:10 +0200 |
| commit | 0321d5f0aa2478ab830990a3637c37566bd9b634 (patch) | |
| tree | e2af4c119f0d76b1dd2f91f120b44da5f6c0ff59 /scheduling/RTLtoBTLproof.v | |
| parent | 86e108c7b95456e986605cb1861cb5128f348ec0 (diff) | |
| download | compcert-kvx-0321d5f0aa2478ab830990a3637c37566bd9b634.tar.gz compcert-kvx-0321d5f0aa2478ab830990a3637c37566bd9b634.zip | |
finish RTLtoBTL proof
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 4af5668c..8a352434 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -737,12 +737,28 @@ Proof. - eapply senv_preserved. Qed. +Theorem all_fundef_liveness_ok b f: + Genv.find_funct_ptr tge b = Some f -> liveness_ok_fundef f. +Proof. + unfold match_prog, match_program in TRANSL. + unfold Genv.find_funct_ptr, tge; simpl; intro X. + destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence. + destruct y as [tf0|]; try congruence. + inversion X as [H1]. subst. clear X. + remember (@Gfun fundef unit f) as f2. + destruct H as [ctx' f1 f2 H0|]; try congruence. + inversion Heqf2 as [H2]. subst; clear Heqf2. + exploit transf_fundef_correct; eauto. + destruct f; econstructor. + inv H1; eapply liveness_ok; eauto. +Qed. + Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (BTL.fsem tprog). Proof. eapply compose_forward_simulations. - eapply transf_program_correct_cfg. - - eapply cfgsem2fsem. eauto. -Admitted. + - eapply cfgsem2fsem. apply all_fundef_liveness_ok. +Qed. End BTL_SIMULATES_RTL. |