fix tr_sis definition

1 files changed, 42 insertions, 24 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 954b4cb4..5f75231a 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -453,8 +453,8 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t
  | 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)).
+Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
+  := transfer_regs (Regset.elements (inputs_exit f tbl or)).
 
 (* TODO: move this elsewhere *)
 Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
@@ -465,38 +465,39 @@ Proof.
   - induction l; simpl; intuition.
 Qed.
 
-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.
+Lemma tr_inputs_exit f tbl or rs r:
+  Regset.In r (inputs_exit f tbl or) -> (tr_inputs f tbl 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 or rs r:
-  ~(Regset.In r (inputs_exit f pc or)) -> (tr_inputs f pc or rs)#r = Vundef.
+Lemma tr_inputs_dead f tbl or rs r:
+  ~(Regset.In r (inputs_exit f tbl or)) -> (tr_inputs f tbl or 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 Regset_In_dec r rs:
-  {  Regset.In r rs } + {  ~(Regset.In r rs)}.
+Local Hint Resolve tr_inputs_exit Regset.mem_2 Regset.mem_1: core.
+
+Lemma tr_inputs_get f tbl or rs r:
+  (tr_inputs f tbl or rs)#r = if Regset.mem r (inputs_exit f tbl or) then rs#r else Vundef.
 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.
+  autodestruct; eauto.
+  intros; apply tr_inputs_dead; eauto.
+  intro X; exploit Regset.mem_1; eauto.
+  congruence.
+Qed.
 
-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).
+Lemma tr_inputs_ext f tbl or rs1 rs2:
+  (forall r, Regset.In r (inputs_exit f tbl or) -> rs1#r = rs2#r) ->
+  (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl 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.
+  intros EQ r. rewrite !tr_inputs_get.
+  autodestruct; auto.
 Qed.
 
 Definition fsem (p: program) :=
@@ -507,16 +508,33 @@ Local Open Scope list_scope.
 Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := 
   match i with
   | Bgoto pc => tr f [pc] None
-  | Bcall sig ros args res pc => tr f [pc] (Some res)
-  | Btailcall sig ros args => tr f [] None
-  | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res)
-  | Breturn or => tr f [] None
-  | Bjumptable reg tbl => tr f tbl None
+  | Bcall _ _ _ res pc => tr f [pc] (Some res)
+  | Btailcall _ _ args => tr f [] None
+  | Bbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
+  | Breturn _ => tr f [] None
+  | Bjumptable _ tbl => tr f tbl None
   end.
 
 Definition tr_regs: function -> final -> regset -> regset :=
   poly_tr tr_inputs.
 
+Definition liveout: function -> final -> Regset.t :=
+  poly_tr inputs_exit.
+
+Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)).
+Proof.
+  destruct fi; simpl; auto.
+Qed.
+
+Local Hint Resolve tr_inputs_get: core.
+
+Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef.
+Proof.
+   Local Opaque inputs_exit.
+   destruct fi; simpl; auto.
+Qed.
+
+
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
 (** Matching BTL and RTL code