Define a struct-level #[safety_constraint(...)] attribute

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<i32>` 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<T>
+where
+ T: PartialOrd + From<i32>,
+{
+ pub positive: bool,
+ conc_value: T,
+}
+
+#[kani::proof]
+fn check_abstract_value() {
+ let value: AbstractValue<i32> = kani::any();
+ assert!(value.is_safe());
+}

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.

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());
+}

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()"

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");
+}

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""

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.

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();
+}

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,
+}

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.

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)]
+ |

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,
+}

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

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,
+}

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

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),
+}