Fix assess with the MIR linker by changing reachability modes (#1816)

kani-driver/src/args.rs

@@ -242,11 +242,12 @@ impl KaniArgs {
         // if we flip the default, this will become: !self.no_restrict_vtable
     }
 
+    /// Assertion reachability checks should be disabled when running with --visualize
     pub fn assertion_reach_checks(&self) -> bool {
-        // Turn them off when visualizing an error trace.
         !self.no_assertion_reach_checks && !self.visualize
     }
 
+    /// Suppress our default value, if the user has supplied it explicitly in --cbmc-args
     pub fn cbmc_object_bits(&self) -> Option<u32> {
         if self.cbmc_args.contains(&OsString::from("--object-bits")) {
             None

kani-driver/src/assess.rs

@@ -216,7 +216,12 @@ pub(crate) fn cargokani_assess_main(mut ctx: KaniSession) -> Result<()> {
     ctx.args.unwind = Some(1);
     ctx.args.tests = true;
     ctx.args.output_format = crate::args::OutputFormat::Terse;
-    ctx.args.jobs = Some(None); // -j, num_cpu
+    ctx.codegen_pub_fns = true;
+    if ctx.args.jobs.is_none() {
+        // assess will default to fully parallel instead of single-threaded.
+        // can be overridden with e.g. `cargo kani --enable-unstable -j 8 assess`
+        ctx.args.jobs = Some(None); // -j, num_cpu
+    }
 
     let outputs = ctx.cargo_build()?;
     let metadata = ctx.collect_kani_metadata(&outputs.metadata)?;
@@ -269,10 +274,15 @@ pub(crate) fn cargokani_assess_main(mut ctx: KaniSession) -> Result<()> {
     let results = runner.check_all_harnesses(&harnesses)?;
 
     // two tables we want to print:
-    // 1. "Reason for failure" map harness to reason, aggredate together
+    // 1. "Reason for failure" will count reasons why harnesses did not succeed
     //    e.g.  successs   6
     //          unwind     234
     println!("{}", build_failure_reasons_table(&results));
+
+    // TODO: Should add another interesting table: Count the actually hit constructs (e.g. 'try', 'InlineAsm', etc)
+    // The above table will just say "unsupported_construct   6" without telling us which constructs.
+    // Tracking issue: https://github.com/model-checking/kani/issues/1819
+
     // 2. "Test cases that might be good proof harness starting points"
     //    e.g.  All Successes and maybe Assertions?
     println!("{}", build_promising_tests_table(&results));

kani-driver/src/call_cargo.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::KaniArgs;
-use crate::session::KaniSession;
+use crate::session::{KaniSession, ReachabilityMode};
 use anyhow::{Context, Result};
 use cargo_metadata::{Metadata, MetadataCommand, Package};
 use std::ffi::OsString;
@@ -62,17 +62,17 @@ impl KaniSession {
 
         // Arguments that will only be passed to the target package.
         let mut pkg_args: Vec<OsString> = vec![];
-        if !self.args.legacy_linker {
-            // Only provide reachability flag to the target package.
-            pkg_args.push("--".into());
-            if self.args.function.is_some() {
-                pkg_args.push("--reachability=pub_fns".into());
-            } else {
-                pkg_args.push("--reachability=harnesses".into());
+        match self.reachability_mode() {
+            ReachabilityMode::Legacy => {
+                // For this mode, we change `kani_args` not `pkg_args`
+                kani_args.push("--reachability=legacy".into());
+            }
+            ReachabilityMode::ProofHarnesses => {
+                pkg_args.extend(["--".into(), "--reachability=harnesses".into()]);
+            }
+            ReachabilityMode::AllPubFns => {
+                pkg_args.extend(["--".into(), "--reachability=pub_fns".into()]);
             }
-        } else {
-            // Pass legacy reachability to the target package and its dependencies.
-            kani_args.push("--reachability=legacy".into());
         }
 
         // Only joing them at the end. All kani flags must come first.

kani-driver/src/call_single_file.rs

@@ -6,7 +6,7 @@ use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
-use crate::session::KaniSession;
+use crate::session::{KaniSession, ReachabilityMode};
 use crate::util::{alter_extension, guess_rlib_name};
 
 /// The outputs of kani-compiler operating on a single Rust source file.
@@ -48,13 +48,14 @@ impl KaniSession {
         }
 
         let mut kani_args = self.kani_specific_flags();
-        if self.args.legacy_linker {
-            kani_args.push("--reachability=legacy".into());
-        } else if self.args.function.is_some() {
-            kani_args.push("--reachability=pub_fns".into());
-        } else {
-            kani_args.push("--reachability=harnesses".into());
-        }
+        kani_args.push(
+            match self.reachability_mode() {
+                ReachabilityMode::Legacy => "--reachability=legacy",
+                ReachabilityMode::ProofHarnesses => "--reachability=harnesses",
+                ReachabilityMode::AllPubFns => "--reachability=pub_fns",
+            }
+            .into(),
+        );
 
         let mut rustc_args = self.kani_rustc_flags();
         // kani-compiler workaround part 1/2: *.symtab.json gets generated in the local

kani-driver/src/session.rs

@@ -14,6 +14,11 @@ pub struct KaniSession {
     /// The common command-line arguments
     pub args: KaniArgs,
 
+    /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from
+    /// a proof harness. Useful when attempting to verify things that were not annotated with kani
+    /// proof attributes.
+    pub codegen_pub_fns: bool,
+
     /// The location we found the 'kani_rustc' command
     pub kani_compiler: PathBuf,
     /// The location we found 'kani_lib.c'
@@ -41,6 +46,7 @@ impl KaniSession {
 
         Ok(KaniSession {
             args,
+            codegen_pub_fns: false,
             kani_compiler: install.kani_compiler()?,
             kani_lib_c: install.kani_lib_c()?,
             kani_c_stubs: install.kani_c_stubs()?,
@@ -54,6 +60,24 @@ impl KaniSession {
         let mut t = self.temporaries.lock().unwrap();
         t.extend(temps.iter().map(|p| (*p).to_owned()));
     }
+
+    /// Determine which symbols Kani should codegen (i.e. by slicing away symbols
+    /// that are considered unreachable.)
+    pub fn reachability_mode(&self) -> ReachabilityMode {
+        if self.args.legacy_linker {
+            ReachabilityMode::Legacy
+        } else if self.args.function.is_some() || self.codegen_pub_fns {
+            ReachabilityMode::AllPubFns
+        } else {
+            ReachabilityMode::ProofHarnesses
+        }
+    }
+}
+
+pub enum ReachabilityMode {
+    Legacy,
+    ProofHarnesses,
+    AllPubFns,
 }
 
 impl Drop for KaniSession {