Allow modifies clause for verification only

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

kani-compiler/src/kani_middle/attributes.rs

@@ -200,6 +200,10 @@ impl<'tcx> KaniAttributes<'tcx> {
             .collect()
     }
 
+    pub(crate) fn is_contract_generated(&self) -> bool {
+        self.map.contains_key(&KaniAttributeKind::IsContractGenerated)
+    }
+
     /// 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).

kani-compiler/src/kani_middle/reachability.rs

@@ -428,6 +428,24 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                         callee,
                                     ),
                                 );
+                            } else if caller == "kani::any" {
+                                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

@@ -20,6 +20,8 @@ use rustc_middle::ty::{self, TyCtxt};
 
 use tracing::debug;
 
+use crate::kani_middle::attributes::KaniAttributes;
+
 /// 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> {
@@ -36,8 +38,11 @@ pub fn transform<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, old_body: &'tcx Body<'t
             replaced = tcx.def_path_debug_str(replacement),
             "transform"
         );
-        let new_body = tcx.optimized_mir(replacement).clone();
+        let mut new_body = tcx.optimized_mir(replacement).clone();
         if check_compatibility(tcx, def_id, old_body, replacement, &new_body) {
+            if KaniAttributes::for_item(tcx, replacement).is_contract_generated() {
+                transform_any_modifies(tcx, &mut new_body);
+            }
             return new_body;
         }
     }
@@ -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 functions generated by contract instrumentation.
+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,29 @@ 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)]
+#[allow(dead_code)]
+pub fn any_modifies<T>() -> T {
+    // while we could use `unreachable!()` or `panic!()` as the body of this
+    // function, both cause Kani to produce a warning on any program that uses
+    // `kani::any()` (see https://github.com/model-checking/kani/issues/2010).
+    // This function is handled via a hook anyway, so we just need to put a body
+    // that rustc does not complain about. An infinite loop works out nicely.
+    #[allow(clippy::empty_loop)]
+    loop {}
+}
+
 /// 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/src/sysroot/contracts/bootstrap.rs

@@ -8,11 +8,7 @@ use proc_macro2::Span;
 use quote::quote;
 use syn::ItemFn;
 
-use super::{
-    helpers::*,
-    shared::{attach_require_kani_any, identifier_for_generated_function},
-    ContractConditionsHandler,
-};
+use super::{helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler};
 
 impl<'a> ContractConditionsHandler<'a> {
     /// The complex case. We are the first time a contract is handled on this function, so
@@ -74,7 +70,6 @@ impl<'a> ContractConditionsHandler<'a> {
         ));
 
         let mut wrapper_sig = sig.clone();
-        attach_require_kani_any(&mut wrapper_sig);
         wrapper_sig.ident = recursion_wrapper_name;
 
         let args = pats_to_idents(&mut wrapper_sig.inputs).collect::<Vec<_>>();

library/kani_macros/src/sysroot/contracts/replace.rs

@@ -8,7 +8,7 @@ use quote::quote;
 
 use super::{
     helpers::*,
-    shared::{attach_require_kani_any, make_unsafe_argument_copies, try_as_result_assign},
+    shared::{make_unsafe_argument_copies, try_as_result_assign},
     ContractConditionsData, ContractConditionsHandler,
 };
 
@@ -39,7 +39,7 @@ impl<'a> ContractConditionsHandler<'a> {
     fn ensure_bootstrapped_replace_body(&self) -> (Vec<syn::Stmt>, Vec<syn::Stmt>) {
         if self.is_first_emit() {
             let return_type = return_type_to_type(&self.annotated_fn.sig.output);
-            (vec![syn::parse_quote!(let result : #return_type = kani::any();)], vec![])
+            (vec![syn::parse_quote!(let result : #return_type = kani::any_modifies();)], vec![])
         } else {
             let stmts = &self.annotated_fn.block.stmts;
             let idx = stmts
@@ -91,7 +91,7 @@ impl<'a> ContractConditionsHandler<'a> {
             ContractConditionsData::Modifies { attr } => {
                 quote!(
                     #(#before)*
-                    #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any();)*
+                    #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)*
                     #(#after)*
                     result
                 )
@@ -112,9 +112,6 @@ impl<'a> ContractConditionsHandler<'a> {
             self.output.extend(quote!(#[kanitool::is_contract_generated(replace)]));
         }
         let mut sig = self.annotated_fn.sig.clone();
-        if self.is_first_emit() {
-            attach_require_kani_any(&mut sig);
-        }
         let body = self.make_replace_body();
         if let Some(ident) = override_function_ident {
             sig.ident = ident;
@@ -129,7 +126,7 @@ impl<'a> ContractConditionsHandler<'a> {
     }
 }
 
-/// Is this statement `let result : <...> = kani::any();`.
+/// Is this statement `let result : <...> = kani::any_modifies();`.
 fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool {
     let Some(syn::LocalInit { diverge: None, expr: e, .. }) = try_as_result_assign(stmt) else {
         return false;
@@ -152,7 +149,7 @@ fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool {
             })
             if path.segments.len() == 2
             && path.segments[0].ident == "kani"
-            && path.segments[1].ident == "any"
+            && path.segments[1].ident == "any_modifies"
             && attrs.is_empty()
         )
     )

library/kani_macros/src/sysroot/contracts/shared.rs

@@ -11,11 +11,9 @@ use std::collections::HashMap;
 
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::{quote, ToTokens};
-use syn::{
-    Attribute, PredicateType, ReturnType, Signature, TraitBound, TypeParamBound, WhereClause,
-};
+use syn::Attribute;
 
-use super::{helpers::return_type_to_type, ContractConditionsHandler, ContractFunctionState};
+use super::{ContractConditionsHandler, ContractFunctionState};
 
 impl ContractFunctionState {
     /// Do we need to emit the `is_contract_generated` tag attribute on the
@@ -88,57 +86,6 @@ pub fn make_unsafe_argument_copies(
     )
 }
 
-/// Looks complicated but does something very simple: attach a bound for
-/// `kani::Arbitrary` on the return type to the provided signature. Pushes it
-/// onto a preexisting where condition, initializing a new `where` condition if
-/// it doesn't already exist.
-///
-/// Very simple example: `fn foo() -> usize { .. }` would be rewritten `fn foo()
-/// -> usize where usize: kani::Arbitrary { .. }`.
-///
-/// This is called when we first emit a replace function. Later we can rely on
-/// this bound already being present.
-pub fn attach_require_kani_any(sig: &mut Signature) {
-    if matches!(sig.output, ReturnType::Default) {
-        // It's the default return type, e.g. `()` so we can skip adding the
-        // constraint.
-        return;
-    }
-    let return_ty = return_type_to_type(&sig.output);
-    let where_clause = sig.generics.where_clause.get_or_insert_with(|| WhereClause {
-        where_token: syn::Token![where](Span::call_site()),
-        predicates: Default::default(),
-    });
-
-    where_clause.predicates.push(syn::WherePredicate::Type(PredicateType {
-        lifetimes: None,
-        bounded_ty: return_ty.into_owned(),
-        colon_token: syn::Token![:](Span::call_site()),
-        bounds: [TypeParamBound::Trait(TraitBound {
-            paren_token: None,
-            modifier: syn::TraitBoundModifier::None,
-            lifetimes: None,
-            path: syn::Path {
-                leading_colon: None,
-                segments: [
-                    syn::PathSegment {
-                        ident: Ident::new("kani", Span::call_site()),
-                        arguments: syn::PathArguments::None,
-                    },
-                    syn::PathSegment {
-                        ident: Ident::new("Arbitrary", Span::call_site()),
-                        arguments: syn::PathArguments::None,
-                    },
-                ]
-                .into_iter()
-                .collect(),
-            },
-        })]
-        .into_iter()
-        .collect(),
-    }))
-}
-
 /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`]
 /// since we can't abstract over mutability. Input is the object to match on and the name of the
 /// function used to convert an `Option<LocalInit>` into the result type (e.g. `as_ref` and `as_mut`

tests/expected/function-contract/modifies/check_invalid_modifies.expected

@@ -0,0 +1,3 @@
+error: `&str` doesn't implement `kani::Arbitrary`. Callee: `kani::Arbitrary::any` \
+       Please, check whether the type of all objects in the modifies clause (including return types) implement `kani::Arbitrary`. \
+       This is a strict condition to use function contracts as verified stubs.

tests/expected/function-contract/modifies/check_invalid_modifies.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check that Kani reports the correct error message when modifies clause
+//! includes objects of types that do not implement `kani::Arbitrary`.
+//! This restriction is only applied when using contracts as verified stubs.
+
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+fn modify(ptr: &mut u32) -> &'static str {
+    *ptr += 1;
+    let msg: &'static str = "done";
+    msg
+}
+
+fn use_modify(ptr: &mut u32) {
+    *ptr = 99;
+    assert!(modify(ptr) == "done");
+}
+
+#[kani::proof]
+#[kani::stub_verified(modify)]
+fn harness() {
+    let mut i = kani::any_where(|x| *x < 100);
+    use_modify(&mut i);
+}

tests/expected/function-contract/modifies/mistake_condition_return.expected

@@ -0,0 +1,4 @@
+Failed Checks: assertion failed: res == 100 \
+ File: "mistake_condition_return.rs", line 31, in use_modify \
+
+VERIFICATION:- FAILED

tests/expected/function-contract/modifies/mistake_condition_return.rs

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Provide an example where users might get confuse on how to constrain
+//! the return value of functions when writing function contracts.
+//! In this case, users must remember that when using contracts as
+//! verified stubs, the return value will be havoced. To retrict the return
+//! value of a function, users may use the `result` keyword in their
+//! ensures clauses.
+
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+// In this case, one may think that by assuming `*ptr == 100`, automatically
+// we can assume the return value of this function will also be equal to 100.
+// However, contract instrumentation will create a separate non-deterministic
+// value to return in this function that can only be constrained by using the
+// `result` keyword. Thus the correct condition would be
+// `#[kani::ensures(result == 100)]`.
+#[kani::ensures(*ptr == 100)]
+fn modify(ptr: &mut u32) -> u32 {
+    *ptr += 1;
+    *ptr
+}
+
+fn use_modify(ptr: &mut u32) {
+    *ptr = 99;
+    let res = modify(ptr);
+    // This assertion won't hold because the return
+    // value of `modify` is unconstrained.
+    assert!(res == 100);
+}
+
+#[kani::proof]
+#[kani::stub_verified(modify)]
+fn harness() {
+    let mut i = kani::any();
+    use_modify(&mut i);
+}

tests/expected/function-contract/modifies/simple_only_verification.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/modifies/simple_only_verification.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check that is possible to use `modifies` clause for verifciation, but not stubbing.
+//! Using contracts as verified stubs require users to ensure the type of any object in
+//! the modifies clause (including return types) to implement `kani::Arbitrary`.
+//! This requirement is not necessary if the contract is only used for verification.
+
+#[kani::requires(*ptr < 100)]
+#[kani::modifies(ptr)]
+fn modify(ptr: &mut u32) -> &'static str {
+    *ptr += 1;
+    let msg: &'static str = "done";
+    msg
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness() {
+    let mut i = kani::any_where(|x| *x < 100);
+    modify(&mut i);
+}