Skip to content

Commit 95e7161

Browse files
author
Yoshiki Takashima
authored
Generate Multiple playback harnesses when multiple crashes exist in a single harness. (rust-lang#2496)
1 parent 7378419 commit 95e7161

File tree

12 files changed

+287
-104
lines changed

12 files changed

+287
-104
lines changed

kani-driver/src/concrete_playback/test_generator.rs

Lines changed: 120 additions & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ use concrete_vals_extractor::{extract_harness_values, ConcreteVal};
1313
use kani_metadata::HarnessMetadata;
1414
use std::collections::hash_map::DefaultHasher;
1515
use std::ffi::OsString;
16-
use std::fs::File;
16+
use std::fs::{read_to_string, File};
1717
use std::hash::{Hash, Hasher};
1818
use std::io::{BufRead, BufReader, Write};
1919
use std::path::Path;
@@ -32,48 +32,65 @@ impl KaniSession {
3232
};
3333

3434
if let Ok(result_items) = &verification_result.results {
35-
match extract_harness_values(result_items) {
36-
None => println!(
35+
let harness_values: Vec<Vec<ConcreteVal>> = extract_harness_values(result_items);
36+
37+
if harness_values.is_empty() {
38+
println!(
3739
"WARNING: Kani could not produce a concrete playback for `{}` because there \
38-
were no failing panic checks.",
40+
were no failing panic checks or satisfiable cover statements.",
3941
harness.pretty_name
40-
),
41-
Some(concrete_vals) => {
42-
let pretty_name = harness.get_harness_name_unqualified();
43-
let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals);
44-
match playback_mode {
45-
ConcretePlaybackMode::Print => {
42+
)
43+
} else {
44+
let unit_tests: Vec<UnitTest> = harness_values
45+
.iter()
46+
.map(|concrete_vals| {
47+
let pretty_name = harness.get_harness_name_unqualified();
48+
format_unit_test(&pretty_name, &concrete_vals)
49+
})
50+
.collect();
51+
match playback_mode {
52+
ConcretePlaybackMode::Print => {
53+
for generated_unit_test in unit_tests.iter() {
4654
println!(
4755
"Concrete playback unit test for `{}`:\n```\n{}\n```",
4856
&harness.pretty_name,
4957
&generated_unit_test.code.join("\n")
5058
);
59+
}
60+
61+
if !unit_tests.is_empty() {
5162
println!(
52-
"INFO: To automatically add the concrete playback unit test `{}` to the \
53-
src code, run Kani with `--concrete-playback=inplace`.",
54-
&generated_unit_test.name
63+
"INFO: To automatically add the concrete playback unit test(s) to the \
64+
src code, run Kani with `--concrete-playback=inplace`.",
5565
);
5666
}
57-
ConcretePlaybackMode::InPlace => {
58-
if !self.args.common_args.quiet {
59-
println!(
60-
"INFO: Now modifying the source code to include the concrete playback unit test `{}`.",
61-
&generated_unit_test.name
62-
);
63-
}
64-
self.modify_src_code(
65-
&harness.original_file,
66-
harness.original_end_line,
67-
&generated_unit_test,
68-
)
69-
.expect(&format!(
70-
"Failed to modify source code for the file `{}`",
71-
&harness.original_file
72-
));
67+
}
68+
ConcretePlaybackMode::InPlace => {
69+
if !self.args.common_args.quiet && !unit_tests.is_empty() {
70+
println!(
71+
"INFO: Now modifying the source code to include the concrete playback unit test:{}.",
72+
unit_tests
73+
.iter()
74+
.map(|generated_unit_test| format!(
75+
"\n - {}",
76+
&generated_unit_test.name
77+
))
78+
.collect::<Vec<String>>()
79+
.join("")
80+
);
7381
}
82+
self.modify_src_code(
83+
&harness.original_file,
84+
harness.original_end_line,
85+
unit_tests,
86+
)
87+
.expect(&format!(
88+
"Failed to modify source code for the file `{}`",
89+
&harness.original_file
90+
));
7491
}
75-
verification_result.generated_concrete_test = true;
7692
}
93+
verification_result.generated_concrete_test = true;
7794
}
7895
}
7996
Ok(())
@@ -84,71 +101,83 @@ impl KaniSession {
84101
&self,
85102
src_path: &str,
86103
proof_harness_end_line: usize,
87-
unit_test: &UnitTest,
104+
unit_tests: Vec<UnitTest>,
88105
) -> Result<()> {
89-
let unit_test_already_in_src =
90-
self.add_test_inplace(src_path, proof_harness_end_line, unit_test)?;
91-
92-
if unit_test_already_in_src {
93-
return Ok(());
106+
// compute range to run rustfmt on.
107+
let concrete_playback_num_lines: usize =
108+
unit_tests.iter().map(|unit_test| unit_test.code.len()).sum();
109+
110+
let is_new_injection =
111+
self.add_tests_inplace(src_path, proof_harness_end_line, unit_tests)?;
112+
113+
if is_new_injection {
114+
let unit_test_start_line = proof_harness_end_line + 1;
115+
let unit_test_end_line = unit_test_start_line + concrete_playback_num_lines - 1;
116+
let src_path = Path::new(src_path);
117+
let (path, file_name) = extract_parent_dir_and_src_file(src_path)?;
118+
let file_line_ranges = vec![FileLineRange {
119+
file: file_name,
120+
line_range: Some((unit_test_start_line, unit_test_end_line)),
121+
}];
122+
self.run_rustfmt(&file_line_ranges, Some(&path))?;
94123
}
95124

96-
// Run rustfmt on just the inserted lines.
97-
let concrete_playback_num_lines = unit_test.code.len();
98-
let unit_test_start_line = proof_harness_end_line + 1;
99-
let unit_test_end_line = unit_test_start_line + concrete_playback_num_lines - 1;
100-
let src_path = Path::new(src_path);
101-
let (path, file_name) = extract_parent_dir_and_src_file(src_path)?;
102-
let file_line_ranges = vec![FileLineRange {
103-
file: file_name,
104-
line_range: Some((unit_test_start_line, unit_test_end_line)),
105-
}];
106-
self.run_rustfmt(&file_line_ranges, Some(&path))?;
107125
Ok(())
108126
}
109127

110128
/// Writes the new source code to a user's source file using a tempfile as the means.
111-
/// Returns whether the unit test was already in the old source code.
112-
fn add_test_inplace(
129+
/// Returns whether new unit test was injected.
130+
fn add_tests_inplace(
113131
&self,
114132
source_path: &str,
115133
proof_harness_end_line: usize,
116-
unit_test: &UnitTest,
134+
mut unit_tests: Vec<UnitTest>,
117135
) -> Result<bool> {
118136
// Read from source
119137
let source_file = File::open(source_path).unwrap();
120138
let source_reader = BufReader::new(source_file);
139+
let source_string = read_to_string(source_path).unwrap();
121140

122-
// Create temp file
123-
let mut temp_file = TempFile::try_new("concrete_playback.tmp")?;
124-
let mut curr_line_num = 0;
125-
126-
// Use a buffered reader/writer to generate the unit test line by line
127-
for line in source_reader.lines().flatten() {
128-
if line.contains(&unit_test.name) {
141+
// filter out existing harnesses.
142+
unit_tests.retain(|unit_test| {
143+
if source_string.contains(&unit_test.name) {
129144
if !self.args.common_args.quiet {
130145
println!(
131146
"Concrete playback unit test `{}/{}` already found in source code, so skipping modification.",
132147
source_path, unit_test.name,
133148
);
134149
}
135-
// the drop impl will take care of flushing and resetting
136-
return Ok(true);
150+
151+
false
152+
} else {
153+
true
137154
}
138-
curr_line_num += 1;
139-
if let Some(temp_writer) = temp_file.writer.as_mut() {
140-
writeln!(temp_writer, "{line}")?;
141-
if curr_line_num == proof_harness_end_line {
142-
for unit_test_line in unit_test.code.iter() {
143-
curr_line_num += 1;
144-
writeln!(temp_writer, "{unit_test_line}")?;
155+
});
156+
157+
// Create temp file
158+
if !unit_tests.is_empty() {
159+
let mut temp_file = TempFile::try_new("concrete_playback.tmp")?;
160+
let mut curr_line_num = 0;
161+
162+
// Use a buffered reader/writer to generate the unit test line by line
163+
for line in source_reader.lines().flatten() {
164+
curr_line_num += 1;
165+
if let Some(temp_writer) = temp_file.writer.as_mut() {
166+
writeln!(temp_writer, "{line}")?;
167+
if curr_line_num == proof_harness_end_line {
168+
for unit_test in unit_tests.iter() {
169+
for unit_test_line in unit_test.code.iter() {
170+
curr_line_num += 1;
171+
writeln!(temp_writer, "{unit_test_line}")?;
172+
}
173+
}
145174
}
146175
}
147176
}
177+
temp_file.rename(source_path).expect("Could not rename file");
148178
}
149179

150-
temp_file.rename(source_path).expect("Could not rename file");
151-
Ok(false)
180+
Ok(!unit_tests.is_empty())
152181
}
153182

154183
/// Run rustfmt on the given src file, and optionally on only the specific lines.
@@ -287,37 +316,28 @@ mod concrete_vals_extractor {
287316
pub interp_val: String,
288317
}
289318

290-
/// Extract a set of concrete values that trigger one assertion failure.
291-
/// This will return None if the failure is not related to a user assertion.
292-
pub fn extract_harness_values(result_items: &[Property]) -> Option<Vec<ConcreteVal>> {
293-
let mut failures = result_items.iter().filter(|prop| {
294-
(prop.property_class() == "assertion" && prop.status == CheckStatus::Failure)
295-
|| (prop.property_class() == "cover" && prop.status == CheckStatus::Satisfied)
296-
});
297-
298-
// Process the first assertion failure.
299-
let first_failure = failures.next();
300-
if let Some(property) = first_failure {
301-
// Extract values for the first assertion that has failed.
302-
let trace = property
303-
.trace
304-
.as_ref()
305-
.expect(&format!("Missing trace for {}", property.property_name()));
306-
let concrete_vals = trace.iter().filter_map(&extract_from_trace_item).collect();
307-
308-
// Print warnings for all the other failures that were not handled in case they expected
309-
// even future checks to be extracted.
310-
for unhandled in failures {
311-
println!(
312-
"WARNING: Unable to extract concrete values from multiple failing assertions. Skipping property `{}` with description `{}`.",
313-
unhandled.property_name(),
314-
unhandled.description,
315-
);
316-
}
317-
Some(concrete_vals)
318-
} else {
319-
None
320-
}
319+
/// Extract a set of concrete values that trigger one assertion
320+
/// failure. Each element of the outer vector corresponds to
321+
/// inputs triggering one assertion failure or cover statement.
322+
pub fn extract_harness_values(result_items: &[Property]) -> Vec<Vec<ConcreteVal>> {
323+
result_items
324+
.iter()
325+
.filter(|prop| {
326+
(prop.property_class() == "assertion" && prop.status == CheckStatus::Failure)
327+
|| (prop.property_class() == "cover" && prop.status == CheckStatus::Satisfied)
328+
})
329+
.map(|property| {
330+
// Extract values for each assertion that has failed.
331+
let trace = property
332+
.trace
333+
.as_ref()
334+
.expect(&format!("Missing trace for {}", property.property_name()));
335+
let concrete_vals: Vec<ConcreteVal> =
336+
trace.iter().filter_map(&extract_from_trace_item).collect();
337+
338+
concrete_vals
339+
})
340+
.collect()
321341
}
322342

323343
/// Extracts individual bytes returned by kani::any() calls.
@@ -569,7 +589,7 @@ mod tests {
569589
}),
570590
}]),
571591
}];
572-
let concrete_vals = extract_harness_values(&processed_items).unwrap();
592+
let concrete_vals = extract_harness_values(&processed_items).pop().unwrap();
573593
let concrete_val = &concrete_vals[0];
574594

575595
assert_eq!(concrete_val.byte_arr, vec![1, 3]);
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
script: playback_opts.sh
4+
expected: playback_opts.expected
Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//! Check that Kani correctly adds tests to the cover checks reachable in a harness.
4+
extern crate kani;
5+
6+
#[cfg(kani)]
7+
mod verify {
8+
use kani::cover;
9+
use std::convert::TryFrom;
10+
use std::num::NonZeroU8;
11+
12+
#[kani::proof]
13+
fn try_nz_u8() {
14+
let val: u8 = kani::any();
15+
let result = NonZeroU8::try_from(val);
16+
match result {
17+
Ok(nz_val) => {
18+
cover!(true, "Ok");
19+
assert_eq!(nz_val.get(), val);
20+
}
21+
Err(_) => {
22+
cover!(true, "Not ok");
23+
assert_eq!(val, 0);
24+
}
25+
}
26+
}
27+
#[test]
28+
fn kani_concrete_playback_try_nz_u8_17663051139329126359() {
29+
let concrete_vals: Vec<Vec<u8>> = vec![
30+
// 0
31+
vec![0],
32+
];
33+
kani::concrete_playback_run(concrete_vals, try_nz_u8);
34+
}
35+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
[TEST] Generate test...
2+
Checking harness verify::try_nz_u8
3+
4+
already found in source code, so skipping modification.
5+
6+
[TEST] Only codegen test...
7+
Building modified.rs
8+
playback_already_existing/kani_concrete_playback
9+
10+
[TEST] Run test...
11+
test result: ok. 2 passed; 0 failed;
12+
13+
[TEST] Json format...
14+
{"artifact":
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#!/usr/bin/env bash
2+
# Copyright Kani Contributors
3+
# SPDX-License-Identifier: Apache-2.0 OR MIT
4+
# Test that concrete playback -Z concrete-playback executes as expected
5+
set -o pipefail
6+
set -o nounset
7+
8+
RS_FILE="modified.rs"
9+
cp original.rs ${RS_FILE}
10+
11+
echo "[TEST] Generate test..."
12+
kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace
13+
14+
echo "[TEST] Only codegen test..."
15+
kani playback -Z concrete-playback --only-codegen ${RS_FILE} -- kani_concrete_playback
16+
17+
echo "[TEST] Run test..."
18+
kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback
19+
20+
echo "[TEST] Json format..."
21+
kani playback -Z concrete-playback ${RS_FILE} --only-codegen --message-format=json -- kani_concrete_playback
22+
23+
# Cleanup
24+
rm ${RS_FILE}
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# Copyright Kani Contributors
2+
# SPDX-License-Identifier: Apache-2.0 OR MIT
3+
script: playback_opts.sh
4+
expected: playback_opts.expected

0 commit comments

Comments
 (0)