From 407ee446eb0894d16dd7caa2530cc383cec03b1d Mon Sep 17 00:00:00 2001 From: jaisnan Date: Mon, 4 Nov 2024 17:00:11 -0500 Subject: [PATCH] Add assert and function body --- .../src/kani_middle/transform/contracts.rs | 5 ++ library/kani_core/src/lib.rs | 3 ++ .../src/sysroot/contracts/bootstrap.rs | 11 ++++ .../src/sysroot/contracts/check.rs | 18 +++++++ .../src/sysroot/contracts/initialize.rs | 2 + .../kani_macros/src/sysroot/contracts/mod.rs | 7 ++- .../src/sysroot/contracts/replace.rs | 52 ++++++++++++++++++- .../function-contract/simple_inline_fail.rs | 15 ++++++ 8 files changed, 110 insertions(+), 3 deletions(-) create mode 100644 tests/expected/function-contract/simple_inline_fail.rs diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 480c480a0aea..d3135264d5cb 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/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 { diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 4919473bf0f1..6533011573a3 100644 --- a/library/kani_core/src/lib.rs +++ b/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. diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 5a9e12a62ae2..3df23fc7eba3 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/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 } } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 863cf882f063..10084f47acc7 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/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)] diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index bd06139b27f5..c07c5bad0491 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/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, }) } } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 41be536ffb6d..a01f6437e86b 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/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 } diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index b28e178bea6d..a8343ec9f0ea 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/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 { + pub fn initial_replace_stmts(&self) -> Vec { 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; diff --git a/tests/expected/function-contract/simple_inline_fail.rs b/tests/expected/function-contract/simple_inline_fail.rs new file mode 100644 index 000000000000..dd448d2cdee6 --- /dev/null +++ b/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"); +}