Stabilize pointer-to-reference cast validity checks (#3426)

This PR stabilizes pointer-to-reference cast validity checks, so that
they are run by default.

Resolves #3425 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

.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

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.

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"