(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* Vericert: 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 Vericert.Commandline open Vericert.Clflags open Vericert.CommonOptions open Vericert.Timing open Vericert.Driveraux open Vericert.Frontend open Vericert.Assembler open Vericert.Linker open Vericert.Diagnostics open Vericert.VericertClflags (* 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 || !option_hls 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 Vericert.Cprint.destination option_dparse ".parsed.c"; set_dest Vericert.PrintCsyntax.destination option_dcmedium ".compcert.c"; set_dest Vericert.PrintClight.destination option_dclight ".light.c"; set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; set_dest Vericert.PrintGibleSeq.destination option_dgblseq ".gblseq"; set_dest Vericert.PrintGiblePar.destination option_dgblpar ".gblpar"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; set_dest Vericert.PrintMach.destination option_dmach ".mach"; set_dest Vericert.AsmToJSON.destination option_sdump !sdump_suffix; (* Parse the ast *) let csyntax = parse_c_file sourcename ifile in if not !option_hls then begin (* Convert to Asm *) let asm = match Vericert.Compiler.apply_partial (Vericert.Compiler.transf_c_program csyntax) Vericert.Asmexpand.expand_program with | Vericert.Errors.OK asm -> asm | Vericert.Errors.Error msg -> let loc = file_loc sourcename in fatal_error loc "%a" print_error msg in (* Dump Asm in binary and JSON format *) Vericert.AsmToJSON.print_if asm sourcename; (* Print Asm in text form *) let oc = open_out ofile in Vericert.PrintAsm.print_program oc asm; close_out oc end else begin let verilog = let translation = if !option_hls_schedule then Vericert.Compiler0.transf_hls_temp else Vericert.Compiler0.transf_hls in match translation csyntax with | Vericert.Errors.OK v -> v | Vericert.Errors.Error msg -> let loc = file_loc sourcename in fatal_error loc "%a" print_error msg in let oc = open_out ofile in Vericert.PrintVerilog.print_program !option_debug_hls oc verilog; close_out oc end (* From C source to asm *) let compile_i_file sourcename preproname = if !option_interp then begin Vericert.Machine.config := Vericert.Machine.compcert_interpreter !Vericert.Machine.config; let csyntax = parse_c_file sourcename preproname in Vericert.Interp.execute csyntax; "" end else if !option_hls then begin compile_c_file sourcename preproname (output_filename ~final:true sourcename ".c" ".v"); "" 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 Vericert.Configuration.arch = "arm" && Vericert.Configuration.model <> "armv6" then {|Target processor options: -mthumb Use Thumb2 instruction encoding -marm Use classic ARM instruction encoding |} else "" let toolchain_help = if not Vericert.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: vericert [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. --simulate Simulate the result with the Verilog semantics. --debug-hls Add debug logic to the Verilog. --initialise-stack initialise the stack to all 0s. |} ^ prepro_help ^ language_support_help ^ Vericert.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) [off] -fram Generate Verilog that is fit for ram inference [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]. HLS Optimisations: -fschedule Schedule the resulting hardware [off]. -fif-conversion If-conversion optimisation [off]. |} ^ 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. -dgblseq Save GibleSeq .gblseq -dgblpar Save GiblePar .gblpar -dhtl Save HTL before Verilog generation .htl -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 ^ {|Vericert.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 Vericert.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 Vericert.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; Exact "--simulate", Set option_simulate; Exact "--debug-hls", Set option_debug_hls; Exact "--initialise-stack", Set option_initial; ] (* Getting version info *) @ version_options tool_name @ (* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Vericert.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 *) @ Vericert.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 Vericert.Configuration.arch = "arm" then if Vericert.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 Vericert.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 "-dgblseq", Set option_dgblseq; Exact "-dgblpar", Set option_dgblpar; Exact "-dhtl", Set option_dhtl; 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_dgblseq := true; option_dgblpar := true; option_dhtl := 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 -> Vericert.AsmToJSON.sdump_folder := s);] @ (* General options *) general_options @ (* Diagnostic options *) warning_options @ (* Vericert.Interpreter mode *) [ Exact "-interp", Set option_interp; Exact "-quiet", Unit (fun () -> Vericert.Interp.trace := 0); Exact "-trace", Unit (fun () -> Vericert.Interp.trace := 2); Exact "-random", Unit (fun () -> Vericert.Interp.mode := Vericert.Interp.Random); Exact "-all", Unit (fun () -> Vericert.Interp.mode := Vericert.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 *) @ f_opt "schedule" option_hls_schedule @ f_opt "if-conv" option_fif_conv @ f_opt "ram" option_fram @ [ (* 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; Vericert.Frontend.init (); parse_cmdline cmdline_actions; Vericert.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