some advance in main liveness lemmas

1 files changed, 68 insertions, 28 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 49660222..50719f67 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 
-      st1 st2 f sp pc rs1 rs2 m
+      ibf 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)
@@ -193,40 +193,80 @@ Let ge := Genv.globalenv prog.
 
 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.
+Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.
+
+Lemma cfgsem2fsem_ibistep_simu sp rs1 m1 rs1' m1' of ib
+  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of): forall
+   rs2 m2,
+  exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of).
 Proof.
+  induction ISTEP; simpl; try_simplify_someHyps; intros.
+  - (* Bop *)
+    inversion_SOME v0; intros EVAL';
+    repeat eexists.
+    inv EVAL'.
 Admitted.
 
+Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
+  (FSTEP: final_step tid ge stk1 f sp rs1 m1 fin t s1)
+  (STACKS: list_forall2 eqlive_stackframes stk1 stk2)
+  : exists s2, final_step tr_inputs ge stk2 f sp rs2 m2 fin t s2
+    /\ eqlive_states s1 s2.
+Proof.
+  destruct FSTEP.
+  - (* Bgoto *)
+    (*eexists; split; simpl ; econstructor; eauto.*)
+Admitted.
+
+Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t:
+  iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m ibf.(entry) t s1 ->
+  list_forall2 eqlive_stackframes stk1 stk2 ->
+  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
+  liveness_ok_function f ->
+  (fn_code f) ! pc = Some ibf ->
+  exists s2 : state,
+    iblock_step tr_inputs (Genv.globalenv prog) stk2 f sp rs2 m ibf.(entry) t s2 /\
+    eqlive_states s1 s2.
+Proof.
+  intros STEP STACKS EQLIVE LIVE PC.
+  unfold liveness_ok_function, liveness_checker in LIVE.
+  destruct list_iblock_checker eqn:LIBC in LIVE; try discriminate.
+  clear LIVE.
+  destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP).
+  exploit cfgsem2fsem_ibistep_simu; eauto.
+  intros (rs2' & m2' & ISTEP2).
+  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP.
+  exploit cfgsem2fsem_finalstep_simu; eauto.
+  intros (s2 & FSTEP2 & STATES). clear FSTEP.
+  unfold iblock_step. repeat eexists; eauto.
+Qed.
+
+
 Local Hint Constructors step: core.
 
-Lemma cfgsem2fsem_step_simu s1 s1' t s2
-  (STEP : step tid (Genv.globalenv prog) s1 t s1')
-  (STATES : eqlive_states s1 s2)
-  :exists s2' : state,
+Lemma cfgsem2fsem_step_simu s1 s1' t s2:
+  step tid (Genv.globalenv prog) s1 t s1' ->
+  eqlive_states s1 s2 ->
+  exists s2' : state,
     step tr_inputs (Genv.globalenv prog) s2 t s2' /\
     eqlive_states s1' s2'.
 Proof.
-  destruct STEP; inv STATES.
-  - (* iblock *)
+  destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES;
+  try (inv STATES; inv LIVE; eexists; split; econstructor; eauto; fail).
+  - inv STATES; simplify_someHyps.
+    intros.
     exploit cfgsem2fsem_ibstep_simu; eauto.
-    intros (s2 & STEP2 & STATES2).
+    intros (s2 & STEP2 & EQUIV2). 
     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.
+  - inv STATES; inv LIVE.
+    eexists; split; econstructor; eauto. all : admit. (* TODO gourdinl *)
+  - inv STATES.
+    inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS.
+    inv STACK.
+    exists (State s2 f sp pc (rs2 # res <- vres) m); split.
+    * apply exec_return.
+    * eapply eqlive_states_intro; eauto.
+Admitted.
 
 Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
 Proof.