From d858606e8400e6aab627f4aac5ec33ce9c2c80fe Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 20 May 2021 18:34:46 +0200 Subject: defines fsem (aka functional semantics) of BTL --- scheduling/BTLtoRTLproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 08a77ae4..bbb984c4 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -292,7 +292,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) @@ -338,7 +338,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. @@ -359,7 +359,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' -- cgit From 43ab0b948ac379e55bbe334a0a541c1680437fbf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 10:40:54 +0200 Subject: most of the proof BTL.fsem -> BTL.cfgsem. --- scheduling/BTLtoRTLproof.v | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index bbb984c4..14e986aa 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -390,8 +390,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. @@ -400,4 +400,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. -- cgit