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 


From 25a4620c95aaa6b017443da29fcf3d033a44a86f Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 21 May 2021 15:59:31 +0200
Subject: improve fsem

---
 scheduling/BTL.v | 45 ++++++++++++++++++++++++++++++---------------
 1 file changed, 30 insertions(+), 15 deletions(-)

(limited to 'scheduling/BTL.v')

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. 
-- 
cgit 


From 6938945d80bf16a6de4986e2815113e938bff6c3 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 25 May 2021 13:36:57 +0200
Subject: starting to experiment SE of fsem

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

(limited to 'scheduling/BTL.v')

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).
 
-- 
cgit 


From 85aa6d418e077a9f492f800b3f61fb5ead705e4d Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 25 May 2021 18:25:22 +0200
Subject: fix Builtin semantics

---
 scheduling/BTL.v | 34 ++++++++++++++++++++++++----------
 1 file changed, 24 insertions(+), 10 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 4ae7a6dd..954b4cb4 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -18,6 +18,8 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad.
 
+Import ListNotations.
+
 (** * Abstract syntax *)
 
 Definition exit := node.  (* we may generalize this with register renamings at exit, 
@@ -159,12 +161,15 @@ Record outcome := out {
    _fin: option final 
 }.
 
-
-
+(* follows RTL semantics to set the result of builtin *)
+Definition reg_builtin_res (res: builtin_res reg): option reg :=
+  match res with
+  | BR r => Some r
+  | _ => None
+  end.
 
 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 lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start.
@@ -286,7 +291,6 @@ 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 :=
@@ -314,10 +318,7 @@ 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')
-         (* 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')
+         t (State stack f sp pc' (regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)) m')
   | exec_Bjumptable arg tbl n pc':
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
@@ -455,8 +456,6 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t
 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.
@@ -503,6 +502,21 @@ Qed.
 Definition fsem (p: program) :=
   Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
 
+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
+  end.
+
+Definition tr_regs: function -> final -> regset -> regset :=
+  poly_tr tr_inputs.
+
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
 (** Matching BTL and RTL code 
-- 
cgit 


From 47599a2ea88799d654ec644fe5ba9892087adb39 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Wed, 26 May 2021 16:27:21 +0200
Subject: fix tr_sis definition

---
 scheduling/BTL.v | 66 +++++++++++++++++++++++++++++++++++---------------------
 1 file changed, 42 insertions(+), 24 deletions(-)

(limited to 'scheduling/BTL.v')

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 
-- 
cgit 


From d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Wed, 26 May 2021 21:42:33 +0200
Subject: end of BTL_SEtheory w.r.t fsem

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

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 5f75231a..6f699cd0 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -391,10 +391,11 @@ Definition semantics (p: program) :=
 (** 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.
 
+(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *)
+
 Lemma transfer_regs_inputs inputs rs r:
   List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
 Proof.
@@ -456,6 +457,9 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t
 Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
   := transfer_regs (Regset.elements (inputs_exit f tbl or)).
 
+(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *)
+
+
 (* 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.
@@ -518,6 +522,7 @@ Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: fina
 Definition tr_regs: function -> final -> regset -> regset :=
   poly_tr tr_inputs.
 
+(* TODO: NOT USEFUL ?
 Definition liveout: function -> final -> Regset.t :=
   poly_tr inputs_exit.
 
@@ -533,7 +538,7 @@ 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" ? *)
 
-- 
cgit 


From e30376ce891d0710757c65e85a24e7d2550a37ed Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 27 May 2021 13:49:35 +0200
Subject: cleaning BTL_SEtheory

---
 scheduling/BTL.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 6f699cd0..bf19f4ac 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -540,6 +540,79 @@ Proof.
 Qed.
 *)
 
+(* * Reasoning modulo extensionality of [regset] into BTL semantics *)
+Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
+  | equiv_stackframe_intro res f sp pc rs1 rs2
+      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
+      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive equiv_state: state -> state -> Prop :=
+  | State_equiv stack f sp pc rs1 m rs2
+     (EQUIV: forall r, rs1#r = rs2#r): 
+     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
+  | Call_equiv stk stk' f args m
+      (STACKS: list_forall2 equiv_stackframe stk stk'):
+      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
+  | Return_equiv stk stk' v m
+      (STACKS: list_forall2 equiv_stackframe stk stk'):
+      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
+  .
+
+Local Hint Constructors equiv_stackframe equiv_state: core.
+
+Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
+Proof.
+  Local Hint Resolve equiv_stackframe_refl: core.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_state_refl s: equiv_state s s.
+Proof.
+  Local Hint Resolve equiv_stack_refl: core.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_stackframe_trans stf1 stf2 stf3:
+  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
+Proof.
+  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma equiv_stack_trans stk1 stk2:
+  list_forall2 equiv_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 equiv_stackframe stk1 stk3.
+Proof.
+  Local Hint Resolve equiv_stackframe_trans: core.
+  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
+Qed.
+
+Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
+Proof.
+  Local Hint Resolve equiv_stack_trans: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma regmap_setres_eq (rs rs': regset) res vres:
+  (forall r, rs # r = rs' # r) ->
+  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
+Proof.
+  intros RSEQ r. destruct res; simpl; try congruence.
+  destruct (peq x r).
+  - subst. repeat (rewrite Regmap.gss). reflexivity.
+  - repeat (rewrite Regmap.gso); auto.
+Qed.
+
+
+
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
 (** Matching BTL and RTL code 
-- 
cgit 


From 43ab0b948ac379e55bbe334a0a541c1680437fbf Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 28 May 2021 10:40:54 +0200
Subject: most of the proof BTL.fsem -> BTL.cfgsem.

---
 scheduling/BTL.v | 308 +++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 267 insertions(+), 41 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index bf19f4ac..389d8d93 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -17,6 +17,7 @@
 Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad.
+Require Import Lia.
 
 Import ListNotations.
 
@@ -380,22 +381,20 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-(** The basic small-step semantics for a BTL program. *)
+(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *)
 
 (* tid = transfer_identity *)
 Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs.
 
-Definition semantics (p: program) :=
+Definition cfgsem (p: program) :=
   Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
 
-(** The "functional" small-step semantics for a BTL program. 
+(** The full "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.
 
-(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *)
-
 Lemma transfer_regs_inputs inputs rs r:
   List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
 Proof.
@@ -414,18 +413,20 @@ Proof.
   - rewrite Regmap.gso; auto.
 Qed.
 
-Fixpoint inputs_exitrec (f:function) (tbl: list exit): Regset.t :=
+Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t :=
   match tbl with
   | nil => Regset.empty
-  | pc::l => let rs:= inputs_exitrec f l in
+  | pc::l => let rs:= union_inputs f l in
              match f.(fn_code)!pc with
              | None => rs
              | Some ib => Regset.union rs ib.(input_regs)
              end
   end.
 
-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)).
+(* TODO: lemma not yet used
+
+Lemma union_inputs_In f tbl r:
+  Regset.In r (union_inputs 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.
@@ -437,27 +438,33 @@ Proof.
     + destruct IHl as (pc' & H1 & H2); eauto.
 Qed.
 
-Lemma inputs_exitrec_notIn f tbl r: 
+Lemma union_inputs_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).
+    -> ~Regset.In r (union_inputs 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
+(* This function computes the union of the inputs associated to the exits
+                   minus the optional register in [or] (typically the result of a call or a builtin).
+   i.e. similar to [pre_output_regs] in RTLpath.
+*)
+Definition pre_inputs (f:function) (tbl: list exit) (or: option reg): Regset.t :=
+ let rs := union_inputs f tbl in
  match or with 
  | Some r => Regset.remove r rs
  | None => rs
- end.
+ end
+ .
 
-Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
-  := transfer_regs (Regset.elements (inputs_exit f tbl or)).
+(* TODO: lemma pre_inputs_In + pre_inputs_notIn ? *)
 
-(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *)
+Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
+  := transfer_regs (Regset.elements (pre_inputs f tbl or)).
 
 
 (* TODO: move this elsewhere *)
@@ -469,8 +476,8 @@ Proof.
   - induction l; simpl; intuition.
 Qed.
 
-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.
+Lemma tr_pre_inputs f tbl or rs r:
+  Regset.In r (pre_inputs f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r.
 Proof.
   intros; eapply transfer_regs_inputs.
   rewrite <- SetoidList_InA_eq_equiv.
@@ -478,17 +485,17 @@ Proof.
 Qed.
 
 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.
+  ~(Regset.In r (pre_inputs 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.
 
-Local Hint Resolve tr_inputs_exit Regset.mem_2 Regset.mem_1: core.
+Local Hint Resolve tr_pre_inputs 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.
+  (tr_inputs f tbl or rs)#r = if Regset.mem r (pre_inputs f tbl or) then rs#r else Vundef.
 Proof.
   autodestruct; eauto.
   intros; apply tr_inputs_dead; eauto.
@@ -496,13 +503,15 @@ Proof.
   congruence.
 Qed.
 
+(* TODO: not yet used
 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, Regset.In r (pre_inputs 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. rewrite !tr_inputs_get.
   autodestruct; auto.
 Qed.
+*)
 
 Definition fsem (p: program) :=
   Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
@@ -524,7 +533,7 @@ Definition tr_regs: function -> final -> regset -> regset :=
 
 (* TODO: NOT USEFUL ?
 Definition liveout: function -> final -> Regset.t :=
-  poly_tr inputs_exit.
+  poly_tr pre_inputs.
 
 Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)).
 Proof.
@@ -535,30 +544,34 @@ 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.
+   Local Opaque pre_inputs.
    destruct fi; simpl; auto.
 Qed.
 *)
 
-(* * Reasoning modulo extensionality of [regset] into BTL semantics *)
+(* * Comparing BTL semantics modulo extensionality of [regset].
+
+NB: This is at least used in BTL_SEtheory (and probably in the future BTL_SchedulerProof).
+
+*)
 Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
-  | equiv_stackframe_intro res f sp pc rs1 rs2
-      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
-      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  | equiv_stackframe_intro res f sp pc (rs1 rs2: regset)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
   .
 
 Inductive equiv_state: state -> state -> Prop :=
-  | State_equiv stack f sp pc rs1 m rs2
-     (EQUIV: forall r, rs1#r = rs2#r): 
-     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
-  | Call_equiv stk stk' f args m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
-  | Return_equiv stk stk' v m
-      (STACKS: list_forall2 equiv_stackframe stk stk'):
-      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
+  | State_equiv stk1 stk2 f sp pc rs1 m rs2
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_state (State stk1 f sp pc rs1 m) (State stk2 f sp pc rs2 m)
+  | Call_equiv stk1 stk2 f args m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Callstate stk1 f args m) (Callstate stk2 f args m)
+  | Return_equiv stk1 stk2 v m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Returnstate stk1 v m) (Returnstate stk2 v m)
   .
-
 Local Hint Constructors equiv_stackframe equiv_state: core.
 
 Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
@@ -571,10 +584,10 @@ Proof.
   Local Hint Resolve equiv_stackframe_refl: core.
   induction stk; simpl; constructor; auto.
 Qed.
+Local Hint Resolve equiv_stack_refl: core.
 
 Lemma equiv_state_refl s: equiv_state s s.
 Proof.
-  Local Hint Resolve equiv_stack_refl: core.
   induction s; simpl; constructor; auto.
 Qed.
 
@@ -584,13 +597,13 @@ Proof.
   destruct 1; intros EQ; inv EQ; try econstructor; eauto.
   intros; eapply eq_trans; eauto.
 Qed.
+Local Hint Resolve equiv_stackframe_trans: core.
 
 Lemma equiv_stack_trans stk1 stk2:
   list_forall2 equiv_stackframe stk1 stk2 -> 
   forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
   list_forall2 equiv_stackframe stk1 stk3.
 Proof.
-  Local Hint Resolve equiv_stackframe_trans: core.
   induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
 Qed.
 
@@ -611,7 +624,220 @@ Proof.
   - repeat (rewrite Regmap.gso); auto.
 Qed.
 
+(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation.
 
+We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories 
+for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc.
+
+*)
+
+Inductive lessdef_stackframe: stackframe -> stackframe -> Prop :=
+  | lessdef_stackframe_intro res f sp pc rs1 rs2
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      :lessdef_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive lessdef_state: state -> state -> Prop :=
+  | State_lessdef stk1 stk2 f sp pc rs1 m1 rs2 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (State stk1 f sp pc rs1 m1) (State stk2 f sp pc rs2 m2)
+  | Call_lessdef stk1 stk2 f args1 args2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (ARGS: Val.lessdef_list args1 args2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Callstate stk1 f args1 m1) (Callstate stk2 f args2 m2)
+  | Return_lessdef stk1 stk2 v1 v2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: Val.lessdef v1 v2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Returnstate stk1 v1 m1) (Returnstate stk2 v2 m2)
+  .
+Local Hint Constructors lessdef_stackframe lessdef_state: core.
+
+Lemma lessdef_stackframe_refl stf: lessdef_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_refl: core.
+Lemma lessdef_stack_refl stk: list_forall2 lessdef_stackframe stk stk.
+Proof.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Local Hint Resolve lessdef_stack_refl: core.
+
+Lemma lessdef_list_refl args: Val.lessdef_list args args.
+Proof.
+  induction args; simpl; auto.
+Qed.
+
+Local Hint Resolve lessdef_list_refl Mem.extends_refl: core.
+
+Lemma lessdef_state_refl s: lessdef_state s s.
+Proof.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Local Hint Resolve Val.lessdef_trans: core.
+Lemma lessdef_stackframe_trans stf1 stf2 stf3:
+  lessdef_stackframe stf1 stf2 -> lessdef_stackframe stf2 stf3 -> lessdef_stackframe stf1 stf3.
+Proof.
+  destruct 1. intros LD; inv LD; try econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_trans: core.
+Lemma lessdef_stack_trans stk1 stk2:
+  list_forall2 lessdef_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 lessdef_stackframe stk2 stk3 -> 
+  list_forall2 lessdef_stackframe stk1 stk3.
+Proof.
+  induction 1; intros stk3 LD; inv LD; econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stack_trans Mem.extends_extends_compose Val.lessdef_list_trans: core.
+Lemma lessdef_state_trans s1 s2 s3: lessdef_state s1 s2 -> lessdef_state s2 s3 -> lessdef_state s1 s3.
+Proof.
+  destruct 1; intros LD; inv LD; econstructor; eauto.
+Qed.
+
+Lemma init_regs_lessdef_preserv args1 args2
+  (ARGS : Val.lessdef_list args1 args2)
+  : forall rl r, Val.lessdef (init_regs args1 rl)#r (init_regs args2 rl)#r.
+Proof.
+  induction ARGS; simpl; auto.
+  intros rl r1; destruct rl; simpl in *; auto.
+  eapply set_reg_lessdef; eauto.
+  intros r2; eauto.
+Qed.
+Local Hint Resolve init_regs_lessdef_preserv: core.
+
+Lemma tr_inputs_lessdef f rs1 rs2 tbl or r
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r.
+Proof.
+  unfold tid; rewrite tr_inputs_get.
+  autodestruct.
+Qed.
+Local Hint Resolve tr_inputs_lessdef: core.
+
+Lemma find_function_lessdef ge ros rs1 rs2 fd
+  (FIND: find_function ge ros rs1 = Some fd)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  : find_function ge ros rs2 = Some fd.
+Proof.
+  destruct ros; simpl in *; auto.
+  exploit Genv.find_funct_inv; eauto.
+  intros (b & EQ).
+  destruct (REGS r); try congruence.
+Qed.
+Local Hint Resolve find_function_lessdef regs_lessdef_regs: core.
+
+
+Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
+  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
+  rs2 m2
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
+     /\ (forall r, Val.lessdef rs1'#r rs2'#r)
+     /\ (Mem.extends m1' m2').
+Proof.
+  induction ISTEP; simpl; try_simplify_someHyps.
+Admitted.
+
+Local Hint Constructors final_step list_forall2: core.
+Local Hint Unfold regs_lessdef: core.
+
+Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
+  (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)
+  (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail).
+  - (* return *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+    destruct or; simpl; auto.
+  - (* tailcall *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+  - (* builtin *)
+    exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto.
+    intros (vl2' & BARGS & VARGS).
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED).
+    eexists; split; simpl; econstructor; eauto.
+    intros; apply set_res_lessdef; eauto.
+  - (* jumptable *)
+    eexists; split; simpl; econstructor; eauto.
+    destruct (REGS arg); try congruence.
+Qed.
+
+Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2
+  (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1)
+  (STACKS : list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS : Mem.extends m1 m2)
+  : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP).
+  exploit fsem2cfgsem_ibistep_simu; eauto.
+  intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2).
+  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS.
+  exploit fsem2cfgsem_finalstep_simu; eauto.
+  intros (s2 & FSTEP2 & LESSDEF). clear FSTEP.
+  unfold iblock_step; eexists; split; eauto.
+Qed.
+
+Local Hint Constructors step: core.
+
+Lemma fsem2cfgsem_step_simu ge s1 t s1' s2
+ (STEP: step tr_inputs ge s1 t s1')
+ (REGS: lessdef_state s1 s2)
+ :exists s2' : state,
+   step tid ge s2 t s2' /\
+   lessdef_state s1' s2'.
+Proof.
+  destruct STEP; inv REGS.
+  - (* iblock *)
+    intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP.
+    intros (s2 & STEP2 & REGS2).
+    eexists; split; eauto.
+  - (* internal call *)
+    exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto.
+    1-2: lia.
+    intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS.
+    eexists; split; econstructor; eauto.
+  - (* external call *)
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS.
+    eexists; split; econstructor; eauto.
+  - (* return *)
+    inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst.
+    inv STF2.
+    eexists; split; econstructor; eauto.
+    intros; eapply set_reg_lessdef; eauto.
+Qed.
+
+Theorem fsem2cfgsem prog:
+  forward_simulation (fsem prog) (cfgsem prog).
+Proof.
+  eapply forward_simulation_step with lessdef_state; simpl; auto.
+  - destruct 1; intros; eexists; intuition eauto. econstructor; eauto.
+  - intros s1 s2 r REGS FINAL; destruct FINAL.
+     inv REGS; inv STACKS; inv REGS0.
+     econstructor; eauto.
+  - intros; eapply fsem2cfgsem_step_simu; eauto.
+Qed.
 
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
-- 
cgit