From 9432515e5814e8614c8f2320a8ae6d268065c9ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 27 Jan 2021 16:42:27 +0000 Subject: Add more proofs for RTLPargen correctness --- src/hls/RTLPar.v | 34 +++++++++++++++++---------- src/hls/RTLPargen.v | 28 +++++++++++++++++----- src/hls/RTLPargenproof.v | 61 +++++++++++++++++++++++++++++++++++++++++------- 3 files changed, 97 insertions(+), 26 deletions(-) (limited to 'src/hls') diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 3707b42..1e5dd43 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -28,11 +28,15 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. +Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlockInstr. Definition bblock_body := list (list instr). Definition bblock := RTLBlockInstr.bblock bblock_body. +Definition is_empty (b: bblock_body) : Prop := + Forall (fun n => Forall (fun m => m = RBnop) n) b. + Definition code : Type := PTree.t bblock. Record function: Type := mkfunction { @@ -140,40 +144,46 @@ Section RELSEM. step (Block stack f sp (mk_bblock (bb :: bbs) cfi) rs m) E0 (Block stack f sp (mk_bblock bbs cfi) rs' m') | exec_RBcall: - forall s f sp rs m res fd ros sig args pc', + forall s f sp rs m res fd ros sig args pc' el, find_function ros rs = Some fd -> funsig fd = sig -> - step (Block s f sp (mk_bblock nil (RBcall sig ros args res pc')) rs m) + is_empty el -> + step (Block s f sp (mk_bblock el (RBcall sig ros args res pc')) rs m) E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m) | exec_RBtailcall: - forall s f stk rs m sig ros args fd m', + forall s f stk rs m sig ros args fd m' el, find_function ros rs = Some fd -> funsig fd = sig -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock nil (RBtailcall sig ros args)) rs m) + is_empty el -> + step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock el (RBtailcall sig ros args)) rs m) E0 (Callstate s fd rs##args m') | exec_RBbuiltin: - forall s f sp rs m ef args res pc' vargs t vres m', + forall s f sp rs m ef args res pc' vargs t vres m' el, eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> - step (Block s f sp (mk_bblock nil (RBbuiltin ef args res pc')) rs m) + is_empty el -> + step (Block s f sp (mk_bblock el (RBbuiltin ef args res pc')) rs m) t (State s f sp pc' (regmap_setres res vres rs) m') | exec_RBcond: - forall s f sp rs m cond args ifso ifnot b pc', + forall s f sp rs m cond args ifso ifnot b pc' el, eval_condition cond rs##args m = Some b -> pc' = (if b then ifso else ifnot) -> - step (Block s f sp (mk_bblock nil (RBcond cond args ifso ifnot)) rs m) + is_empty el -> + step (Block s f sp (mk_bblock el (RBcond cond args ifso ifnot)) rs m) E0 (State s f sp pc' rs m) | exec_RBjumptable: - forall s f sp rs m arg tbl n pc', + forall s f sp rs m arg tbl n pc' el, rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - step (Block s f sp (mk_bblock nil (RBjumptable arg tbl)) rs m) + is_empty el -> + step (Block s f sp (mk_bblock el (RBjumptable arg tbl)) rs m) E0 (State s f sp pc' rs m) | exec_Ireturn: - forall s f stk rs m or m', + forall s f stk rs m or m' el, Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock nil (RBreturn or)) rs m) + is_empty el -> + step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock el (RBreturn or)) rs m) E0 (Returnstate s (regmap_optget or Vundef rs) m') | exec_function_internal: forall s f args m m' stk, diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index f745466..d592206 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -485,13 +485,13 @@ Get a sequence from the basic block. Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := match b with | nil => f - | i :: l => abstract_sequence (update f i) l + | i :: l => update (abstract_sequence f l) i end. Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest := match b with | nil => f - | i :: l => abstract_sequence_par (abstract_sequence f i) l + | i :: l => abstract_sequence (abstract_sequence_par f l) i end. (*| @@ -507,9 +507,21 @@ We define the top-level oracle that will check if two basic blocks are equivalen transformation. |*) +Definition empty_trees (bb: RTLBlock.bblock_body) (bbt: RTLPar.bblock_body) : bool := + match bb with + | nil => + match bbt with + | nil => true + | _ => false + end + | _ => true + end. + Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool := check (abstract_sequence empty (bb_body bb)) - (abstract_sequence_par empty (bb_body bbt)). + (abstract_sequence_par empty (bb_body bbt)) && + check_control_flow_instr (bb_exit bb) (bb_exit bbt) && + empty_trees (bb_body bb) (bb_body bbt). Definition check_scheduled_trees := beq2 schedule_oracle. @@ -539,9 +551,13 @@ Proof. solve_scheduled_trees_correct. Qed. Parameter schedule : RTLBlock.function -> RTLPar.function. Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function := - let tf := schedule f in - if check_scheduled_trees f.(RTLBlock.fn_code) tf.(fn_code) then - Errors.OK tf + let tfcode := fn_code (schedule f) in + if check_scheduled_trees f.(RTLBlock.fn_code) tfcode then + Errors.OK (mkfunction f.(RTLBlock.fn_sig) + f.(RTLBlock.fn_params) + f.(RTLBlock.fn_stacksize) + tfcode + f.(RTLBlock.fn_entrypoint)) else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 21caf7f..730ac98 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -18,8 +18,8 @@ Require Import compcert.common.AST. Require Import compcert.common.Errors. -Require Import compcert.common.Globalenvs. Require Import compcert.common.Linking. +Require Import compcert.common.Globalenvs. Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. @@ -98,8 +98,38 @@ Section CORRECTNESS. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). - Proof - (Genv.senv_transf_partial TRANSL). + Proof (Genv.senv_transf_partial TRANSL). + + Lemma sig_transl_function: + forall (f: RTLBlock.fundef) (tf: RTLPar.fundef), + transl_fundef f = OK tf -> + RTLPar.funsig tf = RTLBlock.funsig f. + Proof. + unfold transl_fundef, transf_partial_fundef, transl_function; intros; + repeat destruct_match; crush; + match goal with H: OK _ = OK _ |- _ => inv H end; auto. + Qed. + + Lemma find_function_translated: + forall ros rs f, + RTLBlock.find_function ge ros rs = Some f -> + exists tf, RTLPar.find_function tge ros rs = Some tf + /\ transl_fundef f = OK tf. + Proof. + destruct ros; simplify; + [ exploit functions_translated; eauto + | rewrite symbols_preserved; destruct_match; + try (apply function_ptr_translated); crush ]. + Qed. + + Lemma schedule_oracle_nil: + forall bb cfi, + schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true -> + is_empty (bb_body bb) /\ bb_exit bb = cfi. + Proof. + unfold schedule_oracle, check_control_flow_instr, is_empty. + simplify; repeat destruct_match; crush. + Qed. Theorem transl_step_correct : forall (S1 : RTLBlock.state) t S2, @@ -118,12 +148,27 @@ Section CORRECTNESS. destruct (check_scheduled_trees (RTLBlock.fn_code f) (fn_code (schedule f))) eqn:?; [| discriminate ]; inv H2 | [ H: context[check_scheduled_trees] |- _ ] => - eapply check_scheduled_trees_correct in H; [| solve [ eauto ] ] + let H2 := fresh "CHECK" in + learn H as H2; + eapply check_scheduled_trees_correct in H2; [| solve [eauto] ] + | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] => + let H2 := fresh "SCHED" in + learn H as H2; + apply schedule_oracle_nil in H2 | [ H: exists _, _ |- _ ] => inv H + | _ => progress simplify end. - induction 1; simplify; repeat t; simplify. + induction 1; repeat t. - - repeat econstructor; eauto. - - admit. - - repeat econstructor; eauto. + { repeat econstructor; eauto. } + { admit. } + { destruct bb'; exploit find_function_translated; simplify; + repeat econstructor; eauto using sig_transl_function. } + { destruct bb'; exploit find_function_translated; simplify; + repeat econstructor; eauto using sig_transl_function. } + { destruct bb'; simplify; subst; repeat econstructor; eauto using Events.eval_builtin_args_preserved, Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } + { destruct bb'; simplify; subst; repeat econstructor; eauto. } + { destruct bb'; simplify; subst; repeat econstructor; eauto. } + { destruct bb'; simplify; subst; repeat econstructor; eauto. } + { repeat econstructor; eauto. } -- cgit