Allow modifies clause for verification only (#3098)

Allow contracts to be used for verification, even if it is not suitable
for stubbing. For that, we remove the requirement that modifies and
return types of a function annotated with contracts must implement
`kani::Arbitrary`, since that is only needed for recursion and stubbing
with contract.

This is done via a new intrinsic `any_modifies` to Kani that should only
be used by contract instrumentation. The `T: Arbitrary` requirement is
only checked when users try to use the contract as stub or to check
recursive functions.

For now, we also require users to annotate their contracts with
`kani::recursion` if they want to use inductive reasoning to verify a
recursive function.

Resolves #2997.

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

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

kani-compiler/src/kani_middle/attributes.rs

@@ -70,6 +70,10 @@ enum KaniAttributeKind {
     /// expanded with additional pointer arguments that are not used in the function
     /// but referenced by the `modifies` annotation.
     InnerCheck,
+    /// Attribute used to mark contracts for functions with recursion.
+    /// We use this attribute to properly instantiate `kani::any_modifies` in
+    /// cases when recursion is present given our contracts instrumentation.
+    Recursion,
 }
 
 impl KaniAttributeKind {
@@ -84,6 +88,7 @@ impl KaniAttributeKind {
             | KaniAttributeKind::StubVerified
             | KaniAttributeKind::Unwind => true,
             KaniAttributeKind::Unstable
+            | KaniAttributeKind::Recursion
             | KaniAttributeKind::ReplacedWith
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::Modifies
@@ -102,13 +107,6 @@ impl KaniAttributeKind {
     pub fn demands_function_contract_use(self) -> bool {
         matches!(self, KaniAttributeKind::ProofForContract)
     }
-
-    /// Would this attribute be placed on a function as part of a function
-    /// contract. E.g. created by `requires`, `ensures`.
-    pub fn is_function_contract(self) -> bool {
-        use KaniAttributeKind::*;
-        matches!(self, CheckedWith | IsContractGenerated)
-    }
 }
 
 /// Bundles together common data used when evaluating the attributes of a given
@@ -200,6 +198,14 @@ impl<'tcx> KaniAttributes<'tcx> {
             .collect()
     }
 
+    pub(crate) fn is_contract_generated(&self) -> bool {
+        self.map.contains_key(&KaniAttributeKind::IsContractGenerated)
+    }
+
+    pub(crate) fn has_recursion(&self) -> bool {
+        self.map.contains_key(&KaniAttributeKind::Recursion)
+    }
+
     /// Parse and extract the `proof_for_contract(TARGET)` attribute. The
     /// returned symbol and DefId are respectively the name and id of `TARGET`,
     /// the span in the span for the attribute (contents).
@@ -316,6 +322,12 @@ impl<'tcx> KaniAttributes<'tcx> {
                         expect_no_args(self.tcx, kind, attr);
                     })
                 }
+                KaniAttributeKind::Recursion => {
+                    expect_single(self.tcx, kind, &attrs);
+                    attrs.iter().for_each(|attr| {
+                        expect_no_args(self.tcx, kind, attr);
+                    })
+                }
                 KaniAttributeKind::Solver => {
                     expect_single(self.tcx, kind, &attrs);
                     attrs.iter().for_each(|attr| {
@@ -452,6 +464,9 @@ impl<'tcx> KaniAttributes<'tcx> {
         self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| {
             match kind {
                 KaniAttributeKind::ShouldPanic => harness.should_panic = true,
+                KaniAttributeKind::Recursion => {
+                    self.tcx.dcx().span_err(self.tcx.def_span(self.item), "The attribute `kani::recursion` should only be used in combination with function contracts.");
+                },
                 KaniAttributeKind::Solver => {
                     harness.solver = parse_solver(self.tcx, attributes[0]);
                 }
@@ -661,12 +676,6 @@ fn has_kani_attribute<F: Fn(KaniAttributeKind) -> bool>(
     tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate)
 }
 
-/// Test if this function was generated by expanding a contract attribute like
-/// `requires` and `ensures`.
-pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool {
-    has_kani_attribute(tcx, def_id, KaniAttributeKind::is_function_contract)
-}
-
 /// Same as [`KaniAttributes::is_harness`] but more efficient because less
 /// attribute parsing is performed.
 pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {

kani-compiler/src/kani_middle/mod.rs

@@ -21,10 +21,8 @@ use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem};
-use stable_mir::mir::pretty::pretty_ty;
-use stable_mir::ty::{BoundVariableKind, FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
-use stable_mir::visitor::{Visitable, Visitor as TypeVisitor};
+use stable_mir::mir::mono::{InstanceKind, MonoItem};
+use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind};
 use stable_mir::{CrateDef, DefId};
 use std::fs::File;
 use std::io::BufWriter;
@@ -89,108 +87,10 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
                 .check_unstable_features(&queries.args().unstable_features);
             def_ids.insert(def_id);
         }
-
-        // We don't short circuit here since this is a type check and can shake
-        // out differently depending on generic parameters.
-        if let MonoItem::Fn(instance) = item {
-            if attributes::is_function_contract_generated(
-                tcx,
-                rustc_internal::internal(tcx, def_id),
-            ) {
-                check_is_contract_safe(tcx, *instance);
-            }
-        }
     }
     tcx.dcx().abort_if_errors();
 }
 
-/// A basic check that ensures a function with a contract does not receive
-/// mutable pointers in its input and does not return raw pointers of any kind.
-///
-/// This is a temporary safety measure because contracts cannot yet reason
-/// about the heap.
-fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
-    struct NoMutPtr<'tcx> {
-        tcx: TyCtxt<'tcx>,
-        is_prohibited: fn(Ty) -> bool,
-        /// Where (top level) did the type we're analyzing come from. Used for
-        /// composing error messages.
-        r#where: &'static str,
-        /// Adjective to describe the kind of pointer we're prohibiting.
-        /// Essentially `is_prohibited` but in English.
-        what: &'static str,
-    }
-
-    impl<'tcx> TypeVisitor for NoMutPtr<'tcx> {
-        type Break = ();
-        fn visit_ty(&mut self, ty: &Ty) -> std::ops::ControlFlow<Self::Break> {
-            if (self.is_prohibited)(*ty) {
-                // TODO make this more user friendly
-                self.tcx.dcx().err(format!(
-                    "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \
-                    as they cannot yet reason about the pointer behavior.", self.r#where, self.what,
-                    pretty_ty(ty.kind())));
-            }
-
-            // Rust's type visitor only recurses into type arguments, (e.g.
-            // `generics` in this match). This is enough for many types, but it
-            // won't look at the field types of structs or enums. So we override
-            // it here and do that ourselves.
-            //
-            // Since the field types also must contain in some form all the type
-            // arguments the visitor will see them as it inspects the fields and
-            // we don't need to call back to `super`.
-            if let TyKind::RigidTy(RigidTy::Adt(adt_def, generics)) = ty.kind() {
-                for variant in adt_def.variants() {
-                    for field in &variant.fields() {
-                        self.visit_ty(&field.ty_with_args(&generics))?;
-                    }
-                }
-                std::ops::ControlFlow::Continue(())
-            } else {
-                // For every other type.
-                ty.super_visit(self)
-            }
-        }
-    }
-
-    fn is_raw_mutable_ptr(ty: Ty) -> bool {
-        let kind = ty.kind();
-        kind.is_raw_ptr() && kind.is_mutable_ptr()
-    }
-
-    fn is_raw_ptr(ty: Ty) -> bool {
-        let kind = ty.kind();
-        kind.is_raw_ptr()
-    }
-
-    // TODO: Replace this with fn_abi.
-    // https://github.com/model-checking/kani/issues/1365
-    let bound_fn_sig = instance.ty().kind().fn_sig().unwrap();
-
-    for var in &bound_fn_sig.bound_vars {
-        if let BoundVariableKind::Ty(t) = var {
-            tcx.dcx().span_err(
-                rustc_internal::internal(tcx, instance.def.span()),
-                format!("Found a bound type variable {t:?} after monomorphization"),
-            );
-        }
-    }
-
-    let fn_typ = bound_fn_sig.skip_binder();
-
-    for (input_ty, (is_prohibited, r#where, what)) in fn_typ
-        .inputs()
-        .iter()
-        .copied()
-        .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable ")))
-        .chain([(fn_typ.output(), (is_raw_ptr as fn(_) -> _, "The return", ""))])
-    {
-        let mut v = NoMutPtr { tcx, is_prohibited, r#where, what };
-        v.visit_ty(&input_ty);
-    }
-}
-
 /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
 pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
     /// Convert MonoItem into a DefId.

kani-compiler/src/kani_middle/provide.rs

@@ -15,6 +15,8 @@ use rustc_middle::util::Providers;
 use rustc_middle::{mir::Body, query::queries, ty::TyCtxt};
 use stable_mir::mir::mono::MonoItem;
 
+use crate::kani_middle::KaniAttributes;
+
 /// Sets up rustc's query mechanism to apply Kani's custom queries to code from
 /// a crate.
 pub fn provide(providers: &mut Providers, queries: &QueryDb) {
@@ -61,6 +63,17 @@ fn run_kani_mir_passes<'tcx>(
     tracing::debug!(?def_id, "Run Kani transformation passes");
     let mut transformed_body = stubbing::transform(tcx, def_id, body);
     stubbing::transform_foreign_functions(tcx, &mut transformed_body);
+    let item_attributes = KaniAttributes::for_item(tcx, def_id);
+    // If we apply `transform_any_modifies` in all contract-generated items,
+    // we will ended up instantiating `kani::any_modifies` for the replace function
+    // every time, even if we are only checking the contract, because the function
+    // is always included during contract instrumentation. Thus, we must only apply
+    // the transformation if we are using a verified stub or in the presence of recursion.
+    if item_attributes.is_contract_generated()
+        && (stubbing::get_stub_key(tcx, def_id).is_some() || item_attributes.has_recursion())
+    {
+        stubbing::transform_any_modifies(tcx, &mut transformed_body);
+    }
     // This should be applied after stubbing so user stubs take precedence.
     ModelIntrinsics::run_pass(tcx, &mut transformed_body);
     tcx.arena.alloc(transformed_body)

kani-compiler/src/kani_middle/reachability.rs

@@ -34,6 +34,7 @@ use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind}
 use stable_mir::CrateItem;
 use stable_mir::{CrateDef, ItemKind};
 
+use crate::kani_middle::attributes::matches_diagnostic as matches_function;
 use crate::kani_middle::coercion;
 use crate::kani_middle::coercion::CoercionBase;
 use crate::kani_middle::stubbing::{get_stub, validate_instance};
@@ -440,6 +441,24 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                         callee,
                                     ),
                                 );
+                            } else if matches_function(self.tcx, self.instance.def, "KaniAny") {
+                                let receiver_ty = args.0[0].expect_ty();
+                                let sep = callee.rfind("::").unwrap();
+                                let trait_ = &callee[..sep];
+                                self.tcx.dcx().span_err(
+                                    rustc_internal::internal(self.tcx, terminator.span),
+                                    format!(
+                                        "`{}` doesn't implement \
+                                        `{}`. Callee: `{}`\nPlease, check whether the type of all \
+                                        objects in the modifies clause (including return types) \
+                                        implement `{}`.\nThis is a strict condition to use \
+                                        function contracts as verified stubs.",
+                                        pretty_ty(receiver_ty.kind()),
+                                        trait_,
+                                        callee,
+                                        trait_,
+                                    ),
+                                );
                             } else {
                                 panic!("unable to resolve call to `{callee}` in `{caller}`")
                             }

kani-compiler/src/kani_middle/stubbing/transform.rs

@@ -23,8 +23,13 @@ use tracing::debug;
 /// Returns the `DefId` of the stub for the function/method identified by the
 /// parameter `def_id`, and `None` if the function/method is not stubbed.
 pub fn get_stub(tcx: TyCtxt, def_id: DefId) -> Option<DefId> {
-    let mapping = get_stub_mapping(tcx)?;
-    mapping.get(&def_id).copied()
+    let stub_map = get_stub_mapping(tcx)?;
+    stub_map.get(&def_id).copied()
+}
+
+pub fn get_stub_key(tcx: TyCtxt, def_id: DefId) -> Option<DefId> {
+    let stub_map = get_stub_mapping(tcx)?;
+    stub_map.iter().find_map(|(&key, &val)| if val == def_id { Some(key) } else { None })
 }
 
 /// Returns the new body of a function/method if it has been stubbed out;
@@ -56,6 +61,48 @@ pub fn transform_foreign_functions<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx
     }
 }
 
+/// Traverse `body` searching for calls to `kani::any_modifies` and replace these calls
+/// with calls to `kani::any`. This happens as a separate step as it is only necessary
+/// for contract-generated functions.
+pub fn transform_any_modifies<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) {
+    let mut visitor = AnyModifiesTransformer { tcx, local_decls: body.clone().local_decls };
+    visitor.visit_body(body);
+}
+
+struct AnyModifiesTransformer<'tcx> {
+    /// The compiler context.
+    tcx: TyCtxt<'tcx>,
+    /// Local declarations of the callee function. Kani searches here for foreign functions.
+    local_decls: IndexVec<Local, LocalDecl<'tcx>>,
+}
+
+impl<'tcx> MutVisitor<'tcx> for AnyModifiesTransformer<'tcx> {
+    fn tcx(&self) -> TyCtxt<'tcx> {
+        self.tcx
+    }
+
+    fn visit_operand(&mut self, operand: &mut Operand<'tcx>, _location: Location) {
+        let func_ty = operand.ty(&self.local_decls, self.tcx);
+        if let ty::FnDef(reachable_function, arguments) = *func_ty.kind() {
+            if let Some(any_modifies) = self.tcx.get_diagnostic_name(reachable_function)
+                && any_modifies.as_str() == "KaniAnyModifies"
+            {
+                let Operand::Constant(function_definition) = operand else {
+                    return;
+                };
+                let kani_any_symbol = self
+                    .tcx
+                    .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny"))
+                    .expect("We should have a `kani::any()` definition at this point.");
+                function_definition.const_ = Const::from_value(
+                    ConstValue::ZeroSized,
+                    self.tcx.type_of(kani_any_symbol).instantiate(self.tcx, arguments),
+                );
+            }
+        }
+    }
+}
+
 struct ForeignFunctionTransformer<'tcx> {
     /// The compiler context.
     tcx: TyCtxt<'tcx>,

library/kani/src/lib.rs

@@ -156,11 +156,27 @@ pub const fn cover(_cond: bool, _msg: &'static str) {}
 /// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
 /// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
 /// valid values for type `T`.
+#[rustc_diagnostic_item = "KaniAny"]
 #[inline(always)]
 pub fn any<T: Arbitrary>() -> T {
     T::any()
 }
 
+/// This function is only used for function contract instrumentation.
+/// It behaves exaclty like `kani::any<T>()`, except it will check for the trait bounds
+/// at compilation time. It allows us to avoid type checking errors while using function
+/// contracts only for verification.
+#[rustc_diagnostic_item = "KaniAnyModifies"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn any_modifies<T>() -> T {
+    // This function should not be reacheable.
+    // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
+    // otherwise, this might not be properly instantiate. We mark this as unreachable to make
+    // sure Kani doesn't report any false positives.
+    unreachable!()
+}
+
 /// This creates a symbolic *valid* value of type `T`.
 /// The value is constrained to be a value accepted by the predicate passed to the filter.
 /// You can assign the return value of this function to a variable that you want to make symbolic.

library/kani_macros/Cargo.toml

@@ -16,3 +16,7 @@ proc-macro2 = "1.0"
 proc-macro-error = "1.0.4"
 quote = "1.0.20"
 syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] }
+
+[package.metadata.rust-analyzer]
+# This package uses rustc crates.
+rustc_private=true

library/kani_macros/src/lib.rs

@@ -52,6 +52,16 @@ pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::should_panic(attr, item)
 }
 
+/// Specifies that a function contains recursion for contract instrumentation.**
+///
+/// This attribute is only used for function-contract instrumentation. Kani uses
+/// this annotation to identify recursive functions and properly instantiate
+/// `kani::any_modifies` to check such functions using induction.
+#[proc_macro_attribute]
+pub fn recursion(attr: TokenStream, item: TokenStream) -> TokenStream {
+    attr_impl::recursion(attr, item)
+}
+
 /// Set Loop unwind limit for proof harnesses
 /// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`.
 /// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
@@ -331,6 +341,7 @@ mod sysroot {
     }
 
     kani_attribute!(should_panic, no_args);
+    kani_attribute!(recursion, no_args);
     kani_attribute!(solver);
     kani_attribute!(stub);
     kani_attribute!(unstable);
@@ -363,6 +374,7 @@ mod regular {
     }
 
     no_op!(should_panic);
+    no_op!(recursion);
     no_op!(solver);
     no_op!(stub);
     no_op!(unstable);