Merge branch 'main' into toolchain-issue

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -123,7 +123,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
                 "https://github.com/model-checking/kani/issues/692",
             ),
-            TerminatorKind::UnwindTerminate => self.codegen_mimic_unimplemented(
+            TerminatorKind::UnwindTerminate(_) => self.codegen_mimic_unimplemented(
                 "TerminatorKind::UnwindTerminate",
                 loc,
                 "https://github.com/model-checking/kani/issues/692",

kani-compiler/src/kani_middle/analysis.rs

@@ -160,7 +160,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
             TerminatorKind::UnwindResume => Key("UnwindResume"),
             TerminatorKind::Return => Key("Return"),
             TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
-            TerminatorKind::UnwindTerminate => Key("UnwindTerminate"),
+            TerminatorKind::UnwindTerminate(_) => Key("UnwindTerminate"),
             TerminatorKind::Unreachable => Key("Unreachable"),
             TerminatorKind::Yield { .. } => Key("Yield"),
         }

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| {

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-08-25"
+channel = "nightly-2023-09-01"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

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) };
+}

tools/build-kani/src/sysroot.rs

@@ -192,12 +192,12 @@ fn is_std_lib(artifact: &Artifact) -> bool {
 /// predicate, it will copy the following files to the `target` folder.
 ///  - `rlib`: Store metadata for future codegen and executable code for concrete executions.
 ///  - shared library which are used for proc_macros.
-fn copy_libs<P>(artifacts: &[Artifact], target: &Path, predicate: P)
+fn copy_libs<P>(artifacts: &[Artifact], target: &Path, mut predicate: P)
 where
     P: FnMut(&Artifact) -> bool,
 {
     assert!(target.is_dir(), "Expected a folder, but found {}", target.display());
-    for artifact in artifacts.iter().cloned().filter(predicate) {
+    for artifact in artifacts.iter().filter(|&x| predicate(x)).cloned() {
         artifact
             .filenames
             .iter()