Merge branch 'main' into delayed-ub-tests

.github/workflows/verify-std-check.yml

@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       # If the head failed, check if it's a new failure.
       - name: Checkout base
@@ -77,7 +77,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome

Cargo.lock

@@ -991,9 +991,9 @@ dependencies = [
 
 [[package]]
 name = "serde_test"
-version = "1.0.176"
+version = "1.0.177"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab"
+checksum = "7f901ee573cab6b3060453d2d5f0bae4e6d628c23c0a962ff9b5f1d7c8d4f1ed"
 dependencies = [
  "serde",
 ]
@@ -1098,15 +1098,15 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.11.0"
+version = "3.12.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b8fcd239983515c23a32fb82099f97d0b11b8c72f654ed659363a95c3dad7a53"
+checksum = "04cbcdd0c794ebb0d4cf35e88edd2f7d2c4c3e9a5a6dab322839b321c6a87a64"
 dependencies = [
  "cfg-if",
  "fastrand",
  "once_cell",
  "rustix",
- "windows-sys 0.52.0",
+ "windows-sys 0.59.0",
 ]
 
 [[package]]

kani-compiler/src/args.rs

@@ -82,9 +82,6 @@ pub enum ExtraChecks {
     /// Check that produced values are valid except for uninitialized values.
     /// See https://github.com/model-checking/kani/issues/920.
     Validity,
-    /// Check pointer validity when casting pointers to references.
-    /// See https://github.com/model-checking/kani/issues/2975.
-    PtrToRefCast,
     /// Check for using uninitialized memory.
     Uninit,
 }

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

@@ -1,7 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::args::ExtraChecks;
 use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
@@ -730,18 +729,14 @@ impl<'tcx> GotocCtx<'tcx> {
             Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
                 let place_ref = self.codegen_place_ref_stable(&p, loc);
-                if self.queries.args().ub_check.contains(&ExtraChecks::PtrToRefCast) {
-                    let place_ref_type = place_ref.typ().clone();
-                    match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
-                        Some(ptr_validity_check_expr) => Expr::statement_expression(
-                            vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
-                            place_ref_type,
-                            loc,
-                        ),
-                        None => place_ref,
-                    }
-                } else {
-                    place_ref
+                let place_ref_type = place_ref.typ().clone();
+                match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
+                    Some(ptr_validity_check_expr) => Expr::statement_expression(
+                        vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
+                        place_ref_type,
+                        loc,
+                    ),
+                    None => place_ref,
                 }
             }
             Rvalue::Len(p) => self.codegen_rvalue_len(p, loc),

kani-driver/src/call_single_file.rs

@@ -135,10 +135,6 @@ impl KaniSession {
             flags.push("--ub-check=validity".into())
         }
 
-        if self.args.common_args.unstable_features.contains(UnstableFeature::PtrToRefCastChecks) {
-            flags.push("--ub-check=ptr_to_ref_cast".into())
-        }
-
         if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) {
             // Automatically enable shadow memory, since the version of uninitialized memory checks
             // without non-determinism depends on it.

kani_metadata/src/unstable.rs

@@ -89,8 +89,6 @@ pub enum UnstableFeature {
     ValidValueChecks,
     /// Ghost state and shadow memory APIs.
     GhostState,
-    /// Automatically check that pointers are valid when casting them to references.
-    PtrToRefCastChecks,
     /// Automatically check that uninitialized memory is not used.
     UninitChecks,
     /// Enable an unstable option or subcommand.

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-08-06"
+channel = "nightly-2024-08-07"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/dangling-ptr-println/main.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ptr-to-ref-cast-checks
 
 //! These tests check that Kani correctly detects dangling pointer dereference inside println macro.
 //! Related issue: <https://github.com/model-checking/kani/issues/3235>.

tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ptr-to-ref-cast-checks
 
 //! This test case checks that raw pointer validity is checked before converting it to a reference, e.g., &(*ptr).
 

tests/std-checks/core/Cargo.toml

@@ -7,7 +7,7 @@ edition = "2021"
 description = "This crate contains contracts and harnesses for core library"
 
 [package.metadata.kani]
-unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true }
+unstable = { function-contracts = true, mem-predicates = true }
 
 [package.metadata.kani.flags]
 output-format = "terse"