Use the clap derive API for the command line arguments of `kani-com…

…piler` (model-checking#2689)

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"}

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<String>,
+ #[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<Directive>,
+ #[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<String>,
+ #[clap(long)]
+ /// A legacy flag that is now ignored.
+ goto_c: bool,
+}

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -178,7 +178,7 @@ impl<'tcx> GotocCtx<'tcx> {
  span: Option<Span>,
  ) -> (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

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() {

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.

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,
  );
  }
  }

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,

kani-compiler/src/kani_compiler.rs

@@ -15,16 +15,17 @@
 //! 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;
 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::<HashMap<_, _>>();
 
  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::<String>(parser::UNSTABLE_FEATURE) {
- queries.unstable_features = features.cloned().collect::<Vec<_>>();
- }
 
- 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)
  });
  }

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);
  }
  }

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

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<String>,
- /// 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<Arguments>,
  /// Information about all target harnesses.
  pub harnesses_info: HashMap<DefPathHash, PathBuf>,
 }
@@ -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")
+ }
 }