From f23126ab78a5d66d74f96211dbc2de434e23e7b0 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Fri, 1 Sep 2023 17:54:31 -0700
Subject: [PATCH] Enable concrete playback for failure of UB checks (#2727)

---
 .../src/concrete_playback/test_generator.rs       |  2 +-
 tests/ui/concrete-playback/ub/null_ptr/expected   | 13 +++++++++++++
 tests/ui/concrete-playback/ub/null_ptr/test.rs    | 15 +++++++++++++++
 tests/ui/concrete-playback/ub/oob_ptr/expected    | 13 +++++++++++++
 tests/ui/concrete-playback/ub/oob_ptr/test.rs     | 15 +++++++++++++++
 5 files changed, 57 insertions(+), 1 deletion(-)
 create mode 100644 tests/ui/concrete-playback/ub/null_ptr/expected
 create mode 100644 tests/ui/concrete-playback/ub/null_ptr/test.rs
 create mode 100644 tests/ui/concrete-playback/ub/oob_ptr/expected
 create mode 100644 tests/ui/concrete-playback/ub/oob_ptr/test.rs

diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
index b2e8fd17ff67..8bd29ae69d2c 100644
--- a/kani-driver/src/concrete_playback/test_generator.rs
+++ b/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| {
diff --git a/tests/ui/concrete-playback/ub/null_ptr/expected b/tests/ui/concrete-playback/ub/null_ptr/expected
new file mode 100644
index 000000000000..062d8bbb0bf0
--- /dev/null
+++ b/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);
+}
+```
diff --git a/tests/ui/concrete-playback/ub/null_ptr/test.rs b/tests/ui/concrete-playback/ub/null_ptr/test.rs
new file mode 100644
index 000000000000..c97f4a764885
--- /dev/null
+++ b/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 };
+}
diff --git a/tests/ui/concrete-playback/ub/oob_ptr/expected b/tests/ui/concrete-playback/ub/oob_ptr/expected
new file mode 100644
index 000000000000..3c20d94b2e06
--- /dev/null
+++ b/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);
+}
+```
diff --git a/tests/ui/concrete-playback/ub/oob_ptr/test.rs b/tests/ui/concrete-playback/ub/oob_ptr/test.rs
new file mode 100644
index 000000000000..d93af9a8903e
--- /dev/null
+++ b/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) };
+}