Skip to content

Commit

Permalink
Add one macro to rule them all...
Browse files Browse the repository at this point in the history 
Also remove any_array() for the std version for now. Bumped into some
issues when trying to enable generic constant expression for `core`.
  • Loading branch information
@celinval
celinval committed Jun 4, 2024
1 parent e231f9d commit 32ef011
Show file tree
Hide file tree
Showing 4 changed files with 101 additions and 214 deletions.
148 changes: 1 addition & 147 deletions library/kani/src/arbitrary.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<const MAX_ARRAY_LENGTH: usize>() -> [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::<T>.
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::<Self, { std::mem::size_of::<Self>() }>() }
}
fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [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: <https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html>
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<T, const N: usize> Arbitrary for [T; N]
where
Expand All @@ -131,37 +16,6 @@ where
}
}

impl<T> Arbitrary for Option<T>
where
T: Arbitrary,
{
fn any() -> Self {
if bool::any() { Some(T::any()) } else { None }
}
}

impl<T, E> Arbitrary for Result<T, E>
where
T: Arbitrary,
E: Arbitrary,
{
fn any() -> Self {
if bool::any() { Ok(T::any()) } else { Err(E::any()) }
}
}

impl<T: ?Sized> Arbitrary for std::marker::PhantomData<T> {
fn any() -> Self {
PhantomData
}
}

impl Arbitrary for std::marker::PhantomPinned {
fn any() -> Self {
PhantomPinned
}
}

impl<T> Arbitrary for std::boxed::Box<T>
where
T: Arbitrary,
Expand Down
9 changes: 2 additions & 7 deletions library/kani/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -45,8 +43,8 @@ pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: 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`.
Expand Down Expand Up @@ -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;
132 changes: 73 additions & 59 deletions library/kani_core/src/arbitrary.rs
View file
Original file line number Diff line number Diff line change
@@ -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::<T>.
#[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::<Self, { mem_mod::size_of::<Self>() }>() }
}
// Disable this for standard library since we cannot enable generic constant expr.
#[cfg(kani_lib)]
fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [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<const MAX_ARRAY_LENGTH: usize>() -> [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::<T>.
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::<Self, { core_path::mem::size_of::<Self>() }>() }
}
// Disable this for standard library since we cannot enable generic constant expr.
#[cfg(kani_sysroot)]
fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [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);
Expand All @@ -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)]
Expand All @@ -104,17 +117,6 @@ macro_rules! generate_arbitrary {
}
}

#[cfg(kani_lib)]
impl<T, const N: usize> Arbitrary for [T; N]
where
T: Arbitrary,
[(); mem_mod::size_of::<[T; N]>()]:,
{
fn any() -> Self {
T::any_array()
}
}

impl<T> Arbitrary for Option<T>
where
T: Arbitrary,
Expand All @@ -133,5 +135,17 @@ macro_rules! generate_arbitrary {
if bool::any() { Ok(T::any()) } else { Err(E::any()) }
}
}

impl<T: ?Sized> Arbitrary for PhantomData<T> {
fn any() -> Self {
PhantomData
}
}

impl Arbitrary for PhantomPinned {
fn any() -> Self {
PhantomPinned
}
}
};
}
Loading

0 comments on commit 32ef011

Please sign in to comment.