From 1c8e0373d735ac88740f96c5da1d929ce3f7b688 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sat, 5 Jun 2021 23:17:33 +0100 Subject: Move HTL renaming pass to own file --- src/hls/HTLgen.v | 240 ------------------------------------------------------- 1 file changed, 240 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 365d981..5babea0 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -563,35 +563,6 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz Pos.max m pc) m 1%positive. - -Lemma max_pc_map_sound: - forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). -Proof. - intros until i. unfold max_pc_function. - apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). - (* extensionality *) - intros. apply H0. rewrite H; auto. - (* base case *) - rewrite PTree.gempty. congruence. - (* inductive case *) - intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. xomega. - apply Ple_trans with a. auto. xomega. -Qed. - -Lemma max_pc_wf : - forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - @map_well_formed T m. -Proof. - unfold map_well_formed. intros. - exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. - apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. - unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. - simplify. transitivity (Z.pos (max_pc_map m)); eauto. -Qed. - Definition transf_module (main : ident) (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; @@ -660,217 +631,6 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -Record renumber_state: Type := - mk_renumber_state { - renumber_freshreg : reg; - renumber_regmap : PTree.t reg; - }. - -Module RenumberState <: State. - Definition st := renumber_state. - - Definition st_prop (st1 st2 : st) := True. - Hint Unfold st_prop : htl_renumber. - - Lemma st_refl : forall (s : st), st_prop s s. - Proof. constructor. Qed. - - Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. - Proof. constructor. Qed. -End RenumberState. - -Module RenumberMonad := Statemonad(RenumberState). -Module RenumberMonadExtra := Monad.MonadExtra(RenumberMonad). - -Section RENUMBER. - Import RenumberMonad. - Import RenumberState. - Import RenumberMonadExtra. - Import MonadNotation. - - Definition map_reg (r: reg) : mon reg := - fun st => OK - (renumber_freshreg st) - (mk_renumber_state (Pos.succ (renumber_freshreg st)) - (PTree.set r (renumber_freshreg st) (renumber_regmap st))) - ltac:(auto with htl_renumber). - - Definition clear_regmap : mon unit := - fun st => OK - tt - (mk_renumber_state (renumber_freshreg st) - (PTree.empty reg)) - ltac:(auto with htl_renumber). - - Definition renumber_reg (r : reg) : mon reg := - do st <- get; - match PTree.get r (renumber_regmap st) with - | Some reg' => ret reg' - | None => map_reg r - end. - - Fixpoint renumber_expr (expr : Verilog.expr) := - match expr with - | Vlit val => ret (Vlit val) - | Vvar reg => - do reg' <- renumber_reg reg; - ret (Vvar reg') - | Vvari reg e => - do reg' <- renumber_reg reg; - do e' <- renumber_expr e; - ret (Vvari reg' e') - | Vinputvar reg => - do reg' <- renumber_reg reg; - ret (Vvar reg') - | Vbinop op e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - ret (Vbinop op e1' e2') - | Vunop op e => - do e' <- renumber_expr e; - ret (Vunop op e') - | Vternary e1 e2 e3 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - do e3' <- renumber_expr e3; - ret (Vternary e1' e2' e3') - | Vrange r e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - do r' <- renumber_reg r; - ret (Vrange r e1' e2') - end. - - Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := - match stmnt with - | Vskip => ret Vskip - | Vseq s1 s2 => - do s1' <- renumber_stmnt s1; - do s2' <- renumber_stmnt s2; - ret (Vseq s1' s2') - | Vcond e s1 s2 => - do e' <- renumber_expr e; - do s1' <- renumber_stmnt s1; - do s2' <- renumber_stmnt s2; - ret (Vcond e' s1' s2') - | Vcase e cs def => - do e' <- renumber_expr e; - do cs' <- sequence (map - (fun (c : (Verilog.expr * Verilog.stmnt)) => - let (c_expr, c_stmnt) := c in - do expr' <- renumber_expr c_expr; - do stmnt' <- renumber_stmnt c_stmnt; - ret (expr', stmnt')) cs); - do def' <- match def with - | None => ret None - | Some d => do def' <- renumber_stmnt d; ret (Some def') - end; - ret (Vcase e' cs' def') - | Vblock e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - ret (Vblock e1' e2') - | Vnonblock e1 e2 => - do e1' <- renumber_expr e1; - do e2' <- renumber_expr e2; - ret (Vnonblock e1' e2') - end. - - Fixpoint xrenumber_reg_assocmap {A} (regmap : list (reg * A)) : mon (list (reg * A)) := - match regmap with - | nil => ret nil - | (r, v) :: l => - do r' <- renumber_reg r; - do l' <- xrenumber_reg_assocmap l; - ret ((r', v) :: l') - end. - - Definition renumber_reg_assocmap {A} (regmap : AssocMap.t A) : mon (AssocMap.t A) := - do l <- xrenumber_reg_assocmap (AssocMap.elements regmap); - ret (AssocMap_Properties.of_list l). - - Definition renumber_module (m : HTL.module) : mon HTL.module := - do mod_start' <- renumber_reg (HTL.mod_start m); - do mod_reset' <- renumber_reg (HTL.mod_reset m); - do mod_clk' <- renumber_reg (HTL.mod_clk m); - do mod_finish' <- renumber_reg (HTL.mod_finish m); - do mod_return' <- renumber_reg (HTL.mod_return m); - do mod_st' <- renumber_reg (HTL.mod_st m); - do mod_stk' <- renumber_reg (HTL.mod_stk m); - do mod_params' <- traverselist renumber_reg (HTL.mod_params m); - do mod_controllogic' <- traverse_ptree1 renumber_stmnt (HTL.mod_controllogic m); - do mod_datapath' <- traverse_ptree1 renumber_stmnt (HTL.mod_datapath m); - - do mod_scldecls' <- renumber_reg_assocmap (HTL.mod_scldecls m); - do mod_arrdecls' <- renumber_reg_assocmap (HTL.mod_arrdecls m); - do mod_externctrl' <- renumber_reg_assocmap (HTL.mod_externctrl m); - - do _ <- clear_regmap; - - match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, - zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with - | left LEDATA, left LECTRL => - ret (HTL.mkmodule - mod_params' - mod_datapath' - mod_controllogic' - (HTL.mod_entrypoint m) - mod_st' - mod_stk' - (HTL.mod_stk_len m) - mod_finish' - mod_return' - mod_start' - mod_reset' - mod_clk' - mod_scldecls' - mod_arrdecls' - mod_externctrl' - (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) - | _, _ => error (Errors.msg "More than 2^32 states.") - end. - - Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := - match fundef with - | Internal m => do renumbered <- renumber_module m; ret (Internal renumbered) - | _ => ret fundef - end. - - Section TRANSF_PROGRAM_STATEFUL. - Import RenumberMonad. - Import RenumberState. - Import RenumberMonadExtra. - Import MonadNotation. - - Variables A B V : Type. - Variable transf_fun: ident -> A -> RenumberMonad.mon B. - - Fixpoint transf_globdefs (l: list (ident * globdef A V)) : RenumberMonad.mon (list (ident * globdef B V)) := - match l with - | nil => RenumberMonad.ret nil - | (id, Gfun f) :: l' => - do tf <- transf_fun id f; - do tl' <- transf_globdefs l'; - RenumberMonad.ret ((id, Gfun tf) :: tl') - | (id, Gvar v) :: l' => - do tl' <- transf_globdefs l'; - RenumberMonad.ret ((id, Gvar v) :: tl') - end. - - Definition transform_stateful_program (init_state : RenumberState.st) (p: AST.program A V) : Errors.res (AST.program B V) := - RenumberMonad.run_mon init_state ( - do gl' <- transf_globdefs p.(prog_defs); - RenumberMonad.ret (mkprogram gl' p.(prog_public) p.(prog_main))). - - End TRANSF_PROGRAM_STATEFUL. - - Definition renumber_program (p : HTL.program) : Errors.res HTL.program := - transform_stateful_program _ _ _ - (fun _ f => renumber_fundef f) - (mk_renumber_state 1%positive (PTree.empty reg)) - p. -End RENUMBER. - Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with -- cgit