From a6332fc2ed04c5a72e4671835ef584c0b31c4f3b Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Thu, 6 Jun 2024 16:07:04 -0400 Subject: [PATCH] (Re)introduce `Invariant` trait (#3190) This PR reintroduces the `Invariant` trait as a mechanism for the specification of type safety invariants. The trait is defined in the Kani library where we also provide `Invariant` implementations for primitive types. In contrast to the previous `Invariant` trait, this version doesn't require the `Arbitrary` bound (i.e., it has the same requirements as `Arbitrary`). This way, the user isn't required to provide an `Arbitrary` implementation in addition to the `Invariant` one. Related #3095 --- library/kani/src/arbitrary.rs | 6 +- library/kani/src/invariant.rs | 102 ++++++++++++++++++++++++ library/kani/src/lib.rs | 2 + tests/kani/Invariant/invariant_impls.rs | 38 +++++++++ tests/kani/Invariant/percentage.rs | 62 ++++++++++++++ 5 files changed, 207 insertions(+), 3 deletions(-) create mode 100644 library/kani/src/invariant.rs create mode 100644 tests/kani/Invariant/invariant_impls.rs create mode 100644 tests/kani/Invariant/percentage.rs diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 938f3c30968f..3f1adc787b79 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module introduces the Arbitrary trait as well as implementation for primitive types and -//! other std containers. +//! This module introduces the `Arbitrary` trait as well as implementation for +//! primitive types and other std containers. use std::{ marker::{PhantomData, PhantomPinned}, @@ -66,7 +66,7 @@ trivial_arbitrary!(i64); trivial_arbitrary!(i128); trivial_arbitrary!(isize); -// We do not constraint floating points values per type spec. Users must add assumptions to their +// We do not constrain floating points values per type spec. Users must add assumptions to their // verification code if they want to eliminate NaN, infinite, or subnormal. trivial_arbitrary!(f32); trivial_arbitrary!(f64); diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs new file mode 100644 index 000000000000..f118f94e995c --- /dev/null +++ b/library/kani/src/invariant.rs @@ -0,0 +1,102 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module introduces the `Invariant` trait as well as its implementation +//! for primitive types. + +/// This trait should be used to specify and check type safety invariants for a +/// type. For type invariants, we refer to the definitions in the Rust's Unsafe +/// Code Guidelines Reference: +/// +/// +/// In summary, the reference distinguishes two kinds of type invariants: +/// - *Validity invariant*: An invariant that all data must uphold any time +/// it's accessed or copied in a typed manner. This invariant is exploited by +/// the compiler to perform optimizations. +/// - *Safety invariant*: An invariant that safe code may assume all data to +/// uphold. This invariant can be temporarily violated by unsafe code, but +/// must always be upheld when interfacing with unknown safe code. +/// +/// Therefore, validity invariants must be upheld at all times, while safety +/// invariants only need to be upheld at the boundaries to safe code. +/// +/// Safety invariants are particularly interesting for user-defined types, and +/// the `Invariant` trait allows you to check them with Kani. +/// +/// It can also be used in tests. It's a programmatic way to specify (in Rust) +/// properties over your data types. Since it's written in Rust, it can be used +/// for static and dynamic checking. +/// +/// For example, let's say you're creating a type that represents a date: +/// +/// ```rust +/// #[derive(kani::Arbitrary)] +/// pub struct MyDate { +/// day: u8, +/// month: u8, +/// year: i64, +/// } +/// ``` +/// You can specify its safety invariant as: +/// ```rust +/// impl kani::Invariant for MyDate { +/// fn is_safe(&self) -> bool { +/// self.month > 0 +/// && self.month <= 12 +/// && self.day > 0 +/// && self.day <= days_in_month(self.year, self.month) +/// } +/// } +/// ``` +/// And use it to check that your APIs are safe: +/// ```rust +/// #[kani::proof] +/// fn check_increase_date() { +/// let mut date: MyDate = kani::any(); +/// // Increase date by one day +/// increase_date(date, 1); +/// assert!(date.is_safe()); +/// } +/// ``` +pub trait Invariant +where + Self: Sized, +{ + fn is_safe(&self) -> bool; +} + +/// Any value is considered safe for the type +macro_rules! trivial_invariant { + ( $type: ty ) => { + impl Invariant for $type { + #[inline(always)] + fn is_safe(&self) -> bool { + true + } + } + }; +} + +trivial_invariant!(u8); +trivial_invariant!(u16); +trivial_invariant!(u32); +trivial_invariant!(u64); +trivial_invariant!(u128); +trivial_invariant!(usize); + +trivial_invariant!(i8); +trivial_invariant!(i16); +trivial_invariant!(i32); +trivial_invariant!(i64); +trivial_invariant!(i128); +trivial_invariant!(isize); + +// We do not constrain the safety invariant for floating points types. +// Users can create a new type wrapping the floating point type and define an +// invariant that checks for NaN, infinite, or subnormal values. +trivial_invariant!(f32); +trivial_invariant!(f64); + +trivial_invariant!(()); +trivial_invariant!(bool); +trivial_invariant!(char); diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 341dd6752916..e81ddbe7904b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -23,6 +23,7 @@ pub mod arbitrary; #[cfg(feature = "concrete_playback")] mod concrete_playback; pub mod futures; +pub mod invariant; pub mod mem; pub mod shadow; pub mod slice; @@ -37,6 +38,7 @@ mod models; pub use arbitrary::Arbitrary; #[cfg(feature = "concrete_playback")] pub use concrete_playback::concrete_playback_run; +pub use invariant::Invariant; #[cfg(not(feature = "concrete_playback"))] /// NOP `concrete_playback` for type checking during verification mode. diff --git a/tests/kani/Invariant/invariant_impls.rs b/tests/kani/Invariant/invariant_impls.rs new file mode 100644 index 000000000000..4f00f4134956 --- /dev/null +++ b/tests/kani/Invariant/invariant_impls.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the `Invariant` implementations that we include in the Kani library +//! with respect to the underlying type invariants. +extern crate kani; +use kani::Invariant; + +macro_rules! check_safe_type { + ( $type: ty ) => { + let value: $type = kani::any(); + assert!(value.is_safe()); + }; +} + +#[kani::proof] +fn check_safe_impls() { + check_safe_type!(u8); + check_safe_type!(u16); + check_safe_type!(u32); + check_safe_type!(u64); + check_safe_type!(u128); + check_safe_type!(usize); + + check_safe_type!(i8); + check_safe_type!(i16); + check_safe_type!(i32); + check_safe_type!(i64); + check_safe_type!(i128); + check_safe_type!(isize); + + check_safe_type!(f32); + check_safe_type!(f64); + + check_safe_type!(()); + check_safe_type!(bool); + check_safe_type!(char); +} diff --git a/tests/kani/Invariant/percentage.rs b/tests/kani/Invariant/percentage.rs new file mode 100644 index 000000000000..f3976f48e249 --- /dev/null +++ b/tests/kani/Invariant/percentage.rs @@ -0,0 +1,62 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `Invariant` implementation behaves as expected when used on a +//! custom type. + +extern crate kani; +use kani::Invariant; + +// We use the default `Arbitrary` implementation, which allows values that +// shouldn't be considered safe for the `Percentage` type. +#[derive(kani::Arbitrary)] +struct Percentage(u8); + +impl Percentage { + pub fn try_new(val: u8) -> Result { + if val <= 100 { + Ok(Self(val)) + } else { + Err(String::from("error: invalid percentage value")) + } + } + + pub fn value(&self) -> u8 { + self.0 + } + + pub fn increase(&self, other: u8) -> Percentage { + let amount = self.0 + other; + Percentage::try_new(amount.min(100)).unwrap() + } +} + +impl kani::Invariant for Percentage { + fn is_safe(&self) -> bool { + self.0 <= 100 + } +} + +#[kani::proof] +fn check_assume_safe() { + let percentage: Percentage = kani::any(); + kani::assume(percentage.is_safe()); + assert!(percentage.value() <= 100); +} + +#[kani::proof] +#[kani::should_panic] +fn check_assert_safe() { + let percentage: Percentage = kani::any(); + assert!(percentage.is_safe()); +} + +#[kani::proof] +fn check_increase_safe() { + let percentage: Percentage = kani::any(); + kani::assume(percentage.is_safe()); + let amount = kani::any(); + kani::assume(amount <= 100); + let new_percentage = percentage.increase(amount); + assert!(new_percentage.is_safe()); +}