Move HTL renaming pass to own file

5 files changed, 249 insertions, 242 deletions

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 <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
 
-Definition max_pc_map {A: Type} (m : Maps.PTree.t A) :=
-  PTree.fold (fun m pc i => 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.