diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 12:00:51 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 12:00:51 +0200 |
| commit | ef5775ea869701eb04c873174c362b314166bf06 (patch) | |
| tree | 634c5364ec95dc649e302a63dee72eadb0e6b73b /scheduling/BTLtoRTLproof.v | |
| parent | 05b24fdb11414100b9b04867e6e2d3a1a9054162 (diff) | |
| parent | 43ab0b948ac379e55bbe334a0a541c1680437fbf (diff) | |
| download | compcert-kvx-ef5775ea869701eb04c873174c362b314166bf06.tar.gz compcert-kvx-ef5775ea869701eb04c873174c362b314166bf06.zip | |
Merge branch 'BTL_fsem' into BTL
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 7b62a844..46f360c5 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -303,7 +303,7 @@ Qed. Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s (STACKS : list_forall2 match_stackframes stack stack') (TRANSF : match_function dupmap f f') - (FS : final_step ge stack f sp rs1 m1 fin t s) + (FS : final_step tid ge stack f sp rs1 m1 fin t s) (i : instruction) (ATpc1 : (RTL.fn_code f') ! pc1 = Some i) (MF : match_final_inst dupmap fin i) @@ -349,7 +349,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi (TRANSF: match_function dupmap f f') (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin)) (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None) - (FS : final_step ge stack f sp rs1 m1 fin t s) + (FS : final_step tid ge stack f sp rs1 m1 fin t s) : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. Proof. intros; exploit iblock_istep_simulation; eauto. @@ -370,7 +370,7 @@ Proof. Qed. Theorem plus_simulation s1 t s1': - step ge s1 t s1' -> + step tid ge s1 t s1' -> forall s2 (MS: match_states s1 s2), exists s2', plus RTL.step tge s2 t s2' @@ -401,8 +401,8 @@ Proof. + inv H1. econstructor; eauto. Qed. -Theorem transf_program_correct: - forward_simulation (semantics prog) (RTL.semantics tprog). +Theorem transf_program_correct_cfg: + forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog). Proof. eapply forward_simulation_plus with match_states. - eapply senv_preserved. @@ -411,4 +411,12 @@ Proof. - eapply plus_simulation. Qed. +Theorem transf_program_correct: + forward_simulation (BTL.fsem prog) (RTL.semantics tprog). +Proof. + eapply compose_forward_simulations. + - eapply fsem2cfgsem. + - eapply transf_program_correct_cfg. +Qed. + End RTL_SIMULATES_BTL. |