From 6938945d80bf16a6de4986e2815113e938bff6c3 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé 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