From e935aed3a6b4520ec08f57f5e1c0b1098a03e86b Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 14:57:34 -0400 Subject: [PATCH 1/7] Delay printing until results are printed. --- kani-driver/src/call_cbmc.rs | 6 ++++++ .../src/concrete_playback/test_generator.rs | 21 +++++++++++-------- kani-driver/src/harness_runner.rs | 7 +++++-- 3 files changed, 23 insertions(+), 11 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 9701efa9c79a..76069684573f 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -53,6 +53,8 @@ pub struct VerificationResult { pub runtime: Duration, /// Whether concrete playback generated a test pub generated_concrete_test: bool, + /// the test case to print for concrete playback. + pub maybe_concrete_test_to_print: Option, } impl KaniSession { @@ -266,6 +268,7 @@ impl VerificationResult { results: Ok(results), runtime, generated_concrete_test: false, + maybe_concrete_test_to_print: None, } } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure @@ -276,6 +279,7 @@ impl VerificationResult { results: Err(output.process_status), runtime, generated_concrete_test: false, + maybe_concrete_test_to_print: None, } } } @@ -288,6 +292,7 @@ impl VerificationResult { results: Ok(vec![]), runtime: Duration::from_secs(0), generated_concrete_test: false, + maybe_concrete_test_to_print: None, } } @@ -302,6 +307,7 @@ impl VerificationResult { results: Err(42), runtime: Duration::from_secs(0), generated_concrete_test: false, + maybe_concrete_test_to_print: None, } } diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 8eeb81106d2c..059375352c38 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -43,15 +43,18 @@ impl KaniSession { let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals); match playback_mode { ConcretePlaybackMode::Print => { - println!( - "Concrete playback unit test for `{}`:\n```\n{}\n```", - &harness.pretty_name, - &generated_unit_test.code.join("\n") - ); - println!( - "INFO: To automatically add the concrete playback unit test `{}` to the \ - src code, run Kani with `--concrete-playback=inplace`.", - &generated_unit_test.name + verification_result.maybe_concrete_test_to_print = Some( + format!( + "Concrete playback unit test for `{}`: +```rust +{} +``` +INFO: To automatically add the concrete playback unit test `{}` to the src code, \ +run Kani with `--concrete-playback=inplace`.", + &harness.pretty_name, + &generated_unit_test.code.join("\n"), + &generated_unit_test.name, + ) ); } ConcretePlaybackMode::InPlace => { diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index d2885c69429a..059417d57003 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -95,8 +95,11 @@ impl KaniSession { // When output is old, we also don't have real results to print. if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old { println!( - "{}", - result.render(&self.args.output_format, harness.attributes.should_panic) + "{}{}", + result.render(&self.args.output_format, harness.attributes.should_panic), + result.maybe_concrete_test_to_print.as_ref() + .map(|message| format!("\n\n{}", message)) + .unwrap_or("".to_string()) ); } From 83df959e58ce558075e967acc94109ae41928725 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 15:31:05 -0400 Subject: [PATCH 2/7] Tests for ordering of harness. --- tests/ui/concrete-playback/message-order/expected | 14 ++++++++++++++ tests/ui/concrete-playback/message-order/main.rs | 9 +++++++++ 2 files changed, 23 insertions(+) create mode 100644 tests/ui/concrete-playback/message-order/expected create mode 100644 tests/ui/concrete-playback/message-order/main.rs diff --git a/tests/ui/concrete-playback/message-order/expected b/tests/ui/concrete-playback/message-order/expected new file mode 100644 index 000000000000..7b5e07374720 --- /dev/null +++ b/tests/ui/concrete-playback/message-order/expected @@ -0,0 +1,14 @@ +VERIFICATION:- SUCCESSFUL + + +Concrete playback unit test for `dummy`: +```rust +#[test] +fn kani_concrete_playback_dummy + let concrete_vals: Vec> = vec![ + // 32778 + vec![10, 128, 0, 0], + ]; + kani::concrete_playback_run(concrete_vals, dummy); +} +``` diff --git a/tests/ui/concrete-playback/message-order/main.rs b/tests/ui/concrete-playback/message-order/main.rs new file mode 100644 index 000000000000..81aa4c6886db --- /dev/null +++ b/tests/ui/concrete-playback/message-order/main.rs @@ -0,0 +1,9 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: --concrete-playback=print --harness dummy -Z concrete-playback + +#[kani::proof] +fn dummy() { + kani::cover!(kani::any::() != 10); +} From 7867bc5401befe68fe6ec2bc5c86ddd22cb3914b Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 15:47:53 -0400 Subject: [PATCH 3/7] cargo fmt. --- .../src/concrete_playback/test_generator.rs | 14 ++++++-------- kani-driver/src/harness_runner.rs | 4 +++- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 059375352c38..e4f59fcb33c1 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -43,19 +43,17 @@ impl KaniSession { let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals); match playback_mode { ConcretePlaybackMode::Print => { - verification_result.maybe_concrete_test_to_print = Some( - format!( - "Concrete playback unit test for `{}`: + verification_result.maybe_concrete_test_to_print = Some(format!( + "Concrete playback unit test for `{}`: ```rust {} ``` INFO: To automatically add the concrete playback unit test `{}` to the src code, \ run Kani with `--concrete-playback=inplace`.", - &harness.pretty_name, - &generated_unit_test.code.join("\n"), - &generated_unit_test.name, - ) - ); + &harness.pretty_name, + &generated_unit_test.code.join("\n"), + &generated_unit_test.name, + )); } ConcretePlaybackMode::InPlace => { if !self.args.common_args.quiet { diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 059417d57003..890f6c433dbd 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -97,7 +97,9 @@ impl KaniSession { println!( "{}{}", result.render(&self.args.output_format, harness.attributes.should_panic), - result.maybe_concrete_test_to_print.as_ref() + result + .maybe_concrete_test_to_print + .as_ref() .map(|message| format!("\n\n{}", message)) .unwrap_or("".to_string()) ); From c132ee86c0df488f3634a98df9f5d2d3ce68d0bc Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 17:28:12 -0400 Subject: [PATCH 4/7] Revert kani-driver. --- kani-driver/src/call_cbmc.rs | 6 ------ .../src/concrete_playback/test_generator.rs | 19 +++++++++---------- kani-driver/src/harness_runner.rs | 9 ++------- 3 files changed, 11 insertions(+), 23 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 76069684573f..9701efa9c79a 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -53,8 +53,6 @@ pub struct VerificationResult { pub runtime: Duration, /// Whether concrete playback generated a test pub generated_concrete_test: bool, - /// the test case to print for concrete playback. - pub maybe_concrete_test_to_print: Option, } impl KaniSession { @@ -268,7 +266,6 @@ impl VerificationResult { results: Ok(results), runtime, generated_concrete_test: false, - maybe_concrete_test_to_print: None, } } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure @@ -279,7 +276,6 @@ impl VerificationResult { results: Err(output.process_status), runtime, generated_concrete_test: false, - maybe_concrete_test_to_print: None, } } } @@ -292,7 +288,6 @@ impl VerificationResult { results: Ok(vec![]), runtime: Duration::from_secs(0), generated_concrete_test: false, - maybe_concrete_test_to_print: None, } } @@ -307,7 +302,6 @@ impl VerificationResult { results: Err(42), runtime: Duration::from_secs(0), generated_concrete_test: false, - maybe_concrete_test_to_print: None, } } diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index e4f59fcb33c1..8eeb81106d2c 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -43,17 +43,16 @@ impl KaniSession { let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals); match playback_mode { ConcretePlaybackMode::Print => { - verification_result.maybe_concrete_test_to_print = Some(format!( - "Concrete playback unit test for `{}`: -```rust -{} -``` -INFO: To automatically add the concrete playback unit test `{}` to the src code, \ -run Kani with `--concrete-playback=inplace`.", + println!( + "Concrete playback unit test for `{}`:\n```\n{}\n```", &harness.pretty_name, - &generated_unit_test.code.join("\n"), - &generated_unit_test.name, - )); + &generated_unit_test.code.join("\n") + ); + println!( + "INFO: To automatically add the concrete playback unit test `{}` to the \ + src code, run Kani with `--concrete-playback=inplace`.", + &generated_unit_test.name + ); } ConcretePlaybackMode::InPlace => { if !self.args.common_args.quiet { diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 890f6c433dbd..d2885c69429a 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -95,13 +95,8 @@ impl KaniSession { // When output is old, we also don't have real results to print. if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old { println!( - "{}{}", - result.render(&self.args.output_format, harness.attributes.should_panic), - result - .maybe_concrete_test_to_print - .as_ref() - .map(|message| format!("\n\n{}", message)) - .unwrap_or("".to_string()) + "{}", + result.render(&self.args.output_format, harness.attributes.should_panic) ); } From 2be936ba9874c2107b4bc19171cb63501093f545 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 17:34:56 -0400 Subject: [PATCH 5/7] Move concrete harness generation to after result print. --- kani-driver/src/call_cbmc.rs | 3 +-- kani-driver/src/harness_runner.rs | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 9701efa9c79a..36dcf34120c0 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -66,7 +66,7 @@ impl KaniSession { let start_time = Instant::now(); - let mut verification_results = if self.args.output_format == crate::args::OutputFormat::Old + let verification_results = if self.args.output_format == crate::args::OutputFormat::Old { if self.run_terminal(cmd).is_err() { VerificationResult::mock_failure() @@ -93,7 +93,6 @@ impl KaniSession { VerificationResult::from(output, harness.attributes.should_panic, start_time) }; - self.gen_and_add_concrete_playback(harness, &mut verification_results)?; Ok(verification_results) } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index d2885c69429a..f1f0befc4ddd 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -89,7 +89,7 @@ impl KaniSession { // Strictly speaking, we're faking success here. This is more "no error" Ok(VerificationResult::mock_success()) } else { - let result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; + let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; // When quiet, we don't want to print anything at all. // When output is old, we also don't have real results to print. @@ -99,7 +99,7 @@ impl KaniSession { result.render(&self.args.output_format, harness.attributes.should_panic) ); } - + self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) } } From a549dc8ac49d5c090486af6a62e8965c98c2c3a7 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 17:39:47 -0400 Subject: [PATCH 6/7] Rustfmt. --- kani-driver/src/call_cbmc.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 36dcf34120c0..daddfdf62f1c 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -66,8 +66,7 @@ impl KaniSession { let start_time = Instant::now(); - let verification_results = if self.args.output_format == crate::args::OutputFormat::Old - { + let verification_results = if self.args.output_format == crate::args::OutputFormat::Old { if self.run_terminal(cmd).is_err() { VerificationResult::mock_failure() } else { From bd475b70908e160c30ff935433c5f293f8debb22 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 26 May 2023 18:20:06 -0400 Subject: [PATCH 7/7] Fix expected: no rust annotation. --- tests/ui/concrete-playback/message-order/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ui/concrete-playback/message-order/expected b/tests/ui/concrete-playback/message-order/expected index 7b5e07374720..415584e1f2dc 100644 --- a/tests/ui/concrete-playback/message-order/expected +++ b/tests/ui/concrete-playback/message-order/expected @@ -2,7 +2,7 @@ VERIFICATION:- SUCCESSFUL Concrete playback unit test for `dummy`: -```rust +``` #[test] fn kani_concrete_playback_dummy let concrete_vals: Vec> = vec![