Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 1 addition & 22 deletions kani-compiler/src/kani_middle/stubbing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,24 +37,6 @@ 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<usize> {
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
Expand All @@ -81,15 +63,12 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul
let new_def_id = rustc_internal::internal(tcx, new_def.def_id());
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 {
let TyKind::RigidTy(RigidTy::FnDef(_, old_args)) = old_ty.kind() else {
unreachable!("Expected function, but found {old_ty}")
};
let TyKind::RigidTy(RigidTy::FnDef(_, new_args)) = new_ty.kind() else {
unreachable!("Expected function, but found {new_ty}")
};
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() {
Expand Down
8 changes: 2 additions & 6 deletions kani-compiler/src/kani_middle/transform/stubs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::{contract_host_param, validate_stub_const};
use crate::kani_middle::stubbing::validate_stub_const;
use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
use crate::kani_middle::transform::{TransformPass, TransformationType};
use crate::kani_queries::QueryDb;
Expand Down Expand Up @@ -46,12 +46,8 @@ impl TransformPass for FnStubPass {
fn transform(&mut 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, mut args)) = ty.kind() {
if let TyKind::RigidTy(RigidTy::FnDef(fn_def, 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)
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-10-24"
channel = "nightly-2024-10-25"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Loading