Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

1 files changed, 112 insertions, 21 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 50719f67..82efff44 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -120,24 +120,48 @@ Proof.
   simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
 Qed.
 
+
+Definition liveness_checker_bool (f: BTL.function): bool :=
+  f.(fn_code)!(f.(fn_entrypoint)) &&& list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)).
+
 Definition liveness_checker (f: BTL.function): res unit :=
-  match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with
+  match liveness_checker_bool f with
   | true => OK tt
   | false => Error (msg "BTL_Livecheck: liveness_checker failed")
   end.
 
+Lemma decomp_liveness_checker f:
+  liveness_checker f = OK tt ->
+  exists ibf, f.(fn_code)!(f.(fn_entrypoint)) = Some ibf /\
+  list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) = true.
+Proof.
+  intros LIVE; unfold liveness_checker in LIVE.
+  destruct liveness_checker_bool eqn:EQL; try congruence.
+  clear LIVE. unfold liveness_checker_bool in EQL.
+  rewrite lazy_and_Some_true in EQL; destruct EQL as [[ibf ENTRY] LIST].
+  eexists; split; eauto.
+Qed.
+
 Lemma liveness_checker_correct f n ibf:
   liveness_checker f = OK tt ->
   f.(fn_code)!n = Some ibf ->
   iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt.
 Proof.
-  unfold liveness_checker.
-  destruct list_iblock_checker eqn:EQL; try congruence.
-  intros _ P. exploit list_iblock_checker_correct; eauto.
+  intros LIVE PC.
+  apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
+  exploit list_iblock_checker_correct; eauto.
   - eapply PTree.elements_correct; eauto.
   - simpl; auto.
 Qed.
 
+Lemma liveness_checker_entrypoint f:
+  liveness_checker f = OK tt ->
+  f.(fn_code)!(f.(fn_entrypoint)) <> None.
+Proof.
+  intros LIVE; apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
+  unfold not; intros CONTRA. congruence.
+Qed.
+
 Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
 
 Inductive liveness_ok_fundef: fundef -> Prop :=
@@ -195,16 +219,79 @@ Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f -
 
 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).
+(*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r
+  (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2)
+  :eqlive_reg (tr_inputs f tbl or rs1) (tid f tbl or rs2).
+Proof.
+  unfold tid; rewrite tr_inputs_get.
+  autodestruct.
+   Qed.*)
+
+Remark is_none_true {A} (fin: option A):
+  is_none fin = true ->
+  fin = None.
+Proof.
+  unfold is_none; destruct fin; congruence.
+Qed.
+
+Local Hint Resolve Regset.mem_2 Regset.subset_2: core.
+Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
+Proof.
+  destruct b1; simpl; intuition.
+Qed.
+
+Lemma list_mem_correct (rl: list reg) (alive: Regset.t):
+  list_mem rl alive = true -> forall r, List.In r rl -> ext alive r.
+Proof.
+  induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto.
+Qed.
+
+Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args.
+Proof.
+  induction args; simpl; auto.
+  intros EQLIVE ALIVE; rewrite IHargs; auto.
+  unfold eqlive_reg in EQLIVE.
+  rewrite EQLIVE; auto.
+Qed.
+
+Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args.
 Proof.
-  induction ISTEP; simpl; try_simplify_someHyps; intros.
+  intros; eapply eqlive_reg_list; eauto.
+  intros; eapply list_mem_correct; eauto.
+Qed.
+
+Lemma cfgsem2fsem_ibistep_simu sp f: forall rs1 m rs1' m' rs2 of ibf res,
+  iblock_istep ge sp rs1 m ibf.(entry) rs1' m' of ->
+  (*iblock_checker (fn_code f) ibf.(entry) ibf.(input_regs) = Some tt ->*)
+  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
+  body_checker (fn_code f) ibf.(entry) ibf.(input_regs) = Some res ->
+(*LIST : list_iblock_checker (fn_code f) (PTree.elements (fn_code f)) = true*)
+  exists rs2', iblock_istep_run ge sp ibf.(entry) rs2 m = Some (out rs2' m' of).
+Proof.
+  induction 1; simpl; repeat inversion_ASSERT; intros; try_simplify_someHyps.
   - (* Bop *)
-    inversion_SOME v0; intros EVAL';
-    repeat eexists.
-    inv EVAL'.
+    intros.
+    erewrite <- eqlive_reg_listmem; eauto.
+    try_simplify_someHyps.
+    (*
+  (*- [> BF <]*)
+    (*intros. inv H1; eexists; reflexivity.*)
+  - (* Bseq stop *)
+    admit. (*
+    inversion_SOME res0.
+    inversion_ASSERT; intros.
+    exploit IHiblock_istep. unfold iblock_checker.
+    rewrite H1. inv H0.
+    inversion_SOME out1.
+              try_simplify_someHyps.*)
+  - inversion_SOME res0.
+    inversion_ASSERT; intros.
+    admit.
+    (* TODO The first induction hyp should not be based on iblock_checker *)
+    (* exploit IHiblock_istep1. unfold iblock_checker.
+       rewrite H2. apply is_none_true in H1. rewrite H1. *)
+  - (* Bcond *)
+       admit.*)
 Admitted.
 
 Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
@@ -215,7 +302,7 @@ Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
 Proof.
   destruct FSTEP.
   - (* Bgoto *)
-    (*eexists; split; simpl ; econstructor; eauto.*)
+    eexists; split; simpl. econstructor; eauto.
 Admitted.
 
 Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t:
@@ -229,19 +316,21 @@ Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t:
     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).
+  unfold liveness_ok_function in LIVE.
+  apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
+  eapply PTree.elements_correct in PC as PCIN.
+  eapply list_iblock_checker_correct in LIST as IBC; eauto.
+  unfold iblock_checker in IBC. generalize IBC; clear IBC.
+  inversion_SOME res; inversion_SOME fin; intros RES BODY FINAL.
+  destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP).
   exploit cfgsem2fsem_ibistep_simu; eauto.
-  intros (rs2' & m2' & ISTEP2).
+  intros (rs2' & 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:
@@ -259,14 +348,16 @@ Proof.
     intros (s2 & STEP2 & EQUIV2). 
     eexists; split; eauto.
   - inv STATES; inv LIVE.
-    eexists; split; econstructor; eauto. all : admit. (* TODO gourdinl *)
+    apply liveness_checker_entrypoint in H0 as ENTRY.
+    destruct ((fn_code f) ! (fn_entrypoint f)) eqn:EQENTRY; try congruence; eauto.
+    eexists; split; repeat econstructor; eauto.
   - 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.
+Qed.
 
 Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
 Proof.