diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-31 15:39:18 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-31 15:39:18 +0100 |
commit | 2e232deb0aed4af2448eb9f1031e8084181174b7 (patch) | |
tree | 6dd781e24a2a260047a8fc9e0a177d1b81bc3b5c /src/hls/RTLBlockInstr.v | |
parent | f3e95ff03f1dc9a9de57721eb1c9c93c19329613 (diff) | |
download | vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.tar.gz vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.zip |
Add list of bb to semantics
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r-- | src/hls/RTLBlockInstr.v | 169 |
1 files changed, 85 insertions, 84 deletions
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) |