preparation and starting final lemma

1 files changed, 100 insertions, 21 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 95b6a155..8d613ef8 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -26,33 +26,33 @@ Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t :=
   | _ => alive
   end.
 
-Definition exit_checker {A} (btl: code) (alive: Regset.t) (s: node) (v: A): option A :=
+Definition exit_checker (btl: code) (alive: Regset.t) (s: node): option unit :=
   SOME next <- btl!s IN
   ASSERT Regset.subset next.(input_regs) alive IN
-  Some v.
+  Some tt.
 
 Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool :=
    match l with
    | nil => true
-   | s :: l' => exit_checker btl alive s true &&& exit_list_checker btl alive l'
+   | s :: l' => exit_checker btl alive s &&& exit_list_checker btl alive l'
    end.
 
 Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit :=
   match fin with
   | Bgoto s =>
-      exit_checker btl alive s tt
+      exit_checker btl alive s
   | Breturn oreg =>
       ASSERT reg_option_mem oreg alive IN Some tt
   | Bcall _ ros args res s =>
       ASSERT list_mem args alive IN
       ASSERT reg_sum_mem ros alive IN
-      exit_checker btl (Regset.add res alive) s tt
+      exit_checker btl (Regset.add res alive) s
   | Btailcall _ ros args =>
       ASSERT list_mem args alive IN
       ASSERT reg_sum_mem ros alive IN Some tt
   | Bbuiltin _ args res s =>
       ASSERT list_mem (params_of_builtin_args args) alive IN
-      exit_checker btl (reg_builtin_res res alive) s tt
+      exit_checker btl (reg_builtin_res res alive) s
   | Bjumptable arg tbl =>
       ASSERT Regset.mem arg alive IN
       ASSERT exit_list_checker btl alive tbl IN Some tt
@@ -273,34 +273,110 @@ Variable prog: BTL.program.
 
 Let ge := Genv.globalenv prog.
 
-Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f.
+Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f.
 
 Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.
-
-(*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r
-  (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2)
+(*
+Lemma tr_inputs_eqlive f rs1 rs2 tbl or r
+  forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2)
   :eqlive_reg (tr_inputs f tbl or rs1) (tid f tbl or rs2).
+REGS' : forall v : val,
+        eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v
+forall v : val,
+eqlive_reg (ext (input_regs ibf))
+  (tid f tbl or rs1) # res <- v
+  (tr_inputs f tbl or rs2) # res <- v
+ 
+
 Proof.
   unfold tid; rewrite tr_inputs_get.
   autodestruct.
-   Qed.*)
+Qed.
+ *)
+Lemma find_funct_liveness_ok v fd:
+  Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd.
+Proof.
+  unfold Genv.find_funct.
+  destruct v; try congruence.
+  destruct (Integers.Ptrofs.eq_dec _ _); try congruence.
+  eapply all_fundef_liveness_ok; eauto.
+Qed.
+
+Lemma find_function_liveness_ok ros rs f:
+  find_function ge ros rs = Some f -> liveness_ok_fundef f.
+Proof.
+  destruct ros as [r|i]; simpl.
+  - intros; eapply find_funct_liveness_ok; eauto.
+  - destruct (Genv.find_symbol ge i); try congruence.
+    eapply all_fundef_liveness_ok; eauto.
+Qed.
 
-Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m fin t s1 stk2 rs2
-  (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s1)
+Lemma find_function_eqlive alive ros rs1 rs2:
+  eqlive_reg (ext alive) rs1 rs2 ->
+  reg_sum_mem ros alive = true ->
+  find_function ge ros rs1 = find_function ge ros rs2.
+Proof.
+  intros EQLIVE.
+  destruct ros; simpl; auto.
+  intros H; erewrite (EQLIVE r); eauto.
+Qed.
+
+Lemma exit_checker_eqlive_ext1 (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2:
+  exit_checker btl (Regset.add r alive) pc = Some tt ->  
+  eqlive_reg (ext alive) rs1 rs2 ->
+  exists ibf, btl!pc = Some ibf /\ (forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)).
+Proof.
+  unfold exit_checker.
+  inversion_SOME next.
+  inversion_ASSERT. try_simplify_someHyps.
+  repeat (econstructor; eauto).
+  intros; eapply eqlive_reg_update; eauto.
+  eapply eqlive_reg_monotonic; eauto.
+  intros r0 [X1 X2]; exploit Regset.subset_2; eauto.
+  rewrite regset_add_spec. intuition subst.
+Qed.
+
+Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2
+  (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s)
   (LIVE: liveness_ok_function f)
+  (REGS: eqlive_reg (ext alive) rs1 rs2)
+  (FCHK: final_inst_checker (fn_code f) alive fin = Some tt)
   (STACKS: list_forall2 eqlive_stackframes stk1 stk2)
-  (*body_checker (fn_code f) (entry ibf) (input_regs ibf) = Some x ->*)
-  (*eqlive_reg (ext x) rs1' rs2' ->*)
-  :exists s2,
-    final_step tr_inputs ge stk2 f sp rs2 m fin t s2
-    /\ eqlive_states s1 s2.
+  :exists s',
+    final_step tr_inputs ge stk2 f sp rs2 m fin t s'
+    /\ eqlive_states s s'.
 Proof.
-  destruct FSTEP.
+  destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros.
   - (* Bgoto *)
     econstructor. econstructor.
     econstructor. econstructor.
     eauto. eauto.
     repeat econstructor; eauto.
+    all: admit.
+  - (* Breturn *)
+    eexists; split. econstructor; eauto.
+    destruct or; simpl in *;
+    try erewrite (REGS r); eauto.
+  - (* Bcall *)
+    exploit exit_checker_eqlive_ext1; eauto.
+    intros (ibf & PC & REGS').
+    eexists; split.
+    + econstructor; eauto.
+      erewrite <- find_function_eqlive; eauto.
+    + erewrite eqlive_reg_listmem; eauto.
+      eapply eqlive_states_call; eauto.
+      eapply find_function_liveness_ok; eauto.
+      repeat (econstructor; eauto).
+      admit.
+  - (* Btailcall *)
+    eexists; split.
+    + econstructor; eauto.
+      erewrite <- find_function_eqlive; eauto.
+    + erewrite eqlive_reg_listmem; eauto.
+      eapply eqlive_states_call; eauto.
+      eapply find_function_liveness_ok; eauto.
+  - (* Bbuiltin *)
+    
 Admitted.
 
 Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m'
@@ -363,6 +439,7 @@ 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))
@@ -372,8 +449,10 @@ Proof.
   induction ib; simpl; try_simplify_someHyps;
   repeat inversion_ASSERT; intros; inv ISTEP.
   - (* BF *)
-    exploit cfgsem2fsem_finalstep_simu; eauto.
-    intros (s2 & FSTEP' & STATES). eauto.
+    generalize BDY; clear BDY.
+    inversion_SOME x; try_simplify_someHyps; intros FCHK.
+    destruct x; exploit cfgsem2fsem_finalstep_simu; eauto.
+    intros (s2 & FSTEP' & STATES); eauto.
   - (* Bseq stop *)
     destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
     generalize BDY; clear BDY.