From d858606e8400e6aab627f4aac5ec33ce9c2c80fe Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 20 May 2021 18:34:46 +0200
Subject: defines fsem (aka functional semantics) of BTL

---
 scheduling/BTL.v | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 74 insertions(+), 7 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 10a000a8..cb60fed1 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -83,7 +83,7 @@ Coercion BF: final >-> iblock.
 
 Record iblock_info := { 
   entry: iblock;
-  input_regs: Regset.t (* extra liveness information ignored by BTL semantics *)
+  input_regs: Regset.t (* extra liveness information for BTL functional semantics *)
 }.
 
 Definition code: Type := PTree.t iblock_info.
@@ -161,6 +161,9 @@ Record outcome := out {
 
 Section RELSEM.
 
+(* final_step is parametrized by a function to transfer regset on each exit *)
+Variable tr_exit: function -> exit -> regset -> regset. 
+
 Variable ge: genv.
 
 Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
@@ -274,7 +277,7 @@ Qed.
 Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
   | exec_Bgoto pc:
       final_step stack f sp rs m (Bgoto pc) E0
-                 (State stack f sp pc rs m)
+                 (State stack f sp pc (tr_exit f pc rs) m)
   | exec_Breturn or stk m':
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
@@ -284,7 +287,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       final_step stack f sp rs m (Bcall sig ros args res pc')
-        E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
+        E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' rs) :: stack) fd rs##args m)
   | exec_Btailcall sig ros args stk m' fd:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
@@ -296,12 +299,12 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
       final_step stack f sp rs m (Bbuiltin ef args res pc')
-         t (State stack f sp pc' (regmap_setres res vres rs) m')
+         t (State stack f sp pc' (tr_exit f pc' (regmap_setres res vres rs)) m')
   | exec_Bjumptable arg tbl n pc':
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
       final_step stack f sp rs m (Bjumptable arg tbl)
-        E0 (State stack f sp pc' rs m)
+        E0 (State stack f sp pc' (tr_exit f pc' rs) m)
 .
 
 (** big-step execution of one iblock *)
@@ -358,11 +361,75 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-(** The small-step semantics for a program. *)
+(** The basic small-step semantics for a BTL program. *)
+
+(* tid = transfer_identity *)
+Definition tid (_:function) (_:exit) (rs:regset) := rs.
 
 Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+  Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
+
+(** The "functional" small-step semantics for a BTL program. 
+    at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
+*)
+
+Definition transfer_regs (inputs: list reg) (rs: regset): regset :=
+  init_regs (rs##inputs) inputs.
+
+Lemma transfer_regs_inputs inputs rs r:
+  List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
+Proof.
+  unfold transfer_regs; induction inputs; simpl; intuition subst.
+  - rewrite Regmap.gss; auto.
+  - destruct (Pos.eq_dec a r).
+    + subst; rewrite Regmap.gss; auto.
+    + rewrite Regmap.gso; auto.
+Qed.
+
+Lemma transfer_regs_dead inputs rs r:
+  ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef.
+Proof.
+  unfold transfer_regs; induction inputs; simpl; intuition subst.
+  - rewrite Regmap.gi; auto.
+  - rewrite Regmap.gso; auto.
+Qed.
+
+Definition inputs_exit (f:function) (pc: exit) : Regset.t :=
+  match f.(fn_code)!pc with
+  | None => Regset.empty
+  | Some ib => ib.(input_regs)
+  end.
+
+Definition tr_inputs (f:function) (pc: exit): regset -> regset 
+  := transfer_regs (Regset.elements (inputs_exit f pc)).
+
+(* TODO: move this elsewhere *)
+Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
+  SetoidList.InA (fun x y => x = y) x l <-> List.In x l.
+Proof.
+  intros x; split.
+  - induction 1; simpl; eauto.
+  - induction l; simpl; intuition.
+Qed.
+
+Lemma tr_inputs_exit f pc rs r:
+  Regset.In r (inputs_exit f pc) -> (tr_inputs f pc rs)#r = rs#r.
+Proof.
+  intros; eapply transfer_regs_inputs.
+  rewrite <- SetoidList_InA_eq_equiv.
+  eapply Regset.elements_1; eauto.
+Qed.
+
+Lemma tr_inputs_dead f pc rs r:
+  ~(Regset.In r (inputs_exit f pc)) -> (tr_inputs f pc rs)#r = Vundef.
+Proof.
+  intros X; eapply transfer_regs_dead; intuition eauto.
+  eapply X. eapply Regset.elements_2. 
+  rewrite -> SetoidList_InA_eq_equiv; eauto.
+Qed.
 
+Definition fsem (p: program) :=
+  Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
 
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
-- 
cgit