Preparation for scheduling proof, main lemmas ok

4 files changed, 41 insertions, 16 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 25a1c545..9f96e74e 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -583,7 +583,6 @@ Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m'
   alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2)
   (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2))
   (LIVE: liveness_ok_function f)
-  (*(PC : (fn_code f) ! pc = Some ibf)*)
   (STACKS: list_forall2 eqlive_stackframes stk1 stk2),
   exists rs2' s',
     iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin))
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 8240c861..ec83b3c1 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -37,7 +37,6 @@ Record match_function (f1 f2: BTL.function): Prop := {
   preserv_fnparams: fn_params f1 = fn_params f2;
   preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
   preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2;
-  (*exists_entrypoint: exists ibf, (fn_code f1)!(fn_entrypoint f1) = Some ibf;*)
   (* preserv_inputs: equiv_input_regs f1 f2; TODO: a-t-on besoin de ça ? *)
   symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 ->
                     exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2);
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index f186581f..aaa2bf80 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -46,11 +46,11 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop :=
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro 
-      st f sp pc rs m st' f'
-      (*(ENTRY: (fn_code f) ! pc = Some ibf)*)
+      st f sp pc rs rs' m st' f'
+      (EQREGS: forall r, rs # r = rs' # r)
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_function f f')
-      : match_states (State st f sp pc rs m) (State st' f' sp pc rs m)
+      : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m)
   | match_states_call
       st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')
@@ -113,17 +113,44 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
-Lemma iblock_step_simulation stk1 stk2 f f' sp rs m ibf t s1 pc
-  (STEP : iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1)
-  (ENTRY : (fn_code f) ! pc = Some ibf)
+(* TODO gourdinl
+   generalize with a None version of the lemma *)
+Lemma iblock_istep_simulation stk1 stk2 f f' sp pc fin rs1 m rs1' m' rs2 ib1 t s
+  (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' (Some fin))
+  (FSTEP : final_step tr_inputs pge stk1 f sp rs1' m' fin t s)
+  (EQREGS: forall r : positive, rs1 # r = rs2 # r)
   (STACKS : list_forall2 match_stackframes stk1 stk2)
   (TRANSF : match_function f f')
-  :exists s2 : state,
-    (fn_code f') ! pc = Some ibf /\
-    iblock_step tr_inputs tpge stk2 f' sp rs m ibf.(entry) t s2 /\
-    match_states s1 s2.
+  :exists ib2 rs2' s',
+       (fn_code f') ! pc = Some ib2
+    /\ iblock_istep tpge sp rs2 m ib2.(entry) rs2' m' (Some fin)
+    /\ final_step tr_inputs tpge stk2 f' sp rs2' m' fin t s'
+    /\ match_states s s'.
+Proof.
+  induction ib1; inv ISTEP; eauto.
+  - (* BF *)
+    admit.
+  - (* Bseq continue *)
+    eauto.
 Admitted.
 
+Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s1 pc
+  (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1)
+  (PC: (fn_code f) ! pc = Some ibf)
+  (EQREGS: forall r : positive, rs # r = rs' # r)
+  (STACKS: list_forall2 match_stackframes stk1 stk2)
+  (TRANSF: match_function f f')
+  :exists ibf' s2,
+    (fn_code f') ! pc = Some ibf' /\
+    iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s2 /\
+    match_states s1 s2.
+Proof.
+  destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP).
+  exploit iblock_istep_simulation; eauto.
+  intros (ibf2 & rs2' & s' & PC' & ISTEP' & FSTEP' & MS').
+  repeat eexists; eauto.
+Qed.
+
 Local Hint Constructors step: core.
 
 Theorem step_simulation s1 s1' t s2
@@ -133,11 +160,11 @@ Theorem step_simulation s1 s1' t s2
     step tr_inputs tpge s2 t s2'
   /\ match_states s1' s2'.
 Proof.
-  destruct STEP as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; inv MS.
+  destruct STEP as [stack ibf f sp n rs m t s PC STEP | | | ]; inv MS.
   - (* iblock *)
-    simplify_someHyps. intros ENTRY.
+    simplify_someHyps. intros PC.
     exploit iblock_step_simulation; eauto.
-    intros (s2 & ENTRY2 & STEP2 & MS2). 
+    intros (ibf' & s2 & PC2 & STEP2 & MS2). 
     eexists; split; eauto.
   - (* function internal *)
     inversion TRANSF as [xf tf MF |]; subst.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 18ff8d5f..513ed40a 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -375,7 +375,7 @@ Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.f
 Proof.
   intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
   erewrite preserv_fnsig; eauto.
-Admitted.
+Qed.
 
 Lemma transf_initial_states s1:
   RTL.initial_state prog s1 ->