From 6cb38f39f5609651691419c6a299b09695a4623c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 16:06:25 +0100 Subject: Continue on Partitioning algorithm --- src/hls/RTLBlock.v | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'src/hls/RTLBlock.v') diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 7169d4a..2aaa010 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -35,13 +35,13 @@ Inductive instruction : Type := Definition bblock_body : Type := list instruction. Inductive control_flow_inst : Type := -| RBcall : signature -> ident -> list reg -> reg -> node -> control_flow_inst -| RBtailcall : signature -> ident -> list reg -> control_flow_inst +| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst +| RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst | RBbuiltin : external_function -> list (builtin_arg reg) -> builtin_res reg -> node -> control_flow_inst | RBcond : condition -> list reg -> node -> node -> control_flow_inst | RBjumptable : reg -> list node -> control_flow_inst -| RBredurn : option reg -> control_flow_inst. +| RBreturn : option reg -> control_flow_inst. Record bblock : Type := mk_bblock { bb_body: bblock_body; @@ -67,3 +67,13 @@ Definition funsig (fd: fundef) := | Internal f => fn_sig f | External ef => ef_sig ef end. + +Definition successors_instr (i : control_flow_inst) : list node := + match i with + | RBcall sig ros args res s => s :: nil + | RBtailcall sig ros args => nil + | RBbuiltin ef args res s => s :: nil + | RBcond cond args ifso ifnot => ifso :: ifnot :: nil + | RBjumptable arg tbl => tbl + | RBreturn optarg => nil + end. -- cgit