improve fsem

1 files changed, 30 insertions, 15 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index cb60fed1..fb6d5cea 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -161,8 +161,16 @@ 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. 
+(** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit.
+
+    In particular, [tr_exit f pc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [f] will start.
+
+    Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call
+    before entering in return address.
+
+*)
+
+Variable tr_exit: function -> exit -> option reg -> regset -> regset. 
 
 Variable ge: genv.
 
@@ -277,7 +285,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 (tr_exit f pc rs) m)
+                 (State stack f sp pc (tr_exit f pc None rs) m)
   | exec_Breturn or stk m':
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
@@ -287,7 +295,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' (tr_exit f pc' rs) :: stack) fd rs##args m)
+        E0 (Callstate (Stackframe res f sp pc' (tr_exit f pc' (Some res) rs) :: stack) fd rs##args m)
   | exec_Btailcall sig ros args stk m' fd:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
@@ -299,12 +307,15 @@ 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' (tr_exit f pc' (regmap_setres res vres rs)) m')
+         (* TODO: not clear that this is the better choice ! 
+            we coud also do something like [regmap_setres res vres (tr_exit f pc' (reg_builtin_res res) rs)]
+         *)
+         t (State stack f sp pc' (tr_exit f pc' None (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' (tr_exit f pc' rs) m)
+        E0 (State stack f sp pc' (tr_exit f pc' None rs) m)
 .
 
 (** big-step execution of one iblock *)
@@ -364,7 +375,7 @@ Inductive final_state: state -> int -> Prop :=
 (** The basic small-step semantics for a BTL program. *)
 
 (* tid = transfer_identity *)
-Definition tid (_:function) (_:exit) (rs:regset) := rs.
+Definition tid (_:function) (_:exit) (_: option reg) (rs:regset) := rs.
 
 Definition semantics (p: program) :=
   Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
@@ -394,14 +405,18 @@ Proof.
   - rewrite Regmap.gso; auto.
 Qed.
 
-Definition inputs_exit (f:function) (pc: exit) : Regset.t :=
+Definition inputs_exit (f:function) (pc: exit) (or:option reg): Regset.t :=
   match f.(fn_code)!pc with
   | None => Regset.empty
-  | Some ib => ib.(input_regs)
+  | Some ib => 
+     match or with 
+     | Some r => Regset.remove r ib.(input_regs)
+     | None => ib.(input_regs)
+     end
   end.
 
-Definition tr_inputs (f:function) (pc: exit): regset -> regset 
-  := transfer_regs (Regset.elements (inputs_exit f pc)).
+Definition tr_inputs (f:function) (pc: exit) (or:option reg): regset -> regset 
+  := transfer_regs (Regset.elements (inputs_exit f pc or)).
 
 (* TODO: move this elsewhere *)
 Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
@@ -412,16 +427,16 @@ Proof.
   - 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.
+Lemma tr_inputs_exit f pc or rs r:
+  Regset.In r (inputs_exit f pc or) -> (tr_inputs f pc or 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.
+Lemma tr_inputs_dead f pc or rs r:
+  ~(Regset.In r (inputs_exit f pc or)) -> (tr_inputs f pc or rs)#r = Vundef.
 Proof.
   intros X; eapply transfer_regs_dead; intuition eauto.
   eapply X. eapply Regset.elements_2.