From f7cb4a1f1906c8b5a29e763078841aa8d644e2b3 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 17 May 2024 21:39:33 +0000 Subject: [PATCH 1/6] Add a `#[derive(Invariant)]` macro --- library/kani_macros/src/derive.rs | 94 ++++++++++++++++++- library/kani_macros/src/lib.rs | 7 ++ .../empty_struct/empty_struct.rs | 38 ++++++++ .../derive-invariant/empty_struct/expected | 2 + .../derive-invariant/generic_struct/expected | 2 + .../generic_struct/generic_struct.rs | 20 ++++ .../derive-invariant/named_struct/expected | 2 + .../named_struct/named_struct.rs | 20 ++++ .../derive-invariant/unnamed_struct/expected | 2 + .../unnamed_struct/unnamed_struct.rs | 17 ++++ 10 files changed, 202 insertions(+), 2 deletions(-) create mode 100644 tests/expected/derive-invariant/empty_struct/empty_struct.rs create mode 100644 tests/expected/derive-invariant/empty_struct/expected create mode 100644 tests/expected/derive-invariant/generic_struct/expected create mode 100644 tests/expected/derive-invariant/generic_struct/generic_struct.rs create mode 100644 tests/expected/derive-invariant/named_struct/expected create mode 100644 tests/expected/derive-invariant/named_struct/named_struct.rs create mode 100644 tests/expected/derive-invariant/unnamed_struct/expected create mode 100644 tests/expected/derive-invariant/unnamed_struct/unnamed_struct.rs diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 7e3dee390330..4e99590fc6a3 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -23,7 +23,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let item_name = &derive_item.ident; // Add a bound `T: Arbitrary` to every type parameter T. - let generics = add_trait_bound(derive_item.generics); + let generics = add_trait_bound_arbitrary(derive_item.generics); // Generate an expression to sum up the heap size of each field. let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); @@ -40,7 +40,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok } /// Add a bound `T: Arbitrary` to every type parameter T. -fn add_trait_bound(mut generics: Generics) -> Generics { +fn add_trait_bound_arbitrary(mut generics: Generics) -> Generics { generics.params.iter_mut().for_each(|param| { if let GenericParam::Type(type_param) = param { type_param.bounds.push(parse_quote!(kani::Arbitrary)); @@ -165,3 +165,93 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream { } } } + +pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::TokenStream { + let derive_item = parse_macro_input!(item as DeriveInput); + let item_name = &derive_item.ident; + + // Add a bound `T: Invariant` to every type parameter T. + let generics = add_trait_bound_invariant(derive_item.generics); + // Generate an expression to sum up the heap size of each field. + let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); + + let body = is_safe_body(&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 { + #body + } + } + }; + proc_macro::TokenStream::from(expanded) +} + +/// Add a bound `T: Invariant` to every type parameter T. +fn add_trait_bound_invariant(mut generics: Generics) -> Generics { + generics.params.iter_mut().for_each(|param| { + if let GenericParam::Type(type_param) = param { + type_param.bounds.push(parse_quote!(kani::Invariant)); + } + }); + generics +} + +fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { + match data { + Data::Struct(struct_data) => struct_safe_conjunction(ident, &struct_data.fields), + Data::Enum(_) => { + abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident; + note = ident.span() => + "`#[derive(Invariant)]` cannot be used for enums such as `{}`", ident + ) + } + Data::Union(_) => { + abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` union", ident; + note = ident.span() => + "`#[derive(Invariant)]` cannot be used for unions such as `{}`", ident + ) + } + } +} + +/// 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 { + match fields { + // Expands to the expression + // `true && self.field1.is_safe() && self.field2.is_safe() && ..` + Fields::Named(ref fields) => { + let safe_calls = fields.named.iter().map(|field| { + let name = &field.ident; + 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 } + }) + } + Fields::Unnamed(ref fields) => { + // Expands to the expression + // `true && self.0.is_safe() && self.1.is_safe() && ..` + let safe_calls = fields.unnamed.iter().enumerate().map(|(i, field)| { + let idx = syn::Index::from(i); + quote_spanned! {field.span()=> + self.#idx.is_safe() + } + }); + // An initial value is required for empty structs + safe_calls.fold(quote! { true }, |acc, call| { + quote! { #acc && #call } + }) + } + // Expands to the expression + // `true` + Fields::Unit => { + quote! { + true + } + } + } +} diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 44a0ca78ea41..bcfb89c4af12 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -107,6 +107,13 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } +/// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro. +#[proc_macro_error] +#[proc_macro_derive(Invariant)] +pub fn derive_invariant(item: TokenStream) -> TokenStream { + derive::expand_derive_invariant(item) +} + /// Add a precondition to this function. /// /// This is part of the function contract API, for more general information see diff --git a/tests/expected/derive-invariant/empty_struct/empty_struct.rs b/tests/expected/derive-invariant/empty_struct/empty_struct.rs new file mode 100644 index 000000000000..64d5679f6fca --- /dev/null +++ b/tests/expected/derive-invariant/empty_struct/empty_struct.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can automatically derive `Invariant` for empty structs. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct Void; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct Void2(()); + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct VoidOfVoid(Void, Void2); + +#[kani::proof] +fn check_empty_struct_invariant_1() { + let void: Void = kani::any(); + assert!(void.is_safe()); +} + + +#[kani::proof] +fn check_empty_struct_invariant_2() { + let void: Void2 = kani::any(); + assert!(void.is_safe()); +} + +#[kani::proof] +fn check_empty_struct_invariant_3() { + let void: VoidOfVoid = kani::any(); + assert!(void.is_safe()); +} diff --git a/tests/expected/derive-invariant/empty_struct/expected b/tests/expected/derive-invariant/empty_struct/expected new file mode 100644 index 000000000000..5e5886bb3e45 --- /dev/null +++ b/tests/expected/derive-invariant/empty_struct/expected @@ -0,0 +1,2 @@ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" diff --git a/tests/expected/derive-invariant/generic_struct/expected b/tests/expected/derive-invariant/generic_struct/expected new file mode 100644 index 000000000000..5e5886bb3e45 --- /dev/null +++ b/tests/expected/derive-invariant/generic_struct/expected @@ -0,0 +1,2 @@ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" diff --git a/tests/expected/derive-invariant/generic_struct/generic_struct.rs b/tests/expected/derive-invariant/generic_struct/generic_struct.rs new file mode 100644 index 000000000000..91c62fac8ece --- /dev/null +++ b/tests/expected/derive-invariant/generic_struct/generic_struct.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can automatically derive `Invariant` for structs with generics. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct Point { + x: X, + y: Y, +} + +#[kani::proof] +fn check_generic_struct_invariant() { + let point: Point = kani::any(); + assert!(point.is_safe()); +} diff --git a/tests/expected/derive-invariant/named_struct/expected b/tests/expected/derive-invariant/named_struct/expected new file mode 100644 index 000000000000..5e5886bb3e45 --- /dev/null +++ b/tests/expected/derive-invariant/named_struct/expected @@ -0,0 +1,2 @@ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" diff --git a/tests/expected/derive-invariant/named_struct/named_struct.rs b/tests/expected/derive-invariant/named_struct/named_struct.rs new file mode 100644 index 000000000000..7e27404bda11 --- /dev/null +++ b/tests/expected/derive-invariant/named_struct/named_struct.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can automatically derive `Invariant` for structs with named fields. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct Point { + x: i32, + y: i32, +} + +#[kani::proof] +fn check_generic_struct_invariant() { + let point: Point = kani::any(); + assert!(point.is_safe()); +} diff --git a/tests/expected/derive-invariant/unnamed_struct/expected b/tests/expected/derive-invariant/unnamed_struct/expected new file mode 100644 index 000000000000..5e5886bb3e45 --- /dev/null +++ b/tests/expected/derive-invariant/unnamed_struct/expected @@ -0,0 +1,2 @@ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" diff --git a/tests/expected/derive-invariant/unnamed_struct/unnamed_struct.rs b/tests/expected/derive-invariant/unnamed_struct/unnamed_struct.rs new file mode 100644 index 000000000000..5dee718d05a6 --- /dev/null +++ b/tests/expected/derive-invariant/unnamed_struct/unnamed_struct.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can automatically derive `Invariant` for structs with unnamed fields. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct Point(i32, i32); + +#[kani::proof] +fn check_generic_struct_invariant() { + let point: Point = kani::any(); + assert!(point.is_safe()); +} From 1720300fe52d82c299231638ed031e987014728f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 10 Jun 2024 19:55:26 +0000 Subject: [PATCH 2/6] Format fix --- tests/expected/derive-invariant/empty_struct/empty_struct.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/expected/derive-invariant/empty_struct/empty_struct.rs b/tests/expected/derive-invariant/empty_struct/empty_struct.rs index 64d5679f6fca..c569d2f13d40 100644 --- a/tests/expected/derive-invariant/empty_struct/empty_struct.rs +++ b/tests/expected/derive-invariant/empty_struct/empty_struct.rs @@ -24,7 +24,6 @@ fn check_empty_struct_invariant_1() { assert!(void.is_safe()); } - #[kani::proof] fn check_empty_struct_invariant_2() { let void: Void2 = kani::any(); From 64d146da95c20db4b68238caae97b0bcfe1b8e01 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 10 Jun 2024 21:21:02 +0000 Subject: [PATCH 3/6] Fix empty struct test --- .../derive-invariant/empty_struct/empty_struct.rs | 12 ++++++------ .../expected/derive-invariant/empty_struct/expected | 8 +++++++- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/tests/expected/derive-invariant/empty_struct/empty_struct.rs b/tests/expected/derive-invariant/empty_struct/empty_struct.rs index c569d2f13d40..4c931ce8aedc 100644 --- a/tests/expected/derive-invariant/empty_struct/empty_struct.rs +++ b/tests/expected/derive-invariant/empty_struct/empty_struct.rs @@ -20,18 +20,18 @@ struct VoidOfVoid(Void, Void2); #[kani::proof] fn check_empty_struct_invariant_1() { - let void: Void = kani::any(); - assert!(void.is_safe()); + let void1: Void = kani::any(); + assert!(void1.is_safe()); } #[kani::proof] fn check_empty_struct_invariant_2() { - let void: Void2 = kani::any(); - assert!(void.is_safe()); + let void2: Void2 = kani::any(); + assert!(void2.is_safe()); } #[kani::proof] fn check_empty_struct_invariant_3() { - let void: VoidOfVoid = kani::any(); - assert!(void.is_safe()); + let void3: VoidOfVoid = kani::any(); + assert!(void3.is_safe()); } diff --git a/tests/expected/derive-invariant/empty_struct/expected b/tests/expected/derive-invariant/empty_struct/expected index 5e5886bb3e45..8fdca72b1ead 100644 --- a/tests/expected/derive-invariant/empty_struct/expected +++ b/tests/expected/derive-invariant/empty_struct/expected @@ -1,2 +1,8 @@ - Status: SUCCESS\ - - Description: "assertion failed: point.is_safe()" + - Description: "assertion failed: void1.is_safe()" + + - Status: SUCCESS\ + - Description: "assertion failed: void2.is_safe()" + + - Status: SUCCESS\ + - Description: "assertion failed: void3.is_safe()" From dbe03cd9ff72e758944549cba1027b0fddf6e9ed Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 13 Jun 2024 20:42:08 +0000 Subject: [PATCH 4/6] Add test in which the invariant check fails --- .../derive-invariant/invariant_fail/expected | 4 +++ .../invariant_fail/invariant_fail.rs | 29 +++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 tests/expected/derive-invariant/invariant_fail/expected create mode 100644 tests/expected/derive-invariant/invariant_fail/invariant_fail.rs diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/invariant_fail/expected new file mode 100644 index 000000000000..824c87a3bce1 --- /dev/null +++ b/tests/expected/derive-invariant/invariant_fail/expected @@ -0,0 +1,4 @@ + - Status: FAILURE\ + - Description: "assertion failed: wrapper.is_safe()" + +Verification failed for - check_invariant_fail \ No newline at end of file diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs new file mode 100644 index 000000000000..51fa3028e20b --- /dev/null +++ b/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that a verification failure is triggered when the derived `Invariant` +//! method is checked but not satisfied. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +struct NotNegative(i32); + +impl kani::Invariant for NotNegative { + fn is_safe(&self) -> bool { + self.0 >= 0 + } +} + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct NotNegativeWrapper { + x: NotNegative, +} + +#[kani::proof] +fn check_invariant_fail() { + let wrapper: NotNegativeWrapper = kani::any(); + assert!(wrapper.is_safe()); +} From 47952103592434dfb4a4bab54aebfabc3c5569e0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 13 Jun 2024 20:43:11 +0000 Subject: [PATCH 5/6] Newline --- tests/expected/derive-invariant/invariant_fail/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/invariant_fail/expected index 824c87a3bce1..511d5901e154 100644 --- a/tests/expected/derive-invariant/invariant_fail/expected +++ b/tests/expected/derive-invariant/invariant_fail/expected @@ -1,4 +1,4 @@ - Status: FAILURE\ - Description: "assertion failed: wrapper.is_safe()" -Verification failed for - check_invariant_fail \ No newline at end of file +Verification failed for - check_invariant_fail From 9a8dbb2d218caf55b312c57c2f6889e6ce643b65 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 13 Jun 2024 23:02:32 +0000 Subject: [PATCH 6/6] Add comment and link to issue --- .../derive-invariant/invariant_fail/invariant_fail.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs index 51fa3028e20b..b1d6f8679835 100644 --- a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs +++ b/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs @@ -6,7 +6,11 @@ extern crate kani; use kani::Invariant; - +// Note: This represents an incorrect usage of `Arbitrary` and `Invariant`. +// +// The `Arbitrary` implementation should respect the type invariant, +// but Kani does not enforce this in any way at the moment. +// #[derive(kani::Arbitrary)] struct NotNegative(i32);