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/Compiler.v | 3 +- src/common/Maps.v | 18 +++- src/hls/HTL.v | 12 +++ src/hls/HTLgen.v | 240 ----------------------------------------------------- src/hls/Renaming.v | 218 ++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 249 insertions(+), 242 deletions(-) create mode 100644 src/hls/Renaming.v diff --git a/src/Compiler.v b/src/Compiler.v index b5b33e7..38a9d0e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -61,6 +61,7 @@ Require Import compcert.lib.Coqlib. Require vericert.hls.Verilog. Require vericert.hls.Veriloggen. Require vericert.hls.Veriloggenproof. +Require vericert.hls.Renaming. Require vericert.hls.HTLgen. Require vericert.hls.RTLBlock. Require vericert.hls.RTLBlockgen. @@ -191,7 +192,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print (print_HTL 1) - @@@ HTLgen.renumber_program + @@@ Renaming.transf_program @@ print (print_HTL 2) @@@ Veriloggen.transl_program. diff --git a/src/common/Maps.v b/src/common/Maps.v index 21a1d9e..3aa0b33 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -93,6 +93,22 @@ Definition contains (A: Type) (i: positive) (m: t A) : bool := | Some _ => true | None => false end. +End PTree. +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := + PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. -End PTree. +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_map. + 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. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 12b6493..1eb86e1 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -30,6 +30,7 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.ValueInt. Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. +Require Import vericert.common.Maps. Require vericert.hls.Verilog. (** The purpose of the hardware transfer language (HTL) is to create a more @@ -246,3 +247,14 @@ Inductive final_state : state -> Integers.int -> Prop := Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). + +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. 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 diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v new file mode 100644 index 0000000..3efc20f --- /dev/null +++ b/src/hls/Renaming.v @@ -0,0 +1,218 @@ +Require Import compcert.common.AST. + +Require Import vericert.hls.HTL. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.AssocMap. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.common.Maps. + +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). + +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 transf_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. -- cgit