From 7e02353ff36bc6d08ede14c4e52c5f46c8f3b7f1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 31 Jul 2024 17:11:01 +0200 Subject: [PATCH 1/2] Reduce memory consumption of cell_stub.rs test (#3399) With MiniSat the test takes 45 seconds instead of 30 seconds, but only consumes 5.5 GB of memory instead of 9 GB. This will hopefully fix CI failures. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../function-contract/interior-mutability/api/cell_stub.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs index d01ca379655f..9752bec5d272 100644 --- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts +// kani-flags: -Zfunction-contracts --solver minisat /// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple. /// This shows that we can generate `kani::any()` for Cell. From b5d306ac9ababf8045cf1f6abefb1616fe0ee651 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 31 Jul 2024 11:58:29 -0400 Subject: [PATCH 2/2] Define a struct-level `#[safety_constraint(...)]` attribute (#3270) This PR defines a struct-level `#[safety_constraint()]` macro attribute that allows users to define the type invariant as the predicate passed as an argument to the attribute. This safety constraint is picked up when deriving `Arbitrary` and `Invariant` implementations so that the values generated with `any()` or checked with `is_safe()` satisfy the constraint. This attribute is similar to the helper attribute introduced in #3283, and they cannot be used together. It's preferable to use this attribute when the constraint implies some relation between different fields. But, at the moment, there's no practical difference between them because the helper attribute allows users to refer to any fields. If we imposed that restriction, this attribute would be the only way to specify struct-wide invariants. An example: ```rs #[derive(kani::Arbitrary)] #[derive(kani::Invariant)] #[safety_constraint(*x == *y)] struct SameCoordsPoint { x: i32, y: i32, } #[kani::proof] fn check_invariant() { let point: SameCoordsPoint = kani::any(); assert!(point.is_safe()); } ``` Resolves #3095 --- library/kani_macros/src/derive.rs | 321 ++++++++++++------ .../abstract-value/abstract-value.rs | 30 ++ .../abstract-value/expected | 7 + .../check-arbitrary/check-arbitrary.rs | 24 ++ .../check-arbitrary/expected | 11 + .../check-invariant/check-invariant.rs | 27 ++ .../check-invariant/expected | 7 + .../grade-example/expected | 11 + .../grade-example/grade-example.rs | 43 +++ .../double-attribute/double-attribute.rs | 16 + .../double-attribute/expected | 6 + .../invalid-pred-error/expected | 19 ++ .../invalid-pred-error/invalid-pred-error.rs | 19 ++ .../mixed-attributes/expected | 6 + .../mixed-attributes/mixed-attributes.rs | 17 + .../no-struct-error/expected | 6 + .../no-struct-error/no-struct-error.rs | 18 + 17 files changed, 490 insertions(+), 98 deletions(-) create mode 100644 tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs create mode 100644 tests/expected/safety-constraint-attribute/abstract-value/expected create mode 100644 tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs create mode 100644 tests/expected/safety-constraint-attribute/check-arbitrary/expected create mode 100644 tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs create mode 100644 tests/expected/safety-constraint-attribute/check-invariant/expected create mode 100644 tests/expected/safety-constraint-attribute/grade-example/expected create mode 100644 tests/expected/safety-constraint-attribute/grade-example/grade-example.rs create mode 100644 tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs create mode 100644 tests/ui/safety-constraint-attribute/double-attribute/expected create mode 100644 tests/ui/safety-constraint-attribute/invalid-pred-error/expected create mode 100644 tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs create mode 100644 tests/ui/safety-constraint-attribute/mixed-attributes/expected create mode 100644 tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs create mode 100644 tests/ui/safety-constraint-attribute/no-struct-error/expected create mode 100644 tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index a7aaa8ae334e..cc936560e510 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -19,20 +19,20 @@ use syn::{ }; pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream { + let trait_name = "Arbitrary"; let derive_item = parse_macro_input!(item as DeriveInput); let item_name = &derive_item.ident; + let body = fn_any_body(&item_name, &derive_item.data); + // Get the safety constraints (if any) to produce type-safe values + let safety_conds_opt = safety_conds_opt(&item_name, &derive_item, trait_name); + // Add a bound `T: Arbitrary` to every type parameter T. 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(); - let body = fn_any_body(&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(safety_cond) = safety_conds_opt { + let expanded = if let Some(safety_conds) = 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(#safety_cond); + kani::assume(#safety_conds); obj } } @@ -94,48 +94,6 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// 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 -/// ``` -/// #[derive(Arbitrary)] -/// #[derive(Invariant)] -/// struct PositivePoint { -/// #[safety_constraint(*x >= 0)] -/// x: i32, -/// #[safety_constraint(*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 safety_conds(ident: &Ident, data: &Data) -> Option { - match data { - 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 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_safety_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. /// @@ -191,6 +149,55 @@ fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream { } } +fn safe_body_default(ident: &Ident, data: &Data) -> TokenStream { + match data { + Data::Struct(struct_data) => safe_body_default_inner(ident, &struct_data.fields), + Data::Enum(_) => unreachable!(), + Data::Union(_) => unreachable!(), + } +} + +fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream { + match fields { + Fields::Named(ref fields) => { + let field_safe_calls: Vec = fields + .named + .iter() + .map(|field| { + let name = &field.ident; + quote_spanned! {field.span()=> + #name.is_safe() + } + }) + .collect(); + if !field_safe_calls.is_empty() { + quote! { #( #field_safe_calls )&&* } + } else { + quote! { true } + } + } + Fields::Unnamed(ref fields) => { + let field_safe_calls: Vec = fields + .unnamed + .iter() + .enumerate() + .map(|(idx, field)| { + let field_idx = Index::from(idx); + quote_spanned! {field.span()=> + #field_idx.is_safe() + } + }) + .collect(); + if !field_safe_calls.is_empty() { + quote! { #( #field_safe_calls )&&* } + } else { + quote! { true } + } + } + Fields::Unit => quote! { true }, + } +} + /// 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(), ..)` @@ -267,6 +274,38 @@ fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { } } +fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option { + let name = ident; + let mut safety_attr = None; + + // Keep the attribute if we find it + for attr in &derive_input.attrs { + if attr.path().is_ident("safety_constraint") { + safety_attr = Some(attr); + } + } + + // Parse the arguments in the `#[safety_constraint(...)]` attribute + if let Some(attr) = safety_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() => + "safety constraint in `{}` could not be parsed: {}", name.to_string(), err + ) + } + + // Return the expression associated to the safety constraint + let safety_expr = expr_args.unwrap(); + Some(quote_spanned! {derive_input.span()=> + #safety_expr + }) + } else { + 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: @@ -318,33 +357,112 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream { } } +fn safe_body_with_calls( + item_name: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> TokenStream { + let safety_conds_opt = safety_conds_opt(&item_name, &derive_input, trait_name); + let safe_body_default = safe_body_default(&item_name, &derive_input.data); + + if let Some(safety_conds) = safety_conds_opt { + quote! { #safe_body_default && #safety_conds } + } else { + safe_body_default + } +} + pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::TokenStream { + let trait_name = "Invariant"; let derive_item = parse_macro_input!(item as DeriveInput); let item_name = &derive_item.ident; + let safe_body = safe_body_with_calls(&item_name, &derive_item, trait_name); + let field_refs = field_refs(&item_name, &derive_item.data); + // 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 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 + #safe_body } } }; proc_macro::TokenStream::from(expanded) } +/// Looks for `#[safety_constraint(...)]` attributes used in the struct or its +/// fields, and returns the constraints if there were any, otherwise returns +/// `None`. +/// Note: Errors out if the attribute is used in both the struct and its fields. +fn safety_conds_opt( + item_name: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> Option { + let has_item_safety_constraint = + has_item_safety_constraint(&item_name, &derive_input, trait_name); + + let has_field_safety_constraints = has_field_safety_constraints(&item_name, &derive_input.data); + + if has_item_safety_constraint && has_field_safety_constraints { + abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, item_name; + note = item_name.span() => + "`#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously" + ) + } + + if has_item_safety_constraint { + Some(safe_body_from_struct_attr(&item_name, &derive_input, trait_name)) + } else if has_field_safety_constraints { + Some(safe_body_from_fields_attr(&item_name, &derive_input.data, trait_name)) + } else { + None + } +} + +fn has_item_safety_constraint(ident: &Ident, derive_input: &DeriveInput, trait_name: &str) -> bool { + let safety_constraints_in_item = + derive_input.attrs.iter().filter(|attr| attr.path().is_ident("safety_constraint")).count(); + if safety_constraints_in_item > 1 { + abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident; + note = ident.span() => + "`#[safety_constraint(...)]` cannot be used more than once." + ) + } + safety_constraints_in_item == 1 +} + +fn has_field_safety_constraints(ident: &Ident, data: &Data) -> bool { + match data { + Data::Struct(struct_data) => has_field_safety_constraints_inner(ident, &struct_data.fields), + Data::Enum(_) => false, + Data::Union(_) => false, + } +} + +/// Checks if the `#[safety_constraint(...)]` attribute is attached to any +/// field. +fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool { + match fields { + Fields::Named(ref fields) => fields + .named + .iter() + .any(|field| field.attrs.iter().any(|attr| attr.path().is_ident("safety_constraint"))), + Fields::Unnamed(_) => false, + Fields::Unit => false, + } +} + /// Add a bound `T: Invariant` to every type parameter T. -fn add_trait_bound_invariant(mut generics: Generics) -> Generics { +pub 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)); @@ -353,17 +471,51 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics { generics } -fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { +fn safe_body_from_struct_attr( + ident: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> TokenStream { + if !matches!(derive_input.data, Data::Struct(_)) { + abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident; + note = ident.span() => + "`#[safety_constraint(...)]` can only be used in structs" + ) + }; + parse_safety_expr_input(ident, derive_input).unwrap() +} + +/// 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 +/// ``` +/// #[derive(Arbitrary)] +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` +/// this function will generate the `TokenStream` +/// ``` +/// *x >= 0 && *y >= 0 +/// ``` +/// which can be used by the `Arbitrary` and `Invariant` to generate and check +/// type-safe values for the struct, respectively. +fn safe_body_from_fields_attr(ident: &Ident, data: &Data, trait_name: &str) -> TokenStream { match data { - Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields), + Data::Struct(struct_data) => safe_body_from_fields_attr_inner(ident, &struct_data.fields), Data::Enum(_) => { - abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident; + abort!(Span::call_site(), "Cannot derive `{}` for `{}` enum", trait_name, 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; + abort!(Span::call_site(), "Cannot derive `{}` for `{}` union", trait_name, ident; note = ident.span() => "`#[derive(Invariant)]` cannot be used for unions such as `{}`", ident ) @@ -371,50 +523,23 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// 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 { +/// Generates an expression resulting from the conjunction of conditions +/// specified as safety constraints for each field. +/// See `safe_body_from_fields_attr` for more details. +fn safe_body_from_fields_attr_inner(ident: &Ident, fields: &Fields) -> TokenStream { match fields { // Expands to the expression - // `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 - // - // Therefore, if `#[safety_constraint()]` isn't specified for any field, this expands to - // `true && self.field1.is_safe() && self.field2.is_safe() && ..` + // ` && && ..` + // where `` is the safety condition specified for the N-th field. Fields::Named(ref fields) => { - let safety_conds: Vec = fields - .named - .iter() - .map(|field| { - let name = &field.ident; - let default_expr = quote_spanned! {field.span()=> - #name.is_safe() - }; - parse_safety_expr(ident, field) - .map(|expr| quote! { #expr && #default_expr}) - .unwrap_or(default_expr) - }) - .collect(); - // An initial value is required for empty structs - safety_conds.iter().fold(quote! { true }, |acc, cond| { - quote! { #acc && #cond } - }) + let safety_conds: Vec = + fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect(); + quote! { #(#safety_conds)&&* } } - 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 } - }) + Fields::Unnamed(_) => { + quote! { + true + } } // Expands to the expression // `true` diff --git a/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs b/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs new file mode 100644 index 000000000000..6e29938d4d5a --- /dev/null +++ b/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +//! In this case, we test the attribute on a struct with a generic type `T` +//! which requires the bound `From` because of the comparisons in the +//! `#[safety_constraint(...)]` predicate. The struct represents an abstract +//! value for which we only track its sign. The actual value is kept private. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint((*positive && *conc_value >= 0.into()) || (!*positive && *conc_value < 0.into()))] +struct AbstractValue +where + T: PartialOrd + From, +{ + pub positive: bool, + conc_value: T, +} + +#[kani::proof] +fn check_abstract_value() { + let value: AbstractValue = kani::any(); + assert!(value.is_safe()); +} diff --git a/tests/expected/safety-constraint-attribute/abstract-value/expected b/tests/expected/safety-constraint-attribute/abstract-value/expected new file mode 100644 index 000000000000..2fc76378041d --- /dev/null +++ b/tests/expected/safety-constraint-attribute/abstract-value/expected @@ -0,0 +1,7 @@ +Check 1: check_abstract_value.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: value.is_safe()" + +VERIFICATION:- SUCCESSFUL + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs b/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs new file mode 100644 index 000000000000..6e2b3ab97812 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint(*x >= 0 && *y >= 0)] +struct Point { + x: i32, + y: i32, +} + +#[kani::proof] +fn check_arbitrary() { + let point: Point = kani::any(); + assert!(point.x >= 0); + assert!(point.y >= 0); + assert!(point.is_safe()); +} diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/expected b/tests/expected/safety-constraint-attribute/check-arbitrary/expected new file mode 100644 index 000000000000..ee1e13bb726d --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-arbitrary/expected @@ -0,0 +1,11 @@ +Check 1: check_arbitrary.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: point.x >= 0" + +Check 2: check_arbitrary.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: point.y >= 0" + +Check 3: check_arbitrary.assertion.3\ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" diff --git a/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs b/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs new file mode 100644 index 000000000000..fce7319779f0 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint(*x == *y)] +struct SameCoordsPoint { + x: i32, + y: i32, +} + +#[kani::proof] +fn check_invariant() { + let point: SameCoordsPoint = kani::any(); + assert!(point.is_safe()); + + // Assuming `point.x != point.y` here should be like assuming `false`. + // The assertion should be unreachable because we're blocking the path. + kani::assume(point.x != point.y); + assert!(false, "this assertion should be unreachable"); +} diff --git a/tests/expected/safety-constraint-attribute/check-invariant/expected b/tests/expected/safety-constraint-attribute/check-invariant/expected new file mode 100644 index 000000000000..a4605f03b7b4 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/check-invariant/expected @@ -0,0 +1,7 @@ +Check 1: check_invariant.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: point.is_safe()" + +Check 2: check_invariant.assertion.2\ + - Status: UNREACHABLE\ + - Description: ""this assertion should be unreachable"" diff --git a/tests/expected/safety-constraint-attribute/grade-example/expected b/tests/expected/safety-constraint-attribute/grade-example/expected new file mode 100644 index 000000000000..fd95a713d65a --- /dev/null +++ b/tests/expected/safety-constraint-attribute/grade-example/expected @@ -0,0 +1,11 @@ +Grade::check_percentage_safety.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: self.percentage <= 100" + +check_grade_safe.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: grade.is_safe()" + +VERIFICATION:- SUCCESSFUL + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs b/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs new file mode 100644 index 000000000000..7998ab27df49 --- /dev/null +++ b/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs @@ -0,0 +1,43 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute works as expected when +//! deriving `Arbitrary` and `Invariant` implementations. + +//! In this case, we test the attribute on a struct that represents a hybrid +//! grade (letter-numerical) which should keep the following equivalences: +//! - A for 90-100% +//! - B for 80-89% +//! - C for 70-79% +//! - D for 60-69% +//! - F for 0-59% +//! +//! In addition, we explicitly test that `percentage` is 0-100% + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint((*letter == 'A' && *percentage >= 90 && *percentage <= 100) || + (*letter == 'B' && *percentage >= 80 && *percentage < 90) || + (*letter == 'C' && *percentage >= 70 && *percentage < 80) || + (*letter == 'D' && *percentage >= 60 && *percentage < 70) || + (*letter == 'F' && *percentage < 60))] +struct Grade { + letter: char, + percentage: u32, +} + +impl Grade { + pub fn check_percentage_safety(&self) { + assert!(self.percentage <= 100); + } +} + +#[kani::proof] +fn check_grade_safe() { + let grade: Grade = kani::any(); + assert!(grade.is_safe()); + grade.check_percentage_safety(); +} diff --git a/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs new file mode 100644 index 000000000000..ef7be7fe0e03 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that there is a compilation error when the `#[safety_constraint(...)]` +//! attribute is used more than once on the same struct. + +extern crate kani; +use kani::Invariant; + +#[derive(Invariant)] +#[safety_constraint(*x >= 0)] +#[safety_constraint(*y >= 0)] +struct Point { + x: i32, + y: i32, +} diff --git a/tests/ui/safety-constraint-attribute/double-attribute/expected b/tests/ui/safety-constraint-attribute/double-attribute/expected new file mode 100644 index 000000000000..899b85e20e9a --- /dev/null +++ b/tests/ui/safety-constraint-attribute/double-attribute/expected @@ -0,0 +1,6 @@ +error: Cannot derive `Invariant` for `Point` + | +| #[derive(Invariant)] + | ^^^^^^^^^ + | +note: `#[safety_constraint(...)]` cannot be used more than once. diff --git a/tests/ui/safety-constraint-attribute/invalid-pred-error/expected b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected new file mode 100644 index 000000000000..e15e3ff7cf7d --- /dev/null +++ b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected @@ -0,0 +1,19 @@ +error[E0308]: mismatched types + | +| #[safety_constraint(x >= 0 && y >= 0)] + | ^ expected `&i32`, found integer + | +help: consider dereferencing the borrow + | +| #[safety_constraint(*x >= 0 && y >= 0)] + | + + +error[E0308]: mismatched types + | +| #[safety_constraint(x >= 0 && y >= 0)] + | ^ expected `&i32`, found integer + | +help: consider dereferencing the borrow + | +| #[safety_constraint(x >= 0 && *y >= 0)] + | diff --git a/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs new file mode 100644 index 000000000000..89c862bb50c3 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that there is a compilation error when the predicate passed to the +//! `#[safety_constraint(...)]` attribute would result in a compiler error. +//! +//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error, +//! otherwise the `#[safety_constraint(...)]` attribute is ignored. + +extern crate kani; + +// Note: The struct fields `x` and `y` are references in this context, we should +// refer to `*x` and `*y` instead. +#[derive(kani::Invariant)] +#[safety_constraint(x >= 0 && y >= 0)] +struct Point { + x: i32, + y: i32, +} diff --git a/tests/ui/safety-constraint-attribute/mixed-attributes/expected b/tests/ui/safety-constraint-attribute/mixed-attributes/expected new file mode 100644 index 000000000000..bca53d41bf13 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/mixed-attributes/expected @@ -0,0 +1,6 @@ +error: Cannot derive `Invariant` for `Point` + | +| #[derive(Invariant)] + | ^^^^^^^^^ + | +note: `#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously diff --git a/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs b/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs new file mode 100644 index 000000000000..931cebd4839d --- /dev/null +++ b/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that there is a compilation error when the `#[safety_constraint(...)]` +//! attribute for struct and the `#[safety_constraint(...)]` attribute for +//! fields is used at the same time. + +extern crate kani; +use kani::Invariant; + +#[derive(Invariant)] +#[safety_constraint(*x >= 0)] +struct Point { + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/expected b/tests/ui/safety-constraint-attribute/no-struct-error/expected new file mode 100644 index 000000000000..df6bd82f00d6 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/no-struct-error/expected @@ -0,0 +1,6 @@ +error: Cannot derive `Invariant` for `MyEnum` + | +| #[derive(kani::Invariant)] + | ^^^^^^^^^^^^^^^ + | +note: `#[safety_constraint(...)]` can only be used in structs diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs new file mode 100644 index 000000000000..092bbe1319c7 --- /dev/null +++ b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani raises an error when a derive macro with the +//! `#[safety_constraint(...)]` attribute is is used in items which are not a +//! struct. +//! +//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error, +//! otherwise the `#[safety_constraint(...)]` attribute is ignored. + +extern crate kani; + +#[derive(kani::Invariant)] +#[safety_constraint(true)] +enum MyEnum { + A, + B(i32), +}