From 2d11fe952455efbb66a4cf9a59d9e39425bd522c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 31 Mar 2020 15:31:41 +0100 Subject: Fix the Makefile build --- driver/Coqup.ml | 438 -------------------------------------------------- driver/CoqupDriver.ml | 438 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 438 insertions(+), 438 deletions(-) delete mode 100644 driver/Coqup.ml create mode 100644 driver/CoqupDriver.ml (limited to 'driver') 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 - * - * 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 . - *) - -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] -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 .o - -E Preprocess only, send result to standard output - -S Compile to assembler only, save result in .s - -o Generate output in - --no-hls Do not use HLS and generate standard flow. -|} ^ - prepro_help ^ - language_support_help ^ - Coqup.DebugInit.debugging_help ^ -{|Optimization options: (use -fno- to turn off -f) - -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 Control constant propagation of floats - (=0: none, =1: limited, =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- to turn off -f) - -ffpu Use FP registers for some integer operations [on] - -fsmall-data Set maximal size for allocation in small data area - -fsmall-const Set maximal size for allocation in small constant area - -falign-functions Set alignment (in bytes) of function entry points - -falign-branch-targets Set alignment (in bytes) of branch targets - -falign-cond-branches 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 .i - -dparse Save C file after parsing and elaboration in .parsed.c - -dc Save generated C in .compcert.c - -dclight Save generated Clight in .light.c - -dcminor Save generated Cminor in .cm - -drtl Save RTL at various optimization points in .rtl. - -dltl Save LTL after register allocation in .ltl - -dmach Save generated Mach code in .mach - -dasm Save generated assembly in .s - -dall Save all generated intermediate files in . - -sdump Save info for post-linking validation in .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/CoqupDriver.ml b/driver/CoqupDriver.ml new file mode 100644 index 0000000..92553c9 --- /dev/null +++ b/driver/CoqupDriver.ml @@ -0,0 +1,438 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * 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 . + *) + +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] +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 .o + -E Preprocess only, send result to standard output + -S Compile to assembler only, save result in .s + -o Generate output in + --no-hls Do not use HLS and generate standard flow. +|} ^ + prepro_help ^ + language_support_help ^ + Coqup.DebugInit.debugging_help ^ +{|Optimization options: (use -fno- to turn off -f) + -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 Control constant propagation of floats + (=0: none, =1: limited, =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- to turn off -f) + -ffpu Use FP registers for some integer operations [on] + -fsmall-data Set maximal size for allocation in small data area + -fsmall-const Set maximal size for allocation in small constant area + -falign-functions Set alignment (in bytes) of function entry points + -falign-branch-targets Set alignment (in bytes) of branch targets + -falign-cond-branches 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 .i + -dparse Save C file after parsing and elaboration in .parsed.c + -dc Save generated C in .compcert.c + -dclight Save generated Clight in .light.c + -dcminor Save generated Cminor in .cm + -drtl Save RTL at various optimization points in .rtl. + -dltl Save LTL after register allocation in .ltl + -dmach Save generated Mach code in .mach + -dasm Save generated assembly in .s + -dall Save all generated intermediate files in . + -sdump Save info for post-linking validation in .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 -- cgit