From 2e0e2829982a74808908bf11c071f71147d57ec5 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Fri, 25 Oct 2024 10:56:08 -0400
Subject: [PATCH] remove contract_host_param

---
 kani-compiler/src/kani_middle/stubbing/mod.rs | 43 +------------------
 .../src/kani_middle/transform/stubs.rs        |  8 +---
 2 files changed, 4 insertions(+), 47 deletions(-)

diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index f5e4517caffc..90bb0173ac55 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -12,9 +12,7 @@ use tracing::{debug, trace};
 use kani_metadata::HarnessMetadata;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Const;
-use rustc_middle::ty::{
-    self, ClauseKind, EarlyBinder, GenericPredicates, ParamEnv, TyCtxt, TypeFoldable,
-};
+use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::ConstOperand;
 use stable_mir::mir::mono::Instance;
@@ -39,40 +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 find_host_effect_arg = |generic_predicates: GenericPredicates| {
-        generic_predicates.predicates.iter().enumerate().find_map(|(idx, (clause, _))| {
-            if let ClauseKind::HostEffect(..) = clause.kind().skip_binder() {
-                Some(idx)
-            } else {
-                None
-            }
-        })
-    };
-
-    let old_generics_predicates =
-        tcx.predicates_of(rustc_internal::internal(tcx, old_def.def_id()));
-    let new_generics_predicates =
-        tcx.predicates_of(rustc_internal::internal(tcx, new_def.def_id()));
-
-    let old_generics_host_effect_index = find_host_effect_arg(old_generics_predicates);
-    let new_generics_host_effect_index = find_host_effect_arg(new_generics_predicates);
-
-    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
@@ -99,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() {
diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs
index ae9f77ba239d..3d72cff0d56d 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::{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;
@@ -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)