diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
commit | 271f87ba08f42340900378c0797511d4071fc1b8 (patch) | |
tree | 8b861fa3221b179bb8e3ad339864cdb7c541d46a /scheduling | |
parent | e6a1df51a2a3d29c58d72453355e50a979e86297 (diff) | |
download | compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.tar.gz compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.zip |
BTL Scheduler oracle and some drafts
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTLScheduleraux.ml | 6 | ||||
-rw-r--r-- | scheduling/BTL_Livecheck.v | 47 | ||||
-rw-r--r-- | scheduling/BTL_Scheduler.v | 2 | ||||
-rw-r--r-- | scheduling/BTLmatchRTL.v | 42 | ||||
-rw-r--r-- | scheduling/RTLtoBTLaux.ml | 6 |
5 files changed, 91 insertions, 12 deletions
diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml index ad0c307d..b87636e1 100644 --- a/scheduling/BTLScheduleraux.ml +++ b/scheduling/BTLScheduleraux.ml @@ -4,6 +4,7 @@ open Registers open BTL open BTLtypes open DebugPrint +open PrintBTL open RTLcommonaux open InstructionScheduler open PrepassSchedulingOracleDeps @@ -243,8 +244,11 @@ let rec do_schedule btl = function let btl' = schedule_blk n ibf btl in do_schedule btl' blks -let btl_scheduler btl = +let btl_scheduler f = + let btl = f.fn_code in (*debug_flag := true;*) let btl' = do_schedule btl (PTree.elements btl) in + debug "Scheduled BTL Code:\n"; + print_btl_code stderr btl'; (*debug_flag := false;*) btl' diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 2baba025..6064e4cd 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -4,8 +4,51 @@ Require Import Errors RTL BTL BTLmatchRTL. (** TODO: adapt stuff RTLpathLivegen *) -Definition liveness_checker (f: BTL.function): res unit := OK tt. (* TODO: implement this ! *) - +Local Open Scope lazy_bool_scope. + +Local Open Scope option_monad_scope. + +Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool := + match rl with + | nil => true + | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive + end. + +(* +Fixpoint iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option Regset.t := + match ib with + | Bseq ib1 ib2 => + SOME alive' <- iblock_checker btl ib1 alive IN + iblock_checker btl ib1 alive' (Some ib2) + | Bnop _ => + iblock_checker btl alive + | Bop _ args dest _ => + ASSERT list_mem args alive IN + iblock_checker btl (Regset.add dest alive) + | Bload _ _ _ args dest _ => + ASSERT list_mem args alive IN + iblock_checker btl (Regset.add dest alive) + | Bstore _ _ args src _ => + ASSERT Regset.mem src alive IN + ASSERT list_mem args alive IN + iblock_checker btl alive + | Bcond _ args (BF (Bgoto s) _) ib2 _ => + ASSERT list_mem args alive IN + SOME _ <- iblock_checker btl ib2 alive None IN + SOME next <- btl!s IN + ASSERT Regset.subset next.(input_regs) alive IN + iblock_checker btl next.(entry) next.(input_regs) None + | Bcond _ _ _ _ _ => None + | BF _ _ => Some tt + end. + +Definition liveness_checker (f: BTL.function): res unit := + match f.(fn_code)!(f.(fn_entrypoint)) with + | Some ibf => iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) + | None => Error (msg "liveness_checker: empty function") + end. + *) +Definition liveness_checker (f: BTL.function): res unit := OK tt. Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. (** TODO: adapt stuff RTLpathLivegenproof *) diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 43d6dd5e..b479204c 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -7,6 +7,8 @@ Require Import Errors Linking BTL_SEtheory. (** External oracle *) Axiom scheduler: BTL.function -> BTL.code. +Extract Constant scheduler => "BTLScheduleraux.btl_scheduler". + (* a specification of the verification to do on each function *) Record match_function (f1 f2: BTL.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index 8994579d..8081b3a6 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -30,21 +30,55 @@ Qed. Local Hint Resolve tr_inputs_lessdef init_regs_lessdef_preserv find_function_lessdef regs_lessdef_regs lessdef_state_refl: core. +Local Hint Unfold regs_lessdef: core. -Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of +Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of + rs2 m2 ib (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. + induction ISTEP; simpl; try_simplify_someHyps; intros. + - (* Bop *) + exploit (@eval_operation_lessdef _ _ ge sp op (rs ## args)); eauto. + intros (v1 & EVAL' & LESSDEF). + do 2 eexists; rewrite EVAL'. repeat (split; eauto). + eapply set_reg_lessdef; eauto. + - (* Bload *) + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. + intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto. + intros (v3 & LOAD' & LESSDEF'). + do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto). + eapply set_reg_lessdef; eauto. + - (* Bstore *) + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. + intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto. + intros (v3 & STORE' & LESSDEF'). + do 2 eexists; rewrite EVAL', STORE'. repeat (split; eauto). + - (* Bseq stop *) + exploit IHISTEP; eauto. intros (rs2' & m2' & IBIS & REGS' & MEMS'). + destruct (iblock_istep_run _ _ _ _ _); try congruence. + destruct o, _fin; simpl in *; try congruence. eauto. + - (* Bseq continue *) + + (* TODO gourdinl induction pb? + exploit IHISTEP1; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1). + rewrite IBIS1; simpl. rewrite iblock_istep_run_equiv in ISTEP2. + exploit IHISTEP2; eauto. intros (rs4 & m4 & IBIS2 & REGS2 & MEMS2). + destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps. + intros; apply IHISTEP1 in MEMS; auto. + exploit IHISTEP2; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1). + + + destruct (iblock_istep_run _ _ _ _ _) eqn:EQb1. + 2: { rewrite iblock_istep_run_equiv in ISTEP1. destruct b1; simpl in *; try congruence. + destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps.*) Admitted. Local Hint Constructors lessdef_stackframe lessdef_state final_step list_forall2 step: 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) diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index d04326ea..e709d846 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -6,7 +6,6 @@ open RTLcommonaux open DebugPrint open BTLtypes open BTLcommonaux -open BTLScheduleraux let encaps_final inst osucc = match inst with @@ -102,19 +101,16 @@ let rtl2btl (f : RTL.coq_function) = let btl = translate_function code entry join_points liveness in let dm = PTree.map (fun n i -> n) btl in (* TODO gourdinl move elsewhere *) - let btl' = btl_scheduler btl in debug "Entry %d\n" (p2i entry); (*debug_flag := true;*) debug "RTL Code: "; print_code code; debug "BTL Code:\n"; print_btl_code stderr btl; - debug "Scheduled BTL Code:\n"; - print_btl_code stderr btl'; (*debug_flag := false;*) debug "Dupmap:\n"; print_ptree print_pint dm; debug "Join points: "; print_true_nodes join_points; debug "\n"; - ((btl', entry), dm) + ((btl, entry), dm) |