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