starting to extend RTLtoBTL with Liveness checking (on BTL side)

8 files changed, 99 insertions, 37 deletions

diff --git a/Makefile b/Makefile
index 3d9e8bdd..60cf380b 100644
--- a/Makefile
+++ b/Makefile
@@ -144,7 +144,7 @@ SCHEDULING= \
   RTLpathSchedulerproof.v  RTLpath.v \
   RTLpathScheduler.v       RTLpathWFcheck.v \
   BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \
-  BTL_SEtheory.v
+  BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v BTL_SEtheory.v
 
 # C front-end modules (in cfrontend/)
 
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
new file mode 100644
index 00000000..2baba025
--- /dev/null
+++ b/scheduling/BTL_Livecheck.v
@@ -0,0 +1,44 @@
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad.
+Require Import Errors RTL BTL BTLmatchRTL.
+
+(** TODO: adapt stuff RTLpathLivegen *)
+
+Definition liveness_checker (f: BTL.function): res unit := OK tt. (* TODO: implement this ! *)
+
+Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
+
+(** TODO: adapt stuff RTLpathLivegenproof *)
+
+Local Notation ext alive := (fun r => Regset.In r alive).
+
+Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
+Proof.
+  destruct (Pos.eq_dec r1 r2).
+  - subst. intuition; eapply Regset.add_1; auto.
+  - intuition. 
+    * right. eapply Regset.add_3; eauto.
+    * eapply Regset.add_2; auto.
+Qed.
+
+Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
+ forall r, (alive r) -> rs1#r = rs2#r.
+
+(* continue to adapt stuff RTLpathLivegenproof *)
+
+Section FSEM_SIMULATES_CFGSEM.
+
+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.
+
+Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
+Proof.
+  exploit liveness_checker_correct.
+Admitted.
+
+End FSEM_SIMULATES_CFGSEM.
+
+
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/scheduling/BTL_Scheduler.v
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/scheduling/BTL_Schedulerproof.v
diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
index 23ff6681..8994579d 100644
--- a/scheduling/BTLmatchRTL.v
+++ b/scheduling/BTLmatchRTL.v
@@ -223,18 +223,6 @@ Record match_function dupmap f f': Prop := {
   preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
 }.
 
-Inductive match_fundef: BTL.fundef -> RTL.fundef -> Prop :=
-  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
-  | match_External ef: match_fundef (External ef) (External ef).
-
-Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop :=
-  | match_stackframe_intro 
-      dupmap res f sp pc rs f' pc'
-      (TRANSF: match_function dupmap f f')
-      (DUPLIC: dupmap!pc = Some pc')
-      : match_stackframes (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
-
-
 (** * Shared verifier between RTL -> BTL and BTL -> RTL *)
 
 Local Open Scope error_monad_scope.
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 765f9cad..75f67d51 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -6,6 +6,18 @@ Require Import Errors Linking BTLtoRTL.
 
 Require Import Linking.
 
+
+Inductive match_fundef: BTL.fundef -> RTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: BTL.stackframe -> RTL.stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc = Some pc')
+      : match_stackframes (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
+
 Inductive match_states: BTL.state -> RTL.state -> Prop :=
   | match_states_intro 
       dupmap st f sp pc rs m st' f' pc'
diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v
index 507fc9d9..309c616e 100644
--- a/scheduling/RTLtoBTL.v
+++ b/scheduling/RTLtoBTL.v
@@ -1,7 +1,7 @@
 Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad BTL.
-Require Export BTLmatchRTL.
+Require Export BTLmatchRTL BTL_Livecheck.
 
 Require Import Errors Linking.
 
@@ -17,6 +17,7 @@ Definition transf_function (f: RTL.function) : res BTL.function :=
   let (tc, te) := tcte in
   let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) tc te in
   do u <- verify_function dupmap f' f;
+  do u <- liveness_checker f';
   OK f'.
 
 Definition transf_fundef (f: RTL.fundef) : res fundef :=
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index ef336de5..18ff8d5f 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -230,20 +230,33 @@ Qed.
 (** * Matching relation on functions *)
 
 (* we simply switch [f] and [tf] in the usual way *)
-Definition match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := 
-  BTLmatchRTL.match_function dupmap tf f.
+Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
+  matchRTL:> BTLmatchRTL.match_function dupmap tf f;
+  liveness_ok: liveness_ok_function tf;
+}.
 
-Definition match_fundef f tf := BTLmatchRTL.match_fundef tf f.
+Local Hint Resolve matchRTL: core.
 
-Definition match_stackframes stk stk' := BTLmatchRTL.match_stackframes stk' stk.
+Inductive match_fundef: RTL.fundef -> BTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: RTL.stackframe -> BTL.stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc)
+      : match_stackframes (RTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc' rs).
 
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
 Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
   intros H _ _ X. inversion X; subst; clear X.
+(*
   eexists; eapply verify_function_correct; simpl; eauto.
-Qed.
+*)
+Admitted.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
@@ -362,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.
-Qed.
+Admitted.
 
 Lemma transf_initial_states s1:
   RTL.initial_state prog s1 ->
@@ -525,8 +538,8 @@ Proof.
   - (* Bgoto *)
     inv MSS2. inversion MIB; subst; try inv H4.
     remember H2 as ODUPLIC; clear HeqODUPLIC.
-    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-    apply DMC in H2 as [ib [FNC MI]]; clear DMC.
+    exploit dupmap_correct; eauto.
+    intros [ib [FNC MI]].
     eexists; left; eexists; split; eauto.
     repeat econstructor; eauto.
     apply iblock_istep_run_equiv in BTL_RUN; eauto.
@@ -584,9 +597,8 @@ Proof.
       * repeat (econstructor; eauto).
         eapply transf_fundef_correct; eauto.
     + (* Bbuiltin *)
-      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-      remember H1 as ODUPLIC; clear HeqODUPLIC.
-      apply DMC in H1 as [ib [FNC MI]]; clear DMC.
+      exploit dupmap_correct; eauto.
+      intros [ib [FNC MI]].
       exists (Some (normRTL (entry ib))); left; eexists; split; eauto.
       econstructor; eauto. econstructor.
       eexists; eexists; split.
@@ -598,9 +610,8 @@ Proof.
     + (* Bjumptable *)
       exploit list_nth_z_rev_dupmap; eauto.
       intros (pc'0 & LNZ & DM).
-      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-      remember DM as ODUPLIC; clear HeqODUPLIC.
-      apply DMC in DM as [ib [FNC MI]]; clear DMC.
+      exploit dupmap_correct; eauto.
+      intros [ib [FNC MI]].
       exists (Some (normRTL (entry ib))); left; eexists; split; eauto.
       econstructor; eauto. econstructor.
       eexists; eexists; split.
@@ -687,11 +698,10 @@ Proof.
     inv H.
     + (* Internal function *)
       inv TRANSF.
-      rename H1 into TRANSF.
-      eapply dupmap_entrypoint in TRANSF as ENTRY.
-      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-      apply DMC in ENTRY as DMC'.
-      destruct DMC' as [ib [CENTRY MI]]; clear DMC.
+      rename H0 into TRANSF.
+      exploit dupmap_entrypoint; eauto. intros ENTRY.
+      exploit dupmap_correct; eauto.
+      intros [ib [CENTRY MI]].
       exists (Some (normRTL (entry ib))); left; eexists; split.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
@@ -705,16 +715,15 @@ Proof.
       * econstructor; eauto.
   - (* Returnstate *)
     inv H. inv STACKS. inv H1.
-    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-    remember DUPLIC as ODUPLIC; clear HeqODUPLIC.
-    apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
+    exploit dupmap_correct; eauto.
+    intros [ib [FNC MI]].
     eexists; left; eexists; split; eauto.
     eapply exec_return.
 Qed.
 
 Local Hint Resolve plus_one star_refl: core.
 
-Theorem transf_program_correct:
+Theorem transf_program_correct_cfg:
   forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog).
 Proof.
   eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states).
@@ -729,4 +738,12 @@ Proof.
   - eapply senv_preserved.
 Qed.
 
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (BTL.fsem tprog).
+Proof.
+  eapply compose_forward_simulations.
+  - eapply transf_program_correct_cfg.
+  - eapply cfgsem2fsem.
+Admitted.
+
 End BTL_SIMULATES_RTL.