From 2e232deb0aed4af2448eb9f1031e8084181174b7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 31 Mar 2022 15:39:18 +0100 Subject: Add list of bb to semantics --- src/hls/RICtransf.v | 4 +- src/hls/RTLBlockInstr.v | 169 +++++++++++++++++++++++---------------------- src/hls/RTLBlockgenproof.v | 3 +- src/hls/RTLPar.v | 11 +-- src/hls/RTLParFUgen.v | 2 +- src/hls/RTLPargen.v | 2 +- src/hls/RTLPargenproof.v | 4 +- 7 files changed, 99 insertions(+), 96 deletions(-) (limited to 'src/hls') diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v index 643a3a7..3b82b29 100644 --- a/src/hls/RICtransf.v +++ b/src/hls/RICtransf.v @@ -58,7 +58,7 @@ Definition add_bb (should_split: bool) (i: list (list instr)) | (a, b) => if should_split then (a, i::b) else (i::a, b) end. -Fixpoint first_split (saw_pred: bool) (bb: bb) := +Fixpoint first_split (saw_pred: bool) (bb: list bb) := match bb with | a :: b => match includes_setpred a with @@ -72,7 +72,7 @@ Fixpoint first_split (saw_pred: bool) (bb: bb) := | nil => (None, (nil, nil)) end. -Definition split_bb (fresh: node) (b: bb) : bb * bb * bb := +Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb := match first_split false b with | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 35ae03e..4631b5a 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -113,28 +113,28 @@ Definition max_reg_instr (m: positive) (i: instr) := match i with | RBnop => m | RBop p op args res => - fold_left Pos.max args (Pos.max res m) + fold_left Pos.max args (Pos.max res m) | RBload p chunk addr args dst => - fold_left Pos.max args (Pos.max dst m) + fold_left Pos.max args (Pos.max dst m) | RBstore p chunk addr args src => - fold_left Pos.max args (Pos.max src m) + fold_left Pos.max args (Pos.max src m) | RBsetpred p' c args p => - fold_left Pos.max args m + fold_left Pos.max args m end. Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := match i with | RBcall sig (inl r) args res s => - fold_left Pos.max args (Pos.max r (Pos.max res m)) + fold_left Pos.max args (Pos.max r (Pos.max res m)) | RBcall sig (inr id) args res s => - fold_left Pos.max args (Pos.max res m) + fold_left Pos.max args (Pos.max res m) | RBtailcall sig (inl r) args => - fold_left Pos.max args (Pos.max r m) + fold_left Pos.max args (Pos.max r m) | RBtailcall sig (inr id) args => - fold_left Pos.max args m + fold_left Pos.max args m | RBbuiltin ef args res s => fold_left Pos.max (params_of_builtin_args args) - (fold_left Pos.max (params_of_builtin_res res) m) + (fold_left Pos.max (params_of_builtin_res res) m) | RBcond cond args ifso ifnot => fold_left Pos.max args m | RBjumptable arg tbl => Pos.max arg m | RBreturn None => m @@ -150,7 +150,7 @@ Definition eval_predf (pr: predset) (p: pred_op) := sat_predicate p (fun x => pr !! (Pos.of_nat x)). #[global] -Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf. + Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf. Proof. unfold Proper. simplify. unfold "==>". intros. @@ -177,8 +177,8 @@ Proof. induction p; simplify; auto; try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto); - [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por]; - erewrite IHp1; try eassumption; erewrite IHp2; eauto. + [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por]; + erewrite IHp1; try eassumption; erewrite IHp2; eauto. Qed. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := @@ -200,10 +200,10 @@ Definition of the instruction state, which contains the following: |*) Record instr_state := mk_instr_state { - is_rs: regset; - is_ps: predset; - is_mem: mem; -}. + is_rs: regset; + is_ps: predset; + is_mem: mem; + }. (*| Top-Level Type Definitions @@ -215,19 +215,19 @@ Section DEFINITION. Context {bblock_body: Type}. Record bblock : Type := mk_bblock { - bb_body: list bblock_body; - bb_exit: cf_instr - }. + bb_body: list bblock_body; + bb_exit: cf_instr + }. Definition code: Type := PTree.t bblock. Record function: Type := mkfunction { - fn_sig: signature; - fn_params: list reg; - fn_stacksize: Z; - fn_code: code; - fn_entrypoint: node - }. + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node + }. Definition fundef := AST.fundef function. @@ -241,12 +241,12 @@ Section DEFINITION. Inductive stackframe : Type := | Stackframe: - forall (res: reg) (**r where to store the result *) - (f: function) (**r calling function *) - (sp: val) (**r stack pointer in calling function *) - (pc: node) (**r program point in calling function *) - (rs: regset) (**r register state in calling function *) - (pr: predset), (**r predicate state of the calling + forall (res: reg) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (pc: node) (**r program point in calling function *) + (rs: regset) (**r register state in calling function *) + (pr: predset), (**r predicate state of the calling function *) stackframe. @@ -258,27 +258,28 @@ Definition of the ``state`` type, which is used by the ``step`` functions. |*) Variant state : Type := - | State: + | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r current function *) (sp: val) (**r stack pointer *) (pc: node) (**r current program point in [c] *) - (il: list bblock_body) + (il: list bblock_body) (**r basic block body that is + currently executing. *) (rs: regset) (**r register state *) (pr: predset) (**r predicate register state *) (m: mem), (**r memory state *) - state - | Callstate: + state + | Callstate: forall (stack: list stackframe) (**r call stack *) (f: fundef) (**r function to call *) (args: list val) (**r arguments to the call *) (m: mem), (**r memory state *) - state - | Returnstate: + state + | Returnstate: forall (stack: list stackframe) (**r call stack *) (v: val) (**r return value for the call *) (m: mem), (**r memory state *) - state. + state. End DEFINITION. @@ -300,26 +301,26 @@ Section RELSEM. match ros with | inl r => Genv.find_funct ge rs#r | inr symb => - match Genv.find_symbol ge symb with - | None => None - | Some b => Genv.find_funct_ptr ge b - end + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end end. Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := | eval_pred_true: - forall i i' p, + forall i i' p, eval_predf (is_ps i) p = true -> eval_pred (Some p) i i' i' | eval_pred_false: - forall i i' p, + forall i i' p, eval_predf (is_ps i) p = false -> eval_pred (Some p) i i' i | eval_pred_none: - forall i i', eval_pred None i i' i. + forall i i', eval_pred None i i' i. -(*| + (*| .. index:: triple: semantics; RTLBlockInstr; instruction @@ -329,39 +330,39 @@ Step Instruction Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop := | exec_RBnop: - forall sp ist, - step_instr sp ist RBnop ist + forall sp ist, + step_instr sp ist RBnop ist | exec_RBop: - forall op v res args rs m sp p ist pr, - eval_operation ge sp op rs##args m = Some v -> - eval_pred p (mk_instr_state rs pr m) - (mk_instr_state (rs#res <- v) pr m) ist -> - step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist + forall op v res args rs m sp p ist pr, + eval_operation ge sp op rs##args m = Some v -> + eval_pred p (mk_instr_state rs pr m) + (mk_instr_state (rs#res <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist | exec_RBload: - forall addr rs args a chunk m v dst sp p pr ist, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - eval_pred p (mk_instr_state rs pr m) - (mk_instr_state (rs#dst <- v) pr m) ist -> - step_instr sp (mk_instr_state rs pr m) - (RBload p chunk addr args dst) ist + forall addr rs args a chunk m v dst sp p pr ist, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + eval_pred p (mk_instr_state rs pr m) + (mk_instr_state (rs#dst <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) + (RBload p chunk addr args dst) ist | exec_RBstore: - forall addr rs args a chunk m src m' sp p pr ist, - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a rs#src = Some m' -> - eval_pred p (mk_instr_state rs pr m) - (mk_instr_state rs pr m') ist -> - step_instr sp (mk_instr_state rs pr m) - (RBstore p chunk addr args src) ist + forall addr rs args a chunk m src m' sp p pr ist, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + eval_pred p (mk_instr_state rs pr m) + (mk_instr_state rs pr m') ist -> + step_instr sp (mk_instr_state rs pr m) + (RBstore p chunk addr args src) ist | exec_RBsetpred: - forall sp rs pr m p c b args p' ist, + forall sp rs pr m p c b args p' ist, Op.eval_condition c rs##args m = Some b -> eval_pred p' (mk_instr_state rs pr m) - (mk_instr_state rs (pr#p <- b) m) ist -> + (mk_instr_state rs (pr#p <- b) m) ist -> step_instr sp (mk_instr_state rs pr m) - (RBsetpred p' c args p) ist. + (RBsetpred p' c args p) ist. -(*| + (*| .. index:: triple: semantics; RTLBlockInstr; control-flow instruction @@ -375,44 +376,44 @@ Step Control-Flow Instruction find_function ros rs = Some fd -> funsig fd = sig -> step_cf_instr (State s f sp pc nil rs pr m) (RBcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) + E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) | exec_RBtailcall: - forall s f stk rs m sig ros args fd m' pc pr, + forall s f stk rs m sig ros args fd m' pc pr, find_function ros rs = Some fd -> funsig fd = sig -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc nil rs pr m) (RBtailcall sig ros args) - E0 (Callstate s fd rs##args m') + E0 (Callstate s fd rs##args m') | exec_RBbuiltin: - forall s f sp rs m ef args res pc' vargs t vres m' pc pr, + forall s f sp rs m ef args res pc' vargs t vres m' pc pr, eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> step_cf_instr (State s f sp pc nil rs pr m) (RBbuiltin ef args res pc') - t (State s f sp pc' nil (regmap_setres res vres rs) pr m') + t (State s f sp pc' nil (regmap_setres res vres rs) pr m') | exec_RBcond: - forall s f sp rs m cond args ifso ifnot b pc pc' pr, + forall s f sp rs m cond args ifso ifnot b pc pc' pr, eval_condition cond rs##args m = Some b -> pc' = (if b then ifso else ifnot) -> step_cf_instr (State s f sp pc nil rs pr m) (RBcond cond args ifso ifnot) - E0 (State s f sp pc' nil rs pr m) + E0 (State s f sp pc' nil rs pr m) | exec_RBjumptable: - forall s f sp rs m arg tbl n pc pc' pr, + forall s f sp rs m arg tbl n pc pc' pr, rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> step_cf_instr (State s f sp pc nil rs pr m) (RBjumptable arg tbl) - E0 (State s f sp pc' nil rs pr m) + E0 (State s f sp pc' nil rs pr m) | exec_RBreturn: - forall s f stk rs m or pc m' pr, + forall s f stk rs m or pc m' pr, Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc nil rs pr m) (RBreturn or) - E0 (Returnstate s (regmap_optget or Vundef rs) m') + E0 (Returnstate s (regmap_optget or Vundef rs) m') | exec_RBgoto: - forall s f sp pc rs pr m pc', + forall s f sp pc rs pr m pc', step_cf_instr (State s f sp pc nil rs pr m) (RBgoto pc') E0 (State s f sp pc' nil rs pr m) | exec_RBpred_cf: - forall s f sp pc rs pr m cf1 cf2 st' p t, + forall s f sp pc rs pr m cf1 cf2 st' p t, step_cf_instr (State s f sp pc nil rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> step_cf_instr (State s f sp pc nil rs pr m) diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index 42d471c..f870278 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -117,7 +117,7 @@ Variant match_states : RTL.state -> RTLBlock.state -> Prop := (PC: find_block_spec tf.(fn_code) pc pc') (STK: Forall2 match_stackframe stk stk'), match_states (RTL.State stk f sp pc rs m) - (State stk' tf sp pc' rs ps m). + (State stk' tf sp pc' nil rs ps m). Definition match_prog (p: RTL.program) (tp: RTLBlock.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. @@ -165,5 +165,6 @@ Section CORRECTNESS. apply senv_preserved. admit. eauto using transl_final_states. + Admitted. End CORRECTNESS. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index a36177e..7ae563d 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -69,7 +69,7 @@ Section RELSEM. step_instr_seq sp state nil state. Inductive step_instr_block (sp : val) - : instr_state -> bb -> instr_state -> Prop := + : instr_state -> list bb -> instr_state -> Prop := | exec_instr_block_cons: forall state i state' state'' instrs, step_instr_seq sp state i state' -> @@ -81,12 +81,12 @@ Section RELSEM. Inductive step: state -> trace -> state -> Prop := | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb pr pr', + forall s (f: function) sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> - step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs pr m) t s' + step_cf_instr ge (State s f sp pc nil rs' pr' m') bb.(bb_exit) t s' -> + step (State s f sp pc nil rs pr m) t s' | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -95,6 +95,7 @@ Section RELSEM. f (Vptr stk Ptrofs.zero) f.(fn_entrypoint) + nil (init_regs args f.(fn_params)) (PMap.init false) m') @@ -106,7 +107,7 @@ Section RELSEM. | exec_return: forall res f sp pc rs s vres m pr, step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m) - E0 (State s f sp pc (rs#res <- vres) pr m). + E0 (State s f sp pc nil (rs#res <- vres) pr m). End RELSEM. diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 49ee6e7..a104056 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -134,7 +134,7 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) | None => ((cycle + 1)%positive, curr :: bb) end. -Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body := +Definition transl_bb (res: resources) (bb: list RTLPar.bb): Errors.res RTLParFU.bblock_body := do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; let (li, tr) := litr in OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index d425049..214da6f 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -227,7 +227,7 @@ We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling transformation. |*) -Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := +Definition empty_trees (bb: list RTLBlock.bb) (bbt: list RTLPar.bb) : bool := match bb with | nil => match bbt with diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 4e88b13..215aef5 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -812,8 +812,8 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := (STACKS: list_forall2 match_stackframes sf sf') (REG: forall x, rs !! x = rs' !! x) (REG: forall x, ps !! x = ps' !! x), - match_states (State sf f sp pc rs ps m) - (State sf' tf sp pc rs' ps' m) + match_states (State sf f sp pc nil rs ps m) + (State sf' tf sp pc nil rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), -- cgit