Add RTLBlock intermediate language

23 files changed, 187 insertions, 10 deletions

diff --git a/Makefile b/Makefile
index 2935c7f..e1a93f6 100644
--- a/Makefile
+++ b/Makefile
@@ -9,8 +9,9 @@ endif
 COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \
   MenhirLib cparser
 
-COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \
-               -R src/extraction vericert.extraction -R src/translation vericert.translation \
+COQINCLUDES := -R src/common vericert.common \
+               -R src/extraction vericert.extraction \
+               -R src/hls vericert.hls \
                -R src vericert \
                $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
 
@@ -19,7 +20,7 @@ COQMAKE := $(COQBIN)coq_makefile
 
 COQDOCFLAGS := --no-lib-name -l
 
-VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v)
+VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v)
 
 PREFIX ?= .
 
diff --git a/_CoqProject b/_CoqProject
index e86312b..72a2e4b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,6 @@
 -R src/common vericert.common
 -R src/extraction vericert.extraction
--R src/translation vericert.translation
--R src/verilog vericert.verilog
+-R src/hls vericert.hls
 -R src vericert
 
 -R lib/CompCert/MenhirLib compcert.MenhirLib
diff --git a/default.nix b/default.nix
index a253285..3c8bc92 100644
--- a/default.nix
+++ b/default.nix
@@ -30,7 +30,7 @@ stdenv.mkDerivation {
 
   buildInputs = [ ncoq ocamlPackages.menhir dune
                   ocaml ocamlPackages.findlib bbv
-                  gcc
+                  gcc ocamlPackages.utop
                 ];
 
   enableParallelBuilding = true;
diff --git a/shell.nix b/shell.nix
index 3906659..887f8fb 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,5 +1,7 @@
 with import <nixpkgs> {};
 
 mkShell {
-  buildInputs = (import ./.).buildInputs ++ [ocamlPackages.ocp-indent verilog yosys];
+  buildInputs = (import ./.).buildInputs ++ [ ocamlPackages.ocp-indent verilog yosys
+                                              ocamlPackages.merlin ocamlPackages.utop
+                                            ];
 }
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index b1a885e..e6ee512 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -16,7 +16,11 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From vericert Require Verilog Value Compiler.
+From vericert Require
+     Verilog
+     Value
+     Compiler
+     RTLBlockgen.
 
 From Coq Require DecidableClass.
 
@@ -162,12 +166,15 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false".
 Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
 Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
+Extract Constant RTLBlockgen.partition => "Partition.partition".
+
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
 
 Cd "src/extraction".
 Separate Extraction
          Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls
+         RTLBlockgen.transl_program
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/verilog/Array.v b/src/hls/Array.v
index fe0f6b2..fe0f6b2 100644
--- a/src/verilog/Array.v
+++ b/src/hls/Array.v
diff --git a/src/verilog/AssocMap.v b/src/hls/AssocMap.v
index 8d8788a..8d8788a 100644
--- a/src/verilog/AssocMap.v
+++ b/src/hls/AssocMap.v
diff --git a/src/verilog/HTL.v b/src/hls/HTL.v
index 620ef14..620ef14 100644
--- a/src/verilog/HTL.v
+++ b/src/hls/HTL.v
diff --git a/src/translation/HTLgen.v b/src/hls/HTLgen.v
index 68e0293..68e0293 100644
--- a/src/translation/HTLgen.v
+++ b/src/hls/HTLgen.v
diff --git a/src/translation/HTLgenproof.v b/src/hls/HTLgenproof.v
index bf63800..22f8f57 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1,4 +1,4 @@
-(*
+ (*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
diff --git a/src/translation/HTLgenspec.v b/src/hls/HTLgenspec.v
index 541f9fa..541f9fa 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
new file mode 100644
index 0000000..9241abe
--- /dev/null
+++ b/src/hls/Partition.ml
@@ -0,0 +1,60 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlock
+
+(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
+   [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
+let find_backedge i n =
+  let succ = RTL.successors_instr i in
+  List.filter (fun s -> P.lt n s) succ
+
+let find_backedges c =
+
+let prepend_instr i = function
+  | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
+
+let rec bblock_from_RTL (c : RTL.code) i =
+  let succ = List.map (fun i -> PTree.get i c) (RTL.successors_instr i) in
+  match i, succ with
+  | RTL.Inop _, Some i::[] -> begin
+      match bblock_from_RTL c i with
+      | Errors.OK bb -> Errors.OK (prepend_instr RBnop bb)
+      | Errors.Error msg -> Errors.Error msg
+    end
+  | RTL.Iop (op, rs, dst, _), Some i::[] -> begin
+      match bblock_from_RTL c i with
+      | Errors.OK bb
+    end
+
+(* Partition a function and transform it into RTLBlock. *)
+let function_from_RTL f =
+  { fn_sig = f.RTL.fn_entrypoint;
+    fn_stacksize = f.RTL.fn_stacksize;
+    fn_entrypoint = f.RTL.fn_entrypoint;
+    fn_code = f.RTL.fn_code
+  }
diff --git a/src/verilog/PrintHTL.ml b/src/hls/PrintHTL.ml
index 44f8b01..44f8b01 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/hls/PrintHTL.ml
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/hls/PrintRTLBlock.ml
diff --git a/src/verilog/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index 0f64066..0f64066 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
diff --git a/src/verilog/PrintVerilog.mli b/src/hls/PrintVerilog.mli
index 6a15ee9..6a15ee9 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/hls/PrintVerilog.mli
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
new file mode 100644
index 0000000..7169d4a
--- /dev/null
+++ b/src/hls/RTLBlock.v
@@ -0,0 +1,69 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require Import
+     Coqlib
+     AST
+     Maps
+     Op
+     RTL
+     Registers.
+
+Definition node := positive.
+
+Inductive instruction : Type :=
+| RBnop : instruction
+| RBop : operation -> list reg -> reg -> instruction
+| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction
+| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction.
+
+Definition bblock_body : Type := list instruction.
+
+Inductive control_flow_inst : Type :=
+| RBcall : signature -> ident -> list reg -> reg -> node -> control_flow_inst
+| RBtailcall : signature -> ident -> list reg -> control_flow_inst
+| RBbuiltin : external_function -> list (builtin_arg reg) ->
+              builtin_res reg -> node -> control_flow_inst
+| RBcond : condition -> list reg -> node -> node -> control_flow_inst
+| RBjumptable : reg -> list node -> control_flow_inst
+| RBredurn : option reg -> control_flow_inst.
+
+Record bblock : Type := mk_bblock {
+    bb_body: bblock_body;
+    bb_exit: option control_flow_inst
+  }.
+
+Definition code : Type := PTree.t bblock.
+
+Record function: Type := mkfunction {
+  fn_sig: signature;
+  fn_params: list reg;
+  fn_stacksize: Z;
+  fn_code: code;
+  fn_entrypoint: node
+}.
+
+Definition fundef := AST.fundef function.
+
+Definition program := AST.program fundef unit.
+
+Definition funsig (fd: fundef) :=
+  match fd with
+  | Internal f => fn_sig f
+  | External ef => ef_sig ef
+  end.
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
new file mode 100644
index 0000000..05f9a32
--- /dev/null
+++ b/src/hls/RTLBlockgen.v
@@ -0,0 +1,39 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert Require
+     RTL.
+From compcert Require Import
+     AST
+     Maps.
+From vericert Require Import
+     RTLBlock.
+
+Parameter partition : RTL.code -> code.
+
+Definition transl_function (f : RTL.function) : function :=
+  mkfunction f.(RTL.fn_sig)
+             f.(RTL.fn_params)
+             f.(RTL.fn_stacksize)
+             (partition f.(RTL.fn_code))
+             f.(RTL.fn_entrypoint).
+
+Definition transl_fundef := transf_fundef transl_function.
+
+Definition transl_program : RTL.program -> program :=
+  transform_program transl_fundef.
diff --git a/src/verilog/Value.v b/src/hls/Value.v
index d6a3d8b..d6a3d8b 100644
--- a/src/verilog/Value.v
+++ b/src/hls/Value.v
diff --git a/src/verilog/ValueInt.v b/src/hls/ValueInt.v
index f1fd056..f1fd056 100644
--- a/src/verilog/ValueInt.v
+++ b/src/hls/ValueInt.v
diff --git a/src/verilog/Verilog.v b/src/hls/Verilog.v
index 3b0dd0a..c5dab9e 100644
--- a/src/verilog/Verilog.v
+++ b/src/hls/Verilog.v
@@ -29,7 +29,7 @@ Require Import Lia.
 
 Import ListNotations.
 
-From vericert Require Import common.Vericertlib common.Show verilog.ValueInt AssocMap Array.
+From vericert Require Import Vericertlib Show ValueInt AssocMap Array.
 From compcert Require Events.
 From compcert Require Import Integers Errors Smallstep Globalenvs.
 
diff --git a/src/translation/Veriloggen.v b/src/hls/Veriloggen.v
index a0be0fa..a0be0fa 100644
--- a/src/translation/Veriloggen.v
+++ b/src/hls/Veriloggen.v
diff --git a/src/translation/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index 9abbd4b..9abbd4b 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v