From c7bc74b1860f30df678bf384a32cd9c6eb113beb Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 6 May 2021 09:07:07 +0200 Subject: start RTL -> BTL --- scheduling/BTL.v | 119 ++++++++++++++++++++++++++++++++----------------------- 1 file changed, 70 insertions(+), 49 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 7bc091ef..fb67d150 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -342,6 +342,8 @@ Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) + (** Matching BTL and RTL code We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. @@ -429,49 +431,10 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i) opc . -(* Partial copy of Duplicate and Duplicateproof. *) - Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := forall pc pc', dupmap!pc = Some pc' -> exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. -Record match_function dupmap f f': Prop := { - dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); - dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); - preserv_fnsig: fn_sig f = RTL.fn_sig f'; - preserv_fnparams: fn_params f = RTL.fn_params f'; - preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' -}. - -Inductive match_fundef: fundef -> RTL.fundef -> Prop := - | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := - | match_stackframe_intro - dupmap res f sp pc rs f' pc' - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). - -Inductive match_states: state -> RTL.state -> Prop := - | match_states_intro - dupmap st f sp pc rs m st' f' pc' - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) - | match_states_call - st st' f f' args m - (STACKS: list_forall2 match_stackframes st st') - (TRANSF: match_fundef f f') - : match_states (Callstate st f args m) (RTL.Callstate st' f' args m) - | match_states_return - st st' v m - (STACKS: list_forall2 match_stackframes st st') - : match_states (Returnstate st v m) (RTL.Returnstate st' v m) - . - (** Shared verifier between RTL -> BTL and BTL -> RTL *) Local Open Scope error_monad_scope. @@ -536,7 +499,6 @@ Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. Global Opaque builtin_res_eq_pos. -(* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := match ib with | BF fi => @@ -801,14 +763,73 @@ Definition verify_function dupmap f f' : res unit := do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); verify_cfg dupmap (fn_code f) (RTL.fn_code f'). -Lemma verify_function_correct dupmap f f' tt: - verify_function dupmap f f' = OK tt -> - fn_sig f = RTL.fn_sig f' -> - fn_params f = RTL.fn_params f' -> - fn_stacksize f = RTL.fn_stacksize f' -> - match_function dupmap f f'. +Definition is_seq (ib: iblock): bool := + match ib with + | Bseq _ _ => true + | _ => false + end. + +Definition is_atom (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ => false + | _ => true + end. + + +Inductive is_right_assoc: iblock -> Prop := + | ira_Bseq ib1 ib2: + is_seq ib1 = false -> + is_right_assoc ib1 -> + is_right_assoc ib2 -> + is_right_assoc (Bseq ib1 ib2) + | ira_Bcond cond args ib1 ib2 i: + is_right_assoc ib1 -> + is_right_assoc ib2 -> + is_right_assoc (Bcond cond args ib1 ib2 i) + | ira_others ib: + is_atom ib = true -> + is_right_assoc ib + . +Local Hint Constructors is_right_assoc: core. + +Fixpoint right_assoc (ib: iblock): iblock := + match ib with + | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2) + | Bcond cond args ib1 ib2 i => + Bcond cond args (right_assoc ib1) (right_assoc ib2) i + | ib => ib + end +with rec_rotate (ib: iblock) rem: iblock := + match ib with + | Bseq ib1 ib2 => + rec_rotate ib1 (rec_rotate ib2 rem) + | Bcond cond args ib1 ib2 i => + Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem + | ib => Bseq ib rem +end. + +Lemma right_assoc_rec_rotate_correct ib: + is_right_assoc (right_assoc ib) + /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)). Proof. - unfold verify_function; intro VERIF. monadInv VERIF. - constructor; eauto. - eapply verify_cfg_correct; eauto. + induction ib; simpl; intuition. Qed. + +Lemma right_assoc_correct ib: + is_right_assoc (right_assoc ib). +Proof. + destruct (right_assoc_rec_rotate_correct ib); auto. +Qed. + +Definition right_assoc_code (cfg: code): code := + (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg). + +Lemma right_assoc_code_correct cfg pc ib : + (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)). +Proof. + unfold right_assoc_code. + rewrite PTree.gmap. + destruct (cfg!pc); simpl; intros; try_simplify_someHyps. + apply right_assoc_correct; auto. +Qed. + -- cgit