From 271f87ba08f42340900378c0797511d4071fc1b8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 31 May 2021 16:55:18 +0200 Subject: BTL Scheduler oracle and some drafts --- driver/Compiler.vexpand | 2 +- scheduling/BTLScheduleraux.ml | 6 +++++- scheduling/BTL_Livecheck.v | 47 +++++++++++++++++++++++++++++++++++++++++-- scheduling/BTL_Scheduler.v | 2 ++ scheduling/BTLmatchRTL.v | 42 ++++++++++++++++++++++++++++++++++---- scheduling/RTLtoBTLaux.ml | 6 +----- test/c/cscript.sh | 21 +++++++++++++++++++ test/c/cscript2.sh | 5 +++++ test/c/pbcompare.sh | 18 +++++++++++++++++ 9 files changed, 136 insertions(+), 13 deletions(-) create mode 100755 test/c/cscript.sh create mode 100755 test/c/cscript2.sh create mode 100755 test/c/pbcompare.sh diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 85f265db..40ea0d68 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -300,7 +300,7 @@ EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply RTLtoBTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply BTLtoRTLproof.transf_program_correct_cfg; eassumption. + eapply BTLtoRTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. 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) diff --git a/test/c/cscript.sh b/test/c/cscript.sh new file mode 100755 index 00000000..f797df7b --- /dev/null +++ b/test/c/cscript.sh @@ -0,0 +1,21 @@ +#!/bin/bash + +CCREF="/home/yuki/Work/VERIMAG/Compcert_riscv_bis/ccomp -static -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_bis/runtime -fno-expanse-rtlcond -fno-expanse-others" +CCTEST="/home/yuki/Work/VERIMAG/Compcert_riscv_third/ccomp -static -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_third/runtime -fno-expanse-rtlcond -fno-expanse-others" + +$CCREF nsieve.c > refout 2>&1 +mv a.out ref.out +$CCTEST nsieve.c > testout 2>&1 +#sort -k1 -n -t, refout -o refout +#sort -k1 -n -t, testout -o testout +qemu-riscv64 ref.out > logref 2>&1 +{ qemu-riscv64 a.out > logtest 2>&1; } 2> logtest +if cat logref | ack "Primes"; then + if cmp -s logref logtest; then + exit 1 + else + exit 0 + fi +else + exit 1 +fi diff --git a/test/c/cscript2.sh b/test/c/cscript2.sh new file mode 100755 index 00000000..350c392d --- /dev/null +++ b/test/c/cscript2.sh @@ -0,0 +1,5 @@ +#/bin/bash + +/home/gourdinl/Work/VERIMAG/Compcert_riscv_third/ccomp -static -fprepass= revlist -U__GNUC__ -stdlib ../../runtime -dclight -dasm -c qsort.c > log 2>&1 + +cat log | ack "instead of Some" diff --git a/test/c/pbcompare.sh b/test/c/pbcompare.sh new file mode 100755 index 00000000..b47c83c4 --- /dev/null +++ b/test/c/pbcompare.sh @@ -0,0 +1,18 @@ +#!/bin/bash + +CCREF="/home/yuki/Work/VERIMAG/Compcert_riscv_bis/ccomp -static -S -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_bis/runtime -fno-expanse-rtlcond -fno-expanse-others" +CCTEST="/home/yuki/Work/VERIMAG/Compcert_riscv_third/ccomp -static -S -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_third/runtime -fno-expanse-rtlcond -fno-expanse-others" + +for prog in *.c; do + $CCREF $prog > refout 2>&1 + $CCTEST $prog > testout 2>&1 + sort -k1 -n -t, refout -o refout + sort -k1 -n -t, testout -o testout + if cmp -s refout testout; then + echo "$prog passed" + else + echo "$prog failed" + diff -y refout testout + exit 1 + fi +done -- cgit