From 294c9e10db208a3a2148d77bce00878381ae5692 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 21 Jun 2024 20:27:54 +0000 Subject: [PATCH 01/32] Add helper attribute for `Invariant` derive macro --- library/kani_macros/src/derive.rs | 50 ++++++++++++++++++++++++++----- library/kani_macros/src/lib.rs | 2 +- 2 files changed, 43 insertions(+), 9 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 4e99590fc6a3..827c6e76cfec 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -199,7 +199,7 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics { fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { match data { - Data::Struct(struct_data) => struct_safe_conjunction(ident, &struct_data.fields), + Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields), Data::Enum(_) => { abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident; note = ident.span() => @@ -215,21 +215,55 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Generates an expression that is the conjunction of `is_safe` calls for each field in the struct. -fn struct_safe_conjunction(_ident: &Ident, fields: &Fields) -> TokenStream { +/// Generates an expression that is the conjunction of invariant conditions for each field in the struct. +fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { match fields { // Expands to the expression + // `true && && && ..` + // where `inv_condN` is either + // * the condition `` specified through the `#[invariant()]` helper attribute, or + // * the call `self.fieldN.is_safe()` + // + // Therefore, if `#[invariant()]` isn't specified for any field, this expands to // `true && self.field1.is_safe() && self.field2.is_safe() && ..` Fields::Named(ref fields) => { - let safe_calls = fields.named.iter().map(|field| { + let inv_conds = fields.named.iter().map(|field| { let name = &field.ident; - quote_spanned! {field.span()=> - self.#name.is_safe() + let mut inv_helper_attr = None; + + // Keep the helper attribute if we find it + for attr in &field.attrs { + if attr.path().is_ident("invariant") { + inv_helper_attr = Some(attr); + } + } + + // Parse the arguments in the invariant helper attribute + if let Some(attr) = inv_helper_attr { + let expr_args: Result = attr.parse_args(); + + // Check if there was an error parsing the arguments + if expr_args.is_err() { + abort!(Span::call_site(), "Cannot derive `Invariant` for `{}`", ident; + note = attr.span() => + "invariant condition in field `{}` could not be parsed - `{:?}`", name.as_ref().unwrap().to_string(), expr_args.map_err(|e| e.to_string()) + ) + } + // Return the expression for the invariant condition + let inv_expr = expr_args.unwrap(); + quote_spanned! {field.span()=> + #inv_expr + } + } else { + // Return call to the field's `is_safe` method + quote_spanned! {field.span()=> + self.#name.is_safe() + } } }); // An initial value is required for empty structs - safe_calls.fold(quote! { true }, |acc, call| { - quote! { #acc && #call } + inv_conds.fold(quote! { true }, |acc, cond| { + quote! { #acc && #cond } }) } Fields::Unnamed(ref fields) => { diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index b10b8a74cdc5..9888361c7760 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -109,7 +109,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro. #[proc_macro_error] -#[proc_macro_derive(Invariant)] +#[proc_macro_derive(Invariant, attributes(invariant))] pub fn derive_invariant(item: TokenStream) -> TokenStream { derive::expand_derive_invariant(item) } From e6a966e8067d3f973387d231bbe06e530c415ad7 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 21 Jun 2024 20:53:44 +0000 Subject: [PATCH 02/32] Add `expected` & `ui` tests --- .../invariant_helper/expected | 9 ++++++ .../invariant_helper/invariant_helper.rs | 32 +++++++++++++++++++ .../ui/derive-invariant/helper-empty/expected | 7 ++++ .../helper-empty/helper-empty.rs | 17 ++++++++++ .../derive-invariant/helper-no-expr/expected | 7 ++++ .../helper-no-expr/helper-no-expr.rs | 17 ++++++++++ .../helper-wrong-expr/expected | 5 +++ .../helper-wrong-expr/helper-wrong-expr.rs | 18 +++++++++++ 8 files changed, 112 insertions(+) create mode 100644 tests/expected/derive-invariant/invariant_helper/expected create mode 100644 tests/expected/derive-invariant/invariant_helper/invariant_helper.rs create mode 100644 tests/ui/derive-invariant/helper-empty/expected create mode 100644 tests/ui/derive-invariant/helper-empty/helper-empty.rs create mode 100644 tests/ui/derive-invariant/helper-no-expr/expected create mode 100644 tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs create mode 100644 tests/ui/derive-invariant/helper-wrong-expr/expected create mode 100644 tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs diff --git a/tests/expected/derive-invariant/invariant_helper/expected b/tests/expected/derive-invariant/invariant_helper/expected new file mode 100644 index 000000000000..fd90475a35ef --- /dev/null +++ b/tests/expected/derive-invariant/invariant_helper/expected @@ -0,0 +1,9 @@ +Check 1: check_invariant_helper_ok.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_fail.assertion.1\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.is_safe()" + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. \ No newline at end of file diff --git a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs b/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs new file mode 100644 index 000000000000..c7b498155cd5 --- /dev/null +++ b/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the invariant attribute helper adds the conditions provided to +//! the attribute to the derived `Invariant` implementation. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[invariant(self.x >= 0)] + x: i32, + #[invariant(self.y >= 0)] + y: i32, +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + kani::assume(pos_point.x >= 0); + kani::assume(pos_point.y >= 0); + assert!(pos_point.is_safe()); +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_helper_fail() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); +} diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected new file mode 100644 index 000000000000..b9db76eb9605 --- /dev/null +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -0,0 +1,7 @@ +error: Cannot derive `Invariant` for `PositivePoint` + --> tests/ui/derive-invariant/helper-empty/helper-empty.rs:11:10 + | +11 | #[derive(kani::Invariant)] + | ^^^^^^^^^^^^^^^ + | +note: invariant condition in field `x` could not be parsed - `Err("expected attribute arguments in parentheses: #[invariant(...)]")` diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs new file mode 100644 index 000000000000..5feacce4f1f6 --- /dev/null +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the compilation error for the invariant attribute helper when an +//! argument isn't provided. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[invariant] + x: i32, + #[invariant(self.y >= 0)] + y: i32, +} \ No newline at end of file diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected new file mode 100644 index 000000000000..bcc6e590d765 --- /dev/null +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -0,0 +1,7 @@ +error: Cannot derive `Invariant` for `PositivePoint` + --> tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs:11:10 + | +11 | #[derive(kani::Invariant)] + | ^^^^^^^^^^^^^^^ + | +note: invariant condition in field `x` could not be parsed - `Err("unexpected end of input, expected an expression")` diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs new file mode 100644 index 000000000000..b28381105d3d --- /dev/null +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the compilation error for the invariant attribute helper when the +//! argument is not a proper expression. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[invariant()] + x: i32, + #[invariant(self.y >= 0)] + y: i32, +} \ No newline at end of file diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected new file mode 100644 index 000000000000..47b2bbf7f345 --- /dev/null +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -0,0 +1,5 @@ +error[E0425]: cannot find value `x` in this scope + --> tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs:14:17 + | +14 | #[invariant(x >= 0)] + | ^ not found in this scope diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs new file mode 100644 index 000000000000..1afdc3c58850 --- /dev/null +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the compilation error for the invariant attribute helper when the +//! argument cannot be evaluated in the struct's context. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + // Note: `x` is unknown, we should refer to `self.x` + #[invariant(x >= 0)] + x: i32, + #[invariant(self.y >= 0)] + y: i32, +} \ No newline at end of file From d8a64a9e56ea2dad600479cc620a08b7d70d59e8 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 21 Jun 2024 21:15:52 +0000 Subject: [PATCH 03/32] Newlines --- tests/ui/derive-invariant/helper-empty/helper-empty.rs | 2 +- tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs | 2 +- .../ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs index 5feacce4f1f6..d668df2b5ae5 100644 --- a/tests/ui/derive-invariant/helper-empty/helper-empty.rs +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -14,4 +14,4 @@ struct PositivePoint { x: i32, #[invariant(self.y >= 0)] y: i32, -} \ No newline at end of file +} diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs index b28381105d3d..4291fa05bbb8 100644 --- a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -14,4 +14,4 @@ struct PositivePoint { x: i32, #[invariant(self.y >= 0)] y: i32, -} \ No newline at end of file +} diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs index 1afdc3c58850..7ae99ce70f82 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -15,4 +15,4 @@ struct PositivePoint { x: i32, #[invariant(self.y >= 0)] y: i32, -} \ No newline at end of file +} From b1c907185f99fb13ad1288a3764cb4655de0984f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 21 Jun 2024 21:16:45 +0000 Subject: [PATCH 04/32] Another newline --- tests/expected/derive-invariant/invariant_helper/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/derive-invariant/invariant_helper/expected b/tests/expected/derive-invariant/invariant_helper/expected index fd90475a35ef..319744ffa466 100644 --- a/tests/expected/derive-invariant/invariant_helper/expected +++ b/tests/expected/derive-invariant/invariant_helper/expected @@ -6,4 +6,4 @@ Check 1: check_invariant_helper_fail.assertion.1\ - Status: FAILURE\ - Description: "assertion failed: pos_point.is_safe()" -Complete - 2 successfully verified harnesses, 0 failures, 2 total. \ No newline at end of file +Complete - 2 successfully verified harnesses, 0 failures, 2 total. From b0f6adc3c9d62e0c6ec2b9992442d7f5091d5a94 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 21 Jun 2024 21:33:59 +0000 Subject: [PATCH 05/32] remove problematic lines --- tests/ui/derive-invariant/helper-empty/expected | 1 - tests/ui/derive-invariant/helper-no-expr/expected | 1 - tests/ui/derive-invariant/helper-wrong-expr/expected | 1 - 3 files changed, 3 deletions(-) diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected index b9db76eb9605..21c0494bc3e2 100644 --- a/tests/ui/derive-invariant/helper-empty/expected +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -1,5 +1,4 @@ error: Cannot derive `Invariant` for `PositivePoint` - --> tests/ui/derive-invariant/helper-empty/helper-empty.rs:11:10 | 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected index bcc6e590d765..f56e30d96079 100644 --- a/tests/ui/derive-invariant/helper-no-expr/expected +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -1,5 +1,4 @@ error: Cannot derive `Invariant` for `PositivePoint` - --> tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs:11:10 | 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index 47b2bbf7f345..4a1c30055b2a 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -1,5 +1,4 @@ error[E0425]: cannot find value `x` in this scope - --> tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs:14:17 | 14 | #[invariant(x >= 0)] | ^ not found in this scope From 3143d82bb2bd1aeea3adbce464f39fb0fc4a15ed Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 16:02:08 +0000 Subject: [PATCH 06/32] Use references for expressions (`Invariant` needs fix) --- library/kani_macros/src/derive.rs | 108 ++++++++++++++++++++++++++++-- library/kani_macros/src/lib.rs | 2 +- 2 files changed, 103 insertions(+), 7 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 827c6e76cfec..746141491591 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -28,15 +28,33 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); let body = fn_any_body(&item_name, &derive_item.data); + let cond_opt = cond_body(&item_name, &derive_item.data); + if let Some(cond) = cond_opt { + + let field_refs = field_refs(&item_name, &derive_item.data); let expanded = quote! { // The generated implementation. impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { fn any() -> Self { - #body + let obj = #body; + #field_refs + kani::assume(#cond); + obj } } }; - proc_macro::TokenStream::from(expanded) + proc_macro::TokenStream::from(expanded) + } else { + let expanded = quote! { + // The generated implementation. + impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { + fn any() -> Self { + #body + } + } + }; + proc_macro::TokenStream::from(expanded) + } } /// Add a bound `T: Arbitrary` to every type parameter T. @@ -75,10 +93,40 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Generate an item initialization where an item can be a struct or a variant. -/// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` -/// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` -/// For unit field, generate an empty initialization. +fn cond_body(ident: &Ident, data: &Data) -> Option { + match data { + Data::Struct(struct_data) => cond_item(ident, &struct_data.fields), + Data::Enum(_) => None, + Data::Union(_) => None, + } +} + +fn field_refs(ident: &Ident, data: &Data) -> TokenStream { + match data { + Data::Struct(struct_data) => field_refs2(ident, &struct_data.fields), + Data::Enum(_) => unreachable!(), + Data::Union(_) => unreachable!(), + } +} + +fn field_refs2(_ident: &Ident, fields: &Fields) -> TokenStream { + match fields { + Fields::Named(ref fields) => { + let field_refs = fields.named.iter().map(|field| { + let name = &field.ident; + quote_spanned! {field.span()=> + let #name = &obj.#name; + } + }); + quote!{ #( #field_refs )* } + } + Fields::Unnamed(_) => unreachable!(), + Fields::Unit => unreachable!(), + } +} + + + fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { match fields { Fields::Named(ref fields) => { @@ -115,6 +163,54 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { } } +fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { + let name = &field.ident; + let mut inv_helper_attr = None; + // Keep the helper attribute if we find it + for attr in &field.attrs { + if attr.path().is_ident("invariant") { + inv_helper_attr = Some(attr); + } + } + + // Parse the arguments in the invariant helper attribute + if let Some(attr) = inv_helper_attr { + let expr_args: Result = attr.parse_args(); + + // Check if there was an error parsing the arguments + if expr_args.is_err() { + abort!(Span::call_site(), "Cannot derive `Invariant` for `{}`", ident; + note = attr.span() => + "invariant condition in field `{}` could not be parsed - `{:?}`", name.as_ref().unwrap().to_string(), expr_args.map_err(|e| e.to_string()) + ) + } + let inv_expr = expr_args.unwrap(); + Some(quote_spanned! {field.span()=> + #inv_expr + }) + // Return the expression for the invariant condition + } else { None } +} +/// Generate an item initialization where an item can be a struct or a variant. +/// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` +/// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` +/// For unit field, generate an empty initialization. +fn cond_item(ident: &Ident, fields: &Fields) -> Option { + match fields { + Fields::Named(ref fields) => { + let conds: Vec = fields.named.iter().filter_map(|field| + extract_expr(ident, field)).collect(); + if !conds.is_empty() { + Some(quote! { #(#conds)&&* }) + } else { + None + } + } + Fields::Unnamed(_) => None, + Fields::Unit => None, + } +} + /// Generate the body of the function `any()` for enums. The cases are: /// 1. For zero-variants enumerations, this will encode a `panic!()` statement. /// 2. For one or more variants, the code will be something like: diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 9888361c7760..924b0e9e2248 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -102,7 +102,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro. #[proc_macro_error] -#[proc_macro_derive(Arbitrary)] +#[proc_macro_derive(Arbitrary, attributes(invariant))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } From 7beec3ebb45b4e908b437806f92ed0787d22325c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 17:39:07 +0000 Subject: [PATCH 07/32] Fixed generation for `Invariant` --- library/kani_macros/src/derive.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 746141491591..727ae9067f85 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -125,8 +125,6 @@ fn field_refs2(_ident: &Ident, fields: &Fields) -> TokenStream { } } - - fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { match fields { Fields::Named(ref fields) => { @@ -191,6 +189,7 @@ fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { // Return the expression for the invariant condition } else { None } } + /// Generate an item initialization where an item can be a struct or a variant. /// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` /// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` @@ -272,10 +271,14 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); let body = is_safe_body(&item_name, &derive_item.data); + let field_refs = field_refs(&item_name, &derive_item.data); + let expanded = quote! { // The generated implementation. impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause { fn is_safe(&self) -> bool { + let obj = self; + #field_refs #body } } From a6fa7eea292881d32530744af02449a48b89683b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 17:39:33 +0000 Subject: [PATCH 08/32] Apply fixes for format --- library/kani_macros/src/derive.rs | 39 ++++++++++++++----------------- 1 file changed, 18 insertions(+), 21 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 727ae9067f85..0dba9eb0fce2 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -30,19 +30,18 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let body = fn_any_body(&item_name, &derive_item.data); let cond_opt = cond_body(&item_name, &derive_item.data); if let Some(cond) = cond_opt { - let field_refs = field_refs(&item_name, &derive_item.data); - let expanded = quote! { - // The generated implementation. - impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { - fn any() -> Self { - let obj = #body; - #field_refs - kani::assume(#cond); - obj + let expanded = quote! { + // The generated implementation. + impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { + fn any() -> Self { + let obj = #body; + #field_refs + kani::assume(#cond); + obj + } } - } - }; + }; proc_macro::TokenStream::from(expanded) } else { let expanded = quote! { @@ -113,12 +112,12 @@ fn field_refs2(_ident: &Ident, fields: &Fields) -> TokenStream { match fields { Fields::Named(ref fields) => { let field_refs = fields.named.iter().map(|field| { - let name = &field.ident; + let name = &field.ident; quote_spanned! {field.span()=> let #name = &obj.#name; } }); - quote!{ #( #field_refs )* } + quote! { #( #field_refs )* } } Fields::Unnamed(_) => unreachable!(), Fields::Unit => unreachable!(), @@ -187,7 +186,9 @@ fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { #inv_expr }) // Return the expression for the invariant condition - } else { None } + } else { + None + } } /// Generate an item initialization where an item can be a struct or a variant. @@ -197,13 +198,9 @@ fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { fn cond_item(ident: &Ident, fields: &Fields) -> Option { match fields { Fields::Named(ref fields) => { - let conds: Vec = fields.named.iter().filter_map(|field| - extract_expr(ident, field)).collect(); - if !conds.is_empty() { - Some(quote! { #(#conds)&&* }) - } else { - None - } + let conds: Vec = + fields.named.iter().filter_map(|field| extract_expr(ident, field)).collect(); + if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } } Fields::Unnamed(_) => None, Fields::Unit => None, From ad2da6f658a6a1d46e588c68c1e7ca3b72550001 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 18:15:21 +0000 Subject: [PATCH 09/32] Some refactoring and documentation --- library/kani_macros/src/derive.rs | 51 +++++++++++++++++++++++-------- 1 file changed, 38 insertions(+), 13 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 0dba9eb0fce2..a2dd2581f589 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -28,32 +28,34 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); let body = fn_any_body(&item_name, &derive_item.data); - let cond_opt = cond_body(&item_name, &derive_item.data); - if let Some(cond) = cond_opt { + + // + let inv_conds_opt = inv_conds(&item_name, &derive_item.data); + + let expanded = if let Some(inv_cond) = inv_conds_opt { let field_refs = field_refs(&item_name, &derive_item.data); - let expanded = quote! { + quote! { // The generated implementation. impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { fn any() -> Self { let obj = #body; #field_refs - kani::assume(#cond); + kani::assume(#inv_cond); obj } } - }; - proc_macro::TokenStream::from(expanded) + } } else { - let expanded = quote! { + quote! { // The generated implementation. impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { fn any() -> Self { #body } } - }; - proc_macro::TokenStream::from(expanded) - } + } + }; + proc_macro::TokenStream::from(expanded) } /// Add a bound `T: Arbitrary` to every type parameter T. @@ -92,7 +94,7 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } -fn cond_body(ident: &Ident, data: &Data) -> Option { +fn inv_conds(ident: &Ident, data: &Data) -> Option { match data { Data::Struct(struct_data) => cond_item(ident, &struct_data.fields), Data::Enum(_) => None, @@ -100,15 +102,38 @@ fn cond_body(ident: &Ident, data: &Data) -> Option { } } +/// Generates the sequence of expressions to initialize the variables used as +/// references to the struct fields. +/// +/// For example, if we're deriving implementations for the struct +/// ``` +/// #[derive(Arbitrary)] +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[invariant(*x >= 0)] +/// x: i32, +/// #[invariant(*y >= 0)] +/// y: i32, +/// } +/// ``` +/// this function will generate the `TokenStream` +/// ``` +/// let x = &obj.x; +/// let y = &obj.y; +/// ``` +/// which allows us to refer to the struct fields without using `self`. +/// Note that the actual stream is generated in the `field_refs_inner` function. fn field_refs(ident: &Ident, data: &Data) -> TokenStream { match data { - Data::Struct(struct_data) => field_refs2(ident, &struct_data.fields), + Data::Struct(struct_data) => field_refs_inner(ident, &struct_data.fields), Data::Enum(_) => unreachable!(), Data::Union(_) => unreachable!(), } } -fn field_refs2(_ident: &Ident, fields: &Fields) -> TokenStream { +/// Generates the sequence of expressions to initialize the variables used as +/// references to the struct fields. See `field_refs` for more details. +fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream { match fields { Fields::Named(ref fields) => { let field_refs = fields.named.iter().map(|field| { From 4c749ecc27fb5623647bbad0ab6ae85e00fc5c56 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 18:38:37 +0000 Subject: [PATCH 10/32] Refactor using `extract_expr` --- library/kani_macros/src/derive.rs | 59 +++++++++---------------------- 1 file changed, 17 insertions(+), 42 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index a2dd2581f589..9677cf4dfa35 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -29,7 +29,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let body = fn_any_body(&item_name, &derive_item.data); - // + // Get the invariant conditions (if any) to produce type-safe values let inv_conds_opt = inv_conds(&item_name, &derive_item.data); let expanded = if let Some(inv_cond) = inv_conds_opt { @@ -149,6 +149,10 @@ fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream { } } +/// Generate an item initialization where an item can be a struct or a variant. +/// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` +/// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` +/// For unit field, generate an empty initialization. fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { match fields { Fields::Named(ref fields) => { @@ -201,25 +205,21 @@ fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { // Check if there was an error parsing the arguments if expr_args.is_err() { - abort!(Span::call_site(), "Cannot derive `Invariant` for `{}`", ident; + abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; note = attr.span() => "invariant condition in field `{}` could not be parsed - `{:?}`", name.as_ref().unwrap().to_string(), expr_args.map_err(|e| e.to_string()) ) } + // Return the expression associated to the invariant condition let inv_expr = expr_args.unwrap(); Some(quote_spanned! {field.span()=> #inv_expr }) - // Return the expression for the invariant condition } else { None } } -/// Generate an item initialization where an item can be a struct or a variant. -/// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` -/// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` -/// For unit field, generate an empty initialization. fn cond_item(ident: &Ident, fields: &Fields) -> Option { match fields { Fields::Named(ref fields) => { @@ -348,42 +348,17 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { // Therefore, if `#[invariant()]` isn't specified for any field, this expands to // `true && self.field1.is_safe() && self.field2.is_safe() && ..` Fields::Named(ref fields) => { - let inv_conds = fields.named.iter().map(|field| { - let name = &field.ident; - let mut inv_helper_attr = None; - - // Keep the helper attribute if we find it - for attr in &field.attrs { - if attr.path().is_ident("invariant") { - inv_helper_attr = Some(attr); - } - } - - // Parse the arguments in the invariant helper attribute - if let Some(attr) = inv_helper_attr { - let expr_args: Result = attr.parse_args(); - - // Check if there was an error parsing the arguments - if expr_args.is_err() { - abort!(Span::call_site(), "Cannot derive `Invariant` for `{}`", ident; - note = attr.span() => - "invariant condition in field `{}` could not be parsed - `{:?}`", name.as_ref().unwrap().to_string(), expr_args.map_err(|e| e.to_string()) - ) - } - // Return the expression for the invariant condition - let inv_expr = expr_args.unwrap(); - quote_spanned! {field.span()=> - #inv_expr - } - } else { - // Return call to the field's `is_safe` method - quote_spanned! {field.span()=> - self.#name.is_safe() - } - } - }); + let inv_conds: Vec = fields + .named + .iter() + .map(|field| { + extract_expr(ident, field).unwrap_or(quote_spanned! {field.span()=> + self.#field.is_safe() + }) + }) + .collect(); // An initial value is required for empty structs - inv_conds.fold(quote! { true }, |acc, cond| { + inv_conds.into_iter().fold(quote! { true }, |acc, cond| { quote! { #acc && #cond } }) } From 29aee755825c6ef1365c271fd761944d414d50d1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 19:23:00 +0000 Subject: [PATCH 11/32] Document remaining funs --- library/kani_macros/src/derive.rs | 37 ++++++++++++++++++++++++++----- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 9677cf4dfa35..0300c2ab18a9 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -94,9 +94,29 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } +/// Parse the condition expressions in `#[invariant()]` attached to struct +/// fields and, it at least one was found, generate a conjunction to be assumed. +/// +/// For example, if we're deriving implementations for the struct +/// ``` +/// #[derive(Arbitrary)] +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[invariant(*x >= 0)] +/// x: i32, +/// #[invariant(*y >= 0)] +/// y: i32, +/// } +/// ``` +/// this function will generate the `TokenStream` +/// ``` +/// *x >= 0 && *y >= 0 +/// ``` +/// which can be passed to `kani::assume` to constrain the values generated +/// through the `Arbitrary` impl so that they are type-safe by construction. fn inv_conds(ident: &Ident, data: &Data) -> Option { match data { - Data::Struct(struct_data) => cond_item(ident, &struct_data.fields), + Data::Struct(struct_data) => inv_conds_inner(ident, &struct_data.fields), Data::Enum(_) => None, Data::Union(_) => None, } @@ -189,9 +209,13 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { } } -fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { +/// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the +/// `#[invariant()]` attribute helper associated with a given field. +/// Return `None` if the attribute isn't specified. +fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { let name = &field.ident; let mut inv_helper_attr = None; + // Keep the helper attribute if we find it for attr in &field.attrs { if attr.path().is_ident("invariant") { @@ -210,6 +234,7 @@ fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { "invariant condition in field `{}` could not be parsed - `{:?}`", name.as_ref().unwrap().to_string(), expr_args.map_err(|e| e.to_string()) ) } + // Return the expression associated to the invariant condition let inv_expr = expr_args.unwrap(); Some(quote_spanned! {field.span()=> @@ -220,11 +245,13 @@ fn extract_expr(ident: &Ident, field: &syn::Field) -> Option { } } -fn cond_item(ident: &Ident, fields: &Fields) -> Option { +/// Generates an expression resulting from the conjunction of conditions +/// specified as invariants for each field. See `inv_conds` for more details. +fn inv_conds_inner(ident: &Ident, fields: &Fields) -> Option { match fields { Fields::Named(ref fields) => { let conds: Vec = - fields.named.iter().filter_map(|field| extract_expr(ident, field)).collect(); + fields.named.iter().filter_map(|field| parse_inv_expr(ident, field)).collect(); if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } } Fields::Unnamed(_) => None, @@ -352,7 +379,7 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { .named .iter() .map(|field| { - extract_expr(ident, field).unwrap_or(quote_spanned! {field.span()=> + parse_inv_expr(ident, field).unwrap_or(quote_spanned! {field.span()=> self.#field.is_safe() }) }) From adacc40282d654ef27b60ea0cd659d32122bc7d2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 19:24:12 +0000 Subject: [PATCH 12/32] Move inner funs around --- library/kani_macros/src/derive.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 0300c2ab18a9..6f6cc04bf11e 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -122,6 +122,20 @@ fn inv_conds(ident: &Ident, data: &Data) -> Option { } } +/// Generates an expression resulting from the conjunction of conditions +/// specified as invariants for each field. See `inv_conds` for more details. +fn inv_conds_inner(ident: &Ident, fields: &Fields) -> Option { + match fields { + Fields::Named(ref fields) => { + let conds: Vec = + fields.named.iter().filter_map(|field| parse_inv_expr(ident, field)).collect(); + if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } + } + Fields::Unnamed(_) => None, + Fields::Unit => None, + } +} + /// Generates the sequence of expressions to initialize the variables used as /// references to the struct fields. /// @@ -245,20 +259,6 @@ fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { } } -/// Generates an expression resulting from the conjunction of conditions -/// specified as invariants for each field. See `inv_conds` for more details. -fn inv_conds_inner(ident: &Ident, fields: &Fields) -> Option { - match fields { - Fields::Named(ref fields) => { - let conds: Vec = - fields.named.iter().filter_map(|field| parse_inv_expr(ident, field)).collect(); - if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } - } - Fields::Unnamed(_) => None, - Fields::Unit => None, - } -} - /// Generate the body of the function `any()` for enums. The cases are: /// 1. For zero-variants enumerations, this will encode a `panic!()` statement. /// 2. For one or more variants, the code will be something like: From 79350dc278f274386e9e71e0d7105e3fe2091e67 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 21:01:59 +0000 Subject: [PATCH 13/32] Fix bug and all tests --- library/kani_macros/src/derive.rs | 36 ++++++++++++------- .../invariant_helper/expected | 6 +++- .../invariant_helper/invariant_helper.rs | 20 ++++++++--- .../ui/derive-invariant/helper-empty/expected | 2 +- .../helper-empty/helper-empty.rs | 2 +- .../derive-invariant/helper-no-expr/expected | 2 +- .../helper-no-expr/helper-no-expr.rs | 2 +- .../helper-wrong-expr/expected | 10 ++++-- .../helper-wrong-expr/helper-wrong-expr.rs | 4 +-- 9 files changed, 57 insertions(+), 27 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 6f6cc04bf11e..91b57132af64 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -170,16 +170,24 @@ fn field_refs(ident: &Ident, data: &Data) -> TokenStream { fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream { match fields { Fields::Named(ref fields) => { - let field_refs = fields.named.iter().map(|field| { - let name = &field.ident; - quote_spanned! {field.span()=> - let #name = &obj.#name; - } - }); - quote! { #( #field_refs )* } + let field_refs: Vec = fields + .named + .iter() + .map(|field| { + let name = &field.ident; + quote_spanned! {field.span()=> + let #name = &obj.#name; + } + }) + .collect(); + if !field_refs.is_empty() { + quote! { #( #field_refs )* } + } else { + quote! {} + } } - Fields::Unnamed(_) => unreachable!(), - Fields::Unit => unreachable!(), + Fields::Unnamed(_) => quote! {}, + Fields::Unit => quote! {}, } } @@ -379,13 +387,15 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { .named .iter() .map(|field| { - parse_inv_expr(ident, field).unwrap_or(quote_spanned! {field.span()=> - self.#field.is_safe() - }) + let name = &field.ident; + let default_expr = quote_spanned! {field.span()=> + #name.is_safe() + }; + parse_inv_expr(ident, field).unwrap_or(default_expr) }) .collect(); // An initial value is required for empty structs - inv_conds.into_iter().fold(quote! { true }, |acc, cond| { + inv_conds.iter().fold(quote! { true }, |acc, cond| { quote! { #acc && #cond } }) } diff --git a/tests/expected/derive-invariant/invariant_helper/expected b/tests/expected/derive-invariant/invariant_helper/expected index 319744ffa466..31b6de54c647 100644 --- a/tests/expected/derive-invariant/invariant_helper/expected +++ b/tests/expected/derive-invariant/invariant_helper/expected @@ -2,8 +2,12 @@ Check 1: check_invariant_helper_ok.assertion.1\ - Status: SUCCESS\ - Description: "assertion failed: pos_point.is_safe()" +Check 1: check_invariant_helper_ok_manual.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + Check 1: check_invariant_helper_fail.assertion.1\ - Status: FAILURE\ - Description: "assertion failed: pos_point.is_safe()" -Complete - 2 successfully verified harnesses, 0 failures, 2 total. +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs b/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs index c7b498155cd5..3b8d6527864a 100644 --- a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs @@ -10,23 +10,33 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - #[invariant(self.x >= 0)] + #[invariant(*x >= 0)] x: i32, - #[invariant(self.y >= 0)] + #[invariant(*y >= 0)] y: i32, } #[kani::proof] fn check_invariant_helper_ok() { let pos_point: PositivePoint = kani::any(); - kani::assume(pos_point.x >= 0); - kani::assume(pos_point.y >= 0); assert!(pos_point.is_safe()); } #[kani::proof] #[kani::should_panic] fn check_invariant_helper_fail() { - let pos_point: PositivePoint = kani::any(); + // In this case, `kani::any()` returns unconstrained values that don't + // respect the invariants. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + assert!(pos_point.is_safe()); +} + +#[kani::proof] +fn check_invariant_helper_ok_manual() { + // In this case, `kani::any()` returns unconstrained values that don't + // respect the invariants. However, we manually constrain them later. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + kani::assume(pos_point.x >= 0); + kani::assume(pos_point.y >= 0); assert!(pos_point.is_safe()); } diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected index 21c0494bc3e2..4ebd0e03e7f0 100644 --- a/tests/ui/derive-invariant/helper-empty/expected +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -1,4 +1,4 @@ -error: Cannot derive `Invariant` for `PositivePoint` +error: Cannot derive impl for `PositivePoint` | 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs index d668df2b5ae5..518a1e35eb56 100644 --- a/tests/ui/derive-invariant/helper-empty/helper-empty.rs +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -12,6 +12,6 @@ use kani::Invariant; struct PositivePoint { #[invariant] x: i32, - #[invariant(self.y >= 0)] + #[invariant(*y >= 0)] y: i32, } diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected index f56e30d96079..4327e47b7cdd 100644 --- a/tests/ui/derive-invariant/helper-no-expr/expected +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -1,4 +1,4 @@ -error: Cannot derive `Invariant` for `PositivePoint` +error: Cannot derive impl for `PositivePoint` | 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs index 4291fa05bbb8..302b9193f9fc 100644 --- a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -12,6 +12,6 @@ use kani::Invariant; struct PositivePoint { #[invariant()] x: i32, - #[invariant(self.y >= 0)] + #[invariant(*y >= 0)] y: i32, } diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index 4a1c30055b2a..041d3aca9f17 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -1,4 +1,10 @@ -error[E0425]: cannot find value `x` in this scope +error[E0308]: mismatched types + --> /home/ubuntu/kani/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs:14:22 | 14 | #[invariant(x >= 0)] - | ^ not found in this scope + | ^ expected `&i32`, found integer + | +help: consider dereferencing the borrow + | +14 | #[invariant(*x >= 0)] + | + \ No newline at end of file diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs index 7ae99ce70f82..fe58042b331a 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -10,9 +10,9 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - // Note: `x` is unknown, we should refer to `self.x` + // Note: `x` is unknown, we should refer to `*x` #[invariant(x >= 0)] x: i32, - #[invariant(self.y >= 0)] + #[invariant(*y >= 0)] y: i32, } From 0c686ba195991667c2f236f34e74ac43530be4ca Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 21:12:32 +0000 Subject: [PATCH 14/32] Add new test for `Arbitrary`-only invariant behavior --- .../invariant_helper/expected | 17 ++++++++++ .../invariant_helper/invariant_helper.rs | 31 +++++++++++++++++++ 2 files changed, 48 insertions(+) create mode 100644 tests/expected/derive-arbitrary/invariant_helper/expected create mode 100644 tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs diff --git a/tests/expected/derive-arbitrary/invariant_helper/expected b/tests/expected/derive-arbitrary/invariant_helper/expected new file mode 100644 index 000000000000..f35f18084911 --- /dev/null +++ b/tests/expected/derive-arbitrary/invariant_helper/expected @@ -0,0 +1,17 @@ +Check 1: check_invariant_helper_ok.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_invariant_helper_ok.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.y >= 0" + +Check 1: check_invariant_helper_fail.assertion.1\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_invariant_helper_fail.assertion.2\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.y >= 0" + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs b/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs new file mode 100644 index 000000000000..2a4f841f9dcd --- /dev/null +++ b/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the invariant attribute helper adds the conditions provided to +//! the attribute to the derived `Arbitrary` implementation. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +struct PositivePoint { + #[invariant(*x >= 0)] + x: i32, + #[invariant(*y >= 0)] + y: i32, +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_helper_fail() { + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} From 43c1d79e4fbba6adec12923718ebfa9efcc4a36f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jun 2024 21:16:02 +0000 Subject: [PATCH 15/32] remove location line from tests --- tests/ui/derive-invariant/helper-wrong-expr/expected | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index 041d3aca9f17..25be472caba4 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -1,5 +1,4 @@ error[E0308]: mismatched types - --> /home/ubuntu/kani/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs:14:22 | 14 | #[invariant(x >= 0)] | ^ expected `&i32`, found integer From d13015f0f870e0332df95e0c7080c8ae22097b77 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 8 Jul 2024 21:24:41 +0000 Subject: [PATCH 16/32] Add newline on `expected` test --- tests/ui/derive-invariant/helper-wrong-expr/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index 25be472caba4..84de40d44478 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -6,4 +6,4 @@ error[E0308]: mismatched types help: consider dereferencing the borrow | 14 | #[invariant(*x >= 0)] - | + \ No newline at end of file + | + From ccf3cf6620a940798337f162a3638a263e54f2ee Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 8 Jul 2024 21:40:32 +0000 Subject: [PATCH 17/32] Add test with functions --- .../invariant_helper_funs/expected | 13 +++++ .../invariant_helper_funs.rs | 47 +++++++++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 tests/expected/derive-invariant/invariant_helper_funs/expected create mode 100644 tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs diff --git a/tests/expected/derive-invariant/invariant_helper_funs/expected b/tests/expected/derive-invariant/invariant_helper_funs/expected new file mode 100644 index 000000000000..31b6de54c647 --- /dev/null +++ b/tests/expected/derive-invariant/invariant_helper_funs/expected @@ -0,0 +1,13 @@ +Check 1: check_invariant_helper_ok.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_ok_manual.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_fail.assertion.1\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.is_safe()" + +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs b/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs new file mode 100644 index 000000000000..415ea0ee2ac3 --- /dev/null +++ b/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs @@ -0,0 +1,47 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that functions can be called in the invariant attribute helpers. +//! This is like the `invariant_helper` test but using a function instead +//! of passing in a predicate. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[invariant(is_coordinate_safe(x))] + x: i32, + #[invariant(is_coordinate_safe(y))] + y: i32, +} + +fn is_coordinate_safe(val: &i32) -> bool { + *val >= 0 +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_helper_fail() { + // In this case, `kani::any()` returns unconstrained values that don't + // respect the invariants. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + assert!(pos_point.is_safe()); +} + +#[kani::proof] +fn check_invariant_helper_ok_manual() { + // In this case, `kani::any()` returns unconstrained values that don't + // respect the invariants. However, we manually constrain them later. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + kani::assume(pos_point.x >= 0); + kani::assume(pos_point.y >= 0); + assert!(pos_point.is_safe()); +} From 07bf2a1f89e8d3da0147f5b96223e46df6cdf1b8 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 8 Jul 2024 21:53:49 +0000 Subject: [PATCH 18/32] Add test where invariant is violated thru mut --- .../invariant_fail_mut/expected | 11 ++++++++ .../invariant_fail_mut/invariant_fail_mut.rs | 28 +++++++++++++++++++ 2 files changed, 39 insertions(+) create mode 100644 tests/expected/derive-invariant/invariant_fail_mut/expected create mode 100644 tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs diff --git a/tests/expected/derive-invariant/invariant_fail_mut/expected b/tests/expected/derive-invariant/invariant_fail_mut/expected new file mode 100644 index 000000000000..0853a68fa79e --- /dev/null +++ b/tests/expected/derive-invariant/invariant_fail_mut/expected @@ -0,0 +1,11 @@ +Check 1: check_invariant_fail_mut.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 2: check_invariant_fail_mut.assertion.2\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.is_safe()" + +VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs b/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs new file mode 100644 index 000000000000..11bed7a32479 --- /dev/null +++ b/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that a verification failure is triggered if we check the invariant +//! after mutating an object to violate it. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[invariant(*x >= 0)] + x: i32, + #[invariant(*y >= 0)] + y: i32, +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_fail_mut() { + let mut pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); + // Set the `x` field to an unsafe value + pos_point.x = -1; + // The object's invariant isn't preserved anymore so the next check fails + assert!(pos_point.is_safe()); +} From 98504bef48b338e389f04e4001facab72b67741f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 8 Jul 2024 22:03:49 +0000 Subject: [PATCH 19/32] minor comment revision --- .../ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs index fe58042b331a..99c759165fb9 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -10,7 +10,7 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - // Note: `x` is unknown, we should refer to `*x` + // Note: `x` is a reference in this context, we should refer to `*x` #[invariant(x >= 0)] x: i32, #[invariant(*y >= 0)] From bac08cb5bb8f6b32cec41998af085a88f67fc146 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 8 Jul 2024 22:04:30 +0000 Subject: [PATCH 20/32] Better handling of error messages --- library/kani_macros/src/derive.rs | 4 ++-- tests/ui/derive-invariant/helper-empty/expected | 2 +- tests/ui/derive-invariant/helper-no-expr/expected | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 91b57132af64..5878db6085f8 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -250,10 +250,10 @@ fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { let expr_args: Result = attr.parse_args(); // Check if there was an error parsing the arguments - if expr_args.is_err() { + if let Err(err) = expr_args { abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; note = attr.span() => - "invariant condition in field `{}` could not be parsed - `{:?}`", name.as_ref().unwrap().to_string(), expr_args.map_err(|e| e.to_string()) + "invariant condition in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err ) } diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected index 4ebd0e03e7f0..2e4c3285d334 100644 --- a/tests/ui/derive-invariant/helper-empty/expected +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -3,4 +3,4 @@ error: Cannot derive impl for `PositivePoint` 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | -note: invariant condition in field `x` could not be parsed - `Err("expected attribute arguments in parentheses: #[invariant(...)]")` +note: invariant condition in field `x` could not be parsed: expected attribute arguments in parentheses: #[invariant(...)] diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected index 4327e47b7cdd..b52ee673daf8 100644 --- a/tests/ui/derive-invariant/helper-no-expr/expected +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -3,4 +3,4 @@ error: Cannot derive impl for `PositivePoint` 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | -note: invariant condition in field `x` could not be parsed - `Err("unexpected end of input, expected an expression")` +note: invariant condition in field `x` could not be parsed: unexpected end of input, expected an expression From 08ffc4d6845f7d8704af9e596d41cdda4b03cce2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 17 Jul 2024 22:05:07 +0000 Subject: [PATCH 21/32] Always check `is_safe()` for each field --- library/kani_macros/src/derive.rs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 5878db6085f8..f02dfc37dde3 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -376,9 +376,10 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { match fields { // Expands to the expression // `true && && && ..` - // where `inv_condN` is either - // * the condition `` specified through the `#[invariant()]` helper attribute, or - // * the call `self.fieldN.is_safe()` + // where `inv_condN` is + // - `self.fieldN.is_safe() && ` if a condition `` was + // specified through the `#[invariant()]` helper attribute, or + // - `self.fieldN.is_safe()` otherwise // // Therefore, if `#[invariant()]` isn't specified for any field, this expands to // `true && self.field1.is_safe() && self.field2.is_safe() && ..` @@ -391,7 +392,9 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { let default_expr = quote_spanned! {field.span()=> #name.is_safe() }; - parse_inv_expr(ident, field).unwrap_or(default_expr) + parse_inv_expr(ident, field) + .map(|expr| quote! { #expr && #default_expr}) + .unwrap_or(default_expr) }) .collect(); // An initial value is required for empty structs From 6722aae5e920937f742bfbd050433b28e6940649 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 17 Jul 2024 22:05:25 +0000 Subject: [PATCH 22/32] Add documentation for traits --- library/kani_macros/src/lib.rs | 108 ++++++++++++++++++++++++++++++++- 1 file changed, 106 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 924b0e9e2248..da299163a6f2 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -100,14 +100,118 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::unstable(attr, item) } -/// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro. +/// Allow users to auto generate `Arbitrary` implementations by using +/// `#[derive(Arbitrary)]` macro. +/// +/// When using `#[derive(Arbitrary)]` on a struct, the `#[invariant()]` +/// attribute can be added to its fields to indicate a type safety invariant +/// condition ``. Since `kani::any()` is always expected to produce +/// type-safe values, **adding `#[invariant(...)]` to any fields will further +/// constrain the objects generated with `kani::any()`**. +/// +/// For example, the `check_positive` harness in this code is expected to +/// pass: +/// +/// ```rs +/// #[derive(kani::Arbitrary)] +/// struct AlwaysPositive { +/// #[invariant(*inner >= 0)] +/// inner: i32, +/// } +/// +/// #[kani::proof] +/// fn check_positive() { +/// let val: AlwaysPositive = kani::any(); +/// assert!(val.inner >= 0); +/// } +/// ``` +/// +/// Therefore, using the `#[invariant(...)]` attribute can lead to vacuous +/// results when the values are over-constrained. For example, in this code +/// the `check_positive` harness will pass too: +/// +/// ```rs +/// #[derive(kani::Arbitrary)] +/// struct AlwaysPositive { +/// #[invariant(*inner >= 0 && *inner < i32::MIN)] +/// inner: i32, +/// } +/// +/// #[kani::proof] +/// fn check_positive() { +/// let val: AlwaysPositive = kani::any(); +/// assert!(val.inner >= 0); +/// } +/// ``` +/// +/// Unfortunately, we made a mistake when specifying the condition because +/// `*inner >= 0 && *inner < i32::MIN` is equivalent to `false`. This results +/// in the relevant assertion being unreachable: +/// +/// ``` +/// Check 1: check_positive.assertion.1 +/// - Status: UNREACHABLE +/// - Description: "assertion failed: val.inner >= 0" +/// - Location: src/main.rs:22:5 in function check_positive +/// ``` +/// +/// As usual, we recommend users to defend against these behaviors by using +/// `kani::cover!(...)` checks and watching out for unreachable assertions in +/// their project's code. #[proc_macro_error] #[proc_macro_derive(Arbitrary, attributes(invariant))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } -/// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro. +/// Allow users to auto generate `Invariant` implementations by using +/// `#[derive(Invariant)]` macro. +/// +/// When using `#[derive(Invariant)]` on a struct, the `#[invariant()]` +/// attribute can be added to its fields to indicate a type safety invariant +/// condition ``. This will ensure that the gets additionally checked when +/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro. +/// +/// For example, the `check_positive` harness in this code is expected to +/// fail: +/// +/// ```rs +/// #[derive(kani::Invariant)] +/// struct AlwaysPositive { +/// #[invariant(*inner >= 0)] +/// inner: i32, +/// } +/// +/// #[kani::proof] +/// fn check_positive() { +/// let val = AlwaysPositive { inner: -1 }; +/// assert!(val.is_safe()); +/// } +/// ``` +/// +/// This is not too surprising since the type safety invariant that we indicated +/// is not being taken into account when we create the `AlwaysPositive` object. +/// +/// As mentioned, the `is_safe()` methods generated by the +/// `#[derive(Invariant)]` macro check the corresponding `is_safe()` method for +/// each field in addition to any type safety invariants specified through the +/// `#[invariant(...)]` attribute. +/// +/// For example, for the `AlwaysPositive` struct from above, we will generate +/// the following implementation: +/// +/// ```rs +/// impl kani::Invariant for AlwaysPositive { +/// fn is_safe(&self) -> bool { +/// let obj = self; +/// let inner = &obj.inner; +/// true && *inner >= 0 && inner.is_safe() +/// } +/// } +/// ``` +/// +/// Note: the assignments to `obj` and `inner` are made so that we can treat the +/// fields as if they were references. #[proc_macro_error] #[proc_macro_derive(Invariant, attributes(invariant))] pub fn derive_invariant(item: TokenStream) -> TokenStream { From f42e724240e8d6bdb04fba44060f4f1c68528658 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 17 Jul 2024 22:07:25 +0000 Subject: [PATCH 23/32] `#[invariant(...)]` -> `#[safety_constraint(...)]` --- library/kani_macros/src/derive.rs | 16 ++++++++-------- library/kani_macros/src/lib.rs | 16 ++++++++-------- .../invariant_helper/invariant_helper.rs | 4 ++-- .../invariant_fail_mut/invariant_fail_mut.rs | 4 ++-- .../invariant_helper/invariant_helper.rs | 4 ++-- .../invariant_helper_funs.rs | 4 ++-- tests/ui/derive-invariant/helper-empty/expected | 2 +- .../helper-empty/helper-empty.rs | 4 ++-- .../helper-no-expr/helper-no-expr.rs | 4 ++-- .../derive-invariant/helper-wrong-expr/expected | 4 ++-- .../helper-wrong-expr/helper-wrong-expr.rs | 4 ++-- 11 files changed, 33 insertions(+), 33 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index f02dfc37dde3..6962eecc0040 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -94,7 +94,7 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Parse the condition expressions in `#[invariant()]` attached to struct +/// Parse the condition expressions in `#[safety_constraint()]` attached to struct /// fields and, it at least one was found, generate a conjunction to be assumed. /// /// For example, if we're deriving implementations for the struct @@ -102,9 +102,9 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { /// #[derive(Arbitrary)] /// #[derive(Invariant)] /// struct PositivePoint { -/// #[invariant(*x >= 0)] +/// #[safety_constraint(*x >= 0)] /// x: i32, -/// #[invariant(*y >= 0)] +/// #[safety_constraint(*y >= 0)] /// y: i32, /// } /// ``` @@ -144,9 +144,9 @@ fn inv_conds_inner(ident: &Ident, fields: &Fields) -> Option { /// #[derive(Arbitrary)] /// #[derive(Invariant)] /// struct PositivePoint { -/// #[invariant(*x >= 0)] +/// #[safety_constraint(*x >= 0)] /// x: i32, -/// #[invariant(*y >= 0)] +/// #[safety_constraint(*y >= 0)] /// y: i32, /// } /// ``` @@ -232,7 +232,7 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { } /// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the -/// `#[invariant()]` attribute helper associated with a given field. +/// `#[safety_constraint()]` attribute helper associated with a given field. /// Return `None` if the attribute isn't specified. fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { let name = &field.ident; @@ -378,10 +378,10 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { // `true && && && ..` // where `inv_condN` is // - `self.fieldN.is_safe() && ` if a condition `` was - // specified through the `#[invariant()]` helper attribute, or + // specified through the `#[safety_constraint()]` helper attribute, or // - `self.fieldN.is_safe()` otherwise // - // Therefore, if `#[invariant()]` isn't specified for any field, this expands to + // Therefore, if `#[safety_constraint()]` isn't specified for any field, this expands to // `true && self.field1.is_safe() && self.field2.is_safe() && ..` Fields::Named(ref fields) => { let inv_conds: Vec = fields diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index da299163a6f2..f1c4494af5d7 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -103,10 +103,10 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// Allow users to auto generate `Arbitrary` implementations by using /// `#[derive(Arbitrary)]` macro. /// -/// When using `#[derive(Arbitrary)]` on a struct, the `#[invariant()]` +/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint()]` /// attribute can be added to its fields to indicate a type safety invariant /// condition ``. Since `kani::any()` is always expected to produce -/// type-safe values, **adding `#[invariant(...)]` to any fields will further +/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further /// constrain the objects generated with `kani::any()`**. /// /// For example, the `check_positive` harness in this code is expected to @@ -115,7 +115,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// ```rs /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { -/// #[invariant(*inner >= 0)] +/// #[safety_constraint(*inner >= 0)] /// inner: i32, /// } /// @@ -126,14 +126,14 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// } /// ``` /// -/// Therefore, using the `#[invariant(...)]` attribute can lead to vacuous +/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous /// results when the values are over-constrained. For example, in this code /// the `check_positive` harness will pass too: /// /// ```rs /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { -/// #[invariant(*inner >= 0 && *inner < i32::MIN)] +/// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)] /// inner: i32, /// } /// @@ -167,7 +167,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// Allow users to auto generate `Invariant` implementations by using /// `#[derive(Invariant)]` macro. /// -/// When using `#[derive(Invariant)]` on a struct, the `#[invariant()]` +/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint()]` /// attribute can be added to its fields to indicate a type safety invariant /// condition ``. This will ensure that the gets additionally checked when /// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro. @@ -178,7 +178,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// ```rs /// #[derive(kani::Invariant)] /// struct AlwaysPositive { -/// #[invariant(*inner >= 0)] +/// #[safety_constraint(*inner >= 0)] /// inner: i32, /// } /// @@ -195,7 +195,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// As mentioned, the `is_safe()` methods generated by the /// `#[derive(Invariant)]` macro check the corresponding `is_safe()` method for /// each field in addition to any type safety invariants specified through the -/// `#[invariant(...)]` attribute. +/// `#[safety_constraint(...)]` attribute. /// /// For example, for the `AlwaysPositive` struct from above, we will generate /// the following implementation: diff --git a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs b/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs index 2a4f841f9dcd..101b25d1f781 100644 --- a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs @@ -9,9 +9,9 @@ use kani::Invariant; #[derive(kani::Arbitrary)] struct PositivePoint { - #[invariant(*x >= 0)] + #[safety_constraint(*x >= 0)] x: i32, - #[invariant(*y >= 0)] + #[safety_constraint(*y >= 0)] y: i32, } diff --git a/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs b/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs index 11bed7a32479..dc659ec66dd6 100644 --- a/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs +++ b/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs @@ -10,9 +10,9 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - #[invariant(*x >= 0)] + #[safety_constraint(*x >= 0)] x: i32, - #[invariant(*y >= 0)] + #[safety_constraint(*y >= 0)] y: i32, } diff --git a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs b/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs index 3b8d6527864a..1ac380335b8b 100644 --- a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs @@ -10,9 +10,9 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - #[invariant(*x >= 0)] + #[safety_constraint(*x >= 0)] x: i32, - #[invariant(*y >= 0)] + #[safety_constraint(*y >= 0)] y: i32, } diff --git a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs b/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs index 415ea0ee2ac3..50419a206825 100644 --- a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs +++ b/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs @@ -11,9 +11,9 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - #[invariant(is_coordinate_safe(x))] + #[safety_constraint(is_coordinate_safe(x))] x: i32, - #[invariant(is_coordinate_safe(y))] + #[safety_constraint(is_coordinate_safe(y))] y: i32, } diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected index 2e4c3285d334..8c7cae62b35e 100644 --- a/tests/ui/derive-invariant/helper-empty/expected +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -3,4 +3,4 @@ error: Cannot derive impl for `PositivePoint` 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | -note: invariant condition in field `x` could not be parsed: expected attribute arguments in parentheses: #[invariant(...)] +note: invariant condition in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)] diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs index 518a1e35eb56..1072f72d07ba 100644 --- a/tests/ui/derive-invariant/helper-empty/helper-empty.rs +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -10,8 +10,8 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - #[invariant] + #[safety_constraint] x: i32, - #[invariant(*y >= 0)] + #[safety_constraint(*y >= 0)] y: i32, } diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs index 302b9193f9fc..916b047b7274 100644 --- a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -10,8 +10,8 @@ use kani::Invariant; #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] struct PositivePoint { - #[invariant()] + #[safety_constraint()] x: i32, - #[invariant(*y >= 0)] + #[safety_constraint(*y >= 0)] y: i32, } diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index 84de40d44478..efa29c758637 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -1,9 +1,9 @@ error[E0308]: mismatched types | -14 | #[invariant(x >= 0)] +14 | #[safety_constraint(x >= 0)] | ^ expected `&i32`, found integer | help: consider dereferencing the borrow | -14 | #[invariant(*x >= 0)] +14 | #[safety_constraint(*x >= 0)] | + diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs index 99c759165fb9..ed179145c7cb 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -11,8 +11,8 @@ use kani::Invariant; #[derive(kani::Invariant)] struct PositivePoint { // Note: `x` is a reference in this context, we should refer to `*x` - #[invariant(x >= 0)] + #[safety_constraint(x >= 0)] x: i32, - #[invariant(*y >= 0)] + #[safety_constraint(*y >= 0)] y: i32, } From b6ec5b91726aa74142e4f0c22601496e0d7d8cf6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 17 Jul 2024 22:18:32 +0000 Subject: [PATCH 24/32] Missing important rename --- library/kani_macros/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index f1c4494af5d7..4e3a8d6f9f5b 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -159,7 +159,7 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// `kani::cover!(...)` checks and watching out for unreachable assertions in /// their project's code. #[proc_macro_error] -#[proc_macro_derive(Arbitrary, attributes(invariant))] +#[proc_macro_derive(Arbitrary, attributes(safety_constraint))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } @@ -213,7 +213,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// Note: the assignments to `obj` and `inner` are made so that we can treat the /// fields as if they were references. #[proc_macro_error] -#[proc_macro_derive(Invariant, attributes(invariant))] +#[proc_macro_derive(Invariant, attributes(safety_constraint))] pub fn derive_invariant(item: TokenStream) -> TokenStream { derive::expand_derive_invariant(item) } From c3fc474ca839c782b73226b7d10e320d98907146 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 18 Jul 2024 15:25:03 +0000 Subject: [PATCH 25/32] Fix helper pick-up and rename tests --- library/kani_macros/src/derive.rs | 4 ++-- .../{invariant_helper => safety_constraint_helper}/expected | 0 .../safety_constraint_helper.rs} | 2 +- .../{invariant_helper => safety_constraint_helper}/expected | 0 .../safety_constraint_helper.rs} | 2 +- .../expected | 0 .../safety_constraint_helper_funs.rs} | 2 +- .../{invariant_fail => safety_invariant_fail}/expected | 0 .../safety_invariant_fail.rs} | 0 .../expected | 0 .../safety_invariant_fail_mut.rs} | 0 tests/ui/derive-invariant/helper-empty/helper-empty.rs | 2 +- tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs | 2 +- tests/ui/derive-invariant/helper-wrong-expr/expected | 4 ++-- .../derive-invariant/helper-wrong-expr/helper-wrong-expr.rs | 2 +- 15 files changed, 10 insertions(+), 10 deletions(-) rename tests/expected/derive-arbitrary/{invariant_helper => safety_constraint_helper}/expected (100%) rename tests/expected/derive-arbitrary/{invariant_helper/invariant_helper.rs => safety_constraint_helper/safety_constraint_helper.rs} (88%) rename tests/expected/derive-invariant/{invariant_helper => safety_constraint_helper}/expected (100%) rename tests/expected/derive-invariant/{invariant_helper/invariant_helper.rs => safety_constraint_helper/safety_constraint_helper.rs} (92%) rename tests/expected/derive-invariant/{invariant_helper_funs => safety_constraint_helper_funs}/expected (100%) rename tests/expected/derive-invariant/{invariant_helper_funs/invariant_helper_funs.rs => safety_constraint_helper_funs/safety_constraint_helper_funs.rs} (93%) rename tests/expected/derive-invariant/{invariant_fail => safety_invariant_fail}/expected (100%) rename tests/expected/derive-invariant/{invariant_fail/invariant_fail.rs => safety_invariant_fail/safety_invariant_fail.rs} (100%) rename tests/expected/derive-invariant/{invariant_fail_mut => safety_invariant_fail_mut}/expected (100%) rename tests/expected/derive-invariant/{invariant_fail_mut/invariant_fail_mut.rs => safety_invariant_fail_mut/safety_invariant_fail_mut.rs} (100%) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 6962eecc0040..3e41100fd810 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -240,12 +240,12 @@ fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { // Keep the helper attribute if we find it for attr in &field.attrs { - if attr.path().is_ident("invariant") { + if attr.path().is_ident("safety_constraint") { inv_helper_attr = Some(attr); } } - // Parse the arguments in the invariant helper attribute + // Parse the arguments in the `#[safety_constraint(...)]` attribute if let Some(attr) = inv_helper_attr { let expr_args: Result = attr.parse_args(); diff --git a/tests/expected/derive-arbitrary/invariant_helper/expected b/tests/expected/derive-arbitrary/safety_constraint_helper/expected similarity index 100% rename from tests/expected/derive-arbitrary/invariant_helper/expected rename to tests/expected/derive-arbitrary/safety_constraint_helper/expected diff --git a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs similarity index 88% rename from tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs rename to tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs index 101b25d1f781..5b608aa2a3c0 100644 --- a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that the invariant attribute helper adds the conditions provided to +//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to //! the attribute to the derived `Arbitrary` implementation. extern crate kani; diff --git a/tests/expected/derive-invariant/invariant_helper/expected b/tests/expected/derive-invariant/safety_constraint_helper/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_helper/expected rename to tests/expected/derive-invariant/safety_constraint_helper/expected diff --git a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs similarity index 92% rename from tests/expected/derive-invariant/invariant_helper/invariant_helper.rs rename to tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs index 1ac380335b8b..d824a706c8b8 100644 --- a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that the invariant attribute helper adds the conditions provided to +//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to //! the attribute to the derived `Invariant` implementation. extern crate kani; diff --git a/tests/expected/derive-invariant/invariant_helper_funs/expected b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_helper_funs/expected rename to tests/expected/derive-invariant/safety_constraint_helper_funs/expected diff --git a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs similarity index 93% rename from tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs rename to tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs index 50419a206825..cc0132273e80 100644 --- a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs +++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that functions can be called in the invariant attribute helpers. +//! Check that functions can be called in the `#[safety_constraint(...)]` attribute helpers. //! This is like the `invariant_helper` test but using a function instead //! of passing in a predicate. diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/safety_invariant_fail/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_fail/expected rename to tests/expected/derive-invariant/safety_invariant_fail/expected diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs similarity index 100% rename from tests/expected/derive-invariant/invariant_fail/invariant_fail.rs rename to tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs diff --git a/tests/expected/derive-invariant/invariant_fail_mut/expected b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_fail_mut/expected rename to tests/expected/derive-invariant/safety_invariant_fail_mut/expected diff --git a/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs similarity index 100% rename from tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs rename to tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs index 1072f72d07ba..3086603cf5db 100644 --- a/tests/ui/derive-invariant/helper-empty/helper-empty.rs +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check the compilation error for the invariant attribute helper when an +//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when an //! argument isn't provided. extern crate kani; diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs index 916b047b7274..080c94371257 100644 --- a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check the compilation error for the invariant attribute helper when the +//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the //! argument is not a proper expression. extern crate kani; diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index efa29c758637..7d14cb1e753a 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -1,9 +1,9 @@ error[E0308]: mismatched types | 14 | #[safety_constraint(x >= 0)] - | ^ expected `&i32`, found integer + | ^ expected `&i32`, found integer | help: consider dereferencing the borrow | 14 | #[safety_constraint(*x >= 0)] - | + + | diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs index ed179145c7cb..66b42e02fd68 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check the compilation error for the invariant attribute helper when the +//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the //! argument cannot be evaluated in the struct's context. extern crate kani; From 1a549bea350470bf7905d53884ce99dfd639389d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 18 Jul 2024 15:34:24 +0000 Subject: [PATCH 26/32] Last renames --- library/kani_macros/src/derive.rs | 46 +++++++++++++++---------------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 3e41100fd810..a7aaa8ae334e 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -29,10 +29,10 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let body = fn_any_body(&item_name, &derive_item.data); - // Get the invariant conditions (if any) to produce type-safe values - let inv_conds_opt = inv_conds(&item_name, &derive_item.data); + // Get the safety constraints (if any) to produce type-safe values + let safety_conds_opt = safety_conds(&item_name, &derive_item.data); - let expanded = if let Some(inv_cond) = inv_conds_opt { + let expanded = if let Some(safety_cond) = safety_conds_opt { let field_refs = field_refs(&item_name, &derive_item.data); quote! { // The generated implementation. @@ -40,7 +40,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok fn any() -> Self { let obj = #body; #field_refs - kani::assume(#inv_cond); + kani::assume(#safety_cond); obj } } @@ -114,21 +114,21 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { /// ``` /// which can be passed to `kani::assume` to constrain the values generated /// through the `Arbitrary` impl so that they are type-safe by construction. -fn inv_conds(ident: &Ident, data: &Data) -> Option { +fn safety_conds(ident: &Ident, data: &Data) -> Option { match data { - Data::Struct(struct_data) => inv_conds_inner(ident, &struct_data.fields), + Data::Struct(struct_data) => safety_conds_inner(ident, &struct_data.fields), Data::Enum(_) => None, Data::Union(_) => None, } } /// Generates an expression resulting from the conjunction of conditions -/// specified as invariants for each field. See `inv_conds` for more details. -fn inv_conds_inner(ident: &Ident, fields: &Fields) -> Option { +/// specified as safety constraints for each field. See `safety_conds` for more details. +fn safety_conds_inner(ident: &Ident, fields: &Fields) -> Option { match fields { Fields::Named(ref fields) => { let conds: Vec = - fields.named.iter().filter_map(|field| parse_inv_expr(ident, field)).collect(); + fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect(); if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } } Fields::Unnamed(_) => None, @@ -234,33 +234,33 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { /// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the /// `#[safety_constraint()]` attribute helper associated with a given field. /// Return `None` if the attribute isn't specified. -fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { +fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { let name = &field.ident; - let mut inv_helper_attr = None; + let mut safety_helper_attr = None; // Keep the helper attribute if we find it for attr in &field.attrs { if attr.path().is_ident("safety_constraint") { - inv_helper_attr = Some(attr); + safety_helper_attr = Some(attr); } } // Parse the arguments in the `#[safety_constraint(...)]` attribute - if let Some(attr) = inv_helper_attr { + if let Some(attr) = safety_helper_attr { let expr_args: Result = attr.parse_args(); // Check if there was an error parsing the arguments if let Err(err) = expr_args { abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; note = attr.span() => - "invariant condition in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err + "safety constraint in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err ) } - // Return the expression associated to the invariant condition - let inv_expr = expr_args.unwrap(); + // Return the expression associated to the safety constraint + let safety_expr = expr_args.unwrap(); Some(quote_spanned! {field.span()=> - #inv_expr + #safety_expr }) } else { None @@ -371,12 +371,12 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Generates an expression that is the conjunction of invariant conditions for each field in the struct. +/// Generates an expression that is the conjunction of safety constraints for each field in the struct. fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { match fields { // Expands to the expression - // `true && && && ..` - // where `inv_condN` is + // `true && && && ..` + // where `safety_condN` is // - `self.fieldN.is_safe() && ` if a condition `` was // specified through the `#[safety_constraint()]` helper attribute, or // - `self.fieldN.is_safe()` otherwise @@ -384,7 +384,7 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { // Therefore, if `#[safety_constraint()]` isn't specified for any field, this expands to // `true && self.field1.is_safe() && self.field2.is_safe() && ..` Fields::Named(ref fields) => { - let inv_conds: Vec = fields + let safety_conds: Vec = fields .named .iter() .map(|field| { @@ -392,13 +392,13 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { let default_expr = quote_spanned! {field.span()=> #name.is_safe() }; - parse_inv_expr(ident, field) + parse_safety_expr(ident, field) .map(|expr| quote! { #expr && #default_expr}) .unwrap_or(default_expr) }) .collect(); // An initial value is required for empty structs - inv_conds.iter().fold(quote! { true }, |acc, cond| { + safety_conds.iter().fold(quote! { true }, |acc, cond| { quote! { #acc && #cond } }) } From eba5ef92507bb72ab1907a9415fc3f658c13ee0d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 18 Jul 2024 16:23:23 +0000 Subject: [PATCH 27/32] Fixes for renaming --- tests/ui/derive-invariant/helper-empty/expected | 2 +- tests/ui/derive-invariant/helper-no-expr/expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected index 8c7cae62b35e..cc663578d9ba 100644 --- a/tests/ui/derive-invariant/helper-empty/expected +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -3,4 +3,4 @@ error: Cannot derive impl for `PositivePoint` 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | -note: invariant condition in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)] +note: safety constraint in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)] diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected index b52ee673daf8..e31316ded8f7 100644 --- a/tests/ui/derive-invariant/helper-no-expr/expected +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -3,4 +3,4 @@ error: Cannot derive impl for `PositivePoint` 11 | #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | -note: invariant condition in field `x` could not be parsed: unexpected end of input, expected an expression +note: safety constraint in field `x` could not be parsed: unexpected end of input, expected an expression From 2e7c94cee9f55f807b12cd268e2189912b927fc9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Jul 2024 18:44:32 +0000 Subject: [PATCH 28/32] Add two more tests --- .../attrs_cfg_guard/attrs_cfg_guard.rs | 24 +++++++++++++++++++ .../derive-invariant/attrs_cfg_guard/expected | 9 +++++++ .../attrs_mixed/attrs_mixed.rs | 24 +++++++++++++++++++ .../derive-invariant/attrs_mixed/expected | 9 +++++++ 4 files changed, 66 insertions(+) create mode 100644 tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs create mode 100644 tests/expected/derive-invariant/attrs_cfg_guard/expected create mode 100644 tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs create mode 100644 tests/expected/derive-invariant/attrs_mixed/expected diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs new file mode 100644 index 000000000000..546695bf3731 --- /dev/null +++ b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute helper is picked up +//! when it's used with `cfg_attr(kani, ...)]`. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[cfg_attr(kani, safety_constraint(*x >= 0))] + x: i32, + #[cfg_attr(kani, safety_constraint(*y >= 0))] + y: i32, +} + +#[kani::proof] +fn check_safety_constraint_cfg() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/expected b/tests/expected/derive-invariant/attrs_cfg_guard/expected new file mode 100644 index 000000000000..edb3e256975d --- /dev/null +++ b/tests/expected/derive-invariant/attrs_cfg_guard/expected @@ -0,0 +1,9 @@ +Check 1: check_safety_constraint_cfg.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_safety_constraint_cfg.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.y >= 0" + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs new file mode 100644 index 000000000000..ff58ff846c67 --- /dev/null +++ b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that in the `#[safety_constraint(...)]` attribute helper it is +//! possible to refer to other struct fields, not just the one associated with +//! the attribute. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint(*x >= 0 && *y >= 0)] + x: i32, + y: i32, +} + +#[kani::proof] +fn check_safety_constraint_cfg() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} diff --git a/tests/expected/derive-invariant/attrs_mixed/expected b/tests/expected/derive-invariant/attrs_mixed/expected new file mode 100644 index 000000000000..edb3e256975d --- /dev/null +++ b/tests/expected/derive-invariant/attrs_mixed/expected @@ -0,0 +1,9 @@ +Check 1: check_safety_constraint_cfg.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_safety_constraint_cfg.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.y >= 0" + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. From 477d9bf33c9f89bb635753e3a6bfd9d4702f8b81 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Jul 2024 18:50:13 +0000 Subject: [PATCH 29/32] Update comments so they're clear. --- .../safety_constraint_helper/safety_constraint_helper.rs | 9 +++++---- .../safety_constraint_helper_funs.rs | 9 +++++---- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs index d824a706c8b8..44a218f8fa63 100644 --- a/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs +++ b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs @@ -25,16 +25,17 @@ fn check_invariant_helper_ok() { #[kani::proof] #[kani::should_panic] fn check_invariant_helper_fail() { - // In this case, `kani::any()` returns unconstrained values that don't - // respect the invariants. + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; assert!(pos_point.is_safe()); } #[kani::proof] fn check_invariant_helper_ok_manual() { - // In this case, `kani::any()` returns unconstrained values that don't - // respect the invariants. However, we manually constrain them later. + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. However, we + // manually constrain them later. let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; kani::assume(pos_point.x >= 0); kani::assume(pos_point.y >= 0); diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs index cc0132273e80..a2c4600eb208 100644 --- a/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs +++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs @@ -30,16 +30,17 @@ fn check_invariant_helper_ok() { #[kani::proof] #[kani::should_panic] fn check_invariant_helper_fail() { - // In this case, `kani::any()` returns unconstrained values that don't - // respect the invariants. + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; assert!(pos_point.is_safe()); } #[kani::proof] fn check_invariant_helper_ok_manual() { - // In this case, `kani::any()` returns unconstrained values that don't - // respect the invariants. However, we manually constrain them later. + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. However, we + // manually constrain them later. let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; kani::assume(pos_point.x >= 0); kani::assume(pos_point.y >= 0); From 11e55972687101c1fb3747e2956c52f96fbb0c1d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Jul 2024 18:52:52 +0000 Subject: [PATCH 30/32] Updated UI tests to not have line numbers --- tests/ui/derive-invariant/helper-empty/expected | 2 +- tests/ui/derive-invariant/helper-no-expr/expected | 2 +- tests/ui/derive-invariant/helper-wrong-expr/expected | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected index cc663578d9ba..d8590a9d22b8 100644 --- a/tests/ui/derive-invariant/helper-empty/expected +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -1,6 +1,6 @@ error: Cannot derive impl for `PositivePoint` | -11 | #[derive(kani::Invariant)] +| #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | note: safety constraint in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)] diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected index e31316ded8f7..e9ac7e3e1124 100644 --- a/tests/ui/derive-invariant/helper-no-expr/expected +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -1,6 +1,6 @@ error: Cannot derive impl for `PositivePoint` | -11 | #[derive(kani::Invariant)] +| #[derive(kani::Invariant)] | ^^^^^^^^^^^^^^^ | note: safety constraint in field `x` could not be parsed: unexpected end of input, expected an expression diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index 7d14cb1e753a..3f661bce9cbb 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -1,9 +1,9 @@ error[E0308]: mismatched types | -14 | #[safety_constraint(x >= 0)] +| #[safety_constraint(x >= 0)] | ^ expected `&i32`, found integer | help: consider dereferencing the borrow | -14 | #[safety_constraint(*x >= 0)] +| #[safety_constraint(*x >= 0)] | From 05dea4505931a609e105249ccb34276fc002fdf9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Jul 2024 19:06:48 +0000 Subject: [PATCH 31/32] Add side-effect test --- .../helper-side-effect/expected | 10 +++++++++ .../helper-side-effect/helper-side-effect.rs | 22 +++++++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 tests/ui/derive-invariant/helper-side-effect/expected create mode 100644 tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs diff --git a/tests/ui/derive-invariant/helper-side-effect/expected b/tests/ui/derive-invariant/helper-side-effect/expected new file mode 100644 index 000000000000..21495a26fa4c --- /dev/null +++ b/tests/ui/derive-invariant/helper-side-effect/expected @@ -0,0 +1,10 @@ +error[E0596]: cannot borrow `*x` as mutable, as it is behind a `&` reference + --> safety_constraint_helper_side_effect/safety_constraint_helper_side_effect.rs:12:28 + | +| #[safety_constraint({*(x.as_mut()) = 0; true})] + | ^ `x` is a `&` reference, so the data it refers to cannot be borrowed as mutable + | +help: consider specifying this binding's type + | +| x: &mut std::boxed::Box: Box, + | +++++++++++++++++++++++++++ diff --git a/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs new file mode 100644 index 000000000000..e80f2ff25796 --- /dev/null +++ b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that side effect expressions in the `#[safety_constraint(...)]` +//! attribute helpers are not allowed. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint({*(x.as_mut()) = 0; true})] + x: Box, + y: i32, +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); +} From bf93601bb4d7d2222c7ac5f59f2c49a6a64dd402 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Jul 2024 19:46:54 +0000 Subject: [PATCH 32/32] Remove path line --- tests/ui/derive-invariant/helper-side-effect/expected | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/ui/derive-invariant/helper-side-effect/expected b/tests/ui/derive-invariant/helper-side-effect/expected index 21495a26fa4c..20b3d17efd38 100644 --- a/tests/ui/derive-invariant/helper-side-effect/expected +++ b/tests/ui/derive-invariant/helper-side-effect/expected @@ -1,5 +1,4 @@ error[E0596]: cannot borrow `*x` as mutable, as it is behind a `&` reference - --> safety_constraint_helper_side_effect/safety_constraint_helper_side_effect.rs:12:28 | | #[safety_constraint({*(x.as_mut()) = 0; true})] | ^ `x` is a `&` reference, so the data it refers to cannot be borrowed as mutable