From 4d7236541250808487820beec0b3f79ac2a901dc Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 4 Aug 2021 19:59:21 +0100 Subject: Correct lookup for called funcs, simplify tr_module --- src/hls/HTLgen.v | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index bacee9c..2e4cf48 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -488,7 +488,13 @@ Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) := Definition map_externctrl_params := xmap_externctrl_params 0. -Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: node * instruction) : mon unit := +Definition rtl_find_func (ge : RTL.genv) (symb : AST.ident) := + match Globalenvs.Genv.find_symbol ge symb with + | None => None + | Some b => Globalenvs.Genv.find_funct_ptr ge b + end. + +Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => match i with @@ -516,7 +522,7 @@ Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") | Icall sig (inr fn) args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned - then match funmap ! fn with + then match rtl_find_func ge fn with | Some (AST.Internal _) => do params <- map_externctrl_params fn args; @@ -526,6 +532,7 @@ Definition transf_instr (funmap : PTree.t RTL.fundef) (fin rtrn stack: reg) (ni: do finish_reg <- map_externctrl fn ctrl_finish; do reset_reg <- map_externctrl fn ctrl_reset; do return_reg <- map_externctrl fn ctrl_return; + do _ <- map_externctrl fn ctrl_clk; let fork_instr := fork reset_reg params in let join_instr := join return_reg reset_reg dst in @@ -568,16 +575,18 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz declare_reg (Some Vinput) r 32) params. + +Definition transf_module (ge : RTL.genv) (main : ident) (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then + do _ <- declare_params (RTL.fn_params f); do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do _ <- collectlist (transf_instr funmap fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); - do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; - do clk <- map_externctrl main ctrl_clk; + do clk <- create_reg (Some Vinput) 1; + do _ <- collectlist (transf_instr ge fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with @@ -614,10 +623,17 @@ Definition max_state (f: function) : state := (st_datapath (init_state st)) (st_controllogic (init_state st)). -Definition prog_funmap (prog : RTL.program) : (PTree.t ) := +Definition prog_funmap (prog : RTL.program) : (PTree.t RTL.fundef) := + AssocMap_Properties.of_list ( + Option.map_option (fun '(ident, def) => match def with + | AST.Gfun f => Some (ident, f) + | _ => None + end) + (AST.prog_defs prog) + ). Definition transl_module (prog : RTL.program) (f : function) : Errors.res HTL.module := - run_mon (max_state f) (transf_module f). + run_mon (max_state f) (transf_module (Globalenvs.Genv.globalenv prog) (AST.prog_main prog) f). Definition transl_fundef prog := transf_partial_fundef (transl_module prog). -- cgit