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

1 files changed, 44 insertions, 0 deletions

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.
+
+