From cf9824cd02c9dd5a8053c1853f26b98ad807766e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 1 Jun 2021 15:33:12 +0200 Subject: Some others main lemmas --- scheduling/BTL_Livecheck.v | 40 +++++++++++++++++++++++++++++++++------- 1 file changed, 33 insertions(+), 7 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index ca7db1da..49660222 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -169,11 +169,11 @@ Inductive eqlive_stackframes: stackframe -> stackframe -> Prop := Inductive eqlive_states: state -> state -> Prop := | eqlive_states_intro - ibf st1 st2 f sp pc rs1 rs2 m + st1 st2 f sp pc rs1 rs2 m (STACKS: list_forall2 eqlive_stackframes st1 st2) - (LIVE: liveness_ok_function f) - (PATH: f.(fn_code)!pc = Some ibf) - (EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2): + (LIVE: liveness_ok_function f): + (*(PATH: f.(fn_code)!pc = Some ibf)*) + (*(EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2):*) eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m) | eqlive_states_call st1 st2 f args m (LIVE: liveness_ok_fundef f) @@ -191,7 +191,19 @@ Variable prog: BTL.program. Let ge := Genv.globalenv prog. -Hypothesis liveness_checker_correct: forall b f, Genv.find_funct_ptr ge b = Some (Internal f) -> liveness_ok_function f. +Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f. + +Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m1 rs2 m2 ib s1 t + (STEP : iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m1 ib t s1) + (STACKS : list_forall2 eqlive_stackframes stk1 stk2) + (LIVE : liveness_ok_function f) + :exists s2 : state, + iblock_step tr_inputs (Genv.globalenv prog) stk2 f sp rs2 m2 ib t s2 /\ + eqlive_states s1 s2. +Proof. +Admitted. + +Local Hint Constructors step: core. Lemma cfgsem2fsem_step_simu s1 s1' t s2 (STEP : step tid (Genv.globalenv prog) s1 t s1') @@ -200,13 +212,27 @@ Lemma cfgsem2fsem_step_simu s1 s1' t s2 step tr_inputs (Genv.globalenv prog) s2 t s2' /\ eqlive_states s1' s2'. Proof. -Admitted. + destruct STEP; inv STATES. + - (* iblock *) + exploit cfgsem2fsem_ibstep_simu; eauto. + intros (s2 & STEP2 & STATES2). + eexists; split; eauto. + - (* internal call *) + inv LIVE. + eexists; split; repeat econstructor; eauto. + - (* external_call *) + eexists; split; repeat econstructor; eauto. + - (* return *) + inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst. + inv STF2. + eexists; split; econstructor; eauto. +Qed. Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog). Proof. eapply forward_simulation_step with eqlive_states; simpl; eauto. - destruct 1, f; intros; eexists; intuition eauto; - repeat econstructor; eauto. + repeat (econstructor; eauto). - intros s1 s2 r STATES FINAL; destruct FINAL. inv STATES; inv STACKS; constructor. - intros. eapply cfgsem2fsem_step_simu; eauto. -- cgit