From dd8d4ae9c320668ac5fd70f72ea76b768edf8165 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 26 Mar 2022 15:48:47 +0000 Subject: Remove literal files again --- src/hls/RTLBlockInstr.v | 142 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 99 insertions(+), 43 deletions(-) (limited to 'src/hls/RTLBlockInstr.v') diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index bd40516..d23850a 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -16,7 +16,6 @@ * along with this program. If not, see . *) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-imports][rtlblockinstr-imports]] *) Require Import Coq.micromega.Lia. Require Import compcert.backend.Registers. @@ -31,20 +30,47 @@ Require Import compcert.verilog.Op. Require Import Predicate. Require Import Vericertlib. -(* rtlblockinstr-imports ends here *) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-def][rtlblockinstr-instr-def]] *) Definition node := positive. +(*| +============= +RTLBlockInstr +============= + +These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have +consistent instructions, which greatly simplifies the proofs, as they will by +default have the same instruction syntax and semantics. The only changes are +therefore at the top-level of the instructions. + +Instruction Definition +====================== + +First, we define the instructions that can be placed into a basic block, meaning +they won't branch. The main changes to how instructions are defined in ``RTL``, +is that these instructions don't have a next node, as they will be in a basic +block, and they also have an optional predicate (``pred_op``). +|*) + Inductive instr : Type := | RBnop : instr -| RBop : option pred_op -> operation -> list reg -> reg -> instr -| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr -| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr -| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr. -(* rtlblockinstr-instr-def ends here *) +| RBop : + option pred_op -> operation -> list reg -> reg -> instr +| RBload : + option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr +| RBstore : + option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr +| RBsetpred : + option pred_op -> condition -> list reg -> predicate -> instr. + +(*| +Control-Flow Instruction Definition +=================================== + +These are the instructions that count as control-flow, and will be placed at the +end of the basic blocks. +|*) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-cf-instr-def][rtlblockinstr-cf-instr-def]] *) Inductive cf_instr : Type := | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr | RBtailcall : signature -> reg + ident -> list reg -> cf_instr @@ -55,9 +81,12 @@ Inductive cf_instr : Type := | RBreturn : option reg -> cf_instr | RBgoto : node -> cf_instr | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. -(* rtlblockinstr-cf-instr-def ends here *) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-helpers][rtlblockinstr-helpers]] *) +(*| +Helper Functions +================ +|*) + Fixpoint successors_instr (i : cf_instr) : list node := match i with | RBcall sig ros args res s => s :: nil @@ -67,7 +96,8 @@ Fixpoint successors_instr (i : cf_instr) : list node := | RBjumptable arg tbl => tbl | RBreturn optarg => nil | RBgoto n => n :: nil - | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil) + | RBpred_cf p c1 c2 => + concat (successors_instr c1 :: successors_instr c2 :: nil) end. Definition max_reg_instr (m: positive) (i: instr) := @@ -136,7 +166,8 @@ Lemma eval_predf_pr_equiv : eval_predf ps p = eval_predf ps' p. Proof. induction p; simplify; auto; - try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; 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. Qed. @@ -146,17 +177,30 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) | _, _ => Regmap.init Vundef end. -(* rtlblockinstr-helpers ends here *) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-state][rtlblockinstr-instr-state]] *) +(*| +Instruction State +----------------- + +Definition of the instruction state, which contains the following: + +:is_rs: This is the current state of the registers. +:is_ps: This is the current state of the predicate registers, which is in a + separate namespace and area compared to the standard registers in [is_rs]. +:is_mem: The current state of the memory. +|*) + Record instr_state := mk_instr_state { is_rs: regset; is_ps: predset; is_mem: mem; }. -(* rtlblockinstr-instr-state ends here *) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-type-def][rtlblockinstr-type-def]] *) +(*| +Top-Level Type Definitions +========================== +|*) + Section DEFINITION. Context {bblock_body: Type}. @@ -193,11 +237,17 @@ Section DEFINITION. (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 *) + (pr: predset), (**r predicate state of the calling + function *) stackframe. -(* rtlblockinstr-type-def ends here *) -(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *) +(*| +State Definition +---------------- + +Definition of the ``state`` type, which is used by the ``step`` functions. +|*) + Variant state : Type := | State: forall (stack: list stackframe) (**r call stack *) @@ -219,13 +269,14 @@ Section DEFINITION. (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. -(* rtlblockinstr-state ends here *) -(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *) End DEFINITION. -(* rtlblockinstr-state ends here *) -(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-semantics][rtlblockinstr-semantics]] *) +(*| +Semantics +========= +|*) + Section RELSEM. Context {bblock_body : Type}. @@ -245,7 +296,8 @@ Section RELSEM. end end. - Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := + Inductive eval_pred: + option pred_op -> instr_state -> instr_state -> instr_state -> Prop := | eval_pred_true: forall i i' p, eval_predf (is_ps i) p = true -> @@ -256,9 +308,7 @@ Section RELSEM. eval_pred (Some p) i i' i | eval_pred_none: forall i i', eval_pred None i i' i. -(* rtlblockinstr-semantics ends here *) -(* [[file:../../docs/scheduler-languages.org::#step_instr][rtlblockinstr-step_instr]] *) Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop := | exec_RBnop: forall sp ist, @@ -266,28 +316,33 @@ Section RELSEM. | 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 -> + 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 + 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 + 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, 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 -> - step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist. -(* rtlblockinstr-step_instr ends here *) + eval_pred p' (mk_instr_state rs pr m) + (mk_instr_state rs (pr#p <- b) m) ist -> + step_instr sp (mk_instr_state rs pr m) + (RBsetpred p' c args p) ist. -(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-step_cf_instr]] *) Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: forall s f sp rs m res fd ros sig args pc pc' pr, @@ -300,7 +355,8 @@ Section RELSEM. 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 rs pr m) (RBtailcall sig ros args) + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) + (RBtailcall sig ros args) 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, @@ -327,13 +383,13 @@ Section RELSEM. E0 (Returnstate s (regmap_optget or Vundef rs) m') | exec_RBgoto: forall s f sp pc rs pr m pc', - step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m) + step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 + (State s f sp pc' rs pr m) | exec_RBpred_cf: forall s f sp pc rs pr m cf1 cf2 st' p t, - step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> - step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. -(* rtlblockinstr-step_cf_instr ends here *) + step_cf_instr (State s f sp pc rs pr m) + (if eval_predf pr p then cf1 else cf2) t st' -> + step_cf_instr (State s f sp pc rs pr m) + (RBpred_cf p cf1 cf2) t st'. -(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-end_RELSEM]] *) End RELSEM. -(* rtlblockinstr-end_RELSEM ends here *) -- cgit