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

tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute automatically generates
+//! the `Arbitrary` implementation, and also that the values it generates
+//! respect the type invariant.
+
+//! 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,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute automatically generates
+//! the `Arbitrary` implementation, and also that the values it generates
+//! respect the type invariant.
+
+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 automatically generates
+//! the `Arbitrary` and `Invariant` implementations for the annotated type.
+
+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 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 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,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute automatically generates
+//! the `Arbitrary` implementation, and also that the values it generates
+//! respect the type invariant.
+
+//! 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,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the predicate passed to
+//! `kani::invariant` attribute would result in a compiler error.
+
+extern crate kani;
+use kani::Invariant;
+
+// Note: The struct fields `x` and `y` are references in this context, we should
+// refer to `*x` and `*y` instead.
+#[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/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),
+}