diff options
Diffstat (limited to 'scheduling')
| -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. |