Add main file and global building

2 files changed, 440 insertions, 6 deletions

diff --git a/driver/Coqup.ml b/driver/Coqup.ml
new file mode 100644
index 0000000..92553c9
--- /dev/null
+++ b/driver/Coqup.ml
@@ -0,0 +1,438 @@
+(* 
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2019-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 Coqup.Commandline
+open Coqup.Clflags
+open Coqup.CommonOptions
+open Coqup.Timing
+open Coqup.Driveraux
+open Coqup.Frontend
+open Coqup.Assembler
+open Coqup.Linker
+open Coqup.Diagnostics
+
+(* Coqup flags *)
+let option_hls = ref true
+
+(* Name used for version string etc. *)
+let tool_name = "C verified high-level synthesis"
+
+(* Optional sdump suffix *)
+let sdump_suffix = ref ".json"
+
+let nolink () =
+  !option_c || !option_S || !option_E || !option_interp
+
+let object_filename sourcename suff =
+  if nolink () then
+    output_filename ~final: !option_c sourcename suff ".o"
+  else
+    tmp_file ".o"
+
+(* From CompCert C AST to asm *)
+
+let compile_c_file sourcename ifile ofile =
+  (* Prepare to dump Clight, RTL, etc, if requested *)
+  let set_dest dst opt ext =
+    dst := if !opt then Some (output_filename sourcename ".c" ext)
+      else None in
+  set_dest Coqup.Cprint.destination option_dparse ".parsed.c";
+  set_dest Coqup.PrintCsyntax.destination option_dcmedium ".compcert.c";
+  set_dest Coqup.PrintClight.destination option_dclight ".light.c";
+  set_dest Coqup.PrintCminor.destination option_dcminor ".cm";
+  set_dest Coqup.PrintRTL.destination option_drtl ".rtl";
+  set_dest Coqup.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
+  set_dest Coqup.PrintLTL.destination option_dltl ".ltl";
+  set_dest Coqup.PrintMach.destination option_dmach ".mach";
+  set_dest Coqup.AsmToJSON.destination option_sdump !sdump_suffix;
+  (* Parse the ast *)
+  let csyntax = parse_c_file sourcename ifile in
+  (* Convert to Asm *)
+  let verilog =
+    match Coqup.Compiler0.transf_hls csyntax with
+    | Coqup.Errors.OK v ->
+        v
+    | Coqup.Errors.Error msg ->
+      let loc = file_loc sourcename in
+        fatal_error loc "%a"  print_error msg in
+  let oc = open_out ofile in
+  Coqup.PrintVerilog.print_program oc verilog;
+  close_out oc
+
+(* From C source to asm *)
+
+let compile_i_file sourcename preproname =
+  if !option_interp then begin
+    Coqup.Machine.config := Coqup.Machine.compcert_interpreter !Coqup.Machine.config;
+    let csyntax = parse_c_file sourcename preproname in
+    Coqup.Interp.execute csyntax;
+        ""
+  end else if !option_S then begin
+    compile_c_file sourcename preproname
+      (output_filename ~final:true sourcename ".c" ".s");
+    ""
+  end else begin
+    let asmname =
+      if !option_dasm
+      then output_filename sourcename ".c" ".s"
+      else tmp_file ".s" in
+    compile_c_file sourcename preproname asmname;
+    let objname = object_filename sourcename ".c" in
+    assemble asmname objname;
+    objname
+  end
+
+(* Processing of a .c file *)
+
+let process_c_file sourcename =
+  ensure_inputfile_exists sourcename;
+  if !option_E then begin
+    preprocess sourcename (output_filename_default "-");
+    ""
+  end else begin
+    let preproname = if !option_dprepro then
+      output_filename sourcename ".c" ".i"
+    else
+      tmp_file ".i" in
+    preprocess sourcename preproname;
+    compile_i_file sourcename preproname
+  end
+
+(* Processing of a .i / .p file (preprocessed C) *)
+
+let process_i_file sourcename =
+  ensure_inputfile_exists sourcename;
+  compile_i_file sourcename sourcename
+
+(* Processing of .S and .s files *)
+
+let process_s_file sourcename =
+  ensure_inputfile_exists sourcename;
+  let objname = object_filename sourcename ".s" in
+  assemble sourcename objname;
+  objname
+
+let process_S_file sourcename =
+  ensure_inputfile_exists sourcename;
+  if !option_E then begin
+    preprocess sourcename (output_filename_default "-");
+    ""
+  end else begin
+    let preproname = tmp_file ".s" in
+    preprocess sourcename preproname;
+    let objname = object_filename sourcename ".S" in
+    assemble preproname objname;
+    objname
+  end
+
+(* Processing of .h files *)
+
+let process_h_file sourcename =
+  if !option_E then begin
+    ensure_inputfile_exists sourcename;
+    preprocess sourcename (output_filename_default "-");
+    ""
+  end else
+    fatal_error no_loc "input file %s ignored (not in -E mode)\n" sourcename
+
+let target_help =
+  if Coqup.Configuration.arch = "arm" && Coqup.Configuration.model <> "armv6" then
+{|Target processor options:
+  -mthumb        Use Thumb2 instruction encoding
+  -marm          Use classic ARM instruction encoding
+|}
+else
+  ""
+
+let toolchain_help =
+  if not Coqup.Configuration.gnu_toolchain then begin
+{|Toolchain options:
+  -t tof:env     Select target processor for the diab toolchain
+|} end else
+    ""
+
+let usage_string =
+  version_string tool_name ^
+  {|Usage: ccomp [options] <source files>
+Recognized source files:
+  .c             C source file
+  .i or .p       C source file that should not be preprocessed
+  .s             Assembly file
+  .S or .sx      Assembly file that must be preprocessed
+  .o             Object file
+  .a             Library file
+Processing options:
+  -c             Compile to object file only (no linking), result in <file>.o
+  -E             Preprocess only, send result to standard output
+  -S             Compile to assembler only, save result in <file>.s
+  -o <file>      Generate output in <file>
+  --no-hls       Do not use HLS and generate standard flow.
+|} ^
+  prepro_help ^
+  language_support_help ^
+ Coqup.DebugInit.debugging_help ^
+{|Optimization options: (use -fno-<opt> to turn off -f<opt>)
+  -O             Optimize the compiled code [on by default]
+  -O0            Do not optimize the compiled code
+  -O1 -O2 -O3    Synonymous for -O
+  -Os            Optimize for code size in preference to code speed
+  -Obranchless   Optimize to generate fewer conditional branches; try to produce
+                 branch-free instruction sequences as much as possible
+  -ftailcalls    Optimize function calls in tail position [on]
+  -fconst-prop   Perform global constant propagation  [on]
+  -ffloat-const-prop <n>  Control constant propagation of floats
+                   (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
+  -fcse          Perform common subexpression elimination [on]
+  -fredundancy   Perform redundancy elimination [on]
+  -finline       Perform inlining of functions [on]
+  -finline-functions-called-once Integrate functions only required by their
+                 single caller [on]
+  -fif-conversion Perform if-conversion (generation of conditional moves) [on]
+Code generation options: (use -fno-<opt> to turn off -f<opt>)
+  -ffpu          Use FP registers for some integer operations [on]
+  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
+  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
+  -falign-functions <n>  Set alignment (in bytes) of function entry points
+  -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
+  -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches
+  -fcommon       Put uninitialized globals in the common section [on].
+|} ^
+ target_help ^
+ toolchain_help ^
+ assembler_help ^
+ linker_help ^
+{|Tracing options:
+  -dprepro       Save C file after preprocessing in <file>.i
+  -dparse        Save C file after parsing and elaboration in <file>.parsed.c
+  -dc            Save generated C in <file>.compcert.c
+  -dclight       Save generated Clight in <file>.light.c
+  -dcminor       Save generated Cminor in <file>.cm
+  -drtl          Save RTL at various optimization points in <file>.rtl.<n>
+  -dltl          Save LTL after register allocation in <file>.ltl
+  -dmach         Save generated Mach code in <file>.mach
+  -dasm          Save generated assembly in <file>.s
+  -dall          Save all generated intermediate files in <file>.<ext>
+  -sdump         Save info for post-linking validation in <file>.json
+|} ^
+  general_help ^
+  warning_help ^
+  {|Coqup.Interpreter mode:
+  -interp        Execute given .c files using the reference interpreter
+  -quiet         Suppress diagnostic messages for the interpreter
+  -trace         Have the interpreter produce a detailed trace of reductions
+  -random        Randomize execution order
+  -all           Simulate all possible execution orders
+|}
+
+let print_usage_and_exit () =
+  printf "%s" usage_string; exit 0
+
+let enforce_buildnr nr =
+  let build = int_of_string Coqup.Version.buildnr in
+  if nr != build then
+    fatal_error no_loc "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\
+Please use matching builds of QSK and CompCert." build nr
+
+let dump_mnemonics destfile =
+  let oc = open_out_bin destfile in
+  let pp = Format.formatter_of_out_channel oc in
+  Coqup.AsmToJSON.pp_mnemonics pp;
+  Format.pp_print_flush pp ();
+  close_out oc;
+  exit 0
+
+let optimization_options = [
+  option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse;
+  option_fredundancy; option_finline; option_finline_functions_called_once;
+]
+
+let set_all opts () = List.iter (fun r -> r := true) opts
+let unset_all opts () = List.iter (fun r -> r := false) opts
+
+let num_source_files = ref 0
+
+let num_input_files = ref 0
+
+let cmdline_actions =
+  let f_opt name ref =
+    [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
+  let check_align n =
+    if n <= 0 || ((n land (n - 1)) <> 0) then
+      error no_loc "requested alignment %d is not a power of 2" n
+    in
+  [
+(* Getting help *)
+  Exact "-help", Unit print_usage_and_exit;
+  Exact "--help", Unit print_usage_and_exit;] @
+(* Use HLS *)
+  [Exact "--no-hls", Unset option_hls;]
+(* Getting version info *)
+  @ version_options tool_name @
+(* Enforcing CompCert build numbers for QSKs and mnemonics dump *)
+  (if Coqup.Version.buildnr <> "" then
+    [ Exact "-qsk-enforce-build", Integer enforce_buildnr;
+      Exact "--qsk-enforce-build", Integer enforce_buildnr;
+      Exact "-dump-mnemonics", String  dump_mnemonics;
+    ]
+   else []) @
+(* Processing options *)
+ [ Exact "-c", Set option_c;
+  Exact "-E", Set option_E;
+  Exact "-S", Set option_S;
+  Exact "-o", String(fun s -> option_o := Some s);
+  Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
+                              option_o := Some s);]
+  (* Preprocessing options *)
+    @ prepro_actions @
+  (* Language support options *)
+    language_support_options
+  (* Debugging options *)
+    @ Coqup.DebugInit.debugging_actions @
+(* Code generation options -- more below *)
+ [
+  Exact "-O0", Unit (unset_all optimization_options);
+  Exact "-O", Unit (set_all optimization_options);
+  _Regexp "-O[123]$", Unit (set_all optimization_options);
+  Exact "-Os", Set option_Osize;
+  Exact "-Obranchless", Set option_Obranchless;
+  Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
+  Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
+  Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n);
+  Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n);
+  Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n);
+  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @
+      f_opt "common" option_fcommon @
+(* Target processor options *)
+  (if Coqup.Configuration.arch = "arm" then
+    if Coqup.Configuration.model = "armv6" then
+      [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *)
+    else
+      [ Exact "-mthumb", Set option_mthumb;
+        Exact "-marm", Unset option_mthumb; ]
+   else []) @
+(* Toolchain options *)
+    (if not Coqup.Configuration.gnu_toolchain then
+       [Exact "-t", String (fun arg -> push_linker_arg "-t"; push_linker_arg arg;
+                             prepro_options := arg :: "-t" :: !prepro_options;
+                             assembler_options := arg :: "-t" :: !assembler_options;)]
+     else
+       []) @
+(* Assembling options *)
+  assembler_actions @
+(* Linking options *)
+  linker_actions @
+(* Tracing options *)
+ [ Exact "-dprepro", Set option_dprepro;
+  Exact "-dparse", Set option_dparse;
+  Exact "-dc", Set option_dcmedium;
+  Exact "-dclight", Set option_dclight;
+  Exact "-dcminor", Set option_dcminor;
+  Exact "-drtl", Set option_drtl;
+  Exact "-dltl", Set option_dltl;
+  Exact "-dalloctrace", Set option_dalloctrace;
+  Exact "-dmach", Set option_dmach;
+  Exact "-dasm", Set option_dasm;
+  Exact "-dall", Self (fun _ ->
+    option_dprepro := true;
+    option_dparse := true;
+    option_dcmedium := true;
+    option_dclight := true;
+    option_dcminor := true;
+    option_drtl := true;
+    option_dltl := true;
+    option_dalloctrace := true;
+    option_dmach := true;
+    option_dasm := true);
+  Exact "-sdump", Set option_sdump;
+  Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s);
+  Exact "-sdump-folder", String (fun s -> Coqup.AsmToJSON.sdump_folder := s);] @
+(* General options *)
+   general_options @
+(* Diagnostic options *)
+  warning_options @
+(* Coqup.Interpreter mode *)
+ [ Exact "-interp", Set option_interp;
+  Exact "-quiet", Unit (fun () -> Coqup.Interp.trace := 0);
+  Exact "-trace", Unit (fun () -> Coqup.Interp.trace := 2);
+  Exact "-random", Unit (fun () -> Coqup.Interp.mode := Coqup.Interp.Random);
+  Exact "-all", Unit (fun () -> Coqup.Interp.mode := Coqup.Interp.All)
+ ]
+(* Optimization options *)
+(* -f options: come in -f and -fno- variants *)
+  @ f_opt "tailcalls" option_ftailcalls
+  @ f_opt "if-conversion" option_fifconversion
+  @ f_opt "const-prop" option_fconstprop
+  @ f_opt "cse" option_fcse
+  @ f_opt "redundancy" option_fredundancy
+  @ f_opt "inline" option_finline
+  @ f_opt "inline-functions-called-once" option_finline_functions_called_once
+(* Code generation options *)
+  @ f_opt "fpu" option_ffpu
+  @ f_opt "sse" option_ffpu (* backward compatibility *)
+  @ [
+(* Catch options that are not handled *)
+  Prefix "-", Self (fun s ->
+      fatal_error no_loc "Unknown option `%s'" s);
+(* File arguments *)
+  Suffix ".c", Self (fun s ->
+      push_action process_c_file s; incr num_source_files; incr num_input_files);
+  Suffix ".i", Self (fun s ->
+      push_action process_i_file s; incr num_source_files; incr num_input_files);
+  Suffix ".p", Self (fun s ->
+      push_action process_i_file s; incr num_source_files; incr num_input_files);
+  Suffix ".s", Self (fun s ->
+      push_action process_s_file s; incr num_source_files; incr num_input_files);
+  Suffix ".S", Self (fun s ->
+      push_action process_S_file s; incr num_source_files; incr num_input_files);
+  Suffix ".sx", Self (fun s ->
+      push_action process_S_file s; incr num_source_files; incr num_input_files);
+  Suffix ".o", Self (fun s -> push_linker_arg s; incr num_input_files);
+  Suffix ".a", Self (fun s -> push_linker_arg s; incr num_input_files);
+  (* GCC compatibility: .o.ext files and .so files are also object files *)
+  _Regexp ".*\\.o\\.", Self (fun s -> push_linker_arg s; incr num_input_files);
+  Suffix ".so", Self (fun s -> push_linker_arg s; incr num_input_files);
+  (* GCC compatibility: .h files can be preprocessed with -E *)
+  Suffix ".h", Self (fun s ->
+      push_action process_h_file s; incr num_source_files; incr num_input_files);
+  ]
+
+let _ =
+  try
+    Gc.set { (Gc.get()) with
+                Gc.minor_heap_size = 524288; (* 512k *)
+                Gc.major_heap_increment = 4194304 (* 4M *)
+           };
+    Printexc.record_backtrace true;
+    Coqup.Frontend.init ();
+    parse_cmdline cmdline_actions;
+    Coqup.DebugInit.init (); (* Initialize the debug functions *)
+    if nolink () && !option_o <> None && !num_source_files >= 2 then
+      fatal_error no_loc "ambiguous '-o' option (multiple source files)";
+    if !num_input_files = 0 then
+      fatal_error no_loc "no input file";
+    let linker_args = time "Total compilation time" perform_actions () in
+    if not (nolink ()) && linker_args <> [] then begin
+      linker (output_filename_default "a.out") linker_args
+    end;
+    check_errors ()
+  with
+  | Sys_error msg
+  | CmdError msg -> error no_loc "%s" msg; exit 2
+  | Abort -> error_summary (); exit 2
+  | e -> crash e
diff --git a/driver/dune b/driver/dune
index 583f201..5dbfcad 100644
--- a/driver/dune
+++ b/driver/dune
@@ -1,9 +1,5 @@
 (include_subdirs no)
 
-(executables
- (names Driver)
+(executable
+ (name CoqupDriver)
  (libraries coqup))
-
-(install
- (section bin)
- (files (Driver.exe as coqup)))