diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 55fdde39347c..24bbfb67ad2a 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -10,7 +10,7 @@ publish = false [dependencies] cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } -clap = { version = "4.1.3", features = ["cargo"] } +clap = { version = "4.1.3", features = ["derive", "cargo"] } home = "0.5" itertools = "0.11" kani_metadata = {path = "../kani_metadata"} diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs new file mode 100644 index 000000000000..b174795b7259 --- /dev/null +++ b/kani-compiler/src/args.rs @@ -0,0 +1,74 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use strum_macros::{AsRefStr, EnumString, EnumVariantNames}; +use tracing_subscriber::filter::Directive; + +#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)] +#[strum(serialize_all = "snake_case")] +pub enum ReachabilityType { + /// Start the cross-crate reachability analysis from all harnesses in the local crate. + Harnesses, + /// Don't perform any reachability analysis. This will skip codegen for this crate. + #[default] + None, + /// Start the cross-crate reachability analysis from all public functions in the local crate. + PubFns, + /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate. + Tests, +} + +/// Command line arguments that this instance of the compiler run was called +/// with. Usually stored in and accessible via [`crate::kani_queries::QueryDb`]. +#[derive(Debug, Default, Clone, clap::Parser)] +pub struct Arguments { + /// Option name used to enable assertion reachability checks. + #[clap(long = "assertion-reach-checks")] + pub check_assertion_reachability: bool, + /// Option name used to enable coverage checks. + #[clap(long = "coverage-checks")] + pub check_coverage: bool, + /// Option name used to dump function pointer restrictions. + #[clap(long = "restrict-vtable-fn-ptrs")] + pub emit_vtable_restrictions: bool, + /// Option name used to use json pretty-print for output files. + #[clap(long = "pretty-json-files")] + pub output_pretty_json: bool, + /// Option used for suppressing global ASM error. + #[clap(long)] + pub ignore_global_asm: bool, + #[clap(long)] + /// Option used to write JSON symbol tables instead of GOTO binaries. + /// + /// When set, instructs the compiler to produce the symbol table for CBMC in JSON format and use symtab2gb. + pub write_json_symtab: bool, + /// Option name used to select which reachability analysis to perform. + #[clap(long = "reachability", default_value = "none")] + pub reachability_analysis: ReachabilityType, + #[clap(long = "enable-stubbing")] + pub stubbing_enabled: bool, + /// Option name used to define unstable features. + #[clap(short = 'Z', long = "unstable")] + pub unstable_features: Vec, + #[clap(long)] + /// Option used for building standard library. + /// + /// Flag that indicates that we are currently building the standard library. + /// Note that `kani` library will not be available if this is `true`. + pub build_std: bool, + #[clap(long)] + /// Option name used to set log level. + pub log_level: Option, + #[clap(long)] + /// Option name used to set the log output to a json file. + pub json_output: bool, + #[clap(long, conflicts_with = "json_output")] + /// Option name used to force logger to use color output. This doesn't work with --json-output. + pub color_output: bool, + #[clap(long)] + /// Pass the kani version to the compiler to ensure cache coherence. + check_version: Option, + #[clap(long)] + /// A legacy flag that is now ignored. + goto_c: bool, +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 27203c7218c6..b87f6f808aa8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -178,7 +178,7 @@ impl<'tcx> GotocCtx<'tcx> { span: Option, ) -> (String, Stmt) { let loc = self.codegen_caller_span(&span); - if self.queries.check_assertion_reachability { + if self.queries.args().check_assertion_reachability { // Generate a unique ID for the assert let assert_id = self.next_check_id(); // Also add the unique ID as a prefix to the assert message so that it can be diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index bc6738e8ead0..b6743174aabb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -16,7 +16,7 @@ impl<'tcx> GotocCtx<'tcx> { debug!(?bb, "Codegen basicblock"); self.current_fn_mut().set_current_bb(bb); let label: String = self.current_fn().find_label(&bb); - let check_coverage = self.queries.check_coverage; + let check_coverage = self.queries.args().check_coverage; // the first statement should be labelled. if there is no statements, then the // terminator should be labelled. match bbd.statements.len() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 52b6ef0cc821..61ab4f97bfe8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -89,7 +89,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Checks whether C-FFI has been enabled or not. /// When enabled, we blindly encode the function type as is. fn is_cffi_enabled(&self) -> bool { - self.queries.unstable_features.contains(&"c-ffi".to_string()) + self.queries.args().unstable_features.contains(&"c-ffi".to_string()) } /// Generate code for a foreign function shim. diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9535e74152ad..34e1a085040b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -3,6 +3,7 @@ //! This file contains the code necessary to interface with the compiler backend +use crate::args::ReachabilityType; use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; use crate::kani_middle::attributes::is_test_harness_description; @@ -12,7 +13,7 @@ use crate::kani_middle::reachability::{ collect_reachable_items, filter_const_crate_items, filter_crate_items, }; use crate::kani_middle::{check_reachable_items, dump_mir_items}; -use crate::kani_queries::{QueryDb, ReachabilityType}; +use crate::kani_queries::QueryDb; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; use cbmc::RoundingMode; @@ -164,9 +165,9 @@ impl GotocCodegenBackend { // No output should be generated if user selected no_codegen. if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { - let pretty = self.queries.lock().unwrap().output_pretty_json; + let pretty = self.queries.lock().unwrap().args().output_pretty_json; write_file(&symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty); - if gcx.queries.write_json_symtab { + if gcx.queries.args().write_json_symtab { write_file(&symtab_goto, ArtifactType::SymTab, &gcx.symbol_table, pretty); symbol_table_to_gotoc(&tcx, &symtab_goto); } else { @@ -225,7 +226,7 @@ impl CodegenBackend for GotocCodegenBackend { // - PubFns: Generate code for all reachable logic starting from the local public functions. // - None: Don't generate code. This is used to compile dependencies. let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); - let reachability = queries.reachability_analysis; + let reachability = queries.args().reachability_analysis; let mut results = GotoCodegenResults::new(tcx, reachability); match reachability { ReachabilityType::Harnesses => { @@ -305,7 +306,7 @@ impl CodegenBackend for GotocCodegenBackend { &base_filename, ArtifactType::Metadata, &results.generate_metadata(), - queries.output_pretty_json, + queries.args().output_pretty_json, ); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index dd43c96f27ea..342e0e0b296b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -78,7 +78,7 @@ impl<'tcx> GotocCtx<'tcx> { ) -> GotocCtx<'tcx> { let fhks = fn_hooks(); let symbol_table = SymbolTable::new(machine_model.clone()); - let emit_vtable_restrictions = queries.emit_vtable_restrictions; + let emit_vtable_restrictions = queries.args().emit_vtable_restrictions; GotocCtx { tcx, queries, diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 6e8e4bdf82ef..666344e012f0 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,6 +15,7 @@ //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to //! `-C llvm-args`. +use crate::args::{Arguments, ReachabilityType}; #[cfg(feature = "cprover")] use crate::codegen_cprover_gotoc::GotocCodegenBackend; use crate::kani_middle::attributes::is_proof_harness; @@ -22,9 +23,9 @@ use crate::kani_middle::check_crate_items; use crate::kani_middle::metadata::gen_proof_metadata; use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::stubbing::{self, harness_stub_map}; -use crate::kani_queries::{QueryDb, ReachabilityType}; -use crate::parser::{self, KaniCompilerParser}; +use crate::kani_queries::QueryDb; use crate::session::init_session; +use clap::Parser; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_driver::{Callbacks, Compilation, RunCompiler}; @@ -202,7 +203,7 @@ impl KaniCompiler { // Only store metadata for harnesses for now. // TODO: This should only skip None. // https://github.com/model-checking/kani/issues/2493 - if self.queries.lock().unwrap().reachability_analysis + if self.queries.lock().unwrap().args().reachability_analysis == ReachabilityType::Harnesses { // Store metadata file. @@ -276,7 +277,8 @@ impl KaniCompiler { name: tcx.crate_name(LOCAL_CRATE).as_str().into(), output_path: metadata_output_path(tcx), }; - if self.queries.lock().unwrap().reachability_analysis == ReachabilityType::Harnesses { + if self.queries.lock().unwrap().args().reachability_analysis == ReachabilityType::Harnesses + { let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(tcx, def_id)); let all_harnesses = harnesses @@ -291,7 +293,7 @@ impl KaniCompiler { .collect::>(); let (no_stubs, with_stubs): (Vec<_>, Vec<_>) = - if self.queries.lock().unwrap().stubbing_enabled { + if self.queries.lock().unwrap().args().stubbing_enabled { // Partition harnesses that don't have stub with the ones with stub. all_harnesses .keys() @@ -353,7 +355,7 @@ impl KaniCompiler { debug!(?filename, "write_metadata"); let out_file = File::create(&filename).unwrap(); let writer = BufWriter::new(out_file); - if self.queries.lock().unwrap().output_pretty_json { + if self.queries.lock().unwrap().args().output_pretty_json { serde_json::to_writer_pretty(writer, &metadata).unwrap(); } else { serde_json::to_writer(writer, &metadata).unwrap(); @@ -380,32 +382,12 @@ impl Callbacks for KaniCompiler { if self.stage.is_init() { let mut args = vec!["kani-compiler".to_string()]; args.extend(config.opts.cg.llvm_args.iter().cloned()); - let matches = parser::parser().get_matches_from(&args); - init_session( - &matches, - matches!(config.opts.error_format, ErrorOutputType::Json { .. }), - ); + let args = Arguments::parse_from(args); + init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); // Configure queries. let queries = &mut (*self.queries.lock().unwrap()); - queries.emit_vtable_restrictions = matches.get_flag(parser::RESTRICT_FN_PTRS); - queries.check_assertion_reachability = matches.get_flag(parser::ASSERTION_REACH_CHECKS); - queries.check_coverage = matches.get_flag(parser::COVERAGE_CHECKS); - queries.output_pretty_json = matches.get_flag(parser::PRETTY_OUTPUT_FILES); - queries.ignore_global_asm = matches.get_flag(parser::IGNORE_GLOBAL_ASM); - queries.write_json_symtab = - cfg!(feature = "write_json_symtab") || matches.get_flag(parser::WRITE_JSON_SYMTAB); - queries.reachability_analysis = matches.reachability_type(); - queries.build_std = matches.get_flag(parser::BUILD_STD); - - if let Some(features) = matches.get_many::(parser::UNSTABLE_FEATURE) { - queries.unstable_features = features.cloned().collect::>(); - } - if matches.get_flag(parser::ENABLE_STUBBING) - && queries.reachability_analysis == ReachabilityType::Harnesses - { - queries.stubbing_enabled = true; - } + queries.set_args(args); debug!(?queries, "config end"); } @@ -420,7 +402,7 @@ impl Callbacks for KaniCompiler { ) -> Compilation { if self.stage.is_init() { self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| { - check_crate_items(tcx, self.queries.lock().unwrap().ignore_global_asm); + check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm); self.process_harnesses(tcx) }); } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 8fe4ab31d0ae..d087aa76c7c4 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -74,7 +74,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) if !def_ids.contains(&def_id) { // Check if any unstable attribute was reached. KaniAttributes::for_item(tcx, def_id) - .check_unstable_features(&queries.unstable_features); + .check_unstable_features(&queries.args().unstable_features); def_ids.insert(def_id); } } diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index dbc2dba993b0..d668d439b96a 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -4,10 +4,11 @@ //! to run during code generation. For example, this can be used to hook up //! custom MIR transformations. +use crate::args::{Arguments, ReachabilityType}; use crate::kani_middle::intrinsics::ModelIntrinsics; use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::stubbing; -use crate::kani_queries::{QueryDb, ReachabilityType}; +use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_interface; use rustc_middle::{ @@ -19,10 +20,11 @@ use rustc_middle::{ /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// the present crate. pub fn provide(providers: &mut Providers, queries: &QueryDb) { - if should_override(queries) { + let args = queries.args(); + if should_override(args) { // Don't override queries if we are only compiling our dependencies. providers.optimized_mir = run_mir_passes; - if queries.stubbing_enabled { + if args.stubbing_enabled { // TODO: Check if there's at least one stub being applied. providers.collect_and_partition_mono_items = collect_and_partition_mono_items; } @@ -32,14 +34,14 @@ pub fn provide(providers: &mut Providers, queries: &QueryDb) { /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// external crates. pub fn provide_extern(providers: &mut ExternProviders, queries: &QueryDb) { - if should_override(queries) { + if should_override(queries.args()) { // Don't override queries if we are only compiling our dependencies. providers.optimized_mir = run_mir_passes_extern; } } -fn should_override(queries: &QueryDb) -> bool { - queries.reachability_analysis != ReachabilityType::None && !queries.build_std +fn should_override(args: &Arguments) -> bool { + args.reachability_analysis != ReachabilityType::None && !args.build_std } /// Returns the optimized code for the external function associated with `def_id` by diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 8ffc8be4f888..7c716a5f38a5 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -8,39 +8,13 @@ use std::{ path::PathBuf, sync::{Arc, Mutex}, }; -use strum_macros::{AsRefStr, EnumString, EnumVariantNames}; - -#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)] -#[strum(serialize_all = "snake_case")] -pub enum ReachabilityType { - /// Start the cross-crate reachability analysis from all harnesses in the local crate. - Harnesses, - /// Don't perform any reachability analysis. This will skip codegen for this crate. - #[default] - None, - /// Start the cross-crate reachability analysis from all public functions in the local crate. - PubFns, - /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate. - Tests, -} + +use crate::args::Arguments; /// This structure should only be used behind a synchronized reference or a snapshot. #[derive(Debug, Default, Clone)] pub struct QueryDb { - pub check_assertion_reachability: bool, - pub check_coverage: bool, - pub emit_vtable_restrictions: bool, - pub output_pretty_json: bool, - pub ignore_global_asm: bool, - /// When set, instructs the compiler to produce the symbol table for CBMC in JSON format and use symtab2gb. - pub write_json_symtab: bool, - pub reachability_analysis: ReachabilityType, - pub stubbing_enabled: bool, - pub unstable_features: Vec, - /// Flag that indicates that we are currently building the standard library. - /// Note that `kani` library will not be available if this is `true`. - pub build_std: bool, - + args: Option, /// Information about all target harnesses. pub harnesses_info: HashMap, } @@ -59,4 +33,12 @@ impl QueryDb { pub fn harness_model_path(&self, harness: &DefPathHash) -> Option<&PathBuf> { self.harnesses_info.get(harness) } + + pub fn set_args(&mut self, args: Arguments) { + self.args = Some(args); + } + + pub fn args(&self) -> &Arguments { + self.args.as_ref().expect("Arguments have not been initialized") + } } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index ad510bcc7dd8..0199642f9a60 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -31,12 +31,12 @@ extern crate rustc_target; // We can't add this directly as a dependency because we need the version to match rustc extern crate tempfile; +mod args; #[cfg(feature = "cprover")] mod codegen_cprover_gotoc; mod kani_compiler; mod kani_middle; mod kani_queries; -mod parser; mod session; use rustc_driver::{RunCompiler, TimePassesCallbacks}; @@ -46,7 +46,7 @@ use std::process::ExitCode; /// Main function. Configure arguments and run the compiler. fn main() -> ExitCode { session::init_panic_hook(); - let (kani_compiler, rustc_args) = parser::is_kani_compiler(env::args().collect()); + let (kani_compiler, rustc_args) = is_kani_compiler(env::args().collect()); // Configure and run compiler. if kani_compiler { @@ -57,3 +57,27 @@ fn main() -> ExitCode { if compiler.run().is_err() { ExitCode::FAILURE } else { ExitCode::SUCCESS } } } + +/// Return whether we should run our flavour of the compiler, and which arguments to pass to rustc. +/// +/// We add a `--kani-compiler` argument to run the Kani version of the compiler, which needs to be +/// filtered out before passing the arguments to rustc. +/// +/// All other Kani arguments are today located inside `--llvm-args`. +pub fn is_kani_compiler(args: Vec) -> (bool, Vec) { + assert!(!args.is_empty(), "Arguments should always include executable name"); + const KANI_COMPILER: &str = "--kani-compiler"; + let mut has_kani_compiler = false; + let new_args = args + .into_iter() + .filter(|arg| { + if arg == KANI_COMPILER { + has_kani_compiler = true; + false + } else { + true + } + }) + .collect(); + (has_kani_compiler, new_args) +} diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs deleted file mode 100644 index 738676f5ff55..000000000000 --- a/kani-compiler/src/parser.rs +++ /dev/null @@ -1,248 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use crate::kani_queries::ReachabilityType; -use clap::{builder::PossibleValuesParser, command, Arg, ArgAction, ArgMatches, Command}; -use std::env; -use std::str::FromStr; -use strum::VariantNames as _; - -/// Option name used to set log level. -pub const LOG_LEVEL: &str = "log-level"; - -/// Option name used to enable goto-c compilation. -pub const GOTO_C: &str = "goto-c"; - -/// Option name used to override Kani library path. -pub const KANI_LIB: &str = "kani-lib"; - -/// Option name used to set the log output to a json file. -pub const JSON_OUTPUT: &str = "json-output"; - -/// Option name used to force logger to use color output. This doesn't work with --json-output. -pub const COLOR_OUTPUT: &str = "color-output"; - -/// Option name used to dump function pointer restrictions. -pub const RESTRICT_FN_PTRS: &str = "restrict-vtable-fn-ptrs"; - -/// Option name used to enable assertion reachability checks. -pub const ASSERTION_REACH_CHECKS: &str = "assertion-reach-checks"; - -/// Option name used to enable coverage checks. -pub const COVERAGE_CHECKS: &str = "coverage-checks"; - -/// Option name used to use json pretty-print for output files. -pub const PRETTY_OUTPUT_FILES: &str = "pretty-json-files"; - -/// Option used for suppressing global ASM error. -pub const IGNORE_GLOBAL_ASM: &str = "ignore-global-asm"; - -/// Option used to write JSON symbol tables instead of GOTO binaries. -pub const WRITE_JSON_SYMTAB: &str = "write-json-symtab"; - -/// Option name used to select which reachability analysis to perform. -pub const REACHABILITY: &str = "reachability"; - -/// Option name used to enable stubbing. -pub const ENABLE_STUBBING: &str = "enable-stubbing"; - -/// Option name used to define unstable features. -pub const UNSTABLE_FEATURE: &str = "unstable"; - -/// Option used for building standard library. -pub const BUILD_STD: &str = "build-std"; - -/// Configure command options for the Kani compiler. -pub fn parser() -> Command { - let app = command!() - .arg( - Arg::new(KANI_LIB) - .long(KANI_LIB) - .value_name("FOLDER_PATH") - .help("Sets the path to locate the kani library.") - .action(ArgAction::Set), - ) - .arg( - Arg::new(GOTO_C) - .long(GOTO_C) - .help("Enables compilation to goto-c intermediate representation.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(LOG_LEVEL) - .long(LOG_LEVEL) - .value_parser(["error", "warn", "info", "debug", "trace"]) - .value_name("LOG_LEVEL") - .help( - "Sets the maximum log level to the value given. Use KANI_LOG for more granular \ - control.", - ) - .action(ArgAction::Set), - ) - .arg( - Arg::new(JSON_OUTPUT) - .long(JSON_OUTPUT) - .help("Print output including logs in json format.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(COLOR_OUTPUT) - .long(COLOR_OUTPUT) - .help("Print output using colors.") - .conflicts_with(JSON_OUTPUT) - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(RESTRICT_FN_PTRS) - .long(RESTRICT_FN_PTRS) - .help("Restrict the targets of virtual table function pointer calls.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(ASSERTION_REACH_CHECKS) - .long(ASSERTION_REACH_CHECKS) - .help("Check the reachability of every assertion.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(COVERAGE_CHECKS) - .long(COVERAGE_CHECKS) - .help("Check the reachability of every statement.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(REACHABILITY) - .long(REACHABILITY) - .value_parser(PossibleValuesParser::new(ReachabilityType::VARIANTS)) - .required(false) - .default_value(ReachabilityType::None.as_ref()) - .help("Selects the type of reachability analysis to perform.") - .action(ArgAction::Set), - ) - .arg( - Arg::new(PRETTY_OUTPUT_FILES) - .long(PRETTY_OUTPUT_FILES) - .help("Output json files in a more human-readable format (with spaces).") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(IGNORE_GLOBAL_ASM) - .long(IGNORE_GLOBAL_ASM) - .help("Suppress error due to the existence of global_asm in a crate") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(WRITE_JSON_SYMTAB) - .long(WRITE_JSON_SYMTAB) - .help("Instruct the compiler to produce GotoC symbol tables in JSON format instead of GOTO binary format.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new(ENABLE_STUBBING) - .long(ENABLE_STUBBING) - .help("Instruct the compiler to perform stubbing.") - .action(ArgAction::SetTrue), - ) - .arg( - Arg::new("check-version") - .long("check-version") - .action(ArgAction::Set) - .help("Pass the kani version to the compiler to ensure cache coherence."), - ) - .arg( - Arg::new(UNSTABLE_FEATURE) - .long(UNSTABLE_FEATURE) - .help("Enable an unstable feature") - .value_name("UNSTABLE_FEATURE") - .action(ArgAction::Append), - ) - .arg( - Arg::new(BUILD_STD) - .long(BUILD_STD) - .help("Enable building the standard library.") - .action(ArgAction::SetTrue), - ); - app -} - -pub trait KaniCompilerParser { - fn reachability_type(&self) -> ReachabilityType; -} - -impl KaniCompilerParser for ArgMatches { - fn reachability_type(&self) -> ReachabilityType { - self.get_one::(REACHABILITY) - .map_or(ReachabilityType::None, |arg| ReachabilityType::from_str(arg).unwrap()) - } -} - -/// Return whether we should run our flavour of the compiler, and which arguments to pass to rustc. -/// -/// We add a `--kani-compiler` argument to run the Kani version of the compiler, which needs to be -/// filtered out before passing the arguments to rustc. -/// -/// All other Kani arguments are today located inside `--llvm-args`. -pub fn is_kani_compiler(args: Vec) -> (bool, Vec) { - assert!(!args.is_empty(), "Arguments should always include executable name"); - const KANI_COMPILER: &str = "--kani-compiler"; - let mut has_kani_compiler = false; - let new_args = args - .into_iter() - .filter(|arg| { - if arg == KANI_COMPILER { - has_kani_compiler = true; - false - } else { - true - } - }) - .collect(); - (has_kani_compiler, new_args) -} - -#[cfg(test)] -mod parser_test { - use super::*; - - #[test] - fn test_rustc_version() { - let args = vec!["kani-compiler", "-V"]; - let matches = parser().get_matches_from(args); - assert!(matches.get_flag("rustc-version")); - } - - #[test] - fn test_kani_flags() { - let args = vec!["kani-compiler", "--goto-c", "--kani-lib", "some/path"]; - let matches = parser().get_matches_from(args); - assert!(matches.get_flag("goto-c")); - assert_eq!(matches.get_one::("kani-lib"), Some(&"some/path".to_string())); - } - - #[test] - fn test_stubbing_flags() { - let args = vec!["kani-compiler", "--enable-stubbing"]; - let matches = parser().get_matches_from(args); - assert!(matches.get_flag("enable-stubbing")); - } - - #[test] - fn test_cargo_kani_hack_noop() { - let args = ["kani-compiler", "some/path"]; - let args = args.map(String::from); - let (is_kani, new_args) = is_kani_compiler(Vec::from(args.clone())); - assert_eq!(args.as_slice(), new_args.as_slice()); - assert!(!is_kani); - } - - #[test] - fn test_cargo_kani_hack_no_args() { - let args = ["kani_compiler", "some/path", "--kani-compiler"]; - let args = args.map(String::from); - let (is_kani, new_args) = is_kani_compiler(Vec::from(args.clone())); - assert_eq!(new_args.len(), 2, "New args should not include --kani-compiler"); - assert_eq!(new_args[0], args[0]); - assert_eq!(new_args[1], args[1]); - assert!(is_kani); - } -} diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index c19501c4a62e..87d25f1e8fc3 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -3,8 +3,7 @@ //! Module used to configure a compiler session. -use crate::parser; -use clap::ArgMatches; +use crate::args::Arguments; use rustc_errors::{ emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, ColorConfig, Diagnostic, TerminalUrl, @@ -13,9 +12,8 @@ use rustc_session::config::ErrorOutputType; use rustc_session::EarlyErrorHandler; use std::io::IsTerminal; use std::panic; -use std::str::FromStr; use std::sync::LazyLock; -use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Registry}; +use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry}; /// Environment variable used to control this session log tracing. const LOG_ENV_VAR: &str = "KANI_LOG"; @@ -69,7 +67,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + Send }); /// Initialize compiler session. -pub fn init_session(args: &ArgMatches, json_hook: bool) { +pub fn init_session(args: &Arguments, json_hook: bool) { // Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate // because we cannot control the RUSTC log format unless if we match the exact tracing // version used by RUSTC. @@ -86,15 +84,15 @@ pub fn init_session(args: &ArgMatches, json_hook: bool) { } /// Initialize the logger using the KANI_LOG environment variable and the --log-level argument. -fn init_logger(args: &ArgMatches) { +fn init_logger(args: &Arguments) { let filter = EnvFilter::from_env(LOG_ENV_VAR); - let filter = if let Some(log_level) = args.get_one::(parser::LOG_LEVEL) { - filter.add_directive(Directive::from_str(log_level).unwrap()) + let filter = if let Some(log_level) = &args.log_level { + filter.add_directive(log_level.clone()) } else { filter }; - if args.get_flag(parser::JSON_OUTPUT) { + if args.json_output { json_logs(filter); } else { hier_logs(args, filter); @@ -109,8 +107,8 @@ fn json_logs(filter: EnvFilter) { } /// Configure global logger to use a hierarchical view. -fn hier_logs(args: &ArgMatches, filter: EnvFilter) { - let use_colors = std::io::stdout().is_terminal() || args.get_flag(parser::COLOR_OUTPUT); +fn hier_logs(args: &Arguments, filter: EnvFilter) { + let use_colors = std::io::stdout().is_terminal() || args.color_output; let subscriber = Registry::default().with(filter); let subscriber = subscriber.with( tracing_subscriber::fmt::layer()