From 0f2bc2259648267a18c03d4f11c9e13907acf30c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Jun 2024 16:22:51 -0700 Subject: [PATCH 1/2] Fix contract of constant fn with effect feature We now check if the host effect index is present. If so, remove it before performing stub operation. --- kani-compiler/src/kani_middle/stubbing/mod.rs | 41 ++++++++++++++++--- .../src/kani_middle/transform/stubs.rs | 8 +++- .../const_fn_with_effect.expected | 2 + .../function-contract/const_fn_with_effect.rs | 18 ++++++++ .../verify_std_cmd/verify_std.expected | 5 ++- .../verify_std_cmd/verify_std.sh | 13 ++++++ 6 files changed, 78 insertions(+), 9 deletions(-) create mode 100644 tests/expected/function-contract/const_fn_with_effect.expected create mode 100644 tests/expected/function-contract/const_fn_with_effect.rs diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 1abcc0ec4f80..b5ca7fb74494 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -17,7 +17,7 @@ use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, MirVisitor}; use stable_mir::mir::Constant; -use stable_mir::ty::FnDef; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; use stable_mir::{CrateDef, CrateItem}; use self::annotations::update_stub_mapping; @@ -37,6 +37,24 @@ pub fn harness_stub_map( stub_pairs } +/// Retrieve the index of the host parameter if old definition has one, but not the new definition. +/// +/// This is to allow constant functions to be stubbed by non-constant functions when the +/// `effect` feature is on. +/// +/// Note that the opposite is not supported today, but users should be able to change their stubs. +/// +/// Note that this has no effect at runtime. +pub fn contract_host_param(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Option { + let old_generics = tcx.generics_of(rustc_internal::internal(tcx, old_def.def_id())); + let new_generics = tcx.generics_of(rustc_internal::internal(tcx, new_def.def_id())); + if old_generics.host_effect_index.is_some() && new_generics.host_effect_index.is_none() { + old_generics.host_effect_index + } else { + None + } +} + /// Checks whether the stub is compatible with the original function/method: do /// the arities and types (of the parameters and return values) match up? This /// does **NOT** check whether the type variables are constrained to implement @@ -61,15 +79,26 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul // Check whether the numbers of generic parameters match. let old_def_id = rustc_internal::internal(tcx, old_def.def_id()); let new_def_id = rustc_internal::internal(tcx, new_def.def_id()); - let old_num_generics = tcx.generics_of(old_def_id).count(); - let stub_num_generics = tcx.generics_of(new_def_id).count(); - if old_num_generics != stub_num_generics { + let old_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value; + let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value; + let TyKind::RigidTy(RigidTy::FnDef(_, mut old_args)) = old_ty.kind() else { + unreachable!("Expected Fn") + }; + let TyKind::RigidTy(RigidTy::FnDef(_, new_args)) = new_ty.kind() else { + unreachable!("Expected Fn") + }; + if let Some(idx) = contract_host_param(tcx, old_def, new_def) { + old_args.0.remove(idx); + } + + // TODO: We should check for the parameter type too or replacement will fail. + if old_args.0.len() != new_args.0.len() { let msg = format!( "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}", old_def.name(), - old_num_generics, + old_args.0.len(), new_def.name(), - stub_num_generics + new_args.0.len(), ); return Err(msg); } diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 7c4319319b8e..53db34dc902f 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -3,7 +3,7 @@ //! This module contains code related to the MIR-to-MIR pass that performs the //! stubbing of functions and methods. use crate::kani_middle::codegen_units::Stubs; -use crate::kani_middle::stubbing::validate_stub_const; +use crate::kani_middle::stubbing::{contract_host_param, validate_stub_const}; use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; @@ -46,8 +46,12 @@ impl TransformPass for FnStubPass { fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); let ty = instance.ty(); - if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() { + if let TyKind::RigidTy(RigidTy::FnDef(fn_def, mut args)) = ty.kind() { if let Some(replace) = self.stubs.get(&fn_def) { + if let Some(idx) = contract_host_param(tcx, fn_def, *replace) { + debug!(?idx, "FnStubPass::transform remove_host_param"); + args.0.remove(idx); + } let new_instance = Instance::resolve(*replace, &args).unwrap(); debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform"); if let Some(body) = FnStubValidator::validate(tcx, (fn_def, *replace), new_instance) diff --git a/tests/expected/function-contract/const_fn_with_effect.expected b/tests/expected/function-contract/const_fn_with_effect.expected new file mode 100644 index 000000000000..10cf9fe451f0 --- /dev/null +++ b/tests/expected/function-contract/const_fn_with_effect.expected @@ -0,0 +1,2 @@ +Checking harness check... +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/const_fn_with_effect.rs b/tests/expected/function-contract/const_fn_with_effect.rs new file mode 100644 index 000000000000..d57c1f42fe16 --- /dev/null +++ b/tests/expected/function-contract/const_fn_with_effect.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zmem-predicates + +//! Check that Kani contract can be applied to a constant function. +//! + +#![feature(effects)] + +#[kani::requires(kani::mem::can_dereference(arg))] +const unsafe fn dummy(arg: *const T) -> T { + std::ptr::read(arg) +} + +#[kani::proof_for_contract(dummy)] +fn check() { + unsafe { dummy(&kani::any::()) }; +} diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index 449148c5d904..aa30da375dd3 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -6,7 +6,10 @@ VERIFICATION:- SUCCESSFUL Checking harness verify::harness... VERIFICATION:- SUCCESSFUL +Checking harness verify::check_dummy_read... +VERIFICATION:- SUCCESSFUL + Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 3 successfully verified harnesses, 0 failures, 3 total. +Complete - 4 successfully verified harnesses, 0 failures, 4 total. diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 0cc2bab48429..3253ad29756e 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -47,6 +47,19 @@ pub mod verify { fn fake_function(x: bool) -> bool { x } + + #[kani::proof_for_contract(dummy_read)] + fn check_dummy_read() { + let val: char = kani::any(); + assert_eq!(unsafe { dummy_read(&val) }, val); + } + + /// Ensure we can verify constant functions. + #[kani::requires(kani::mem::can_dereference(ptr))] + #[rustc_diagnostic_item = "dummy_read"] + const unsafe fn dummy_read(ptr: *const T) -> T { + *ptr + } } ' From 3d52d94953f56239381de9b62f0fb4d4ef2d46db Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Jun 2024 19:13:35 -0700 Subject: [PATCH 2/2] Apply suggestions from code review --- kani-compiler/src/kani_middle/stubbing/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index b5ca7fb74494..f21a02b7681e 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -82,10 +82,10 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul let old_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value; let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value; let TyKind::RigidTy(RigidTy::FnDef(_, mut old_args)) = old_ty.kind() else { - unreachable!("Expected Fn") + unreachable!("Expected function, but found {old_ty}") }; let TyKind::RigidTy(RigidTy::FnDef(_, new_args)) = new_ty.kind() else { - unreachable!("Expected Fn") + unreachable!("Expected function, but found {new_ty}") }; if let Some(idx) = contract_host_param(tcx, old_def, new_def) { old_args.0.remove(idx);