From 0321d5f0aa2478ab830990a3637c37566bd9b634 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 18 Jun 2021 11:46:10 +0200 Subject: finish RTLtoBTL proof --- scheduling/RTLtoBTLproof.v | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') 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. -- cgit