From d0efa5da5503465eb88bfa86c22d5737624de7f2 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 13:00:39 -0400 Subject: [PATCH 1/7] annotate all ensures closures --- .../src/sysroot/contracts/check.rs | 3 +- .../src/sysroot/contracts/replace.rs | 3 +- .../src/sysroot/contracts/shared.rs | 29 +++++++++++++++++-- ...simple_ensures_pass_no_annotation.expected | 6 ++++ .../simple_ensures_pass_no_annotation.rs | 14 +++++++++ 5 files changed, 51 insertions(+), 4 deletions(-) create mode 100644 tests/expected/function-contract/simple_ensures_pass_no_annotation.expected create mode 100644 tests/expected/function-contract/simple_ensures_pass_no_annotation.rs diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index e76286b398cb..24021f9adaca 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -34,7 +34,8 @@ impl<'a> ContractConditionsHandler<'a> { ) } ContractConditionsData::Ensures { attr } => { - let (remembers, ensures_clause) = build_ensures(attr); + let (remembers, ensures_clause) = + build_ensures(attr, return_type_to_type(&self.annotated_fn.sig.output)); // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 7a522ea98e08..8edcf8ab1a4a 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -80,7 +80,8 @@ impl<'a> ContractConditionsHandler<'a> { ) } ContractConditionsData::Ensures { attr } => { - let (remembers, ensures_clause) = build_ensures(attr); + let (remembers, ensures_clause) = + build_ensures(attr, return_type_to_type(&self.annotated_fn.sig.output)); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #remembers diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 2682c0781661..f111c46a5fd0 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -11,9 +11,11 @@ use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; +use std::borrow::{Borrow, Cow}; use std::hash::{DefaultHasher, Hash, Hasher}; use syn::{ - spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path, + spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, + PatType, Path, Token, Type, TypeReference, }; use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; @@ -165,7 +167,7 @@ pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalI /// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;` /// where x is a unique hash. This is returned as the first return parameter. The second /// return parameter is the expression formed by passing in the result variable into the input closure. -pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { +pub fn build_ensures<'a>(data: &ExprClosure, return_type: Cow<'a, Type>) -> (TokenStream2, Expr) { let mut remembers_exprs = HashMap::new(); let mut vis = OldVisitor { t: OldLifter::new(), remembers_exprs: &mut remembers_exprs }; let mut expr = &mut data.clone(); @@ -175,6 +177,29 @@ pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { .iter() .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect)); + *expr + .inputs + .first_mut() + .expect("Ensures closure should have the output to the function as an argument") = + syn::Pat::Type(PatType { + attrs: vec![], + pat: Box::new( + expr.inputs + .first() + .expect("Ensures closure should have the output to the function as an argument") + .clone(), + ), + colon_token: Token![:](Span::call_site()), + ty: Box::new(Type::Reference(TypeReference { + and_token: Token![&](Span::call_site()), + lifetime: None, + mutability: None, + elem: Box::new( + as Borrow>::borrow(&return_type.to_owned()).clone(), + ), + })), + }); + let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); (remembers_stmts, Expr::Verbatim(quote!((#expr)(&#result)))) } diff --git a/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected b/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected new file mode 100644 index 000000000000..0779b6dc88f8 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass_no_annotation.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|result| (*result == x) | (*result == y)"\ +in function max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_ensures_pass_no_annotation.rs b/tests/expected/function-contract/simple_ensures_pass_no_annotation.rs new file mode 100644 index 000000000000..a3bf30e1c0f7 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass_no_annotation.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|result| (*result == x) | (*result == y))] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn max_harness() { + let _ = Box::new(9_usize); + max(7, 6); +} From 3877cd4ba1d4ee65d35e046fe830c724e4390ff1 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 13:41:22 -0400 Subject: [PATCH 2/7] add paren --- .../src/sysroot/contracts/shared.rs | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index f111c46a5fd0..2251a3d3841f 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -15,7 +15,7 @@ use std::borrow::{Borrow, Cow}; use std::hash::{DefaultHasher, Hash, Hasher}; use syn::{ spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, - PatType, Path, Token, Type, TypeReference, + PatParen, PatType, Path, Token, Type, TypeReference, }; use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; @@ -183,12 +183,18 @@ pub fn build_ensures<'a>(data: &ExprClosure, return_type: Cow<'a, Type>) -> (Tok .expect("Ensures closure should have the output to the function as an argument") = syn::Pat::Type(PatType { attrs: vec![], - pat: Box::new( - expr.inputs - .first() - .expect("Ensures closure should have the output to the function as an argument") - .clone(), - ), + pat: Box::new(syn::Pat::Paren(PatParen { + attrs: vec![], + paren_token: syn::token::Paren::default(), + pat: Box::new( + expr.inputs + .first() + .expect( + "Ensures closure should have the output to the function as an argument", + ) + .clone(), + ), + })), colon_token: Token![:](Span::call_site()), ty: Box::new(Type::Reference(TypeReference { and_token: Token![&](Span::call_site()), From bac90a6c9fed43f657143a665ffa0837b868969c Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 14:34:31 -0400 Subject: [PATCH 3/7] helper function --- library/kani/src/lib.rs | 4 ++ .../src/sysroot/contracts/check.rs | 3 +- .../src/sysroot/contracts/replace.rs | 3 +- .../src/sysroot/contracts/shared.rs | 37 ++----------------- 4 files changed, 9 insertions(+), 38 deletions(-) diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index acf1e08e0441..d14011cba0e5 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -326,3 +326,7 @@ pub use kani_macros::*; pub(crate) use kani_macros::unstable_feature as unstable; pub mod contracts; + +pub fn apply_closure bool>(f: U, x: &T) -> bool { + f(x) +} diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 24021f9adaca..e76286b398cb 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -34,8 +34,7 @@ impl<'a> ContractConditionsHandler<'a> { ) } ContractConditionsData::Ensures { attr } => { - let (remembers, ensures_clause) = - build_ensures(attr, return_type_to_type(&self.annotated_fn.sig.output)); + let (remembers, ensures_clause) = build_ensures(attr); // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 8edcf8ab1a4a..7a522ea98e08 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -80,8 +80,7 @@ impl<'a> ContractConditionsHandler<'a> { ) } ContractConditionsData::Ensures { attr } => { - let (remembers, ensures_clause) = - build_ensures(attr, return_type_to_type(&self.annotated_fn.sig.output)); + let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #remembers diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 2251a3d3841f..0bda7ce92ba8 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/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 std::borrow::{Borrow, Cow}; use std::hash::{DefaultHasher, Hash, Hasher}; use syn::{ - spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, - PatParen, PatType, Path, Token, Type, TypeReference, + spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path, }; use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; @@ -167,7 +165,7 @@ pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalI /// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;` /// where x is a unique hash. This is returned as the first return parameter. The second /// return parameter is the expression formed by passing in the result variable into the input closure. -pub fn build_ensures<'a>(data: &ExprClosure, return_type: Cow<'a, Type>) -> (TokenStream2, Expr) { +pub fn build_ensures<'a>(data: &ExprClosure) -> (TokenStream2, Expr) { let mut remembers_exprs = HashMap::new(); let mut vis = OldVisitor { t: OldLifter::new(), remembers_exprs: &mut remembers_exprs }; let mut expr = &mut data.clone(); @@ -177,37 +175,8 @@ pub fn build_ensures<'a>(data: &ExprClosure, return_type: Cow<'a, Type>) -> (Tok .iter() .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect)); - *expr - .inputs - .first_mut() - .expect("Ensures closure should have the output to the function as an argument") = - syn::Pat::Type(PatType { - attrs: vec![], - pat: Box::new(syn::Pat::Paren(PatParen { - attrs: vec![], - paren_token: syn::token::Paren::default(), - pat: Box::new( - expr.inputs - .first() - .expect( - "Ensures closure should have the output to the function as an argument", - ) - .clone(), - ), - })), - colon_token: Token![:](Span::call_site()), - ty: Box::new(Type::Reference(TypeReference { - and_token: Token![&](Span::call_site()), - lifetime: None, - mutability: None, - elem: Box::new( - as Borrow>::borrow(&return_type.to_owned()).clone(), - ), - })), - }); - let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - (remembers_stmts, Expr::Verbatim(quote!((#expr)(&#result)))) + (remembers_stmts, Expr::Verbatim(quote!(kani::apply_closure(#expr, &#result)))) } trait OldTrigger { From 8bfa02f80497b75934dbe2aceaf7df407b3a4349 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 14:45:05 -0400 Subject: [PATCH 4/7] remove 'a --- library/kani_macros/src/sysroot/contracts/shared.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 0bda7ce92ba8..65fcd515eae2 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -165,7 +165,7 @@ pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalI /// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;` /// where x is a unique hash. This is returned as the first return parameter. The second /// return parameter is the expression formed by passing in the result variable into the input closure. -pub fn build_ensures<'a>(data: &ExprClosure) -> (TokenStream2, Expr) { +pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { let mut remembers_exprs = HashMap::new(); let mut vis = OldVisitor { t: OldLifter::new(), remembers_exprs: &mut remembers_exprs }; let mut expr = &mut data.clone(); From 1d1cbf7b0c87f00c564172864fc9373e73360650 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 17:16:41 -0400 Subject: [PATCH 5/7] change to internal and create test for mutability --- library/kani/src/internal.rs | 7 +++++++ library/kani/src/lib.rs | 4 ---- library/kani_macros/src/sysroot/contracts/shared.rs | 2 +- .../ui/function-contracts/mutating_ensures_error.expected | 1 + tests/ui/function-contracts/mutating_ensures_error.rs | 1 + 5 files changed, 10 insertions(+), 5 deletions(-) create mode 100644 tests/ui/function-contracts/mutating_ensures_error.expected create mode 100644 tests/ui/function-contracts/mutating_ensures_error.rs diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index a910c333b112..509f2cf51962 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -90,3 +90,10 @@ pub fn untracked_deref(_: &T) -> T { #[doc(hidden)] #[rustc_diagnostic_item = "KaniInitContracts"] pub fn init_contracts() {} + +/// This should only be used within contracts. The intent is to +/// perform type inference on a closure's argument +#[doc(hidden)] +pub fn apply_closure bool>(f: U, x: &T) -> bool { + f(x) +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index d14011cba0e5..acf1e08e0441 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -326,7 +326,3 @@ pub use kani_macros::*; pub(crate) use kani_macros::unstable_feature as unstable; pub mod contracts; - -pub fn apply_closure bool>(f: U, x: &T) -> bool { - f(x) -} diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 65fcd515eae2..1ab791d9a117 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -176,7 +176,7 @@ pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect)); let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - (remembers_stmts, Expr::Verbatim(quote!(kani::apply_closure(#expr, &#result)))) + (remembers_stmts, Expr::Verbatim(quote!(kani::internal::apply_closure(#expr, &#result)))) } trait OldTrigger { diff --git a/tests/ui/function-contracts/mutating_ensures_error.expected b/tests/ui/function-contracts/mutating_ensures_error.expected new file mode 100644 index 000000000000..4e9bb3984298 --- /dev/null +++ b/tests/ui/function-contracts/mutating_ensures_error.expected @@ -0,0 +1 @@ +cannot assign to `*_x`, as `Fn` closures cannot mutate their captured variables diff --git a/tests/ui/function-contracts/mutating_ensures_error.rs b/tests/ui/function-contracts/mutating_ensures_error.rs new file mode 100644 index 000000000000..8b137891791f --- /dev/null +++ b/tests/ui/function-contracts/mutating_ensures_error.rs @@ -0,0 +1 @@ + From b28f752736bec3792048eb97c174877ea9cf38c5 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 17:24:18 -0400 Subject: [PATCH 6/7] forgot to copy paste test in --- .../ui/function-contracts/mutating_ensures_error.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/ui/function-contracts/mutating_ensures_error.rs b/tests/ui/function-contracts/mutating_ensures_error.rs index 8b137891791f..ab8de24be46a 100644 --- a/tests/ui/function-contracts/mutating_ensures_error.rs +++ b/tests/ui/function-contracts/mutating_ensures_error.rs @@ -1 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|_| {*_x += 1; true})] +fn unit(_x: &mut u32) { +} + +#[kani::proof_for_contract(id)] +fn harness() { + let mut x = kani::any(); + unit(&mut x); +} From 34359f550a52ce4132910f4357d92a8b335d008f Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Fri, 28 Jun 2024 17:24:55 -0400 Subject: [PATCH 7/7] forgot to copy paste test in --- tests/ui/function-contracts/mutating_ensures_error.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/tests/ui/function-contracts/mutating_ensures_error.rs b/tests/ui/function-contracts/mutating_ensures_error.rs index ab8de24be46a..2fc5f3c8d702 100644 --- a/tests/ui/function-contracts/mutating_ensures_error.rs +++ b/tests/ui/function-contracts/mutating_ensures_error.rs @@ -3,12 +3,10 @@ // kani-flags: -Zfunction-contracts #[kani::ensures(|_| {*_x += 1; true})] -fn unit(_x: &mut u32) { -} +fn unit(_x: &mut u32) {} #[kani::proof_for_contract(id)] fn harness() { let mut x = kani::any(); unit(&mut x); } -