feat: add concrete playback support for multiple failing harnesses (r…

…ust-lang#1558) * add sorting of harnesses * add mult harnesses test * remove --harness from existing tests * remove --harness from docs page * add better comment for sort_harnesses * refactor: switch tests to use 'print' flag * refactor: copy harnesses instead of in-place modification * refactor: update sort fn name
celinval · Aug 25, 2022 · 5574f5d · 5574f5d
1 parent 60053df
commit 5574f5d
Show file tree

Hide file tree

Showing 30 changed files with 95 additions and 40 deletions.
diff --git a/docs/src/debugging-verification-failures.md b/docs/src/debugging-verification-failures.md
@@ -52,7 +52,7 @@ You can then debug the binary with tools like `rust-gdb` or `lldb`.
 
 ### Example
 
-Running `kani --harness proof_harness --enable-unstable --concrete-playback=print` on the following source file:
+Running `kani --enable-unstable --concrete-playback=print` on the following source file:
 ```rust
 #[kani::proof]
 fn proof_harness() {

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -316,8 +316,8 @@ impl<'tcx> GotocCtx<'tcx> {
             pretty_name,
             mangled_name,
             original_file: loc.filename().unwrap(),
-            original_start_line: loc.start_line().unwrap().to_string(),
-            original_end_line: loc.end_line().unwrap().to_string(),
+            original_start_line: loc.start_line().unwrap() as usize,
+            original_end_line: loc.end_line().unwrap() as usize,
             unwind_value: None,
         }
     }

diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
@@ -50,7 +50,6 @@ pub struct KaniArgs {
     #[structopt(
         long,
         requires("enable-unstable"),
-        requires("harness"),
         conflicts_with_all(&["visualize", "dry-run"]),
         possible_values = &ConcretePlaybackMode::variants(),
         case_insensitive = true,

diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs
@@ -51,11 +51,7 @@ impl KaniSession {
                     &concrete_playback.unit_test_name
                 );
             }
-            let proof_harness_end_line: usize = harness
-                .original_end_line
-                .parse()
-                .expect(&format!("Invalid proof harness end line: {}", harness.original_end_line));
-            self.modify_src_code(&harness.original_file, proof_harness_end_line, &concrete_playback)
+            self.modify_src_code(&harness.original_file, harness.original_end_line, &concrete_playback)
                 .expect("Failed to modify source code");
         }
     }

diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
@@ -56,11 +56,12 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
 
     let metadata = ctx.collect_kani_metadata(&outputs.metadata)?;
     let harnesses = ctx.determine_targets(&metadata)?;
+    let sorted_harnesses = metadata::sort_harnesses_by_loc(&harnesses);
     let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from("target"));
 
     let mut failed_harnesses: Vec<&HarnessMetadata> = Vec::new();
 
-    for harness in &harnesses {
+    for harness in &sorted_harnesses {
         let harness_filename = harness.pretty_name.replace("::", "-");
         let report_dir = report_base.join(format!("report-{}", harness_filename));
         let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", harness_filename));
@@ -77,7 +78,7 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
         }
     }
 
-    ctx.print_final_summary(&harnesses, &failed_harnesses)
+    ctx.print_final_summary(&sorted_harnesses, &failed_harnesses)
 }
 
 fn standalone_main() -> Result<()> {
@@ -103,11 +104,12 @@ fn standalone_main() -> Result<()> {
 
     let metadata = ctx.collect_kani_metadata(&[outputs.metadata])?;
     let harnesses = ctx.determine_targets(&metadata)?;
+    let sorted_harnesses = metadata::sort_harnesses_by_loc(&harnesses);
     let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from("."));
 
     let mut failed_harnesses: Vec<&HarnessMetadata> = Vec::new();
 
-    for harness in &harnesses {
+    for harness in &sorted_harnesses {
         let harness_filename = harness.pretty_name.replace("::", "-");
         let report_dir = report_base.join(format!("report-{}", harness_filename));
         let specialized_obj = append_path(&linked_obj, &format!("for-{}", harness_filename));
@@ -128,7 +130,7 @@ fn standalone_main() -> Result<()> {
         }
     }
 
-    ctx.print_final_summary(&harnesses, &failed_harnesses)
+    ctx.print_final_summary(&sorted_harnesses, &failed_harnesses)
 }
 
 impl KaniSession {

diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
@@ -18,8 +18,8 @@ fn generate_mock_harness() -> HarnessMetadata {
         pretty_name: String::from("harness"),
         mangled_name: String::from("harness"),
         original_file: String::from("target_file.rs"),
-        original_start_line: String::from("0"),
-        original_end_line: String::from("0"),
+        original_start_line: 0,
+        original_end_line: 0,
         unwind_value: None,
     }
 }
@@ -151,13 +151,28 @@ impl KaniSession {
     }
 }
 
+/// Sort harnesses such that for two harnesses in the same file, it is guaranteed that later
+/// appearing harnesses get processed earlier.
+/// This is necessary for the concrete playback feature (with in-place unit test modification)
+/// because it guarantees that injected unit tests will not change the location of to-be-processed harnesses.
+pub fn sort_harnesses_by_loc(harnesses: &[HarnessMetadata]) -> Vec<HarnessMetadata> {
+    let mut harnesses_clone = harnesses.to_vec();
+    harnesses_clone.sort_unstable_by(|harness1, harness2| {
+        harness1
+            .original_file
+            .cmp(&harness2.original_file)
+            .then(harness1.original_start_line.cmp(&harness2.original_start_line).reverse())
+    });
+    harnesses_clone
+}
+
 pub fn mock_proof_harness(name: &str, unwind_value: Option<u32>) -> HarnessMetadata {
     HarnessMetadata {
         pretty_name: name.into(),
         mangled_name: name.into(),
         original_file: "<unknown>".into(),
-        original_start_line: "<unknown>".into(),
-        original_end_line: "<unknown>".into(),
+        original_start_line: 0,
+        original_end_line: 0,
         unwind_value,
     }
 }

diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
@@ -13,9 +13,9 @@ pub struct HarnessMetadata {
     /// The (currently full-) path to the file this proof harness was declared within
     pub original_file: String,
     /// The line in that file where the proof harness begins
-    pub original_start_line: String,
+    pub original_start_line: usize,
     /// The line in that file where the proof harness ends
-    pub original_end_line: String,
+    pub original_end_line: usize,
     /// Optional data to store unwind value
     pub unwind_value: Option<u32>,
 }
diff --git a/tests/ui/concrete-playback/array/main.rs b/tests/ui/concrete-playback/array/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 #[kani::unwind(10)]

diff --git a/tests/ui/concrete-playback/bool/main.rs b/tests/ui/concrete-playback/bool/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/custom/main.rs b/tests/ui/concrete-playback/custom/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 struct MyStruct {
     field1: u8,

diff --git a/tests/ui/concrete-playback/f32/main.rs b/tests/ui/concrete-playback/f32/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 /// Note: Don't include NaN because there are multiple possible NaN values.
 #[kani::proof]

diff --git a/tests/ui/concrete-playback/f64/main.rs b/tests/ui/concrete-playback/f64/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 /// Note: Don't include NaN because there are multiple possible NaN values.
 #[kani::proof]

diff --git a/tests/ui/concrete-playback/i128/main.rs b/tests/ui/concrete-playback/i128/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/i16/main.rs b/tests/ui/concrete-playback/i16/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/i32/main.rs b/tests/ui/concrete-playback/i32/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/i64/main.rs b/tests/ui/concrete-playback/i64/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/i8/main.rs b/tests/ui/concrete-playback/i8/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/isize/main.rs b/tests/ui/concrete-playback/isize/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/mult-harnesses/expected b/tests/ui/concrete-playback/mult-harnesses/expected
@@ -0,0 +1,27 @@
+VERIFICATION:- FAILED
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_harness2
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 255
+        vec![255]
+    ];
+    kani::concrete_playback_run(concrete_vals, harness2);
+}
+```
+
+VERIFICATION:- FAILED
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_harness1
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 0
+        vec![0]
+    ];
+    kani::concrete_playback_run(concrete_vals, harness1);
+}
+```
diff --git a/tests/ui/concrete-playback/mult-harnesses/main.rs b/tests/ui/concrete-playback/mult-harnesses/main.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --enable-unstable --concrete-playback=print
+
+#[kani::proof]
+pub fn harness1() {
+    let u8_1: u8 = kani::any();
+    assert!(u8_1 != u8::MIN);
+}
+
+#[kani::proof]
+pub fn harness2() {
+    let u8_2: u8 = kani::any();
+    assert!(u8_2 != u8::MAX);
+}
diff --git a/tests/ui/concrete-playback/non_zero/main.rs b/tests/ui/concrete-playback/non_zero/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 use std::num::NonZeroU8;
 

diff --git a/tests/ui/concrete-playback/option/main.rs b/tests/ui/concrete-playback/option/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/result/main.rs b/tests/ui/concrete-playback/result/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/slice-formula/main.rs b/tests/ui/concrete-playback/slice-formula/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 //! We explicitly don't check what concrete values are returned for `_u8_1` and `_u8_3` as they could be anything.
 //! In practice, though, they will likely be 0.

diff --git a/tests/ui/concrete-playback/u128/main.rs b/tests/ui/concrete-playback/u128/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/u16/main.rs b/tests/ui/concrete-playback/u16/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/u32/main.rs b/tests/ui/concrete-playback/u32/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/u64/main.rs b/tests/ui/concrete-playback/u64/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/u8/main.rs b/tests/ui/concrete-playback/u8/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {

diff --git a/tests/ui/concrete-playback/usize/main.rs b/tests/ui/concrete-playback/usize/main.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --harness harness --enable-unstable --concrete-playback=Print
+// kani-flags: --enable-unstable --concrete-playback=print
 
 #[kani::proof]
 pub fn harness() {