Skip to content

Commit f3b5a97

Browse files
authored
Refactor harness running (#1684)
1 parent f6b86ec commit f3b5a97

File tree

8 files changed

+197
-146
lines changed

8 files changed

+197
-146
lines changed

kani-driver/src/cbmc_output_parser.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
//! Module for parsing CBMC's JSON output. In general, this output follows
55
//! the structure:
6-
//! ```
6+
//! ```text
77
//! [
88
//! Program,
99
//! Message,

kani-driver/src/concrete_playback.rs

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -213,16 +213,6 @@ impl KaniSession {
213213
}
214214
Ok(())
215215
}
216-
217-
/// Helper function to inform the user that they tried to generate concrete playback unit tests when there were no failing harnesses.
218-
pub fn inform_if_no_failed(&self, failed_harnesses: &[&HarnessMetadata]) {
219-
if self.args.concrete_playback.is_some() && !self.args.quiet && failed_harnesses.is_empty()
220-
{
221-
println!(
222-
"INFO: The concrete playback feature never generated unit tests because there were no failing harnesses."
223-
)
224-
}
225-
}
226216
}
227217

228218
/// Generate a unit test from a list of concrete values.

kani-driver/src/harness_runner.rs

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
use anyhow::Result;
5+
use kani_metadata::HarnessMetadata;
6+
use std::path::{Path, PathBuf};
7+
8+
use crate::call_cbmc::VerificationStatus;
9+
use crate::session::KaniSession;
10+
use crate::util::specialized_harness_name;
11+
12+
/// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
13+
/// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
14+
///
15+
/// This struct is basically just a nicer way of passing many arguments to [`Self::check_all_harnesses`]
16+
pub(crate) struct HarnessRunner<'sess> {
17+
/// The underlying kani session
18+
pub sess: &'sess KaniSession,
19+
/// The build CBMC goto binary for the "whole program" (will be specialized to each proof harness)
20+
pub linked_obj: &'sess Path,
21+
/// The directory we should output cbmc-viewer reports to
22+
pub report_base: &'sess Path,
23+
/// An unfortunate behavior difference between `kani` and `cargo kani`: `cargo kani` never deletes the specialized goto binaries, while `kani` does unless `--keep-temps` is provided
24+
pub retain_specialized_harnesses: bool,
25+
26+
/// The collection of symtabs that went into the goto binary
27+
/// (TODO: this is only for --gen-c, which possibly should not be done here (i.e. not from within harness running)?
28+
/// <https://github.com/model-checking/kani/pull/1684>)
29+
pub symtabs: &'sess [PathBuf],
30+
}
31+
32+
/// The result of checking a single harness. This both hangs on to the harness metadata
33+
/// (as a means to identify which harness), and provides that harness's verification result.
34+
pub(crate) struct HarnessResult<'sess> {
35+
pub harness: &'sess HarnessMetadata,
36+
pub result: VerificationStatus,
37+
}
38+
39+
impl<'sess> HarnessRunner<'sess> {
40+
/// Given a [`HarnessRunner`] (to abstract over how these harnesses were generated), this runs
41+
/// the proof-checking process for each harness in `harnesses`.
42+
pub(crate) fn check_all_harnesses<'a>(
43+
&self,
44+
harnesses: &'a [HarnessMetadata],
45+
) -> Result<Vec<HarnessResult<'a>>> {
46+
let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
47+
48+
let mut results = vec![];
49+
50+
for harness in &sorted_harnesses {
51+
let harness_filename = harness.pretty_name.replace("::", "-");
52+
let report_dir = self.report_base.join(format!("report-{}", harness_filename));
53+
let specialized_obj = specialized_harness_name(self.linked_obj, &harness_filename);
54+
if !self.retain_specialized_harnesses {
55+
let mut temps = self.sess.temporaries.borrow_mut();
56+
temps.push(specialized_obj.to_owned());
57+
}
58+
self.sess.run_goto_instrument(
59+
self.linked_obj,
60+
&specialized_obj,
61+
self.symtabs,
62+
&harness.mangled_name,
63+
)?;
64+
65+
let result = self.sess.check_harness(&specialized_obj, &report_dir, harness)?;
66+
results.push(HarnessResult { harness, result });
67+
}
68+
69+
Ok(results)
70+
}
71+
}
72+
73+
impl KaniSession {
74+
/// Run the verification process for a single harness
75+
pub(crate) fn check_harness(
76+
&self,
77+
binary: &Path,
78+
report_dir: &Path,
79+
harness: &HarnessMetadata,
80+
) -> Result<VerificationStatus> {
81+
if !self.args.quiet {
82+
println!("Checking harness {}...", harness.pretty_name);
83+
}
84+
85+
if self.args.visualize {
86+
self.run_visualize(binary, report_dir, harness)?;
87+
// Strictly speaking, we're faking success here. This is more "no error"
88+
Ok(VerificationStatus::Success)
89+
} else {
90+
self.run_cbmc(binary, harness)
91+
}
92+
}
93+
94+
/// Concludes a session by printing a summary report and exiting the process with an
95+
/// error code (if applicable).
96+
///
97+
/// Note: Takes `self` "by ownership". This function wants to be able to drop before
98+
/// exiting with an error code, if needed.
99+
pub(crate) fn print_final_summary(self, results: &[HarnessResult<'_>]) -> Result<()> {
100+
let (successes, failures): (Vec<_>, Vec<_>) =
101+
results.iter().partition(|r| r.result == VerificationStatus::Success);
102+
103+
let succeeding = successes.len();
104+
let failing = failures.len();
105+
let total = succeeding + failing;
106+
107+
if self.args.concrete_playback.is_some() && !self.args.quiet && failures.is_empty() {
108+
println!(
109+
"INFO: The concrete playback feature never generated unit tests because there were no failing harnesses."
110+
)
111+
}
112+
113+
if !self.args.quiet && !self.args.visualize && total > 1 {
114+
if failing > 0 {
115+
println!("Summary:");
116+
}
117+
for failure in failures.iter() {
118+
println!("Verification failed for - {}", failure.harness.pretty_name);
119+
}
120+
121+
println!(
122+
"Complete - {} successfully verified harnesses, {} failures, {} total.",
123+
succeeding, failing, total
124+
);
125+
}
126+
127+
#[cfg(feature = "unsound_experiments")]
128+
self.args.unsound_experiments.print_warnings();
129+
130+
if failing > 0 {
131+
// Failure exit code without additional error message
132+
drop(self);
133+
std::process::exit(1);
134+
}
135+
136+
Ok(())
137+
}
138+
}

kani-driver/src/main.rs

Lines changed: 21 additions & 103 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,10 @@
33

44
use anyhow::Result;
55
use args_toml::join_args;
6-
use call_cbmc::VerificationStatus;
7-
use kani_metadata::HarnessMetadata;
8-
use session::KaniSession;
6+
97
use std::ffi::OsString;
10-
use std::path::{Path, PathBuf};
8+
use std::path::PathBuf;
119
use structopt::StructOpt;
12-
use util::append_path;
1310

1411
mod args;
1512
mod args_toml;
@@ -22,6 +19,7 @@ mod call_single_file;
2219
mod call_symtab;
2320
mod cbmc_output_parser;
2421
mod concrete_playback;
22+
mod harness_runner;
2523
mod metadata;
2624
mod session;
2725
mod util;
@@ -61,30 +59,19 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
6159

6260
let metadata = ctx.collect_kani_metadata(&outputs.metadata)?;
6361
let harnesses = ctx.determine_targets(&metadata)?;
64-
let sorted_harnesses = metadata::sort_harnesses_by_loc(&harnesses);
6562
let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from("target"));
6663

67-
let mut failed_harnesses: Vec<&HarnessMetadata> = Vec::new();
68-
69-
for harness in &sorted_harnesses {
70-
let harness_filename = harness.pretty_name.replace("::", "-");
71-
let report_dir = report_base.join(format!("report-{}", harness_filename));
72-
let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", harness_filename));
73-
ctx.run_goto_instrument(
74-
&linked_obj,
75-
&specialized_obj,
76-
&outputs.symtabs,
77-
&harness.mangled_name,
78-
)?;
64+
let runner = harness_runner::HarnessRunner {
65+
sess: &ctx,
66+
linked_obj: &linked_obj,
67+
report_base: &report_base,
68+
symtabs: &outputs.symtabs,
69+
retain_specialized_harnesses: true,
70+
};
7971

80-
let result = ctx.check_harness(&specialized_obj, &report_dir, harness)?;
81-
if result == VerificationStatus::Failure {
82-
failed_harnesses.push(harness);
83-
}
84-
}
72+
let results = runner.check_all_harnesses(&harnesses)?;
8573

86-
ctx.inform_if_no_failed(&failed_harnesses);
87-
ctx.print_final_summary(&sorted_harnesses, &failed_harnesses)
74+
ctx.print_final_summary(&results)
8875
}
8976

9077
fn standalone_main() -> Result<()> {
@@ -112,88 +99,19 @@ fn standalone_main() -> Result<()> {
11299

113100
let metadata = ctx.collect_kani_metadata(&[outputs.metadata])?;
114101
let harnesses = ctx.determine_targets(&metadata)?;
115-
let sorted_harnesses = metadata::sort_harnesses_by_loc(&harnesses);
116102
let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from("."));
117103

118-
let mut failed_harnesses: Vec<&HarnessMetadata> = Vec::new();
119-
120-
for harness in &sorted_harnesses {
121-
let harness_filename = harness.pretty_name.replace("::", "-");
122-
let report_dir = report_base.join(format!("report-{}", harness_filename));
123-
let specialized_obj = append_path(&linked_obj, &format!("for-{}", harness_filename));
124-
{
125-
let mut temps = ctx.temporaries.borrow_mut();
126-
temps.push(specialized_obj.to_owned());
127-
}
128-
ctx.run_goto_instrument(
129-
&linked_obj,
130-
&specialized_obj,
131-
&[&outputs.symtab],
132-
&harness.mangled_name,
133-
)?;
134-
135-
let result = ctx.check_harness(&specialized_obj, &report_dir, harness)?;
136-
if result == VerificationStatus::Failure {
137-
failed_harnesses.push(harness);
138-
}
139-
}
140-
141-
ctx.inform_if_no_failed(&failed_harnesses);
142-
ctx.print_final_summary(&sorted_harnesses, &failed_harnesses)
143-
}
144-
145-
impl KaniSession {
146-
fn check_harness(
147-
&self,
148-
binary: &Path,
149-
report_dir: &Path,
150-
harness: &HarnessMetadata,
151-
) -> Result<VerificationStatus> {
152-
if !self.args.quiet {
153-
println!("Checking harness {}...", harness.pretty_name);
154-
}
155-
156-
if self.args.visualize {
157-
self.run_visualize(binary, report_dir, harness)?;
158-
// Strictly speaking, we're faking success here. This is more "no error"
159-
Ok(VerificationStatus::Success)
160-
} else {
161-
self.run_cbmc(binary, harness)
162-
}
163-
}
104+
let runner = harness_runner::HarnessRunner {
105+
sess: &ctx,
106+
linked_obj: &linked_obj,
107+
report_base: &report_base,
108+
symtabs: &[outputs.symtab],
109+
retain_specialized_harnesses: false,
110+
};
164111

165-
fn print_final_summary(
166-
self,
167-
harnesses: &[HarnessMetadata],
168-
failed_harnesses: &[&HarnessMetadata],
169-
) -> Result<()> {
170-
if !self.args.quiet && !self.args.visualize && harnesses.len() > 1 {
171-
if !failed_harnesses.is_empty() {
172-
println!("Summary:");
173-
}
174-
for harness in failed_harnesses.iter() {
175-
println!("Verification failed for - {}", harness.pretty_name);
176-
}
112+
let results = runner.check_all_harnesses(&harnesses)?;
177113

178-
println!(
179-
"Complete - {} successfully verified harnesses, {} failures, {} total.",
180-
harnesses.len() - failed_harnesses.len(),
181-
failed_harnesses.len(),
182-
harnesses.len()
183-
);
184-
}
185-
186-
#[cfg(feature = "unsound_experiments")]
187-
self.args.unsound_experiments.print_warnings();
188-
189-
if !failed_harnesses.is_empty() {
190-
// Failure exit code without additional error message
191-
drop(self);
192-
std::process::exit(1);
193-
}
194-
195-
Ok(())
196-
}
114+
ctx.print_final_summary(&results)
197115
}
198116

199117
#[derive(Debug, PartialEq, Eq)]

kani-driver/src/metadata.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -155,8 +155,8 @@ impl KaniSession {
155155
/// appearing harnesses get processed earlier.
156156
/// This is necessary for the concrete playback feature (with in-place unit test modification)
157157
/// because it guarantees that injected unit tests will not change the location of to-be-processed harnesses.
158-
pub fn sort_harnesses_by_loc(harnesses: &[HarnessMetadata]) -> Vec<HarnessMetadata> {
159-
let mut harnesses_clone = harnesses.to_vec();
158+
pub fn sort_harnesses_by_loc(harnesses: &[HarnessMetadata]) -> Vec<&HarnessMetadata> {
159+
let mut harnesses_clone: Vec<_> = harnesses.iter().by_ref().collect();
160160
harnesses_clone.sort_unstable_by(|harness1, harness2| {
161161
harness1
162162
.original_file

0 commit comments

Comments
 (0)