From 32ef0113dd1157aa3740832b86233cf0b30df767 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 3 Jun 2024 19:11:41 -0700 Subject: [PATCH] Add one macro to rule them all... Also remove any_array() for the std version for now. Bumped into some issues when trying to enable generic constant expression for `core`. --- library/kani/src/arbitrary.rs | 148 +---------------------------- library/kani/src/lib.rs | 9 +- library/kani_core/src/arbitrary.rs | 132 +++++++++++++------------ library/kani_core/src/lib.rs | 26 ++++- 4 files changed, 101 insertions(+), 214 deletions(-) diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 938f3c30968f8..5399ed4ebe5e1 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -4,122 +4,7 @@ //! This module introduces the Arbitrary trait as well as implementation for primitive types and //! other std containers. -use std::{ - marker::{PhantomData, PhantomPinned}, - num::*, -}; - -/// This trait should be used to generate symbolic variables that represent any valid value of -/// its type. -pub trait Arbitrary -where - Self: Sized, -{ - fn any() -> Self; - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - // the requirement defined in the where clause must appear on the `impl`'s method `any_array` - // but also on the corresponding trait's method - where - [(); std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:, - { - [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) - } -} - -/// The given type can be represented by an unconstrained symbolic value of size_of::. -macro_rules! trivial_arbitrary { - ( $type: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. - unsafe { crate::any_raw_internal::() }>() } - } - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - where - // `generic_const_exprs` requires all potential errors to be reflected in the signature/header. - // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail. - [(); { std::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:, - { - unsafe { - crate::any_raw_internal::< - [Self; MAX_ARRAY_LENGTH], - { std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() }, - >() - } - } - } - }; -} - -trivial_arbitrary!(u8); -trivial_arbitrary!(u16); -trivial_arbitrary!(u32); -trivial_arbitrary!(u64); -trivial_arbitrary!(u128); -trivial_arbitrary!(usize); - -trivial_arbitrary!(i8); -trivial_arbitrary!(i16); -trivial_arbitrary!(i32); -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 -// verification code if they want to eliminate NaN, infinite, or subnormal. -trivial_arbitrary!(f32); -trivial_arbitrary!(f64); - -trivial_arbitrary!(()); - -impl Arbitrary for bool { - #[inline(always)] - fn any() -> Self { - let byte = u8::any(); - crate::assume(byte < 2); - byte == 1 - } -} - -/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] -/// Ref: -impl Arbitrary for char { - #[inline(always)] - fn any() -> Self { - // Generate an arbitrary u32 and constrain it to make it a valid representation of char. - let val = u32::any(); - crate::assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)); - unsafe { char::from_u32_unchecked(val) } - } -} - -macro_rules! nonzero_arbitrary { - ( $type: ty, $base: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - let val = <$base>::any(); - crate::assume(val != 0); - unsafe { <$type>::new_unchecked(val) } - } - } - }; -} - -nonzero_arbitrary!(NonZeroU8, u8); -nonzero_arbitrary!(NonZeroU16, u16); -nonzero_arbitrary!(NonZeroU32, u32); -nonzero_arbitrary!(NonZeroU64, u64); -nonzero_arbitrary!(NonZeroU128, u128); -nonzero_arbitrary!(NonZeroUsize, usize); - -nonzero_arbitrary!(NonZeroI8, i8); -nonzero_arbitrary!(NonZeroI16, i16); -nonzero_arbitrary!(NonZeroI32, i32); -nonzero_arbitrary!(NonZeroI64, i64); -nonzero_arbitrary!(NonZeroI128, i128); -nonzero_arbitrary!(NonZeroIsize, isize); +use crate::Arbitrary; impl Arbitrary for [T; N] where @@ -131,37 +16,6 @@ where } } -impl Arbitrary for Option -where - T: Arbitrary, -{ - fn any() -> Self { - if bool::any() { Some(T::any()) } else { None } - } -} - -impl Arbitrary for Result -where - T: Arbitrary, - E: Arbitrary, -{ - fn any() -> Self { - if bool::any() { Ok(T::any()) } else { Err(E::any()) } - } -} - -impl Arbitrary for std::marker::PhantomData { - fn any() -> Self { - PhantomData - } -} - -impl Arbitrary for std::marker::PhantomPinned { - fn any() -> Self { - PhantomPinned - } -} - impl Arbitrary for std::boxed::Box where T: Arbitrary, diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 39f91ff887927..0c9f508714218 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -33,10 +33,8 @@ pub mod internal; mod models; -pub use arbitrary::Arbitrary; #[cfg(feature = "concrete_playback")] pub use concrete_playback::concrete_playback_run; -use kani_core; #[cfg(not(feature = "concrete_playback"))] /// NOP `concrete_playback` for type checking during verification mode. @@ -45,8 +43,8 @@ pub fn concrete_playback_run(_: Vec>, _: F) { } pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; -// Declare core Kani intrinsics. -kani_core::kani_intrinsics!(); +// Declare common Kani features. +kani_core::kani_lib!(kani); /// `implies!(premise => conclusion)` means that if the `premise` is true, so /// must be the `conclusion`. @@ -116,7 +114,4 @@ macro_rules! cover { #[cfg(not(feature = "concrete_playback"))] pub use core::assert as __kani__workaround_core_assert; -// Kani proc macros must be in a separate crate -pub use kani_macros::*; - pub mod contracts; diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 051cb80001448..e13485f4102bb 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -1,71 +1,70 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -/// The given type can be represented by an unconstrained symbolic value of size_of::. -#[macro_export] -macro_rules! trivial_arbitrary { - ( $type: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. - unsafe { any_raw_internal::() }>() } - } - // Disable this for standard library since we cannot enable generic constant expr. - #[cfg(kani_lib)] - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - where - // `generic_const_exprs` requires all potential errors to be reflected in the signature/header. - // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail. - [(); { mem_mod::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:, - { - unsafe { - any_raw_internal::< - [Self; MAX_ARRAY_LENGTH], - { mem_mod::size_of::<[Self; MAX_ARRAY_LENGTH]>() }, - >() - } - } - } - }; -} - -#[macro_export] -macro_rules! nonzero_arbitrary { - ( $type: ty, $base: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - let val = <$base>::any(); - assume(val != 0); - unsafe { <$type>::new_unchecked(val) } - } - } - }; -} - - #[macro_export] macro_rules! generate_arbitrary { - ($mem_path:path) => { - use $mem_path as mem_mod; + ($core:path) => { + use core_path::marker::{PhantomData, PhantomPinned}; + use $core as core_path; pub trait Arbitrary where Self: Sized, { fn any() -> Self; - #[cfg(kani_lib)] + #[cfg(kani_sysroot)] fn any_array() -> [Self; MAX_ARRAY_LENGTH] // the requirement defined in the where clause must appear on the `impl`'s method `any_array` // but also on the corresponding trait's method where - [(); mem_mod::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:, + [(); core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:, { [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) } } + macro_rules! nonzero_arbitrary { + ( $type: ty, $base: ty ) => { + use core_path::num::*; + impl Arbitrary for $type { + #[inline(always)] + fn any() -> Self { + let val = <$base>::any(); + assume(val != 0); + unsafe { <$type>::new_unchecked(val) } + } + } + }; + } + + /// The given type can be represented by an unconstrained symbolic value of size_of::. + macro_rules! trivial_arbitrary { + ( $type: ty ) => { + impl Arbitrary for $type { + #[inline(always)] + fn any() -> Self { + // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. + unsafe { any_raw_internal::() }>() } + } + // Disable this for standard library since we cannot enable generic constant expr. + #[cfg(kani_sysroot)] + fn any_array() -> [Self; MAX_ARRAY_LENGTH] + where + // `generic_const_exprs` requires all potential errors to be reflected in the signature/header. + // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail. + [(); { core_path::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:, + { + unsafe { + any_raw_internal::< + [Self; MAX_ARRAY_LENGTH], + { core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() }, + >() + } + } + } + }; + } + // Generate trivial arbitrary values trivial_arbitrary!(u8); trivial_arbitrary!(u16); @@ -81,6 +80,20 @@ macro_rules! generate_arbitrary { trivial_arbitrary!(i128); trivial_arbitrary!(isize); + nonzero_arbitrary!(NonZeroU8, u8); + nonzero_arbitrary!(NonZeroU16, u16); + nonzero_arbitrary!(NonZeroU32, u32); + nonzero_arbitrary!(NonZeroU64, u64); + nonzero_arbitrary!(NonZeroU128, u128); + nonzero_arbitrary!(NonZeroUsize, usize); + + nonzero_arbitrary!(NonZeroI8, i8); + nonzero_arbitrary!(NonZeroI16, i16); + nonzero_arbitrary!(NonZeroI32, i32); + nonzero_arbitrary!(NonZeroI64, i64); + nonzero_arbitrary!(NonZeroI128, i128); + nonzero_arbitrary!(NonZeroIsize, isize); + // Implement arbitrary for non-trivial types impl Arbitrary for bool { #[inline(always)] @@ -104,17 +117,6 @@ macro_rules! generate_arbitrary { } } - #[cfg(kani_lib)] - impl Arbitrary for [T; N] - where - T: Arbitrary, - [(); mem_mod::size_of::<[T; N]>()]:, - { - fn any() -> Self { - T::any_array() - } - } - impl Arbitrary for Option where T: Arbitrary, @@ -133,5 +135,17 @@ macro_rules! generate_arbitrary { if bool::any() { Ok(T::any()) } else { Err(E::any()) } } } + + impl Arbitrary for PhantomData { + fn any() -> Self { + PhantomData + } + } + + impl Arbitrary for PhantomPinned { + fn any() -> Self { + PhantomPinned + } + } }; } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 56db537852f56..451cc27aeed8e 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -22,10 +22,34 @@ mod arbitrary; pub use kani_macros::*; +/// Users should only need to invoke this. +/// +/// Options are: +/// - `kani`: Add definitions needed for Kani library. +/// - `core`: Define a `kani` module inside `core` crate. +/// - `std`: TODO: Define a `kani` module inside `std` crate. Users must define kani inside core. +#[macro_export] +macro_rules! kani_lib { + (core) => { + #[cfg(kani)] + #[unstable(feature = "kani", issue = "none")] + pub mod kani { + pub use kani_core::{ensures, proof, proof_for_contract, requires, should_panic}; + kani_core::kani_intrinsics!(); + kani_core::generate_arbitrary!(core); + } + }; + + (kani) => { + pub use kani_core::*; + kani_core::kani_intrinsics!(); + kani_core::generate_arbitrary!(std); + }; +} + #[macro_export] macro_rules! kani_intrinsics { () => { - /// Creates an assumption that will be valid after this statement run. Note that the assumption /// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the /// program will exit successfully.