starting to experiment SE of fsem

1 files changed, 74 insertions, 17 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index fb6d5cea..4ae7a6dd 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -159,18 +159,22 @@ Record outcome := out {
    _fin: option final 
 }.
 
+
+
+
 Section RELSEM.
 
+
 (** [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.
+    In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may 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 tr_exit: function -> list exit -> option reg -> regset -> regset.
 
 Variable ge: genv.
 
@@ -282,10 +286,13 @@ Proof.
     destruct o; try_simplify_someHyps; subst; eauto.
 Qed.
 
+Import ListNotations.
+Local Open Scope list_scope.
+
 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 None 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' ->
@@ -295,7 +302,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' (Some res) 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 ->
@@ -308,14 +315,14 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       external_call ef ge vargs m t vres m' ->
       final_step stack f sp rs m (Bbuiltin ef args res pc')
          (* 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)]
+            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')
+         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' None rs) m)
+        E0 (State stack f sp pc' (tr_exit f tbl None rs) m)
 .
 
 (** big-step execution of one iblock *)
@@ -375,7 +382,7 @@ Inductive final_state: state -> int -> Prop :=
 (** The basic small-step semantics for a BTL program. *)
 
 (* tid = transfer_identity *)
-Definition tid (_:function) (_:exit) (_: option reg) (rs:regset) := rs.
+Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs.
 
 Definition semantics (p: program) :=
   Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
@@ -405,19 +412,51 @@ Proof.
   - rewrite Regmap.gso; auto.
 Qed.
 
-Definition inputs_exit (f:function) (pc: exit) (or:option reg): Regset.t :=
-  match f.(fn_code)!pc with
-  | None => Regset.empty
-  | Some ib => 
-     match or with 
-     | Some r => Regset.remove r ib.(input_regs)
-     | None => ib.(input_regs)
-     end
+Fixpoint inputs_exitrec (f:function) (tbl: list exit): Regset.t :=
+  match tbl with
+  | nil => Regset.empty
+  | pc::l => let rs:= inputs_exitrec f l in
+             match f.(fn_code)!pc with
+             | None => rs
+             | Some ib => Regset.union rs ib.(input_regs)
+             end
   end.
 
-Definition tr_inputs (f:function) (pc: exit) (or:option reg): regset -> regset 
+Lemma inputs_exitrec_In f tbl r:
+  Regset.In r (inputs_exitrec f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)).
+Proof.
+  induction tbl as [|pc l]; simpl; intros.
+  - exploit Regset.empty_1; eauto. intuition.
+  - destruct ((fn_code f) ! pc) eqn:ATpc.
+    + exploit Regset.union_1; eauto.
+      destruct 1 as [X1|X1].
+      * destruct IHl as (pc' & H1 & H2); eauto.
+      * eexists; intuition eauto.
+    + destruct IHl as (pc' & H1 & H2); eauto.
+Qed.
+
+Lemma inputs_exitrec_notIn f tbl r: 
+   (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs))
+    -> ~Regset.In r (inputs_exitrec f tbl).
+Proof.
+  induction tbl as [|pc l]; simpl; intuition eauto.
+  - exploit Regset.empty_1; eauto.
+  - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto.
+    exploit Regset.union_1; intuition eauto.
+Qed.
+
+Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t :=
+ let rs := inputs_exitrec f tbl in
+ match or with 
+ | Some r => Regset.remove r rs
+ | None => rs
+ end.
+
+Definition tr_inputs (f:function) (pc: list 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,
   SetoidList.InA (fun x y => x = y) x l <-> List.In x l.
@@ -443,6 +482,24 @@ Proof.
   rewrite -> SetoidList_InA_eq_equiv; eauto.
 Qed.
 
+Definition Regset_In_dec r rs:
+  {  Regset.In r rs } + {  ~(Regset.In r rs)}.
+Proof.
+  destruct (Regset.mem r rs) eqn: IsIN.
+  + left. abstract (eapply Regset.mem_2; auto).
+  + right.
+    abstract (intro H; exploit Regset.mem_1; eauto; congruence).
+Defined.
+
+Lemma tr_inputs_ext f pc or rs1 rs2:
+  (forall r, Regset.In r (inputs_exit f pc or) -> rs1#r = rs2#r) ->
+  (forall r, (tr_inputs f pc or rs1)#r = (tr_inputs f pc or rs2)#r).
+Proof.
+  intros EQ r. destruct (Regset_In_dec r (inputs_exit f pc or)).
+  + rewrite! tr_inputs_exit; eauto.
+  + rewrite! tr_inputs_dead; eauto.
+Qed.
+
 Definition fsem (p: program) :=
   Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).