From 06a289e9b2eccff77a1a627f8ee1ef637d694a1b Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Wed, 26 Oct 2022 20:07:31 +0000 Subject: [PATCH] Add `--codegen-pub-fns` and use it from `assess` --- kani-driver/src/args.rs | 27 ++++++++++++++++++++++++++- kani-driver/src/assess.rs | 13 +++++++++++-- kani-driver/src/call_cargo.rs | 20 ++++++++++---------- kani-driver/src/call_single_file.rs | 15 ++++++++------- 4 files changed, 55 insertions(+), 20 deletions(-) diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 48e5daccdeda..5dae51f56407 100644 --- a/kani-driver/src/args.rs +++ b/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 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 { 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 { 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 { diff --git a/kani-driver/src/assess.rs b/kani-driver/src/assess.rs index 2fd1ea0f33ba..0902ce00f1f1 100644 --- a/kani-driver/src/assess.rs +++ b/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)); diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 2fc3f3558708..a8f00cae5577 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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 = 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. diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 1e7d15c526b2..1cc5c02a1454 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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