Change kani-compiler to use -C llvm-args for Kani specific flags (rust-lang#2185)

Changed how `kani-driver` passess arguments to `kani-compiler`. We now have one option, `--kani-compiler`, that changes how we configure rustc, and all the other Kani specific arguments are added to `-C llvm-args`. We no longer need to keep the arguments in a certain order or need to use KANI_FLAGS environment variable.

In the `kani-compiler` we no longer parse the arguments before invoking rustc, we initially detect whether users want to use the Kani flavour of the compiler by looking for a `--kani-compiler` flag.

If `--kani-compiler` flag is found, we configure rustc's driver to use our custom backend and our custom callback. We then invoke the driver with the command line arguments excluding the `--kani-compiler` flag. During the callback configuration we initialize the Kani specific flags that are passed via `-C llvm-args`.

If there isn't any `--kani-compiler` flag, we just invoke rustc with all the given arguments.


Co-authored-by: Zyad Hassan <[email protected]>

Author: celinval

kani-compiler/kani_queries/src/lib.rs

@@ -1,19 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use std::sync::atomic::{AtomicBool, Ordering};
-#[cfg(not(feature = "unsound_experiments"))]
-use std::sync::Mutex;
+use std::sync::{Arc, Mutex};
 use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 
 #[cfg(feature = "unsound_experiments")]
 mod unsound_experiments;
 
 #[cfg(feature = "unsound_experiments")]
-use {
-    crate::unsound_experiments::UnsoundExperiments,
-    std::sync::{Arc, Mutex},
-};
+use crate::unsound_experiments::UnsoundExperiments;
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
@@ -56,60 +51,78 @@ pub trait UserInput {
     fn get_stubbing_enabled(&self) -> bool;
 
     #[cfg(feature = "unsound_experiments")]
-    fn get_unsound_experiments(&self) -> Arc<Mutex<UnsoundExperiments>>;
+    fn get_unsound_experiments(&self) -> UnsoundExperiments;
+    #[cfg(feature = "unsound_experiments")]
+    fn set_unsound_experiments(&mut self, experiments: UnsoundExperiments);
 }
 
-#[derive(Debug, Default)]
+/// This structure should only be used behind a synchronized reference or a snapshot.
+#[derive(Debug, Clone)]
 pub struct QueryDb {
-    check_assertion_reachability: AtomicBool,
-    emit_vtable_restrictions: AtomicBool,
-    json_pretty_print: AtomicBool,
-    ignore_global_asm: AtomicBool,
-    reachability_analysis: Mutex<ReachabilityType>,
+    check_assertion_reachability: bool,
+    emit_vtable_restrictions: bool,
+    json_pretty_print: bool,
+    ignore_global_asm: bool,
+    reachability_analysis: ReachabilityType,
     stubbing_enabled: bool,
     #[cfg(feature = "unsound_experiments")]
-    unsound_experiments: Arc<Mutex<UnsoundExperiments>>,
+    unsound_experiments: UnsoundExperiments,
+}
+
+impl QueryDb {
+    pub fn new() -> Arc<Mutex<QueryDb>> {
+        Arc::new(Mutex::new(QueryDb {
+            check_assertion_reachability: false,
+            emit_vtable_restrictions: false,
+            json_pretty_print: false,
+            ignore_global_asm: false,
+            reachability_analysis: ReachabilityType::None,
+            stubbing_enabled: false,
+            #[cfg(feature = "unsound_experiments")]
+            unsound_experiments: unsound_experiments::UnsoundExperiments { zero_init_vars: false },
+        }))
+    }
 }
 
 impl UserInput for QueryDb {
     fn set_emit_vtable_restrictions(&mut self, restrictions: bool) {
-        self.emit_vtable_restrictions.store(restrictions, Ordering::Relaxed);
+        self.emit_vtable_restrictions = restrictions;
     }
 
     fn get_emit_vtable_restrictions(&self) -> bool {
-        self.emit_vtable_restrictions.load(Ordering::Relaxed)
+        self.emit_vtable_restrictions
     }
 
     fn set_check_assertion_reachability(&mut self, reachability: bool) {
-        self.check_assertion_reachability.store(reachability, Ordering::Relaxed);
+        self.check_assertion_reachability = reachability;
     }
 
     fn get_check_assertion_reachability(&self) -> bool {
-        self.check_assertion_reachability.load(Ordering::Relaxed)
+        self.check_assertion_reachability
     }
 
     fn set_output_pretty_json(&mut self, pretty_json: bool) {
-        self.json_pretty_print.store(pretty_json, Ordering::Relaxed);
+        self.json_pretty_print = pretty_json;
     }
 
     fn get_output_pretty_json(&self) -> bool {
-        self.json_pretty_print.load(Ordering::Relaxed)
+        self.json_pretty_print
     }
 
     fn set_ignore_global_asm(&mut self, global_asm: bool) {
-        self.ignore_global_asm.store(global_asm, Ordering::Relaxed);
+        self.ignore_global_asm = global_asm;
     }
 
     fn get_ignore_global_asm(&self) -> bool {
-        self.ignore_global_asm.load(Ordering::Relaxed)
+        self.ignore_global_asm
     }
 
     fn set_reachability_analysis(&mut self, reachability: ReachabilityType) {
-        *self.reachability_analysis.get_mut().unwrap() = reachability;
+        self.reachability_analysis = reachability;
     }
 
     fn get_reachability_analysis(&self) -> ReachabilityType {
-        *self.reachability_analysis.lock().unwrap()
+        self.reachability_analysis
     }
 
     fn set_stubbing_enabled(&mut self, stubbing_enabled: bool) {
@@ -121,7 +134,12 @@ impl UserInput for QueryDb {
     }
 
     #[cfg(feature = "unsound_experiments")]
-    fn get_unsound_experiments(&self) -> Arc<Mutex<UnsoundExperiments>> {
-        self.unsound_experiments.clone()
+    fn get_unsound_experiments(&self) -> UnsoundExperiments {
+        self.unsound_experiments
+    }
+
+    #[cfg(feature = "unsound_experiments")]
+    fn set_unsound_experiments(&mut self, experiments: UnsoundExperiments) {
+        self.unsound_experiments = experiments
     }
 }

kani-compiler/kani_queries/src/unsound_experiments.rs

@@ -3,7 +3,7 @@
 
 #![cfg(feature = "unsound_experiments")]
 
-#[derive(Debug, Default)]
+#[derive(Debug, Clone, Copy, Default)]
 pub struct UnsoundExperiments {
     /// Zero initilize variables.
     /// This is useful for experiments to see whether assigning constant values produces better

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -45,19 +45,23 @@ use std::io::Write as IoWrite;
 use std::iter::FromIterator;
 use std::path::{Path, PathBuf};
 use std::process::Command;
-use std::rc::Rc;
+use std::sync::{Arc, Mutex};
 use std::time::Instant;
 use tempfile::Builder as TempFileBuilder;
 use tracing::{debug, error, info};
 
 #[derive(Clone)]
 pub struct GotocCodegenBackend {
-    queries: Rc<QueryDb>,
+    /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc`
+    /// initialization, which may happen after this object is created.
+    /// Since we don't have any guarantees on when the compiler creates the Backend object, neither
+    /// in which thread it will be used, we prefer to explicitly synchronize any query access.
+    queries: Arc<Mutex<QueryDb>>,
 }
 
 impl GotocCodegenBackend {
-    pub fn new(queries: &Rc<QueryDb>) -> Self {
-        GotocCodegenBackend { queries: Rc::clone(queries) }
+    pub fn new(queries: Arc<Mutex<QueryDb>>) -> Self {
+        GotocCodegenBackend { queries }
     }
 }
 
@@ -67,7 +71,7 @@ impl CodegenBackend for GotocCodegenBackend {
     }
 
     fn provide(&self, providers: &mut Providers) {
-        provide::provide(providers, &self.queries);
+        provide::provide(providers, &self.queries.lock().unwrap());
     }
 
     fn provide_extern(&self, providers: &mut ty::query::ExternProviders) {
@@ -84,7 +88,7 @@ impl CodegenBackend for GotocCodegenBackend {
 
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions
-        let mut gcx = GotocCtx::new(tcx, self.queries.clone());
+        let mut gcx = GotocCtx::new(tcx, (*self.queries.lock().unwrap()).clone());
         check_target(tcx.sess);
         check_options(tcx.sess);
         check_crate_items(&gcx);
@@ -170,7 +174,7 @@ impl CodegenBackend for GotocCodegenBackend {
         if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() {
             let outputs = tcx.output_filenames(());
             let base_filename = outputs.output_path(OutputType::Object);
-            let pretty = self.queries.get_output_pretty_json();
+            let pretty = self.queries.lock().unwrap().get_output_pretty_json();
             write_file(&base_filename, ArtifactType::SymTab, &gcx.symbol_table, pretty);
             write_file(&base_filename, ArtifactType::TypeMap, &type_map, pretty);
             write_file(&base_filename, ArtifactType::Metadata, &metadata, pretty);

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

@@ -42,13 +42,13 @@ use rustc_target::abi::Endian;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use rustc_target::spec::Target;
 use std::path::Path;
-use std::rc::Rc;
 
 pub struct GotocCtx<'tcx> {
     /// the typing context
     pub tcx: TyCtxt<'tcx>,
-    /// the query system for kani
-    pub queries: Rc<QueryDb>,
+    /// a snapshot of the query values. The queries shouldn't change at this point,
+    /// so we just keep a copy.
+    pub queries: QueryDb,
     /// the generated symbol table for gotoc
     pub symbol_table: SymbolTable,
     pub hooks: GotocHooks<'tcx>,
@@ -79,7 +79,7 @@ pub struct GotocCtx<'tcx> {
 
 /// Constructor
 impl<'tcx> GotocCtx<'tcx> {
-    pub fn new(tcx: TyCtxt<'tcx>, queries: Rc<QueryDb>) -> GotocCtx<'tcx> {
+    pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> GotocCtx<'tcx> {
         let fhks = fn_hooks();
         let mm = machine_model_from_session(tcx.sess);
         let symbol_table = SymbolTable::new(mm);