Skip to content

Commit 6997afb

Browse files
author
Carolyn Zech
committed
Print tables of which functions we verified and which we skipped
1 parent 6f946bb commit 6997afb

File tree

12 files changed

+352
-86
lines changed

12 files changed

+352
-86
lines changed

‎kani-driver/src/autoharness/mod.rs‎

Lines changed: 103 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,89 @@
44
use std::str::FromStr;
55

66
use crate::args::Timeout;
7+
use crate::args::autoharness_args::{CargoAutoharnessArgs, StandaloneAutoharnessArgs};
78
use crate::call_cbmc::VerificationStatus;
89
use crate::call_single_file::to_rustc_arg;
910
use crate::harness_runner::HarnessResult;
1011
use crate::session::KaniSession;
12+
use crate::{InvocationType, print_kani_version, project, verify_project};
1113
use anyhow::Result;
14+
use comfy_table::Table as PrettyTable;
15+
use kani_metadata::{AutoHarnessSkipReason, KaniMetadata};
1216

1317
const AUTOHARNESS_TIMEOUT: &str = "30s";
1418
const LOOP_UNWIND_DEFAULT: u32 = 20;
1519

20+
pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> {
21+
let mut session = KaniSession::new(args.verify_opts)?;
22+
session.enable_autoharness();
23+
session.add_default_bounds();
24+
session.add_auto_harness_args(
25+
args.common_autoharness_args.include_function,
26+
args.common_autoharness_args.exclude_function,
27+
);
28+
let project = project::cargo_project(&mut session, false)?;
29+
let metadata = project.metadata.clone();
30+
let res = verify_project(project, session);
31+
print_skipped_fns(metadata);
32+
res
33+
}
34+
35+
pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> {
36+
let mut session = KaniSession::new(args.verify_opts)?;
37+
session.enable_autoharness();
38+
session.add_default_bounds();
39+
session.add_auto_harness_args(
40+
args.common_autoharness_args.include_function,
41+
args.common_autoharness_args.exclude_function,
42+
);
43+
44+
if !session.args.common_args.quiet {
45+
print_kani_version(InvocationType::Standalone);
46+
}
47+
48+
let project = project::standalone_project(&args.input, args.crate_name, &session)?;
49+
let metadata = project.metadata.clone();
50+
let res = verify_project(project, session);
51+
print_skipped_fns(metadata);
52+
res
53+
}
54+
55+
/// Print a table of the functions that we skipped and why.
56+
fn print_skipped_fns(metadata: Vec<KaniMetadata>) {
57+
let mut skipped_fns = PrettyTable::new();
58+
skipped_fns.set_header(vec!["Skipped Function", "Reason for Skipping"]);
59+
60+
for md in metadata {
61+
let skipped_md = md.autoharness_skipped_fns.unwrap();
62+
skipped_fns.add_rows(skipped_md.into_iter().filter_map(|(func, reason)| match reason {
63+
AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => {
64+
Some(vec![func, format!("{}: {}", reason, args.join(", "))])
65+
}
66+
AutoHarnessSkipReason::GenericFn
67+
| AutoHarnessSkipReason::NoBody
68+
| AutoHarnessSkipReason::UserFilter => Some(vec![func, reason.to_string()]),
69+
// We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation.
70+
// For those we don't insert during instrumentation that are in this category (manual harnesses or Kani trait implementations),
71+
// it should be obvious that we wouldn't generate harnesses, so reporting those functions as "skipped" is unlikely to be useful.
72+
AutoHarnessSkipReason::KaniImpl => None,
73+
}));
74+
}
75+
76+
if skipped_fns.is_empty() {
77+
println!(
78+
"\nSkipped Functions: None. Kani generated automatic harnesses for all functions in the package."
79+
);
80+
return;
81+
}
82+
83+
println!("\nKani did not generate automatic harnesses for the following functions.");
84+
println!(
85+
"If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832"
86+
);
87+
println!("{skipped_fns}");
88+
}
89+
1690
impl KaniSession {
1791
/// Enable autoharness mode.
1892
pub fn enable_autoharness(&mut self) {
@@ -52,48 +126,50 @@ impl KaniSession {
52126
let failing = failures.len();
53127
let total = succeeding + failing;
54128

55-
// TODO: it would be nice if we had access to which functions the user included/excluded here
56-
// so that we could print a comparison for them of any of the included functions that we skipped.
57-
println!("Autoharness Summary:");
58-
println!(
59-
"Note that Kani will only generate an automatic harness for a function if it determines that each of its arguments implement the Arbitrary trait."
60-
);
61-
println!(
62-
"Examine the summary closely to determine which functions were automatically verified."
63-
);
64-
if failing > 0 {
65-
println!(
66-
"Also note that Kani sets default --harness-timeout of {AUTOHARNESS_TIMEOUT} and --default-unwind of {LOOP_UNWIND_DEFAULT}."
67-
);
68-
println!(
69-
"If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract)."
70-
);
71-
}
129+
println!("\nAutoharness Summary:");
130+
131+
let mut verified_fns = PrettyTable::new();
132+
verified_fns.set_header(vec![
133+
"Selected Function",
134+
"Kind of Automatic Harness",
135+
"Verification Result",
136+
]);
72137

73-
// Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place.
74138
for success in successes {
75-
println!("Verification succeeded for - {}", success.harness.pretty_name);
139+
verified_fns.add_row(vec![
140+
success.harness.pretty_name.clone(),
141+
success.harness.attributes.kind.to_string(),
142+
success.result.status.to_string(),
143+
]);
76144
}
77145

78146
for failure in failures {
79-
println!("Verification failed for - {}", failure.harness.pretty_name);
147+
verified_fns.add_row(vec![
148+
failure.harness.pretty_name.clone(),
149+
failure.harness.attributes.kind.to_string(),
150+
failure.result.status.to_string(),
151+
]);
80152
}
81153

82-
if total > 0 {
154+
println!("{verified_fns}");
155+
156+
if failing > 0 {
83157
println!(
84-
"Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
158+
"Note that `kani autoharness` sets default --harness-timeout of {AUTOHARNESS_TIMEOUT} and --default-unwind of {LOOP_UNWIND_DEFAULT}."
85159
);
86-
} else {
87160
println!(
88-
"No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."
161+
"If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract)."
89162
);
163+
}
164+
165+
if total > 0 {
90166
println!(
91-
"If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive."
167+
"Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
92168
);
169+
} else {
170+
println!("No functions were eligible for automatic verification.");
93171
}
94172

95-
// Manual harness summary may come afterward, so separate them with a new line.
96-
println!();
97173
Ok(())
98174
}
99175
}

‎kani-driver/src/call_cbmc.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ use std::fmt::Write;
1212
use std::path::Path;
1313
use std::sync::OnceLock;
1414
use std::time::{Duration, Instant};
15+
use strum_macros::Display;
1516
use tokio::process::Command as TokioCommand;
1617

1718
use crate::args::common::Verbosity;
@@ -29,7 +30,7 @@ use crate::util::render_command;
2930
/// Note: Kissat was marginally better, but it is an external solver which could be more unstable.
3031
static DEFAULT_SOLVER: CbmcSolver = CbmcSolver::Cadical;
3132

32-
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
33+
#[derive(Clone, Copy, Debug, Display, PartialEq, Eq)]
3334
pub enum VerificationStatus {
3435
Success,
3536
Failure,

‎kani-driver/src/harness_runner.rs‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -246,10 +246,6 @@ impl KaniSession {
246246
let (automatic, manual): (Vec<_>, Vec<_>) =
247247
results.iter().partition(|r| r.harness.is_automatically_generated);
248248

249-
if self.auto_harness {
250-
self.print_autoharness_summary(automatic)?;
251-
}
252-
253249
let (successes, failures): (Vec<_>, Vec<_>) =
254250
manual.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
255251

@@ -269,10 +265,8 @@ impl KaniSession {
269265
}
270266
}
271267

272-
// We currently omit a summary if there was just 1 harness
273-
if failing > 0 {
274-
println!("Manual Harness Summary:");
275-
}
268+
println!("Manual Harness Summary:");
269+
276270
for failure in failures.iter() {
277271
println!("Verification failed for - {}", failure.harness.pretty_name);
278272
}
@@ -304,7 +298,11 @@ impl KaniSession {
304298
self.show_coverage_summary()?;
305299
}
306300

307-
if failing > 0 {
301+
if self.auto_harness {
302+
self.print_autoharness_summary(automatic)?;
303+
}
304+
305+
if failing > 0 && !self.auto_harness {
308306
// Failure exit code without additional error message
309307
drop(self);
310308
std::process::exit(1);

‎kani-driver/src/main.rs‎

Lines changed: 9 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ use std::ffi::OsString;
55
use std::process::ExitCode;
66

77
use anyhow::Result;
8+
use autoharness::{autoharness_cargo, autoharness_standalone};
89
use time::{OffsetDateTime, format_description};
910

1011
use args::{CargoKaniSubcommand, check_is_valid};
@@ -73,26 +74,21 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
7374
return list_cargo(*list_args, args.verify_opts);
7475
}
7576

77+
if let Some(CargoKaniSubcommand::Autoharness(autoharness_args)) = args.command {
78+
return autoharness_cargo(*autoharness_args);
79+
}
80+
7681
let mut session = match args.command {
7782
Some(CargoKaniSubcommand::Assess(assess_args)) => {
7883
let sess = session::KaniSession::new(args.verify_opts)?;
7984
return assess::run_assess(sess, *assess_args);
8085
}
81-
Some(CargoKaniSubcommand::Autoharness(args)) => {
82-
let mut sess = session::KaniSession::new(args.verify_opts)?;
83-
sess.enable_autoharness();
84-
sess.add_default_bounds();
85-
sess.add_auto_harness_args(
86-
args.common_autoharness_args.include_function,
87-
args.common_autoharness_args.exclude_function,
88-
);
89-
90-
sess
91-
}
9286
Some(CargoKaniSubcommand::Playback(args)) => {
9387
return playback_cargo(*args);
9488
}
95-
Some(CargoKaniSubcommand::List(_)) => unreachable!(),
89+
Some(CargoKaniSubcommand::Autoharness(_)) | Some(CargoKaniSubcommand::List(_)) => {
90+
unreachable!()
91+
}
9692
None => session::KaniSession::new(args.verify_opts)?,
9793
};
9894

@@ -115,20 +111,7 @@ fn standalone_main() -> Result<()> {
115111

116112
let (session, project) = match args.command {
117113
Some(StandaloneSubcommand::Autoharness(args)) => {
118-
let mut session = KaniSession::new(args.verify_opts)?;
119-
session.enable_autoharness();
120-
session.add_default_bounds();
121-
session.add_auto_harness_args(
122-
args.common_autoharness_args.include_function,
123-
args.common_autoharness_args.exclude_function,
124-
);
125-
126-
if !session.args.common_args.quiet {
127-
print_kani_version(InvocationType::Standalone);
128-
}
129-
130-
let project = project::standalone_project(&args.input, args.crate_name, &session)?;
131-
(session, project)
114+
return autoharness_standalone(*args);
132115
}
133116
Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args),
134117
Some(StandaloneSubcommand::List(list_args)) => {

‎kani_metadata/src/harness.rs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
use crate::CbmcSolver;
55
use serde::{Deserialize, Serialize};
66
use std::path::PathBuf;
7+
use strum_macros::Display;
78

89
/// A CBMC-level `assigns` contract that needs to be enforced on a function.
910
#[derive(Clone, Debug, Serialize, Deserialize, PartialEq)]
@@ -59,13 +60,16 @@ pub struct HarnessAttributes {
5960
pub verified_stubs: Vec<String>,
6061
}
6162

62-
#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
63+
#[derive(Clone, Eq, PartialEq, Debug, Display, Serialize, Deserialize)]
6364
pub enum HarnessKind {
6465
/// Function was annotated with `#[kani::proof]`.
66+
#[strum(serialize = "#[kani::proof]")]
6567
Proof,
6668
/// Function was annotated with `#[kani::proof_for_contract(target_fn)]`.
69+
#[strum(serialize = "#[kani::proof_for_contract]")]
6770
ProofForContract { target_fn: String },
6871
/// This is a test harness annotated with `#[test]`.
72+
#[strum(serialize = "#[test]")]
6973
Test,
7074
}
7175

‎tests/script-based-pre/cargo_autoharness_contracts/contracts.expected‎

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,9 +20,25 @@ arithmetic_overflow\
2020
- Status: SUCCESS\
2121
- Description: "attempt to compute `unchecked_mul` which would overflow"
2222

23-
Verification succeeded for - should_pass::unchecked_mul
24-
Verification succeeded for - should_pass::has_loop_contract
25-
Verification succeeded for - should_pass::has_recursion_gcd
26-
Verification succeeded for - should_pass::div
27-
Verification failed for - should_fail::max
23+
Manual Harness Summary:
24+
No proof harnesses (functions with #[kani::proof]) were found to verify.
25+
26+
Autoharness Summary:
27+
+--------------------------------+-----------------------------+---------------------+
28+
| Selected Function | Kind of Automatic Harness | Verification Result |
29+
+====================================================================================+
30+
| should_pass::unchecked_mul | #[kani::proof_for_contract] | Success |
31+
|--------------------------------+-----------------------------+---------------------|
32+
| should_pass::has_loop_contract | #[kani::proof] | Success |
33+
|--------------------------------+-----------------------------+---------------------|
34+
| should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success |
35+
|--------------------------------+-----------------------------+---------------------|
36+
| should_pass::div | #[kani::proof_for_contract] | Success |
37+
|--------------------------------+-----------------------------+---------------------|
38+
| should_fail::max | #[kani::proof_for_contract] | Failure |
39+
+--------------------------------+-----------------------------+---------------------+
40+
Note that `kani autoharness` sets default --harness-timeout of 30s and --default-unwind of 20.
41+
If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract).
2842
Complete - 4 successfully verified functions, 1 failures, 5 total.
43+
44+
Skipped Functions: None. Kani generated automatic harnesses for all functions in the package.

‎tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,14 @@
11
Autoharness: Checking function yes_harness against all possible inputs...
2-
Verification succeeded for - yes_harness
2+
3+
Manual Harness Summary:
4+
No proof harnesses (functions with #[kani::proof]) were found to verify.
5+
6+
Autoharness Summary:
7+
+-------------------+---------------------------+---------------------+
8+
| Selected Function | Kind of Automatic Harness | Verification Result |
9+
+=====================================================================+
10+
| yes_harness | #[kani::proof] | Success |
11+
+-------------------+---------------------------+---------------------+
312
Complete - 1 successfully verified functions, 0 failures, 1 total.
13+
14+
Skipped Functions: None. Kani generated automatic harnesses for all functions in the package.

‎tests/script-based-pre/cargo_autoharness_exclude/exclude.expected‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,23 @@
11
Autoharness: Checking function include::simple against all possible inputs...
22
VERIFICATION:- SUCCESSFUL
3-
Verification succeeded for - include::simple
4-
Complete - 1 successfully verified functions, 0 failures, 1 total.
3+
4+
Manual Harness Summary:
5+
No proof harnesses (functions with #[kani::proof]) were found to verify.
6+
7+
Autoharness Summary:
8+
+-------------------+---------------------------+---------------------+
9+
| Selected Function | Kind of Automatic Harness | Verification Result |
10+
+=====================================================================+
11+
| include::simple | #[kani::proof] | Success |
12+
+-------------------+---------------------------+---------------------+
13+
Complete - 1 successfully verified functions, 0 failures, 1 total.
14+
15+
Kani did not generate automatic harnesses for the following functions.
16+
If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832
17+
+------------------+--------------------------------+
18+
| Skipped Function | Reason for Skipping |
19+
+===================================================+
20+
| excluded::simple | Did not match provided filters |
21+
|------------------+--------------------------------|
22+
| include::generic | Generic Function |
23+
+------------------+--------------------------------+

0 commit comments

Comments
 (0)