Complete translation from simple RTL to Verilog

1 files changed, 162 insertions, 101 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 605448b..c2614ec 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -20,7 +20,7 @@ From Coq Require Import FSets.FMapPositive.
 
 From coqup Require Import Verilog Coquplib.
 
-From compcert Require Errors Op AST Integers.
+From compcert Require Errors Op AST Integers Maps.
 From compcert Require Import RTL.
 
 Definition node : Type := positive.
@@ -28,90 +28,95 @@ Definition reg : Type := positive.
 Definition ident : Type := positive.
 
 Inductive statetrans : Type :=
-  | StateGoto (p : node)
-  | StateCond (c : expr) (t f : node).
+| StateGoto (p : node)
+| StateCond (c : expr) (t f : node).
 
 Record state: Type := mkstate {
-  st_variables: PositiveMap.t (nat * expr);
+  st_freshreg : reg;
+  st_freshstate : node;
   st_stm : PositiveMap.t stmnt;
   st_statetrans : PositiveMap.t statetrans;
+  st_decl : list (reg * nat);
+  st_fin : option reg;
+  st_ret : option reg;
 }.
 
+(** Map from initial register allocations to new allocations. *)
+Definition mapping: Type := PositiveMap.t reg.
+
 Definition init_state : state :=
-  mkstate (PositiveMap.empty (nat * expr)) (PositiveMap.empty stmnt) (PositiveMap.empty statetrans).
+  mkstate 1%positive
+          1%positive
+          (PositiveMap.empty stmnt)
+          (PositiveMap.empty statetrans)
+          nil
+          None
+          None.
 
-Inductive res (A: Type) (S: Type): Type :=
-  | Error: Errors.errmsg -> res A S
-  | OK: A -> S -> res A S.
+Inductive res (A: Type) (s: state): Type :=
+| Error : Errors.errmsg -> res A s
+| OK : A -> forall (_ : state), res A s.
 
-Arguments OK [A S].
-Arguments Error [A S].
+Arguments OK [A s].
+Arguments Error [A s].
 
-Definition mon (A: Type) : Type := res A state.
+Definition mon (A: Type) : Type := forall (s: state), res A s.
 
-Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s.
+Definition ret {A: Type} (x: A) : mon A :=
+  fun (s : state) => OK x s.
 
 Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
-    match f with
+  fun (s : state) =>
+    match f s with
     | Error msg => Error msg
-    | OK a s => g a
+    | OK a s' =>
+      match g a s' with
+      | Error msg => Error msg
+      | OK b s'' => OK b s''
+      end
     end.
 
 Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
   bind f (fun xy => g (fst xy) (snd xy)).
 
-Definition bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B :=
-  match f with
-  | Error msg => Error msg
-  | OK a s => g a s
-  end.
-
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X ident, A at level 100, B at level 200).
-Notation "'do' ( X , Y ) <- A ; B" := (bindS A (fun X Y => B))
-   (at level 200, X ident, Y ident, A at level 100, B at level 200).
+(at level 200, X ident, A at level 100, B at level 200).
+Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
+(at level 200, X ident, Y ident, A at level 100, B at level 200).
 
 Definition handle_error {A: Type} (f g: mon A) : mon A :=
-  match f with
-  | OK a s' => OK a s'
-  | Error _ => g
-  end.
-
-Module PTree.
-  Export Maps.PTree.
-
-  Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B)
-           (m : t A) (s : state) (i : positive)
-           {struct m} : mon (t B) :=
-    match m with
-    | Leaf => OK Leaf s
-    | Node l o r =>
-      let newo :=
-          match o with
-          | None => OK None s
-          | Some x =>
-            match f (prev i) x s with
-            | Error err => Error err
-            | OK val s' => OK (Some val) s'
-            end
-          end in
-      match newo with
-      | OK no s =>
-        do (nl, s') <- xtraverse f l s (xO i);
-        do (nr, s'') <- xtraverse f r s' (xI i);
-        OK (Node nl no nr) s''
-      | Error msg => Error msg
-      end
+  fun (s : state) =>
+    match f s with
+    | OK a s' => OK a s'
+    | Error _ => g s
     end.
 
-  Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m :=
-    xtraverse f m init_state xH.
+Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: state) => Error err.
+
+Definition get : mon state := fun s => OK s s.
+
+Definition set (s: state) : mon unit := fun _ => OK tt s.
 
-  Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f).
+Definition run_mon {A: Type} (s: state) (m: mon A): Errors.res A :=
+    match m s with
+    | OK a s' => Errors.OK a
+    | Error err => Errors.Error err
+    end.
+
+Definition map_state (f: state -> state): mon state :=
+  fun s => let s' := f s in OK s' s'.
 
-End PTree.
+Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
+  match l with
+  | nil => ret nil
+  | x::xs =>
+    do r <- f x;
+    do rs <- traverselist f xs;
+    ret (r::rs)
+  end.
 
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
 Definition bop (op : binop) (r1 r2 : reg) : option expr :=
   Some (Vbinop op (Vvar r1) (Vvar r2)).
@@ -176,37 +181,77 @@ Definition translate_instr (op : Op.operation) (args : list reg) : option expr :
   | _, _ => None
   end.
 
-Definition add_instr (n : node) (n' : node) (s : state) (st : stmnt) : mon node :=
-  OK n' (mkstate s.(st_variables)
-                 (PositiveMap.add n st s.(st_stm))
-                 (PositiveMap.add n (StateGoto n') s.(st_statetrans))).
-
-Definition option_err {A : Type} (str : string) (v : option A) (s : state) : mon A :=
-  match v with
-  | Some v' => OK v' s
-  | _ => Error (Errors.msg str)
-  end.
-
-Definition transf_instr (n : node) (i : instruction) (s : state) : mon node :=
-  match i with
-  | Inop n' =>
-    add_instr n n' s Vskip
-  | Iop op args dst n' =>
-    match translate_instr op args with
-    | Some instr => add_instr n n' s (nonblock dst instr)
-    | _ => Error (Errors.msg "Instruction is not implemented.")
-    end
-  | Iload _ _ _ _ _ => Error (Errors.msg "Loads are not implemented.")
-  | Istore _ _ _ _ _ => Error (Errors.msg "Stores are not implemented.")
-  | Icall _ _ _ _ _ => Error (Errors.msg "Calls are not implemented.")
-  | Itailcall _ _ _ => Error (Errors.msg "Tailcalls are not implemented.")
-  | Ibuiltin _ _ _ _ => Error (Errors.msg "Builtin functions not implemented.")
-  | Icond cond args n1 n2 => Error (Errors.msg "Condition not implemented.")
-  | Ijumptable _ _ => Error (Errors.msg "Jumptable not implemented.")
-  | Ireturn r =>
-    match r with
-    | Some x => OK n s
-    | None => OK n s
+Definition add_instr (n : node) (n' : node) (st : stmnt) : mon node :=
+  fun s =>
+    OK n' (mkstate s.(st_freshreg)
+                   (Pos.max (Pos.succ n) s.(st_freshstate))
+                   (PositiveMap.add n st s.(st_stm))
+                   (PositiveMap.add n (StateGoto n') s.(st_statetrans))
+                   s.(st_decl)
+                   s.(st_fin)
+                   s.(st_ret)).
+
+Definition add_reg (r: reg) (s: state) : state :=
+  mkstate (Pos.max (Pos.succ r) s.(st_freshreg))
+          s.(st_freshstate)
+          s.(st_stm)
+          s.(st_statetrans)
+          ((r, 32%nat) :: s.(st_decl))
+          s.(st_fin)
+          s.(st_ret).
+
+Definition add_instr_reg (r: reg) (n: node) (n': node) (st: stmnt) : mon node :=
+  do _ <- map_state (add_reg r);
+  add_instr n n' st.
+
+Definition decl_fresh_reg (sz : nat) : mon reg :=
+  fun s =>
+    let r := s.(st_freshreg) in
+    OK r (mkstate
+         (Pos.succ r)
+         s.(st_freshstate)
+         s.(st_stm)
+         s.(st_statetrans)
+         ((r, sz) :: s.(st_decl))
+         s.(st_fin)
+         s.(st_ret)).
+
+Definition add_fin_ret (f r: reg) : mon unit :=
+  fun s => OK tt (mkstate
+    s.(st_freshreg)
+    s.(st_freshstate)
+    s.(st_stm)
+    s.(st_statetrans)
+    s.(st_decl)
+    (Some f) (Some r)).
+
+Definition transf_instr (ni: node * instruction) : mon node :=
+  match ni with
+    (n, i) =>
+    match i with
+    | Inop n' => add_instr n n' Vskip
+    | Iop op args dst n' =>
+      match translate_instr op args with
+      | Some instr => add_instr_reg dst n n' (block dst instr)
+      | _ => error (Errors.msg "Instruction is not implemented.")
+      end
+    | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.")
+    | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.")
+    | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
+    | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
+    | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
+    | Icond cond args n1 n2 => error (Errors.msg "Condition not implemented.")
+    | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented.")
+    | Ireturn r =>
+      do fin <- decl_fresh_reg 1%nat;
+      do rtrn <- decl_fresh_reg 32%nat;
+      do _ <- add_fin_ret fin rtrn;
+      match r with
+      | Some r' =>
+        add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)) :: block rtrn (Vvar r') :: nil))
+      | None =>
+        add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)) :: nil))
+      end
     end
   end.
 
@@ -225,23 +270,39 @@ Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr *
 Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
   Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)).
 
-Definition make_globals (globals : PositiveMap.t (nat * expr)) : verilog := nil.
+Fixpoint allocate_regs (e : list (reg * nat)) {struct e} : list module_item :=
+  match e with
+  | (r, n)::es => Vdecl r n (Vlit (ZToValue n 0%Z)) :: allocate_regs es
+  | nil => nil
+  end.
 
-Definition make_verilog (s : state) : verilog :=
-  let r := 500%positive in
-  (make_statetrans r s.(st_statetrans)) :: (make_stm r s.(st_stm))
-                                        :: (make_globals s.(st_variables)).
+Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item :=
+  (Valways (Voredge (Vposedge clk) (Vposedge rst))
+    (Vcond (Vbinop Veq (Vvar rst) (Vlit (ZToValue 1%nat 1%Z)))
+      (nonblock st (posToExpr entry))
+      (make_statetrans st s.(st_statetrans))))
+  :: (Valways Valledge (make_stm st s.(st_stm)))
+  :: (allocate_regs s.(st_decl)).
 
 (** To start out with, the assumption is made that there is only one
     function/module in the original code. *)
-Definition transf_module (m: function) : Errors.res verilog :=
-  match PTree.traverse transf_instr m.(fn_code) with
-  | OK _ s => Errors.OK (make_verilog s)
-  | Error err => Errors.Error err
+
+Definition transf_module (f: function) : mon module :=
+  do _ <- traverselist transf_instr (Maps.PTree.elements f.(fn_code));
+  do start <- decl_fresh_reg 1%nat;
+  do rst <- decl_fresh_reg 1%nat;
+  do clk <- decl_fresh_reg 1%nat;
+  do st <- decl_fresh_reg 32%nat;
+  do current_state <- get;
+  let mi := make_module_items f.(fn_entrypoint) clk st rst current_state in
+  match current_state.(st_fin), current_state.(st_ret) with
+  | Some fin, Some rtrn =>
+    ret (mkmodule start rst clk fin rtrn f.(fn_params) mi)
+  | _, _ => error (Errors.msg "Veriloggen: finish and return signals not generated")
   end.
 
 Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
-         {struct flist} : option function :=
+{struct flist} : option function :=
   match flist with
   | (i, AST.Gfun (AST.Internal f)) :: xs =>
     if Pos.eqb i main
@@ -251,8 +312,8 @@ Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef
   | nil => None
   end.
 
-Definition transf_program (d : program) : Errors.res verilog :=
+Definition transf_program (d : program) : Errors.res module :=
   match main_function d.(AST.prog_main) d.(AST.prog_defs) with
-  | Some m => transf_module m
-  | _ => Errors.Error (Errors.msg "Could not find main module")
+  | Some f => run_mon init_state (transf_module f)
+  | _ => Errors.Error (Errors.msg "Veriloggen: could not find main module")
   end.