Add assert and function body

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

@@ -473,6 +473,10 @@ impl FunctionWithContractPass {
                 self.unused_closures.insert(recursion_closure);
                 self.unused_closures.insert(check_closure);
             }
+            ContractMode::Inplace => {
+                self.unused_closures.insert(replace_closure);
+                self.unused_closures.insert(recursion_closure);
+            }
         }
     }
 }
@@ -486,6 +490,7 @@ enum ContractMode {
     RecursiveCheck = 1,
     SimpleCheck = 2,
     Replace = 3,
+    Inplace = 4,
 }
 
 fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef {

library/kani_core/src/lib.rs

@@ -458,6 +458,9 @@ macro_rules! kani_intrinsics {
             /// Stub the body with its contract.
             pub const REPLACE: Mode = 3;
 
+            /// Put the function under a contract inline
+            pub const INLINE: Mode = 4;
+
             /// Creates a non-fatal property with the specified condition and message.
             ///
             /// This check will not impact the program control flow even when it fails.

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

@@ -20,15 +20,22 @@ impl<'a> ContractConditionsHandler<'a> {
         let modifies_name = &self.modify_name;
         let recursion_name = &self.recursion_name;
         let check_name = &self.check_name;
+        let inline_name = &self.inline_name;
 
         let replace_closure = self.replace_closure();
         let check_closure = self.check_closure();
+        let inline_closure = self.inline_closure();
+
+        println!("\n\nInline closure\n: {}\n\n", &inline_closure);
+        println!("Replace name: {}", replace_name);
+
         let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure);
 
         let span = Span::call_site();
         let replace_ident = Ident::new(&self.replace_name, span);
         let check_ident = Ident::new(&self.check_name, span);
         let recursion_ident = Ident::new(&self.recursion_name, span);
+        let inline_ident = Ident::new(&self.inline_name, span);
 
         // The order of `attrs` and `kanitool::{checked_with,
         // is_contract_generated}` is important here, because macros are
@@ -72,6 +79,10 @@ impl<'a> ContractConditionsHandler<'a> {
                         #check_closure;
                         kani_register_contract(#check_ident)
                     }
+                    kani::internal::INLINE => {
+                        #inline_closure;
+                        kani_register_contract(#inline_ident)
+                    }
                     _ => #block
                 }
             }

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

@@ -114,6 +114,20 @@ impl<'a> ContractConditionsHandler<'a> {
         )
     }
 
+    pub fn inline_closure(&self) -> TokenStream2 {
+        let replace_ident = Ident::new(&self.replace_name, Span::call_site());
+        let sig = &self.annotated_fn.sig;
+        let output = &sig.output;
+        let before = self.initial_replace_stmts();
+        let body = self.expand_inline_body(&before, &vec![]);
+
+        quote!(
+            #[kanitool::is_contract_generated(replace)]
+            #[allow(dead_code, unused_variables, unused_mut)]
+            #body;
+        )
+    }
+
     /// Expand the check body.
     ///
     /// First find the modifies body and expand that. Then expand the rest of the body.
@@ -136,6 +150,10 @@ impl<'a> ContractConditionsHandler<'a> {
         let wrapper_ident = Ident::new(WRAPPER_ARG, Span::call_site());
         let modifies_ident = Ident::new(&self.modify_name, Span::call_site());
         let stmts = &body.stmts;
+
+        let res = quote!(#(#stmts)*);
+        println!("\n\nStatement (body of function): {}\n\n", res.to_string());
+
         quote!(
             #[kanitool::is_contract_generated(wrapper)]
             #[allow(dead_code, unused_variables, unused_mut)]

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

@@ -75,6 +75,7 @@ impl<'a> ContractConditionsHandler<'a> {
         let replace_name = generate_name("replace");
         let recursion_name = generate_name("recursion_check");
         let modifies_name = generate_name("modifies");
+        let inline_name = generate_name("inline");
 
         Ok(Self {
             condition_type,
@@ -85,6 +86,7 @@ impl<'a> ContractConditionsHandler<'a> {
             replace_name,
             recursion_name,
             modify_name: modifies_name,
+            inline_name,
         })
     }
 }

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

@@ -485,6 +485,8 @@ struct ContractConditionsHandler<'a> {
     recursion_name: String,
     /// The name of the modifies closure.
     modify_name: String,
+    /// The name of the inline closure.
+    inline_name: String,
 }
 
 /// Which kind of contract attribute are we dealing with?
@@ -550,5 +552,8 @@ fn contract_main(
         Err(e) => return e.into_compile_error().into(),
     };
 
-    handler.dispatch_on(function_state).into()
+    let res = handler.dispatch_on(function_state).into();
+    // println!("res: {}", &res);
+    // panic!("res panic: {}", &res);
+    res
 }

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

@@ -16,7 +16,7 @@ use super::{
 
 impl<'a> ContractConditionsHandler<'a> {
     /// Create initial set of replace statements which is the return havoc.
-    fn initial_replace_stmts(&self) -> Vec<syn::Stmt> {
+    pub fn initial_replace_stmts(&self) -> Vec<syn::Stmt> {
         let return_type = return_type_to_type(&self.annotated_fn.sig.output);
         let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
         vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)]
@@ -69,7 +69,55 @@ impl<'a> ContractConditionsHandler<'a> {
     ///
     /// `use_nondet_result` will only be true if this is the first time we are
     /// generating a replace function.
-    fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
+    pub fn expand_inline_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
+        match &self.condition_type {
+            ContractConditionsData::Requires { attr } => {
+                let Self { attr_copy, .. } = self;
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+
+                let body = &self.annotated_fn.block;
+                let stmts = &body.stmts;
+                quote!({
+                    kani::assert(#attr, stringify!(#attr_copy));
+                    #(#stmts)*
+                })
+            }
+            ContractConditionsData::Ensures { attr } => {
+                let (remembers, ensures_clause) = build_ensures(attr);
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+
+                let (asserts, rest_of_before) = split_for_remembers(before, ClosureType::Replace);
+
+                quote!({
+                    #(#asserts)*
+                    #remembers
+                    #(#rest_of_before)*
+                    #(#after)*
+                    kani::assume(#ensures_clause);
+                    #result
+                })
+            }
+            ContractConditionsData::Modifies { attr } => {
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+                quote!({
+                    #(#before)*
+                    #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)*
+                    #(#after)*
+                    #result
+                })
+            }
+        }
+    }
+
+    /// Create the body of a stub for this contract.
+    ///
+    /// Wraps the conditions from this attribute around a prior call. If
+    /// `use_nondet_result` is `true` we will use `kani::any()` to create a
+    /// result, otherwise whatever the `body` of our annotated function was.
+    ///
+    /// `use_nondet_result` will only be true if this is the first time we are
+    /// generating a replace function.
+    pub fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 let Self { attr_copy, .. } = self;

tests/expected/function-contract/simple_inline_fail.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::requires(divisor != 0)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
+fn div(dividend: u32, divisor: u32) -> u32 {
+    dividend / divisor
+}
+
+#[kani::proof]
+#[kani::stub_verified(div)]
+fn main() {
+    assert!(div(9, 4) == 2, "contract doesn't guarantee equality");
+}