(* *********************************************************************)
(* *)
(* 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 ___ ___ <___@______.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 .
*)
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 ~suffix:suff
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 ~suffix: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.PrintDHTL.destination option_ddhtl ".dhtl";
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
(* let _ = Vericert.Smtpredicate.check_smt (Vericert.Predicate0.Pimp ((Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)),(Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)))) in *)
match translation csyntax with
| Vericert.Errors.OK v ->
if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n"; v
| Vericert.Errors.Error msg ->
if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n";
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 ~suffix:".v");
""
end else begin
let asmname =
if !option_dasm
then output_filename sourcename ~suffix:".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 ~suffix:".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]