Some others main lemmas

1 files changed, 33 insertions, 7 deletions

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.