From 06e5c1dfdb60e45de6b9efa9cdb82031acf5aed2 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 1 Jun 2021 14:37:59 +0200
Subject: preparing liveness proof main theorem

---
 scheduling/BTL_Livecheck.v | 45 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 43 insertions(+), 2 deletions(-)

(limited to 'scheduling/BTL_Livecheck.v')

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 6015d91f..ca7db1da 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -140,6 +140,10 @@ Qed.
 
 Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
 
+Inductive liveness_ok_fundef: fundef -> Prop :=
+  | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f)
+  | liveness_ok_External ef: liveness_ok_fundef (External ef).
+
 (** TODO: adapt stuff RTLpathLivegenproof *)
 
 Local Notation ext alive := (fun r => Regset.In r alive).
@@ -156,6 +160,29 @@ Qed.
 Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
  forall r, (alive r) -> rs1#r = rs2#r.
 
+Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
+  | eqlive_stackframes_intro ibf res f sp pc rs1 rs2
+      (LIVE: liveness_ok_function f)
+      (ENTRY: f.(fn_code)!pc = Some ibf)
+      (EQUIV: forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)):
+       eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). 
+
+Inductive eqlive_states: state -> state -> Prop :=
+  | eqlive_states_intro 
+      ibf st1 st2 f sp pc rs1 rs2 m
+      (STACKS: list_forall2 eqlive_stackframes st1 st2)
+      (LIVE: liveness_ok_function f)
+      (PATH: f.(fn_code)!pc = Some ibf)
+      (EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2):
+      eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m)
+  | eqlive_states_call st1 st2 f args m
+      (LIVE: liveness_ok_fundef f)
+      (STACKS: list_forall2 eqlive_stackframes st1 st2):
+      eqlive_states (Callstate st1 f args m) (Callstate st2 f args m)
+  | eqlive_states_return st1 st2 v m
+      (STACKS: list_forall2 eqlive_stackframes st1 st2):
+      eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).
+
 (* continue to adapt stuff RTLpathLivegenproof *)
 
 Section FSEM_SIMULATES_CFGSEM.
@@ -166,11 +193,25 @@ 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).
+Lemma cfgsem2fsem_step_simu s1 s1' t s2
+  (STEP : step tid (Genv.globalenv prog) s1 t s1')
+  (STATES : eqlive_states s1 s2)
+  :exists s2' : state,
+    step tr_inputs (Genv.globalenv prog) s2 t s2' /\
+    eqlive_states s1' s2'.
 Proof.
-  exploit liveness_checker_correct.
 Admitted.
 
+Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
+Proof.
+  eapply forward_simulation_step with eqlive_states; simpl; eauto.
+  - destruct 1, f; intros; eexists; intuition eauto;
+    repeat econstructor; eauto.
+  - intros s1 s2 r STATES FINAL; destruct FINAL.
+    inv STATES; inv STACKS; constructor.
+  - intros. eapply cfgsem2fsem_step_simu; eauto.
+Qed.
+
 End FSEM_SIMULATES_CFGSEM.
 
 
-- 
cgit