Add --codegen-pub-fns and use it from assess

kani-driver/src/args.rs

@@ -137,6 +137,12 @@ pub struct KaniArgs {
     #[structopt(long, hidden_short_help(true))]
     pub only_codegen: bool,
 
+    /// 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.
+    #[structopt(long, hidden = true, requires("enable-unstable"))]
+    pub codegen_pub_fns: bool,
+
     /// Disable the new MIR Linker. Using this option may result in missing symbols from the
     /// `std` library. See <https://github.com/model-checking/kani/issues/1213> for more details.
     #[structopt(long, hidden = true)]
@@ -242,11 +248,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
@@ -255,6 +262,18 @@ impl KaniArgs {
         }
     }
 
+    /// Determine which symbols Kani should codegen (i.e. by slicing away symbols
+    /// that are considered unreachable.)
+    pub fn reachability_mode(&self) -> ReachabilityMode {
+        if self.legacy_linker {
+            ReachabilityMode::Legacy
+        } else if self.function.is_some() || self.codegen_pub_fns {
+            ReachabilityMode::AllPubFns
+        } else {
+            ReachabilityMode::ProofHarnesses
+        }
+    }
+
     /// Computes how many threads should be used to verify harnesses.
     pub fn jobs(&self) -> Option<usize> {
         match self.jobs {
@@ -265,6 +284,12 @@ impl KaniArgs {
     }
 }
 
+pub enum ReachabilityMode {
+    Legacy,
+    ProofHarnesses,
+    AllPubFns,
+}
+
 arg_enum! {
     #[derive(Copy, Clone, Debug, PartialEq, Eq)]
     pub enum ConcretePlaybackMode {

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.args.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,14 @@ 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.
+
     // 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

@@ -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.args.reachability_mode() {
+            crate::args::ReachabilityMode::Legacy => {
+                // For this mode, we change `kani_args` not `pkg_args`
+                kani_args.push("--reachability=legacy".into());
+            }
+            crate::args::ReachabilityMode::ProofHarnesses => {
+                pkg_args.extend(["--".into(), "--reachability=harnesses".into()]);
+            }
+            crate::args::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

@@ -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.args.reachability_mode() {
+                crate::args::ReachabilityMode::Legacy => "--reachability=legacy",
+                crate::args::ReachabilityMode::ProofHarnesses => "--reachability=harnesses",
+                crate::args::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