Enable concrete playback for failure of UB checks (model-checking#2727)

kani-driver/src/concrete_playback/test_generator.rs

@@ -325,7 +325,7 @@ mod concrete_vals_extractor {
  result_items
  .iter()
  .filter(|prop| {
- (prop.property_class() == "assertion" && prop.status == CheckStatus::Failure)
+ (prop.property_class() != "unwind" && prop.status == CheckStatus::Failure)
  || (prop.property_class() == "cover" && prop.status == CheckStatus::Satisfied)
  })
  .map(|property| {

tests/ui/concrete-playback/ub/null_ptr/expected

@@ -0,0 +1,13 @@
+VERIFICATION:- FAILED
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_null_ptr
+ let concrete_vals: Vec<Vec<u8>> = vec![
+ // 15
+ vec![15, 0, 0, 0],
+ ];
+ kani::concrete_playback_run(concrete_vals, null_ptr);
+}
+```

tests/ui/concrete-playback/ub/null_ptr/test.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Zconcrete-playback --concrete-playback=print
+
+// This test checks that Kani generates a concrete playback test for UB checks
+// (e.g. dereferencing a null pointer)
+
+#[kani::proof]
+fn null_ptr() {
+ let x = 42;
+ let nd: i32 = kani::any();
+ let ptr: *const i32 = if nd != 15 { &x as *const i32 } else { std::ptr::null() };
+ let _y = unsafe { *ptr };
+}

tests/ui/concrete-playback/ub/oob_ptr/expected

@@ -0,0 +1,13 @@
+VERIFICATION:- FAILED
+
+Concrete playback
+```
+#[test]
+fn kani_concrete_playback_oob_ptr
+ let concrete_vals: Vec<Vec<u8>> = vec![
+ // 3ul
+ vec![3, 0, 0, 0, 0, 0, 0, 0],
+ ];
+ kani::concrete_playback_run(concrete_vals, oob_ptr);
+}
+```

tests/ui/concrete-playback/ub/oob_ptr/test.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Zconcrete-playback --concrete-playback=print
+
+// This test checks that Kani generates a concrete playback test for UB checks
+// (e.g. dereferencing a pointer that is outside the object bounds)
+
+#[kani::proof]
+fn oob_ptr() {
+ let v = vec![1, 2, 3];
+ // BUG: predicate should use strict less-than, i.e. `*idx < v.len()`
+ let idx: usize = kani::any_where(|idx| *idx <= v.len());
+ let _x = unsafe { *v.get_unchecked(idx) };
+}