Simplify compiler queries structure (internal) (#2486)

Cargo.lock

@@ -529,7 +529,6 @@ dependencies = [
  "home",
  "itertools",
  "kani_metadata",
- "kani_queries",
  "lazy_static",
  "num",
  "regex",
@@ -601,15 +600,6 @@ dependencies = [
  "strum_macros",
 ]
 
-[[package]]
-name = "kani_queries"
-version = "0.29.0"
-dependencies = [
- "strum",
- "strum_macros",
- "tracing",
-]
-
 [[package]]
 name = "lazy_static"
 version = "1.4.0"

kani-compiler/Cargo.toml

@@ -14,7 +14,6 @@ cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional =
 clap = { version = "4.1.3", features = ["cargo"] }
 home = "0.5"
 itertools = "0.10"
-kani_queries = {path = "kani_queries"}
 kani_metadata = {path = "../kani_metadata"}
 lazy_static = "1.4.0"
 num = { version = "0.4.0", optional = true }

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

@@ -21,7 +21,6 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
-use kani_queries::UserInput;
 use rustc_span::Span;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
@@ -151,7 +150,7 @@ impl<'tcx> GotocCtx<'tcx> {
         span: Option<Span>,
     ) -> (String, Stmt) {
         let loc = self.codegen_caller_span(&span);
-        if self.queries.get_check_assertion_reachability() {
+        if self.queries.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/foreign_function.rs

@@ -14,7 +14,6 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle;
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::{InternString, InternedString};
-use kani_queries::UserInput;
 use lazy_static::lazy_static;
 use rustc_middle::ty::Instance;
 use rustc_target::abi::call::Conv;
@@ -90,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.get_unstable_features().contains(&"c-ffi".to_string())
+        self.queries.unstable_features.contains(&"c-ffi".to_string())
     }
 
     /// Generate code for a foreign function shim.

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -14,6 +14,7 @@ use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_const_crate_items, filter_crate_items,
 };
+use crate::kani_queries::{QueryDb, ReachabilityType};
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
 use cbmc::RoundingMode;
@@ -22,7 +23,6 @@ use kani_metadata::artifact::convert_type;
 use kani_metadata::CompilerArtifactStub;
 use kani_metadata::UnsupportedFeature;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
-use kani_queries::{QueryDb, ReachabilityType, UserInput};
 use rustc_codegen_ssa::back::archive::{
     get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder,
 };
@@ -167,9 +167,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().get_output_pretty_json();
+            let pretty = self.queries.lock().unwrap().output_pretty_json;
             write_file(&symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
-            if gcx.queries.get_write_json_symtab() {
+            if gcx.queries.write_json_symtab {
                 write_file(&symtab_goto, ArtifactType::SymTab, &gcx.symbol_table, pretty);
                 symbol_table_to_gotoc(&tcx, &symtab_goto);
             } else {
@@ -220,7 +220,7 @@ impl CodegenBackend for GotocCodegenBackend {
         let queries = self.queries.lock().unwrap().clone();
         check_target(tcx.sess);
         check_options(tcx.sess);
-        check_crate_items(tcx, queries.get_ignore_global_asm());
+        check_crate_items(tcx, queries.ignore_global_asm);
 
         // Codegen all items that need to be processed according to the selected reachability mode:
         //
@@ -229,7 +229,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.get_reachability_analysis();
+        let reachability = queries.reachability_analysis;
         let mut results = GotoCodegenResults::new(tcx, reachability);
         match reachability {
             ReachabilityType::Harnesses => {
@@ -304,7 +304,7 @@ impl CodegenBackend for GotocCodegenBackend {
                 &base_filename,
                 ArtifactType::Metadata,
                 &results.generate_metadata(),
-                queries.get_output_pretty_json(),
+                queries.output_pretty_json,
             );
         }
         codegen_results(tcx, rustc_metadata, &results.machine_model)

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -18,11 +18,11 @@ use super::vtable_ctx::VtableCtx;
 use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks};
 use crate::codegen_cprover_gotoc::utils::full_crate_name;
 use crate::codegen_cprover_gotoc::UnsupportedConstructs;
+use crate::kani_queries::QueryDb;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{InternedString, MachineModel};
 use kani_metadata::HarnessMetadata;
-use kani_queries::{QueryDb, UserInput};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::mir::interpret::Allocation;
 use rustc_middle::span_bug;
@@ -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.get_emit_vtable_restrictions();
+        let emit_vtable_restrictions = queries.emit_vtable_restrictions;
         GotocCtx {
             tcx,
             queries,

kani-compiler/src/kani_compiler.rs

@@ -18,11 +18,11 @@
 #[cfg(feature = "cprover")]
 use crate::codegen_cprover_gotoc::GotocCodegenBackend;
 use crate::kani_middle::stubbing;
+use crate::kani_queries::{QueryDb, ReachabilityType};
 use crate::parser::{self, KaniCompilerParser};
 use crate::session::init_session;
 use clap::ArgMatches;
 use itertools::Itertools;
-use kani_queries::{QueryDb, ReachabilityType, UserInput};
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_driver::{Callbacks, Compilation, RunCompiler};
@@ -136,25 +136,23 @@ impl Callbacks for KaniCompiler {
 
             // Configure queries.
             let queries = &mut (*self.queries.lock().unwrap());
-            queries.set_emit_vtable_restrictions(matches.get_flag(parser::RESTRICT_FN_PTRS));
-            queries
-                .set_check_assertion_reachability(matches.get_flag(parser::ASSERTION_REACH_CHECKS));
-            queries.set_output_pretty_json(matches.get_flag(parser::PRETTY_OUTPUT_FILES));
-            queries.set_ignore_global_asm(matches.get_flag(parser::IGNORE_GLOBAL_ASM));
-            queries.set_write_json_symtab(
-                cfg!(feature = "write_json_symtab") || matches.get_flag(parser::WRITE_JSON_SYMTAB),
-            );
-            queries.set_reachability_analysis(matches.reachability_type());
+            queries.emit_vtable_restrictions = matches.get_flag(parser::RESTRICT_FN_PTRS);
+            queries.check_assertion_reachability = matches.get_flag(parser::ASSERTION_REACH_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();
 
             if let Some(features) = matches.get_many::<String>(parser::UNSTABLE_FEATURE) {
-                queries.set_unstable_features(&features.cloned().collect::<Vec<_>>());
+                queries.unstable_features = features.cloned().collect::<Vec<_>>();
             }
 
             // If appropriate, collect and set the stub mapping.
             if matches.get_flag(parser::ENABLE_STUBBING)
-                && queries.get_reachability_analysis() == ReachabilityType::Harnesses
+                && queries.reachability_analysis == ReachabilityType::Harnesses
             {
-                queries.set_stubbing_enabled(true);
+                queries.stubbing_enabled = true;
             }
             self.args = Some(matches);
             debug!(?queries, "config end");
@@ -167,7 +165,7 @@ impl Callbacks for KaniCompiler {
         _compiler: &rustc_interface::interface::Compiler,
         rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
     ) -> Compilation {
-        if self.stubs.is_none() && self.queries.lock().unwrap().get_stubbing_enabled() {
+        if self.stubs.is_none() && self.queries.lock().unwrap().stubbing_enabled {
             rustc_queries.global_ctxt().unwrap().enter(|tcx| {
                 let stubs = self.stubs.insert(self.collect_stubs(tcx));
                 debug!(?stubs, "after_analysis");

kani-compiler/src/kani_middle/mod.rs

@@ -5,7 +5,7 @@
 
 use std::collections::HashSet;
 
-use kani_queries::{QueryDb, UserInput};
+use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
 use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::span_bug;
@@ -66,7 +66,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
         let def_id = item.def_id();
         if !def_ids.contains(&def_id) {
             // Check if any unstable attribute was reached.
-            check_unstable_features(tcx, queries.get_unstable_features(), def_id);
+            check_unstable_features(tcx, &queries.unstable_features, def_id);
             def_ids.insert(def_id);
         }
     }

kani-compiler/src/kani_middle/provide.rs

@@ -7,7 +7,7 @@
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::stubbing;
 use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items;
-use kani_queries::{QueryDb, UserInput};
+use crate::kani_queries::QueryDb;
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_interface;
 use rustc_middle::{
@@ -19,7 +19,7 @@ use rustc_middle::{
 /// the present crate.
 pub fn provide(providers: &mut Providers, queries: &QueryDb) {
     providers.optimized_mir = run_mir_passes;
-    if queries.get_stubbing_enabled() {
+    if queries.stubbing_enabled {
         providers.collect_and_partition_mono_items = collect_and_partition_mono_items;
     }
 }