diff options
-rw-r--r-- | src/hls/Gible.v (renamed from src/hls/RTLBlockInstr.v) | 461 | ||||
-rw-r--r-- | src/hls/GiblePar.v | 75 | ||||
-rw-r--r-- | src/hls/GibleSeq.v | 70 | ||||
-rw-r--r-- | src/hls/IfConversion.v | 2 | ||||
-rw-r--r-- | src/hls/RTLBlock.v | 137 | ||||
-rw-r--r-- | src/hls/RTLBlockgen.v | 4 | ||||
-rw-r--r-- | src/hls/RTLPar.v | 119 |
7 files changed, 431 insertions, 437 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/Gible.v index 2d48650..22d25f8 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/Gible.v @@ -35,6 +35,7 @@ Require Import compcert.common.Globalenvs. Require Import compcert.common.Memory. Require Import compcert.common.Values. Require Import compcert.lib.Integers. +Require Import compcert.common.Smallstep. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. @@ -56,17 +57,6 @@ 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. - (*| .. index:: triple: definition; RTLBlockInstr; control-flow instruction @@ -89,6 +79,18 @@ Inductive cf_instr : Type := | RBgoto : node -> cf_instr | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr. +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 +| RBexit : option pred_op -> cf_instr -> instr. + (*| Helper Functions ================ @@ -107,19 +109,6 @@ Fixpoint successors_instr (i : cf_instr) : list node := concat (successors_instr c1 :: successors_instr c2 :: nil) end. -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) - | RBload p chunk addr args dst => - fold_left Pos.max args (Pos.max dst m) - | RBstore p chunk addr args src => - fold_left Pos.max args (Pos.max src m) - | RBsetpred p' c args p => - 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 => @@ -141,6 +130,20 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2) end. +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) + | RBload p chunk addr args dst => + fold_left Pos.max args (Pos.max dst m) + | RBstore p chunk addr args src => + fold_left Pos.max args (Pos.max src m) + | RBsetpred p' c args p => + fold_left Pos.max args m + | RBexit _ c => max_reg_cfi m c + end. + Definition regset := Regmap.t val. Definition predset := PMap.t bool. @@ -203,21 +206,119 @@ Record instr_state := mk_instr_state { is_mem: mem; }. +Variant istate : Type := + | Iexec : instr_state -> istate + | Iterm : instr_state -> cf_instr -> istate. + +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 -> + eval_pred (Some p) i i' i' +| eval_pred_false: + 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'. + +Section RELABSTR. + + Context {A B : Type} (ge : Genv.t A B). + +(*| +.. index:: + triple: semantics; RTLBlockInstr; instruction + +Step Instruction +============================= +|*) + +Variant step_instr: val -> istate -> instr -> istate -> Prop := + | exec_RBnop: + 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 (Iexec (mk_instr_state rs pr m)) (RBop p op args res) (Iexec 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 (Iexec (mk_instr_state rs pr m)) + (RBload p chunk addr args dst) (Iexec 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 (Iexec (mk_instr_state rs pr m)) + (RBstore p chunk addr args src) (Iexec 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 (Iexec (mk_instr_state rs pr m)) + (RBsetpred p' c args p) (Iexec ist) + | exec_RBexit_Some: + forall p c sp b i, + eval_predf (is_ps i) p = b -> + step_instr sp (Iexec i) (RBexit (Some p) c) (if b then Iterm i c else Iexec i) + | exec_RBexit_None: + forall c sp i, + step_instr sp (Iexec i) (RBexit None c) (Iterm i c) +. + +End RELABSTR. + +(*| +A big-step semantics describing the execution of a list of instructions. This +uses a higher-order function ``step_i``, so that this ``Inductive`` can be +nested to describe the execution of nested lists. +|*) + +Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop): + val -> istate -> list A -> istate -> Prop := +| exec_RBcons: + forall state i state' state'' instrs sp, + step_i sp state i state' -> + step_list step_i sp state' instrs state'' -> + step_list step_i sp state (i :: instrs) state'' +| exec_RBnil: + forall state sp, + step_list step_i sp state nil state. + (*| Top-Level Type Definitions ========================== |*) -Section DEFINITION. +Module Type BlockType. + + Parameter t: Type. + + Section STEP. + Context {A B : Type}. + Parameter step: Genv.t A B -> val -> istate -> t -> istate -> Prop. + End STEP. - Context {bblock_body: Type}. + Parameter max_reg : positive -> node -> t -> positive. - Record bblock : Type := mk_bblock { - bb_body: bblock_body; - bb_exit: cf_instr - }. + Parameter length : t -> nat. - Definition code: Type := PTree.t bblock. +End BlockType. + +Module Gible(B : BlockType). + + Definition code: Type := PTree.t B.t. Record function: Type := mkfunction { fn_sig: signature; @@ -279,8 +380,6 @@ though is that executing basic blocks uses big-step semantics. (m: mem), (**r memory state *) state. -End DEFINITION. - (*| Old version of state ~~~~~~~~~~~~~~~~~~~~ @@ -324,167 +423,173 @@ Semantics ========= |*) -Section RELSEM. + Section RELSEM. - Context {bblock_body : Type}. + Definition genv := Genv.t fundef unit. - Definition genv := Genv.t (@fundef bblock_body) unit. + Context (ge: genv). - Context (ge: genv). - - Definition find_function - (ros: reg + ident) (rs: regset) : option fundef := - 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 - end. - - 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 -> - eval_pred (Some p) i i' i' - | eval_pred_false: - 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'. + Definition find_function + (ros: reg + ident) (rs: regset) : option fundef := + 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 + end. (*| .. index:: - triple: semantics; RTLBlockInstr; instruction + triple: semantics; RTLBlockInstr; control-flow instruction -Step Instruction +Step Control-Flow Instruction ============================= + +These control-flow instruction semantics are essentially the same as in RTL, +with the addition of a recursive conditional instruction, which is used to +support if-conversion. |*) - Variant step_instr: val -> instr_state -> instr -> instr_state -> Prop := - | exec_RBnop: - 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 - | 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 - | 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 - | 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. + 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, + find_function ros rs = Some fd -> + funsig fd = sig -> + step_cf_instr + (State s f sp pc rs pr m) (RBcall sig ros args res pc') + 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, + 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) + 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, + 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 rs pr m) (RBbuiltin ef args res pc') + t (State s f sp pc' (regmap_setres res vres rs) pr m') + | exec_RBcond: + 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 rs pr m) + (RBcond cond args ifso ifnot) + E0 (State s f sp pc' rs pr m) + | exec_RBjumptable: + 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 rs pr m) + (RBjumptable arg tbl) + E0 (State s f sp pc' rs pr m) + | exec_RBreturn: + 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 rs pr m) + (RBreturn or) + 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) + | 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'. (*| -A big-step semantics describing the execution of a list of instructions. This -uses a higher-order function ``step_i``, so that this ``Inductive`` can be -nested to describe the execution of nested lists. +Top-level step +-------------- + +The step function itself then uses this big step of the list of instructions to +then show a transition from basic block to basic block. The one particular +aspect of this is that the basic block is also part of the state, which has to +be correctly set during the execution of the function. Function calls and +function returns then also need to set the basic block properly. This means +that the basic block of the returning function also needs to be stored in the +stackframe, as that is the only assumption one can make when returning from a +function. |*) - Inductive step_list {A} (step_i: val -> instr_state -> A -> instr_state -> Prop): - val -> instr_state -> list A -> instr_state -> Prop := - | exec_RBcons: - forall state i state' state'' instrs sp, - step_i sp state i state' -> - step_list step_i sp state' instrs state'' -> - step_list step_i sp state (i :: instrs) state'' - | exec_RBnil: - forall state sp, - step_list step_i sp state nil state. + Variant step: state -> trace -> state -> Prop := + | exec_bblock: + forall s f sp pc rs rs' m m' bb pr pr' t state cf, + f.(fn_code) ! pc = Some bb -> + B.step ge sp (Iexec (mk_instr_state rs pr m)) bb (Iterm (mk_instr_state rs' pr' m') cf) -> + step_cf_instr (State s f sp pc rs' pr' m') cf t state -> + step (State s f sp pc rs pr m) t state + | exec_function_internal: + forall s f args m m' stk, + Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> + step (Callstate s (Internal f) args m) + E0 (State s f + (Vptr stk Ptrofs.zero) + f.(fn_entrypoint) + (init_regs args f.(fn_params)) + (PMap.init false) + m') + | exec_function_external: + forall s ef args res t m m', + external_call ef ge args m t res m' -> + step (Callstate s (External ef) args m) + t (Returnstate s res m') + | 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). + + End RELSEM. + + Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = signature_main -> + initial_state p (Callstate nil f nil m0). + + Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate nil (Vint r) m) r. (*| -.. index:: - triple: semantics; RTLBlockInstr; control-flow instruction - -Step Control-Flow Instruction -============================= +Semantics +========= -These control-flow instruction semantics are essentially the same as in RTL, -with the addition of a recursive conditional instruction, which is used to -support if-conversion. +We first describe the semantics by assuming a global program environment with +type ~genv~ which was declared earlier. |*) - 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, - find_function ros rs = Some fd -> - funsig fd = sig -> - step_cf_instr - (State s f sp pc rs pr m) (RBcall sig ros args res pc') - 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, - 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) - 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, - 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 rs pr m) (RBbuiltin ef args res pc') - t (State s f sp pc' (regmap_setres res vres rs) pr m') - | exec_RBcond: - 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 rs pr m) - (RBcond cond args ifso ifnot) - E0 (State s f sp pc' rs pr m) - | exec_RBjumptable: - 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 rs pr m) - (RBjumptable arg tbl) - E0 (State s f sp pc' rs pr m) - | exec_RBreturn: - 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 rs pr m) - (RBreturn or) - 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) - | 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'. - -End RELSEM. + Definition semantics (p: program) := + Semantics step (initial_state p) final_state (Genv.globalenv p). + + Definition max_reg_function (f: function) := + Pos.max + (PTree.fold B.max_reg f.(fn_code) 1%positive) + (fold_left Pos.max f.(fn_params) 1%positive). + + Definition max_pc_function (f: function) : positive := + PTree.fold + (fun m pc i => + (Pos.max m + (pc + match Z.of_nat (B.length i) + with Z.pos p => p | _ => 1 end))%positive) + f.(fn_code) 1%positive. + +End Gible. diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v new file mode 100644 index 0000000..8eb06ae --- /dev/null +++ b/src/hls/GiblePar.v @@ -0,0 +1,75 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Events. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Values. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. +Require Import vericert.hls.Gible. + +(*| +======== +RTLBlock +======== +|*) + +Module BB <: BlockType. + + Definition t := list (list (list instr)). + + Section RELSEM. + + Context {A B: Type} (ge: Genv.t A B). + + Definition step_instr_list := step_list (step_instr ge). + Definition step_instr_seq := step_list step_instr_list. + Definition step_instr_block := step_list step_instr_seq. + +(*| +Instruction list step +--------------------- + +The ``step_instr_list`` definition describes the execution of a list of +instructions in one big step, inductively traversing the list of instructions +and applying the ``step_instr``. + +This is simply using the high-level function ``step_list``, which is a general +function that can execute lists of things, given their execution rule. +|*) + + Definition step := step_instr_block. + + End RELSEM. + + Definition max_reg (m : positive) (pc : node) (bb : t) := + fold_left + (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) + bb m. + + Definition length : t -> nat := @length (list (list instr)). + +End BB. + +Module GiblePar := Gible(BB). diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v new file mode 100644 index 0000000..321d639 --- /dev/null +++ b/src/hls/GibleSeq.v @@ -0,0 +1,70 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Events. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Values. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. + +Require Import vericert.hls.Gible. + +(*| +======== +RTLBlock +======== +|*) + +Module BB <: BlockType. + + Definition t := list instr. + + Section RELSEM. + + Context {A B: Type} (ge: Genv.t A B). + +(*| +Instruction list step +--------------------- + +The ``step_instr_list`` definition describes the execution of a list of +instructions in one big step, inductively traversing the list of instructions +and applying the ``step_instr``. + +This is simply using the high-level function ``step_list``, which is a general +function that can execute lists of things, given their execution rule. +|*) + + Definition step := step_list (step_instr ge). + + End RELSEM. + + Definition max_reg (m : positive) (n: node) (i : t) : positive := + fold_left max_reg_instr i m. + + Definition length : t -> nat := @length instr. + +End BB. + +Module GibleSeq := Gible(BB). diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 2516109..4e62a68 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -106,7 +106,7 @@ Fixpoint get_loops (b: bourdoncle): list node := end. Definition is_loop (b: list node) (n: node) := - any (fun x => Pos.eqb x n) b. + any (Pos.eqb n) b. Definition is_flat_cfi (n: cf_instr) := match n with diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v deleted file mode 100644 index 19ac4f5..0000000 --- a/src/hls/RTLBlock.v +++ /dev/null @@ -1,137 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -Require Import compcert.backend.Registers. -Require Import compcert.common.AST. -Require Import compcert.common.Events. -Require Import compcert.common.Globalenvs. -Require Import compcert.common.Memory. -Require Import compcert.common.Smallstep. -Require Import compcert.common.Values. -Require Import compcert.lib.Coqlib. -Require Import compcert.lib.Integers. -Require Import compcert.lib.Maps. -Require Import compcert.verilog.Op. - -Require Import vericert.hls.RTLBlockInstr. - -(*| -======== -RTLBlock -======== -|*) - -Definition bb := list instr. - -Definition bblock := @bblock bb. -Definition code := @code bb. -Definition function := @function bb. -Definition fundef := @fundef bb. -Definition program := @program bb. -Definition funsig := @funsig bb. -Definition stackframe := @stackframe bb. -Definition state := @state bb. - -Definition genv := @genv bb. - -(*| -Semantics -========= - -We first describe the semantics by assuming a global program environment with -type ~genv~ which was declared earlier. -|*) - -Section RELSEM. - - Context (ge: genv). - -(*| -Instruction list step ---------------------- - -The ``step_instr_list`` definition describes the execution of a list of -instructions in one big step, inductively traversing the list of instructions -and applying the ``step_instr``. - -This is simply using the high-level function ``step_list``, which is a general -function that can execute lists of things, given their execution rule. -|*) - - Definition step_instr_list := step_list (step_instr ge). - -(*| -Top-level step --------------- - -The step function itself then uses this big step of the list of instructions to -then show a transition from basic block to basic block. The one particular -aspect of this is that the basic block is also part of the state, which has to -be correctly set during the execution of the function. Function calls and -function returns then also need to set the basic block properly. This means -that the basic block of the returning function also needs to be stored in the -stackframe, as that is the only assumption one can make when returning from a -function. -|*) - - Variant step: state -> trace -> state -> Prop := - | exec_bblock: - forall s f sp pc rs rs' m m' bb pr pr' t state, - f.(fn_code) ! pc = Some bb -> - step_instr_list 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 state -> - step (State s f sp pc rs pr m) t state - | exec_function_internal: - forall s f args m m' stk bb cf, - Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) -> - step (Callstate s (Internal f) args m) - E0 (State s f - (Vptr stk Ptrofs.zero) - f.(fn_entrypoint) - (init_regs args f.(fn_params)) - (PMap.init false) - m') - | exec_function_external: - forall s ef args res t m m', - external_call ef ge args m t res m' -> - step (Callstate s (External ef) args m) - t (Returnstate s res m') - | 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). - -End RELSEM. - -Inductive initial_state (p: program): state -> Prop := -| initial_state_intro: forall b f m0, - let ge := Genv.globalenv p in - Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some b -> - Genv.find_funct_ptr ge b = Some f -> - funsig f = signature_main -> - initial_state p (Callstate nil f nil m0). - -Inductive final_state: state -> int -> Prop := -| final_state_intro: forall r m, - final_state (Returnstate nil (Vint r) m) r. - -Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index cb18147..8f81e21 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -31,8 +31,8 @@ Require Import compcert.lib.Floats. Require Import vericert.common.DecEq. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlockInstr. -Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. #[local] Open Scope positive. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v deleted file mode 100644 index e6aa002..0000000 --- a/src/hls/RTLPar.v +++ /dev/null @@ -1,119 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -Require Import compcert.backend.Registers. -Require Import compcert.common.AST. -Require Import compcert.common.Events. -Require Import compcert.common.Globalenvs. -Require Import compcert.common.Memory. -Require Import compcert.common.Smallstep. -Require Import compcert.common.Values. -Require Import compcert.lib.Coqlib. -Require Import compcert.lib.Integers. -Require Import compcert.lib.Maps. -Require Import compcert.verilog.Op. - -Require Import vericert.hls.RTLBlockInstr. - -Definition bb := list (list (list instr)). - -Definition bblock := @bblock bb. -Definition code := @code bb. -Definition function := @function bb. -Definition fundef := @fundef bb. -Definition program := @program bb. -Definition funsig := @funsig bb. -Definition stackframe := @stackframe bb. -Definition state := @state bb. -Definition genv := @genv bb. - -Section RELSEM. - - Context (ge: genv). - - Definition step_instr_list := step_list (step_instr ge). - Definition step_instr_seq := step_list step_instr_list. - Definition step_instr_block := step_list step_instr_seq. - - Variant step: state -> trace -> state -> Prop := - | exec_bblock: - forall s f sp pc rs rs' m m' bb pr pr' state t, - 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 state -> - step (State s f sp pc rs pr m) t state - | exec_function_internal: - forall s f args m m' stk bb cf, - Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) -> - step (Callstate s (Internal f) args m) - E0 (State s f - (Vptr stk Ptrofs.zero) - f.(fn_entrypoint) - (init_regs args f.(fn_params)) - (PMap.init false) - m') - | exec_function_external: - forall s ef args res t m m', - external_call ef ge args m t res m' -> - step (Callstate s (External ef) args m) - t (Returnstate s res m') - | 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). - -End RELSEM. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f m0, - let ge := Genv.globalenv p in - Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some b -> - Genv.find_funct_ptr ge b = Some f -> - funsig f = signature_main -> - initial_state p (Callstate nil f nil m0). - -Inductive final_state: state -> int -> Prop := - | final_state_intro: forall r m, - final_state (Returnstate nil (Vint r) m) r. - -Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). - -Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) := - let max_body := - fold_left - (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) - bb.(bb_body) m - in - max_reg_cfi max_body bb.(bb_exit). - -Definition max_reg_function (f: function) := - Pos.max - (PTree.fold max_reg_bblock f.(fn_code) 1%positive) - (fold_left Pos.max f.(fn_params) 1%positive). - -Definition max_pc_function (f: function) : positive := - PTree.fold - (fun m pc i => - (Pos.max m - (pc + match Zlength i.(bb_body) - with Z.pos p => p | _ => 1 end))%positive) - f.(fn_code) 1%positive. |