From 291e6d0f2391792725c0c4df23d96c96e1cac3ef Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 12:44:12 -0700 Subject: [PATCH 01/21] Contract support for inductive verification of recursion --- library/kani_macros/src/sysroot/contracts.rs | 68 ++++++++++++++- .../gcd_rec_comparison_pass.expected | 9 ++ .../gcd_rec_comparison_pass.rs | 72 ++++++++++++++++ .../function-contract/gcd_rec_failure_code.rs | 84 +++++++++++++++++++ .../gcd_rec_failure_contract.rs | 84 +++++++++++++++++++ .../gcd_rec_replacement_pass.expected | 15 ++++ .../gcd_rec_replacement_pass.rs | 72 ++++++++++++++++ .../gcd_rec_simple_pass.expected | 9 ++ .../function-contract/gcd_rec_simple_pass.rs | 29 +++++++ 9 files changed, 440 insertions(+), 2 deletions(-) create mode 100644 tests/expected/function-contract/gcd_rec_comparison_pass.expected create mode 100644 tests/expected/function-contract/gcd_rec_comparison_pass.rs create mode 100644 tests/expected/function-contract/gcd_rec_failure_code.rs create mode 100644 tests/expected/function-contract/gcd_rec_failure_contract.rs create mode 100644 tests/expected/function-contract/gcd_rec_replacement_pass.expected create mode 100644 tests/expected/function-contract/gcd_rec_replacement_pass.rs create mode 100644 tests/expected/function-contract/gcd_rec_simple_pass.expected create mode 100644 tests/expected/function-contract/gcd_rec_simple_pass.rs diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 242d3e4deba0..1bdc4fd6e494 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -772,6 +772,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool let check_fn_name = identifier_for_generated_function(&item_fn, "check", item_hash); let replace_fn_name = identifier_for_generated_function(&item_fn, "replace", item_hash); + let recursion_wrapper_name = + identifier_for_generated_function(&item_fn, "recursion_wrapper", item_hash); // Constructing string literals explicitly here, because `stringify!` // doesn't work. Let's say we have an identifier `check_fn` and we were @@ -781,7 +783,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // instead the *expression* `stringify!(check_fn)`. let replace_fn_name_str = syn::LitStr::new(&replace_fn_name.to_string(), Span::call_site()); - let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + let recursion_wrapper_name_str = + syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site()); // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are @@ -794,13 +797,40 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool let ItemFn { attrs, vis, sig, block } = &item_fn; handler.output.extend(quote!( #(#attrs)* - #[kanitool::checked_with = #check_fn_name_str] + #[kanitool::checked_with = #recursion_wrapper_name_str] #[kanitool::replaced_with = #replace_fn_name_str] #vis #sig { #block } )); + let mut wrapper_sig = sig.clone(); + wrapper_sig.ident = recursion_wrapper_name; + + let args = pats_to_idents(&mut wrapper_sig.inputs).collect::>(); + let also_args = args.iter(); + let (call_check, call_replace) = if is_probably_impl_fn(sig) { + (quote!(Self::#check_fn_name), quote!(Self::#replace_fn_name)) + } else { + (quote!(#check_fn_name), quote!(#replace_fn_name)) + }; + + handler.output.extend(quote!( + #[allow(dead_code, unused_variables)] + #[kanitool::is_contract_generated(recursion_wrapper)] + #wrapper_sig { + static mut REENTRY: bool = false; + if unsafe { REENTRY } { + #call_replace(#(#args),*) + } else { + unsafe { REENTRY = true }; + let result = #call_check(#(#also_args),*); + unsafe { REENTRY = false }; + result + } + } + )); + handler.emit_check_function(check_fn_name); handler.emit_replace_function(replace_fn_name, true); } @@ -809,6 +839,40 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool output.into() } +fn pats_to_idents

(sig: &mut syn::punctuated::Punctuated) -> impl Iterator + '_ { + sig.iter_mut().enumerate().map(|(i, arg)| match arg { + syn::FnArg::Receiver(_) => Ident::new("self", Span::call_site()), + syn::FnArg::Typed(syn::PatType { + pat, .. + }) => { + let ident = Ident::new(&format!("arg{i}"), Span::mixed_site()); + *pat.as_mut() = syn::Pat::Ident(syn::PatIdent { + attrs: vec![], + by_ref: None, + mutability: None, + ident: ident.clone(), + subpat: None, + }); + ident + } + }) +} + +struct SelfDetector(bool); + +impl<'ast> Visit<'ast> for SelfDetector { + fn visit_path(&mut self, i: &'ast syn::Path) { + self.0 |= i.get_ident().map_or(false, |i| i == "self") + || i.get_ident().map_or(false, |i| i == "Self") + } +} + +fn is_probably_impl_fn(sig: &Signature) -> bool { + let mut self_detector = SelfDetector(false); + self_detector.visit_signature(sig); + self_detector.0 +} + /// This is very similar to the kani_attribute macro, but it instead creates /// key-value style attributes which I find a little easier to parse. macro_rules! passthrough { diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected new file mode 100644 index 000000000000..7106ad6f7320 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected @@ -0,0 +1,9 @@ +assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +assertion\ +- Status: SUCCESS\ +- Description: "result != 0 && x % result == 0 && y % result == 0" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.rs b/tests/expected/function-contract/gcd_rec_comparison_pass.rs new file mode 100644 index 000000000000..b818570bd36d --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res) + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn harness_as_check() { + gcd_harness() +} + +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_rec_failure_code.rs b/tests/expected/function-contract/gcd_rec_failure_code.rs new file mode 100644 index 000000000000..00410c43fbe7 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_failure_code.rs @@ -0,0 +1,84 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res + 1) + } +} + +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} + + + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn harness_as_check() { + gcd_harness() +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn gcd_as_replace() { + gcd_harness() +} + +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_rec_failure_contract.rs b/tests/expected/function-contract/gcd_rec_failure_contract.rs new file mode 100644 index 000000000000..c9fc27ffa430 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_failure_contract.rs @@ -0,0 +1,84 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +// Changed `0` to `1` in `x % result == 0` to mess with this contract +#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res) + } +} +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} + + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn harness_as_check() { + gcd_harness() +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn gcd_as_replace() { + gcd_harness() +} + +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected new file mode 100644 index 000000000000..808f63b40e46 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected @@ -0,0 +1,15 @@ +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: self.num % f2.num == 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: self.den % f2.den == 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: gcd1 == gcd2" + +gcd.assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" \ No newline at end of file diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs new file mode 100644 index 000000000000..f7ce2bbf8b49 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res) + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn gcd_as_replace() { + gcd_harness() +} + +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected new file mode 100644 index 000000000000..7106ad6f7320 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected @@ -0,0 +1,9 @@ +assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +assertion\ +- Status: SUCCESS\ +- Description: "result != 0 && x % result == 0 && y % result == 0" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.rs b/tests/expected/function-contract/gcd_rec_simple_pass.rs new file mode 100644 index 000000000000..437852dede80 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_simple_pass.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res) + } +} + +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} From 18d7271b2d384049e11e18498e156ef970a642d6 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 12:53:08 -0700 Subject: [PATCH 02/21] Fix test cases, formatting --- library/kani_macros/src/sysroot/contracts.rs | 8 +- .../gcd_rec_code_fail.expected | 3 + .../function-contract/gcd_rec_code_fail.rs | 28 +++++++ .../gcd_rec_comparison_pass.expected | 2 +- .../gcd_rec_contract_fail.expected | 3 + .../gcd_rec_contract_fail.rs | 29 +++++++ .../function-contract/gcd_rec_failure_code.rs | 84 ------------------- .../gcd_rec_failure_contract.rs | 84 ------------------- .../gcd_rec_replacement_pass.expected | 4 +- .../gcd_rec_simple_pass.expected | 2 +- 10 files changed, 72 insertions(+), 175 deletions(-) create mode 100644 tests/expected/function-contract/gcd_rec_code_fail.expected create mode 100644 tests/expected/function-contract/gcd_rec_code_fail.rs create mode 100644 tests/expected/function-contract/gcd_rec_contract_fail.expected create mode 100644 tests/expected/function-contract/gcd_rec_contract_fail.rs delete mode 100644 tests/expected/function-contract/gcd_rec_failure_code.rs delete mode 100644 tests/expected/function-contract/gcd_rec_failure_contract.rs diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 1bdc4fd6e494..c9980eac9bce 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -839,12 +839,12 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool output.into() } -fn pats_to_idents

(sig: &mut syn::punctuated::Punctuated) -> impl Iterator + '_ { +fn pats_to_idents

( + sig: &mut syn::punctuated::Punctuated, +) -> impl Iterator + '_ { sig.iter_mut().enumerate().map(|(i, arg)| match arg { syn::FnArg::Receiver(_) => Ident::new("self", Span::call_site()), - syn::FnArg::Typed(syn::PatType { - pat, .. - }) => { + syn::FnArg::Typed(syn::PatType { pat, .. }) => { let ident = Ident::new(&format!("arg{i}"), Span::mixed_site()); *pat.as_mut() = syn::Pat::Ident(syn::PatIdent { attrs: vec![], diff --git a/tests/expected/function-contract/gcd_rec_code_fail.expected b/tests/expected/function-contract/gcd_rec_code_fail.expected new file mode 100644 index 000000000000..80dbaadbf4c7 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_code_fail.expected @@ -0,0 +1,3 @@ +Failed Checks: result != 0 && x % result == 0 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_code_fail.rs b/tests/expected/function-contract/gcd_rec_code_fail.rs new file mode 100644 index 000000000000..01c1372bd1a5 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_code_fail.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res + 1) + } +} + +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected index 7106ad6f7320..da647dfd40aa 100644 --- a/tests/expected/function-contract/gcd_rec_comparison_pass.expected +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected @@ -6,4 +6,4 @@ assertion\ - Status: SUCCESS\ - Description: "result != 0 && x % result == 0 && y % result == 0" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.expected b/tests/expected/function-contract/gcd_rec_contract_fail.expected new file mode 100644 index 000000000000..bfb470192a39 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_contract_fail.expected @@ -0,0 +1,3 @@ +Failed Checks: result != 0 && x % result == 1 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.rs b/tests/expected/function-contract/gcd_rec_contract_fail.rs new file mode 100644 index 000000000000..9225b55e877e --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_contract_fail.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +// Changed `0` to `1` in `x % result == 0` to mess with this contract +#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { + min + } else { + gcd(min, res) + } +} +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/gcd_rec_failure_code.rs b/tests/expected/function-contract/gcd_rec_failure_code.rs deleted file mode 100644 index 00410c43fbe7..000000000000 --- a/tests/expected/function-contract/gcd_rec_failure_code.rs +++ /dev/null @@ -1,84 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts -type T = u8; - -/// Euclid's algorithm for calculating the GCD of two numbers -#[kani::requires(x != 0 && y != 0)] -#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] -fn gcd(x: T, y: T) -> T { - let mut max = x; - let mut min = y; - if min > max { - let val = max; - max = min; - min = val; - } - let res = max % min; - if res == 0 { - min - } else { - gcd(min, res + 1) - } -} - -#[kani::proof_for_contract(gcd)] -fn simple_harness() { - let _ = gcd(kani::any(), kani::any()); -} - - - -struct Frac { - pub num: T, - pub den: T, -} - -impl Frac { - // constructor - pub fn new(num: T, den: T) -> Self { - Frac { num, den } - } - - /// Method to simplify fraction - /// For example, `Frac { num: 10, den: 15 }` gets simplified to - /// `Frac { num: 2, num: 3 }` - pub fn simplify(&self) -> Frac { - let gcd = gcd(self.num, self.den); - Frac::new(self.num / gcd, self.den / gcd) - } - - pub fn check_equals(&self, f2: Frac) { - assert_eq!(self.num % f2.num, 0); - assert_eq!(self.den % f2.den, 0); - let gcd1 = self.num / f2.num; - let gcd2 = self.den / f2.den; - assert_eq!(gcd1, gcd2); - } -} - -#[kani::proof_for_contract(gcd)] -#[kani::unwind(12)] -fn harness_as_check() { - gcd_harness() -} - -#[kani::proof] -#[kani::stub_verified(gcd)] -fn gcd_as_replace() { - gcd_harness() -} - -fn gcd_harness() { - // Needed to avoid having `free` be removed as unused function. This is - // because DFCC contract enforcement assumes that a definition for `free` - // exists. - let _ = Box::new(9_usize); - let num: T = kani::any(); - let den: T = kani::any(); - kani::assume(num != 0); - kani::assume(den != 0); - let frac = Frac::new(num, den); - let simplified_frac = frac.simplify(); - frac.check_equals(simplified_frac); -} diff --git a/tests/expected/function-contract/gcd_rec_failure_contract.rs b/tests/expected/function-contract/gcd_rec_failure_contract.rs deleted file mode 100644 index c9fc27ffa430..000000000000 --- a/tests/expected/function-contract/gcd_rec_failure_contract.rs +++ /dev/null @@ -1,84 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts -type T = u8; - -/// Euclid's algorithm for calculating the GCD of two numbers -#[kani::requires(x != 0 && y != 0)] -// Changed `0` to `1` in `x % result == 0` to mess with this contract -#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] -fn gcd(x: T, y: T) -> T { - let mut max = x; - let mut min = y; - if min > max { - let val = max; - max = min; - min = val; - } - - let res = max % min; - if res == 0 { - min - } else { - gcd(min, res) - } -} -#[kani::proof_for_contract(gcd)] -fn simple_harness() { - let _ = gcd(kani::any(), kani::any()); -} - - -struct Frac { - pub num: T, - pub den: T, -} - -impl Frac { - // constructor - pub fn new(num: T, den: T) -> Self { - Frac { num, den } - } - - /// Method to simplify fraction - /// For example, `Frac { num: 10, den: 15 }` gets simplified to - /// `Frac { num: 2, num: 3 }` - pub fn simplify(&self) -> Frac { - let gcd = gcd(self.num, self.den); - Frac::new(self.num / gcd, self.den / gcd) - } - - pub fn check_equals(&self, f2: Frac) { - assert_eq!(self.num % f2.num, 0); - assert_eq!(self.den % f2.den, 0); - let gcd1 = self.num / f2.num; - let gcd2 = self.den / f2.den; - assert_eq!(gcd1, gcd2); - } -} - -#[kani::proof_for_contract(gcd)] -#[kani::unwind(12)] -fn harness_as_check() { - gcd_harness() -} - -#[kani::proof] -#[kani::stub_verified(gcd)] -fn gcd_as_replace() { - gcd_harness() -} - -fn gcd_harness() { - // Needed to avoid having `free` be removed as unused function. This is - // because DFCC contract enforcement assumes that a definition for `free` - // exists. - let _ = Box::new(9_usize); - let num: T = kani::any(); - let den: T = kani::any(); - kani::assume(num != 0); - kani::assume(den != 0); - let frac = Frac::new(num, den); - let simplified_frac = frac.simplify(); - frac.check_equals(simplified_frac); -} diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected index 808f63b40e46..29c61cf9437c 100644 --- a/tests/expected/function-contract/gcd_rec_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected @@ -12,4 +12,6 @@ Frac::check_equals.assertion\ gcd.assertion\ - Status: SUCCESS\ -- Description: "x != 0 && y != 0" \ No newline at end of file +- Description: "x != 0 && y != 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected index 7106ad6f7320..da647dfd40aa 100644 --- a/tests/expected/function-contract/gcd_rec_simple_pass.expected +++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected @@ -6,4 +6,4 @@ assertion\ - Status: SUCCESS\ - Description: "result != 0 && x % result == 0 && y % result == 0" -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL From 6ea4a1bd7f29a0fac7800663fc61a29e300dba71 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 13:27:16 -0700 Subject: [PATCH 03/21] Update Documentation --- library/kani_macros/src/sysroot/contracts.rs | 121 ++++++++++++++----- 1 file changed, 93 insertions(+), 28 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index c9980eac9bce..43a0f47ca0a1 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -60,29 +60,31 @@ //! arrow represents the expansion of a `requires` or `ensures` macro. //! //! ```plain -//! v -//! +-----------+ -//! | Untouched | -//! | Function | -//! +-----+-----+ -//! | -//! Emit | Generate + Copy Attributes -//! +-----------------+------------------+ -//! | | | -//! | | | -//! v v v -//! +----------+ +-------+ +---------+ -//! | Original |<-+ | Check |<-+ | Replace |<-+ -//! +--+-------+ | +---+---+ | +----+----+ | -//! | | Ignore | | Augment | | Augment -//! +----------+ +------+ +-------+ -//! -//! | | | | -//! +--------------+ +------------------------------+ -//! Presence of Presence of -//! "checked_with" "is_contract_generated" -//! -//! State is detected via +//! │ Start +//! ▼ +//! ┌───────────┐ +//! │ Untouched │ +//! │ Function │ +//! └─────┬─────┘ +//! │ +//! Emit │ Generate + Copy Attributes +//! ┌─────────────────┴─────┬──────────┬─────────────────┐ +//! │ │ │ │ +//! │ │ │ │ +//! ▼ ▼ ▼ ▼ +//! ┌──────────┐ ┌───────────┐ ┌───────┐ ┌─────────┐ +//! │ Original │◄─┐ │ Recursion │ │ Check │◄─┐ │ Replace │◄─┐ +//! └──┬───────┘ │ │ Wrapper │ └───┬───┘ │ └────┬────┘ │ +//! │ │ Ignore └───────────┘ │ │ Augment │ │ Augment +//! └──────────┘ └──────┘ └───────┘ +//! +//! │ │ │ │ +//! └───────────────┘ └─────────────────────────────────────────────┘ +//! +//! Presence of Presence of +//! "checked_with" "is_contract_generated" +//! +//! State is detected via //! ``` //! //! All named arguments of the annotated function are unsafely shallow-copied @@ -95,12 +97,12 @@ //! //! ## Check function //! -//! Generates a `check__` function that assumes preconditions +//! Generates a `_check_` function that assumes preconditions //! and asserts postconditions. The check function is also marked as generated //! with the `#[kanitool::is_contract_generated(check)]` attribute. //! //! Decorates the original function with `#[kanitool::checked_by = -//! "check__"]`. +//! "_check_"]`. //! //! The check function is a copy of the original function with preconditions //! added before the body and postconditions after as well as injected before @@ -109,17 +111,63 @@ //! //! ## Replace Function //! -//! As the mirror to that also generates a `replace__` +//! As the mirror to that also generates a `_replace_` //! function that asserts preconditions and assumes postconditions. The replace //! function is also marked as generated with the //! `#[kanitool::is_contract_generated(replace)]` attribute. //! //! Decorates the original function with `#[kanitool::replaced_by = -//! "replace__"]`. +//! "_replace_"]`. //! //! The replace function has the same signature as the original function but its //! body is replaced by `kani::any()`, which generates a non-deterministic //! value. +//! +//! ## Inductive Verification +//! +//! To to efficiently check recursive functions we verify them inductively. To +//! be able to do this we need both the check and replace functions we have seen +//! before. +//! +//! Inductive verification is comprised of a hypothesis and an induction step. +//! The hypothesis in this case is the replace function. It represents the +//! assumption that the contracts holds if the preconditions are satisfied. The +//! induction step is the check function, which ensures that the contract holds, +//! assuming the preconditions hold. +//! +//! Since the induction revolves around the recursive call we can simply set it +//! up upon entry into the body of the function under verification. We use a +//! global variable that tracks whether we are re-entering the function +//! recursively and starts off as `false`. On entry to the function we flip the +//! variable to `true` and dispatch to the check (induction step). if the check +//! recursively calls our function our re-entry tracker now reads `true` and we +//! dispatch to the replacement (application of induction hypothesis). Because +//! the replacement function only checks the conditions and does not perform +//! other computation we will only ever go "one recursion level deep", making +//! inductive verification very efficient. Once the check function returns we +//! flip the tracker variable back to `false` in case the function is called +//! more than one in it's harness. +//! +//! To facilitate all this we generate a `_recursion_wrapper_` +//! function with the following shape: +//! +//! ```ignored +//! fn recursion_wrapper_...(fn args ...) { +//! static REENTRY: bool = false; +//! +//! if unsafe { REENTRY } { +//! call_replace(fn args...) +//! } else { +//! unsafe { reentry = true }; +//! let result = call_check(fn args...); +//! unsafe { reentry = false }; +//! result +//! } +//! } +//! ``` +//! +//! We register this function as `#[kanitool::checked_with = +//! "recursion_wrapper_..."]` instead of the check function. //! //! # Complete example //! @@ -134,7 +182,7 @@ //! Turns into //! //! ``` -//! #[kanitool::checked_with = "div_check_965916"] +//! #[kanitool::checked_with = "div_recursion_wrapper_965916"] //! #[kanitool::replaced_with = "div_replace_965916"] //! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } //! @@ -164,6 +212,22 @@ //! std::mem::forget(divisor_renamed); //! result //! } +//! +//! #[allow(dead_code)] +//! #[allow(unused_variables)] +//! #[kanitool::is_contract_generated(recursion_wrapper)] +//! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 { +//! static REENTRY: bool = false; +//! +//! if unsafe { REENTRY } { +//! div_replace_965916(dividend, divisor) +//! } else { +//! unsafe { reentry = true }; +//! let result = div_check_965916(dividend, divisor); +//! unsafe { reentry = false }; +//! result +//! } +//! } //! ``` use proc_macro::{Diagnostic, TokenStream}; @@ -196,6 +260,7 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } + /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { From 92c595a81c6e477072577a2557b1fe6784fa71bf Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 13:30:20 -0700 Subject: [PATCH 04/21] Formatting test cases --- tests/expected/function-contract/gcd_rec_code_fail.rs | 6 +----- tests/expected/function-contract/gcd_rec_comparison_pass.rs | 6 +----- tests/expected/function-contract/gcd_rec_contract_fail.rs | 6 +----- .../expected/function-contract/gcd_rec_replacement_pass.rs | 6 +----- tests/expected/function-contract/gcd_rec_simple_pass.rs | 6 +----- 5 files changed, 5 insertions(+), 25 deletions(-) diff --git a/tests/expected/function-contract/gcd_rec_code_fail.rs b/tests/expected/function-contract/gcd_rec_code_fail.rs index 01c1372bd1a5..5f63cb247ebf 100644 --- a/tests/expected/function-contract/gcd_rec_code_fail.rs +++ b/tests/expected/function-contract/gcd_rec_code_fail.rs @@ -15,11 +15,7 @@ fn gcd(x: T, y: T) -> T { min = val; } let res = max % min; - if res == 0 { - min - } else { - gcd(min, res + 1) - } + if res == 0 { min } else { gcd(min, res + 1) } } #[kani::proof_for_contract(gcd)] diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.rs b/tests/expected/function-contract/gcd_rec_comparison_pass.rs index b818570bd36d..b08d94504bf7 100644 --- a/tests/expected/function-contract/gcd_rec_comparison_pass.rs +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.rs @@ -16,11 +16,7 @@ fn gcd(x: T, y: T) -> T { } let res = max % min; - if res == 0 { - min - } else { - gcd(min, res) - } + if res == 0 { min } else { gcd(min, res) } } struct Frac { diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.rs b/tests/expected/function-contract/gcd_rec_contract_fail.rs index 9225b55e877e..3fe34cb2effc 100644 --- a/tests/expected/function-contract/gcd_rec_contract_fail.rs +++ b/tests/expected/function-contract/gcd_rec_contract_fail.rs @@ -17,11 +17,7 @@ fn gcd(x: T, y: T) -> T { } let res = max % min; - if res == 0 { - min - } else { - gcd(min, res) - } + if res == 0 { min } else { gcd(min, res) } } #[kani::proof_for_contract(gcd)] fn simple_harness() { diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs index f7ce2bbf8b49..d8a5bbd234ed 100644 --- a/tests/expected/function-contract/gcd_rec_replacement_pass.rs +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs @@ -16,11 +16,7 @@ fn gcd(x: T, y: T) -> T { } let res = max % min; - if res == 0 { - min - } else { - gcd(min, res) - } + if res == 0 { min } else { gcd(min, res) } } struct Frac { diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.rs b/tests/expected/function-contract/gcd_rec_simple_pass.rs index 437852dede80..ae55efa62b45 100644 --- a/tests/expected/function-contract/gcd_rec_simple_pass.rs +++ b/tests/expected/function-contract/gcd_rec_simple_pass.rs @@ -16,11 +16,7 @@ fn gcd(x: T, y: T) -> T { } let res = max % min; - if res == 0 { - min - } else { - gcd(min, res) - } + if res == 0 { min } else { gcd(min, res) } } #[kani::proof_for_contract(gcd)] From 481e7b5f58e0ceb07b6de2fdaeb40b2ca253cf47 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 13:37:22 -0700 Subject: [PATCH 05/21] More whitespace --- library/kani_macros/src/sysroot/contracts.rs | 26 ++++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 43a0f47ca0a1..0eda8ab93ba2 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -77,13 +77,13 @@ //! └──┬───────┘ │ │ Wrapper │ └───┬───┘ │ └────┬────┘ │ //! │ │ Ignore └───────────┘ │ │ Augment │ │ Augment //! └──────────┘ └──────┘ └───────┘ -//! +//! //! │ │ │ │ //! └───────────────┘ └─────────────────────────────────────────────┘ -//! +//! //! Presence of Presence of //! "checked_with" "is_contract_generated" -//! +//! //! State is detected via //! ``` //! @@ -122,19 +122,19 @@ //! The replace function has the same signature as the original function but its //! body is replaced by `kani::any()`, which generates a non-deterministic //! value. -//! +//! //! ## Inductive Verification -//! +//! //! To to efficiently check recursive functions we verify them inductively. To //! be able to do this we need both the check and replace functions we have seen //! before. -//! +//! //! Inductive verification is comprised of a hypothesis and an induction step. //! The hypothesis in this case is the replace function. It represents the //! assumption that the contracts holds if the preconditions are satisfied. The //! induction step is the check function, which ensures that the contract holds, //! assuming the preconditions hold. -//! +//! //! Since the induction revolves around the recursive call we can simply set it //! up upon entry into the body of the function under verification. We use a //! global variable that tracks whether we are re-entering the function @@ -147,14 +147,14 @@ //! inductive verification very efficient. Once the check function returns we //! flip the tracker variable back to `false` in case the function is called //! more than one in it's harness. -//! +//! //! To facilitate all this we generate a `_recursion_wrapper_` //! function with the following shape: -//! +//! //! ```ignored //! fn recursion_wrapper_...(fn args ...) { //! static REENTRY: bool = false; -//! +//! //! if unsafe { REENTRY } { //! call_replace(fn args...) //! } else { @@ -165,7 +165,7 @@ //! } //! } //! ``` -//! +//! //! We register this function as `#[kanitool::checked_with = //! "recursion_wrapper_..."]` instead of the check function. //! @@ -212,13 +212,13 @@ //! std::mem::forget(divisor_renamed); //! result //! } -//! +//! //! #[allow(dead_code)] //! #[allow(unused_variables)] //! #[kanitool::is_contract_generated(recursion_wrapper)] //! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 { //! static REENTRY: bool = false; -//! +//! //! if unsafe { REENTRY } { //! div_replace_965916(dividend, divisor) //! } else { From ad7c2de968f50c215b1ba265705225587ee1cf14 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 13:45:21 -0700 Subject: [PATCH 06/21] This whitespace stuff is getting ridiculous --- library/kani_macros/src/sysroot/contracts.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 0eda8ab93ba2..91c2f6328dd3 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -260,7 +260,6 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } - /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { From 65a2a17c3338996fcba2d358a16cb03932465eaf Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 5 Oct 2023 14:08:17 -0700 Subject: [PATCH 07/21] AAttach require any --- library/kani_macros/src/sysroot/contracts.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 91c2f6328dd3..bcc630e3b2cb 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -869,6 +869,7 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool )); 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::>(); From a31176c79098205ca0b2c2b199cdf06653754551 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Sun, 8 Oct 2023 12:47:59 -0400 Subject: [PATCH 08/21] Fix names in test cases --- .../expected/function-contract/arbitrary_ensures_fail.expected | 2 +- .../expected/function-contract/arbitrary_ensures_pass.expected | 2 +- .../expected/function-contract/arbitrary_requires_pass.expected | 2 +- tests/expected/function-contract/gcd_failure_code.expected | 2 +- tests/expected/function-contract/gcd_failure_contract.expected | 2 +- tests/expected/function-contract/gcd_success.expected | 2 +- tests/expected/function-contract/simple_ensures_fail.expected | 2 +- tests/expected/function-contract/simple_ensures_pass.expected | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected index 587dc3f46975..0a59d2cea5eb 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.expected +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: FAILURE\ - Description: "result == x"\ in function max diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected index af1e09d1fe62..85619fa84c22 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.expected +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: SUCCESS\ - Description: "result == x || result == y"\ in function max diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index 814fe6757ca3..d7560355afe3 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -1,4 +1,4 @@ -div.arithmetic_overflow\ +arithmetic_overflow\ - Status: SUCCESS\ - Description: "attempt to divide by zero"\ in function div diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected index 9488e9dcac9a..c7fe5a721abb 100644 --- a/tests/expected/function-contract/gcd_failure_code.expected +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +assertion\ - Status: FAILURE\ - Description: "result != 0 && x % result == 0 && y % result == 0"\ in function gcd diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected index 3ae94b199d6e..aeadfb563ab9 100644 --- a/tests/expected/function-contract/gcd_failure_contract.expected +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +assertion\ - Status: FAILURE\ - Description: "result != 0 && x % result == 1 && y % result == 0"\ in function gcd\ diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected index d75b31b151df..73b531d424b9 100644 --- a/tests/expected/function-contract/gcd_success.expected +++ b/tests/expected/function-contract/gcd_success.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +assertion\ - Status: SUCCESS\ - Description: "result != 0 && x % result == 0 && y % result == 0"\ in function gcd diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected index a65fff824ea6..8e9b42d42640 100644 --- a/tests/expected/function-contract/simple_ensures_fail.expected +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: FAILURE\ - Description: "result == x"\ in function max diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected index b3e15aefcb9d..5a7874964413 100644 --- a/tests/expected/function-contract/simple_ensures_pass.expected +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: SUCCESS\ - Description: "(result == x) | (result == y)"\ in function max From ba9ea4eddec677687cd3e8a425ce8e83e57c067e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 11:54:33 -0700 Subject: [PATCH 09/21] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani_macros/src/sysroot/contracts.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index bcc630e3b2cb..4cd4024e1c83 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -139,14 +139,14 @@ //! up upon entry into the body of the function under verification. We use a //! global variable that tracks whether we are re-entering the function //! recursively and starts off as `false`. On entry to the function we flip the -//! variable to `true` and dispatch to the check (induction step). if the check +//! variable to `true` and dispatch to the check (induction step). If the check //! recursively calls our function our re-entry tracker now reads `true` and we //! dispatch to the replacement (application of induction hypothesis). Because //! the replacement function only checks the conditions and does not perform //! other computation we will only ever go "one recursion level deep", making //! inductive verification very efficient. Once the check function returns we //! flip the tracker variable back to `false` in case the function is called -//! more than one in it's harness. +//! more than once in its harness. //! //! To facilitate all this we generate a `_recursion_wrapper_` //! function with the following shape: From 690219369ea7bc410c76a5aabdbf9c93afe3e456 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 11:54:16 -0700 Subject: [PATCH 10/21] Suggestions from Zyad --- library/kani_macros/src/sysroot/contracts.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 4cd4024e1c83..f40633d2dca5 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -125,7 +125,7 @@ //! //! ## Inductive Verification //! -//! To to efficiently check recursive functions we verify them inductively. To +//! To efficiently check recursive functions we verify them inductively. To //! be able to do this we need both the check and replace functions we have seen //! before. //! @@ -153,7 +153,7 @@ //! //! ```ignored //! fn recursion_wrapper_...(fn args ...) { -//! static REENTRY: bool = false; +//! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { //! call_replace(fn args...) @@ -217,7 +217,7 @@ //! #[allow(unused_variables)] //! #[kanitool::is_contract_generated(recursion_wrapper)] //! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 { -//! static REENTRY: bool = false; +//! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { //! div_replace_965916(dividend, divisor) From 832f92cdbaf7c4a4434a112ef132e3a26ffdb2fc Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 20:46:16 -0400 Subject: [PATCH 11/21] Better self detector --- library/kani_macros/src/sysroot/contracts.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index f40633d2dca5..afa7b0c7f7db 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -908,7 +908,7 @@ fn pats_to_idents

( sig: &mut syn::punctuated::Punctuated, ) -> impl Iterator + '_ { sig.iter_mut().enumerate().map(|(i, arg)| match arg { - syn::FnArg::Receiver(_) => Ident::new("self", Span::call_site()), + syn::FnArg::Receiver(_) => Ident::from(syn::Token![self](Span::call_site())), syn::FnArg::Typed(syn::PatType { pat, .. }) => { let ident = Ident::new(&format!("arg{i}"), Span::mixed_site()); *pat.as_mut() = syn::Pat::Ident(syn::PatIdent { @@ -927,8 +927,11 @@ struct SelfDetector(bool); impl<'ast> Visit<'ast> for SelfDetector { fn visit_path(&mut self, i: &'ast syn::Path) { - self.0 |= i.get_ident().map_or(false, |i| i == "self") - || i.get_ident().map_or(false, |i| i == "Self") + self.0 |= i.is_ident(&Ident::from(syn::Token![Self](Span::call_site()))) + } + + fn visit_receiver(&mut self, node: &'ast Receiver) { + self.0 = true; } } From 081f7d69cbee53fdd32178e9b42233dd5b6163ef Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 20:46:53 -0400 Subject: [PATCH 12/21] Unused name --- library/kani_macros/src/sysroot/contracts.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index afa7b0c7f7db..beb220bc1597 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -930,7 +930,7 @@ impl<'ast> Visit<'ast> for SelfDetector { self.0 |= i.is_ident(&Ident::from(syn::Token![Self](Span::call_site()))) } - fn visit_receiver(&mut self, node: &'ast Receiver) { + fn visit_receiver(&mut self, _node: &'ast Receiver) { self.0 = true; } } From 5ebfac50ebf5ccd3ae887af450d66e2cd00fd701 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 20:58:40 -0400 Subject: [PATCH 13/21] Fix import error, add fail on two test case --- library/kani_macros/src/sysroot/contracts.rs | 2 +- .../function-contract/fail_on_two.expected | 5 +++++ .../expected/function-contract/fail_on_two.rs | 19 +++++++++++++++++++ 3 files changed, 25 insertions(+), 1 deletion(-) create mode 100644 tests/expected/function-contract/fail_on_two.expected create mode 100644 tests/expected/function-contract/fail_on_two.rs diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index beb220bc1597..b8de928a8ca5 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -930,7 +930,7 @@ impl<'ast> Visit<'ast> for SelfDetector { self.0 |= i.is_ident(&Ident::from(syn::Token![Self](Span::call_site()))) } - fn visit_receiver(&mut self, _node: &'ast Receiver) { + fn visit_receiver(&mut self, _node: &'ast syn::Receiver) { self.0 = true; } } diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected new file mode 100644 index 000000000000..87cb6d4ccca7 --- /dev/null +++ b/tests/expected/function-contract/fail_on_two.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: FAILURE\ +- Description: "internal error: entered unreachable code: fail on two" + +Failed Checks: internal error: entered unreachable code: fail on two diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs new file mode 100644 index 000000000000..c7c64537f537 --- /dev/null +++ b/tests/expected/function-contract/fail_on_two.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + + +#[kani::ensures(result < 3)] +fn fail_on_two(i: i32) -> i32 { + match i { + 0 => fail_on_two(i + 1), + 1 => 2, + _ => unreachable!("fail on two"), + } +} + +#[kani::proof_for_contract(fail_on_two)] +fn harness() { + let first = fail_on_two(0); + let _ = fail_on_two(first); +} \ No newline at end of file From 67795bac7a12be19444c5e923e1dd9257dc89aed Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 21:51:29 -0400 Subject: [PATCH 14/21] fmt --- tests/expected/function-contract/fail_on_two.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs index c7c64537f537..940d44d6bdce 100644 --- a/tests/expected/function-contract/fail_on_two.rs +++ b/tests/expected/function-contract/fail_on_two.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts - #[kani::ensures(result < 3)] fn fail_on_two(i: i32) -> i32 { match i { @@ -16,4 +15,4 @@ fn fail_on_two(i: i32) -> i32 { fn harness() { let first = fail_on_two(0); let _ = fail_on_two(first); -} \ No newline at end of file +} From 6c58d3769ca5a24c814bebd2c8ecdd5ee6c974bf Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 22:22:12 -0400 Subject: [PATCH 15/21] Added test case for, and fixed self detector --- library/kani_macros/src/sysroot/contracts.rs | 66 ++++++++++++++++++-- 1 file changed, 61 insertions(+), 5 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index b8de928a8ca5..075f3747aacb 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -858,6 +858,7 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // // The same care is taken when we emit check and replace functions. // emit the check function. + let is_impl_fn = is_probably_impl_fn(&item_fn); let ItemFn { attrs, vis, sig, block } = &item_fn; handler.output.extend(quote!( #(#attrs)* @@ -874,7 +875,7 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool let args = pats_to_idents(&mut wrapper_sig.inputs).collect::>(); let also_args = args.iter(); - let (call_check, call_replace) = if is_probably_impl_fn(sig) { + let (call_check, call_replace) = if is_impl_fn { (quote!(Self::#check_fn_name), quote!(Self::#replace_fn_name)) } else { (quote!(#check_fn_name), quote!(#replace_fn_name)) @@ -926,8 +927,8 @@ fn pats_to_idents

( struct SelfDetector(bool); impl<'ast> Visit<'ast> for SelfDetector { - fn visit_path(&mut self, i: &'ast syn::Path) { - self.0 |= i.is_ident(&Ident::from(syn::Token![Self](Span::call_site()))) + fn visit_ident(&mut self, i: &'ast syn::Ident) { + self.0 |= i == &Ident::from(syn::Token![Self](Span::mixed_site())) } fn visit_receiver(&mut self, _node: &'ast syn::Receiver) { @@ -935,9 +936,9 @@ impl<'ast> Visit<'ast> for SelfDetector { } } -fn is_probably_impl_fn(sig: &Signature) -> bool { +fn is_probably_impl_fn(fun: &ItemFn) -> bool { let mut self_detector = SelfDetector(false); - self_detector.visit_signature(sig); + self_detector.visit_item_fn(fun); self_detector.0 } @@ -966,3 +967,58 @@ macro_rules! passthrough { passthrough!(stub_verified, false); passthrough!(proof_for_contract, true); + +#[cfg(test)] +mod test { + macro_rules! detect_impl_fn { + ($expect_pass:expr, $($tt:tt)*) => {{ + let syntax = stringify!($($tt)*); + let ast = syn::parse_str(syntax).unwrap(); + assert!($expect_pass == super::is_probably_impl_fn(&ast), + "Incorrect detection.\nExpected is_impl_fun: {}\nInput Expr; {}\nParsed: {:?}", + $expect_pass, + syntax, + ast + ); + }} + } + + #[test] + fn detect_impl_fn_by_receiver() { + detect_impl_fn!(true, fn self_by_ref(&self, u: usize) -> bool {}); + + detect_impl_fn!(true, fn self_by_self(self, u: usize) -> bool {}); + } + + #[test] + fn detect_impl_fn_by_self_ty() { + detect_impl_fn!(true, fn self_by_construct(u: usize) -> Self {}); + detect_impl_fn!(true, fn self_by_wrapped_construct(u: usize) -> Arc {}); + + detect_impl_fn!(true, fn self_by_other_arg(u: usize, slf: Self) {}); + + detect_impl_fn!(true, fn self_by_other_wrapped_arg(u: usize, slf: Vec) {}) + } + + #[test] + fn detect_impl_fn_by_qself() { + detect_impl_fn!( + true, + fn self_by_mention(u: usize) { + Self::other(u) + } + ); + } + + #[test] + fn detect_no_impl_fn() { + detect_impl_fn!( + false, + fn self_by_mention(u: usize) { + let self_name = 18; + let self_lit = "self"; + let self_lit = "Self"; + } + ); + } +} From 8ad2ae00bc9bd0bcc051882529da251400f43048 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 10 Oct 2023 22:24:29 -0400 Subject: [PATCH 16/21] Actually run the new test in regression --- scripts/kani-regression.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 23546bf68ccd..b2462c6d1ff7 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -35,6 +35,9 @@ cargo test -p kani-compiler cargo test -p kani-driver cargo test -p kani_metadata cargo test -p kani --lib # skip doc tests. +# Test the actual macros, skipping doc tests and enabling extra traits for "syn" +# so we can debug print AST +RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib # Declare testing suite information (suite and mode) TESTS=( From 9cd5ed1e0550c906a9c530ef9af80aba865a03d7 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 11 Oct 2023 12:12:43 -0700 Subject: [PATCH 17/21] Expand test case to also fail on postcondition --- .../function-contract/fail_on_two.expected | 7 +++++++ tests/expected/function-contract/fail_on_two.rs | 16 ++++++++++++++++ 2 files changed, 23 insertions(+) diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected index 87cb6d4ccca7..32fc28012d3a 100644 --- a/tests/expected/function-contract/fail_on_two.expected +++ b/tests/expected/function-contract/fail_on_two.expected @@ -3,3 +3,10 @@ assertion\ - Description: "internal error: entered unreachable code: fail on two" Failed Checks: internal error: entered unreachable code: fail on two + + +assertion\ +- Status: FAILURE\ +- Description: "result < 3" + +Failed Checks: result < 3 diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs index 940d44d6bdce..c70cd8abd3c0 100644 --- a/tests/expected/function-contract/fail_on_two.rs +++ b/tests/expected/function-contract/fail_on_two.rs @@ -16,3 +16,19 @@ fn harness() { let first = fail_on_two(0); let _ = fail_on_two(first); } + +#[kani::ensures(result < 3)] +fn fail_on_two_in_postcondition(i: i32) -> i32 { + let j = i + 1; + if i < 2 { + fail_on_two_in_postcondition(j) + } else { + j + } +} + +#[kani::proof_for_contract(fail_on_two_in_postcondition)] +fn harness2() { + let first = fail_on_two_in_postcondition(1); + let _ = fail_on_two_in_postcondition(first); +} \ No newline at end of file From dd45198327d0d9e597230b570f1678532236d0ba Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 11 Oct 2023 12:17:21 -0700 Subject: [PATCH 18/21] Explanation for test case --- tests/expected/function-contract/fail_on_two.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs index c70cd8abd3c0..8de84fc28188 100644 --- a/tests/expected/function-contract/fail_on_two.rs +++ b/tests/expected/function-contract/fail_on_two.rs @@ -2,6 +2,20 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts +//! The test cases try to ensure applying the hypothesis is only done in +//! inductive verification of a function call. E.g. on every second encounter of +//! the called function in its own call stack rather than globally in the +//! program. +//! +//! In each case we have a recursive function that is called and we expect that +//! the recursive call within the first call has the hypothesis applied. (That's +//! not actually tested here but separately.) +//! +//! Then we call the function again and we've set up the cases such that *if* +//! the actual body is used then that call with fail (once because of panic, +//! once because the postcondition is violated). If instead the hypothesis (e.g. +//! contract replacement) is used we'd expect the verification to succeed. + #[kani::ensures(result < 3)] fn fail_on_two(i: i32) -> i32 { match i { From d2e33799f49e8ce18c410ec49980827372a1ddb8 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 11 Oct 2023 12:33:45 -0700 Subject: [PATCH 19/21] fmt --- tests/expected/function-contract/fail_on_two.rs | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs index 8de84fc28188..4302cdc7da33 100644 --- a/tests/expected/function-contract/fail_on_two.rs +++ b/tests/expected/function-contract/fail_on_two.rs @@ -34,15 +34,11 @@ fn harness() { #[kani::ensures(result < 3)] fn fail_on_two_in_postcondition(i: i32) -> i32 { let j = i + 1; - if i < 2 { - fail_on_two_in_postcondition(j) - } else { - j - } + if i < 2 { fail_on_two_in_postcondition(j) } else { j } } #[kani::proof_for_contract(fail_on_two_in_postcondition)] fn harness2() { let first = fail_on_two_in_postcondition(1); let _ = fail_on_two_in_postcondition(first); -} \ No newline at end of file +} From 281e6c11b5aa7399252ad60b632a30c9d11f0f8c Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 17 Oct 2023 13:52:12 -0700 Subject: [PATCH 20/21] A few missing bits of documentation. --- library/kani/src/contracts.rs | 23 ++++++++- library/kani_macros/src/sysroot/contracts.rs | 54 ++++++++++++++++++++ 2 files changed, 75 insertions(+), 2 deletions(-) diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 8a99f4892b0a..227bb5b27132 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -134,8 +134,8 @@ //! one specification attribute is considered to "have a contract" and any //! absent specification type defaults to its most general interpretation //! (`true`). All functions with not a single specification attribute are -//! considered "not to have a contract" and are ineligible for use as the -//! target of a [`proof_for_contract`][macro@proof_for_contract] of +//! considered "not to have a contract" and are ineligible for use as the target +//! of a [`proof_for_contract`][macro@proof_for_contract] of //! [`stub_verified`][macro@stub_verified] attribute. //! //! ## Contract Use Attributes Overview @@ -170,4 +170,23 @@ //! //! Unlike `proof_for_contract` multiple `stub_verified` attributes are allowed //! on the same proof harness though they must target different functions. +//! +//! ## Inductive Verification +//! +//! Function contracts by default use inductive verification to efficiently +//! verify recursive functions. In inductive verification a recursive function +//! is executed once and every recursive call is instead uses the contract +//! replacement. In this way a great many recursive calls can be checked with a +//! single verification pass. +//! +//! The downside of inductive verification is that the return value of a +//! contracted function must implement `kani::Arbitrary`. Due to restrictions to +//! code generation in proc macros the contract macros cannot determine reliably +//! in all cases whether a given function with a contract is recursive. As a +//! result it conservatively sets up inductive verification for every function +//! and requires the `kani::Arbitrary` constraint for contract checks. +//! +//! If you feel strongly about this issue you can join the discussion on issue +//! [#2823](https://github.com/model-checking/kani/issues/2823) to enable +//! opt-out of inductive verification. pub use super::{ensures, proof_for_contract, requires, stub_verified}; diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 075f3747aacb..856395eb7243 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -905,6 +905,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool output.into() } +/// Convert every use of a pattern in this signature to a simple, fresh, binding-only +/// argument ([`syn::PatIdent`]) and return the [`Ident`] that was generated. fn pats_to_idents

( sig: &mut syn::punctuated::Punctuated, ) -> impl Iterator + '_ { @@ -924,6 +926,8 @@ fn pats_to_idents

( }) } +/// The visitor used by [`is_probably_impl_fn`]. See function documentation for +/// more information. struct SelfDetector(bool); impl<'ast> Visit<'ast> for SelfDetector { @@ -936,6 +940,56 @@ impl<'ast> Visit<'ast> for SelfDetector { } } +/// Try to determine if this function is part of an `impl`. +/// +/// Detects *methods* by the presence of a receiver argument. Heuristically +/// detects *associated functions* buy the use of `Self` anywhere. +/// +/// Why do we need this? It's because if we want to call this `fn`, or any other +/// `fn` we generate into the same context we need to use `foo()` or +/// `Self::foo()` respectively depending on whether this is a plain or +/// associated function or Rust will complain. For the contract machinery we +/// need to generate and then call various functions we generate as well as the +/// original contracted function and so we need to determine how to call them +/// correctly. +/// +/// We can only solve this heuristically. The fundamental problem with Rust +/// macros is that they only see the syntax that's given to them and no other +/// context. It is however that context (of an `impl` block) that definitively +/// determines whether the `fn` is a plain function or an associated function. +/// +/// The heuristic itself is flawed, but it's the best we can do. For instance +/// this is perfectly legal +/// +/// ``` +/// struct S; +/// impl S { +/// #[i_want_to_call_you] +/// fn helper(u: usize) -> bool { +/// u < 8 +/// } +/// } +/// ``` +/// +/// This function would have to be called `S::helper()` but to the +/// `#[i_want_to_call_you]` attribute this function looks just like a bare +/// function because it never mentions `self` or `Self`. While this is a rare +/// case, the following is much more likely and suffers from the same problem, +/// because we can't know that `Vec == Self`. +/// +/// ``` +/// impl Vec { +/// fn new() -> Vec { +/// Vec { cap: 0, buf: NonNull::dangling() } +/// } +/// } +/// ``` +/// +/// **Side note:** You may be tempted to suggest that we could try and parse +/// `syn::ImplItemFn` and distinguish that from `syn::ItemFn` to distinguish +/// associated function from plain functions. However parsing in an attribute +/// placed on *any* `fn` will always succeed for *both* `syn::ImplItemFn` and +/// `syn::ItemFn`, thus not letting us distinguish between the two. fn is_probably_impl_fn(fun: &ItemFn) -> bool { let mut self_detector = SelfDetector(false); self_detector.visit_item_fn(fun); From e651f6ec5cd2839c6fba8ed5ea0033e43f4f5cce Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 17 Oct 2023 14:41:24 -0700 Subject: [PATCH 21/21] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani/src/contracts.rs | 6 +++--- library/kani_macros/src/sysroot/contracts.rs | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 227bb5b27132..a211a8ba905c 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -175,13 +175,13 @@ //! //! Function contracts by default use inductive verification to efficiently //! verify recursive functions. In inductive verification a recursive function -//! is executed once and every recursive call is instead uses the contract -//! replacement. In this way a great many recursive calls can be checked with a +//! is executed once and every recursive call instead uses the contract +//! replacement. In this way many recursive calls can be checked with a //! single verification pass. //! //! The downside of inductive verification is that the return value of a //! contracted function must implement `kani::Arbitrary`. Due to restrictions to -//! code generation in proc macros the contract macros cannot determine reliably +//! code generation in proc macros, the contract macros cannot determine reliably //! in all cases whether a given function with a contract is recursive. As a //! result it conservatively sets up inductive verification for every function //! and requires the `kani::Arbitrary` constraint for contract checks. diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 856395eb7243..a497e0ca8cee 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -943,7 +943,7 @@ impl<'ast> Visit<'ast> for SelfDetector { /// Try to determine if this function is part of an `impl`. /// /// Detects *methods* by the presence of a receiver argument. Heuristically -/// detects *associated functions* buy the use of `Self` anywhere. +/// detects *associated functions* by the use of `Self` anywhere. /// /// Why do we need this? It's because if we want to call this `fn`, or any other /// `fn` we generate into the same context we need to use `foo()` or