Fix the Makefile build

1 files changed, 0 insertions, 438 deletions

diff --git a/driver/Coqup.ml b/driver/Coqup.ml
deleted file mode 100644
index 92553c9..0000000
--- a/driver/Coqup.ml
+++ /dev/null
@@ -1,438 +0,0 @@
-(* 
- * 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