Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add experimental API to generate arbitrary pointers #3538

Merged
merged 12 commits into from
Oct 5, 2024
19 changes: 19 additions & 0 deletions library/kani_core/src/arbitrary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,16 @@
//! by an unconstrained symbolic value of their size (e.g., `u8`, `u16`, `u32`, etc.).
//!
//! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.

mod pointer;

#[macro_export]
#[allow(clippy::crate_in_macro_def)]
macro_rules! generate_arbitrary {
($core:path) => {
use core_path::marker::{PhantomData, PhantomPinned};
use core_path::mem::MaybeUninit;
use core_path::ptr::{self, addr_of_mut};
use $core as core_path;

pub trait Arbitrary
Expand Down Expand Up @@ -157,6 +162,15 @@ macro_rules! generate_arbitrary {
}
}

impl<T> Arbitrary for MaybeUninit<T>
where
T: Arbitrary,
{
fn any() -> Self {
if crate::kani::any() { MaybeUninit::new(T::any()) } else { MaybeUninit::uninit() }
}
}

arbitrary_tuple!(A);
arbitrary_tuple!(A, B);
arbitrary_tuple!(A, B, C);
Expand All @@ -169,6 +183,11 @@ macro_rules! generate_arbitrary {
arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J);
arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K);
arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L);

pub use self::arbitrary_ptr::*;
mod arbitrary_ptr {
kani_core::ptr_generator!();
}
};
}

Expand Down
371 changes: 371 additions & 0 deletions library/kani_core/src/arbitrary/pointer.rs

Large diffs are not rendered by default.

51 changes: 42 additions & 9 deletions library/kani_macros/src/derive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,37 @@ use syn::{
parse_quote,
};

#[cfg(feature = "no_core")]
macro_rules! kani_path {
($span:expr) => {
quote_spanned! { $span => core::kani }
};
() => {
quote! { core::kani }
};
}

#[cfg(not(feature = "no_core"))]
macro_rules! kani_path {
($span:expr) => {
quote_spanned! { $span => kani }
};
() => {
quote! { kani }
};
}

/// Generate the Arbitrary implementation for the given type.
///
/// Note that we cannot use `proc_macro_crate::crate_name()` to discover the name for `kani` crate
/// since we define it as an extern crate via `rustc` command line.
///
/// In order to support core, we check the `no_core` feature.
pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream {
let trait_name = "Arbitrary";
let derive_item = parse_macro_input!(item as DeriveInput);
let item_name = &derive_item.ident;
let kani_path = kani_path!();

let body = fn_any_body(&item_name, &derive_item.data);
// Get the safety constraints (if any) to produce type-safe values
Expand All @@ -36,19 +63,19 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
let field_refs = field_refs(&item_name, &derive_item.data);
quote! {
// The generated implementation.
impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
impl #impl_generics #kani_path::Arbitrary for #item_name #ty_generics #where_clause {
fn any() -> Self {
let obj = #body;
#field_refs
kani::assume(#safety_conds);
#kani_path::assume(#safety_conds);
obj
}
}
}
} else {
quote! {
// The generated implementation.
impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
impl #impl_generics #kani_path::Arbitrary for #item_name #ty_generics #where_clause {
fn any() -> Self {
#body
}
Expand All @@ -60,9 +87,10 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok

/// Add a bound `T: Arbitrary` to every type parameter T.
fn add_trait_bound_arbitrary(mut generics: Generics) -> Generics {
let kani_path = kani_path!();
generics.params.iter_mut().for_each(|param| {
if let GenericParam::Type(type_param) = param {
type_param.bounds.push(parse_quote!(kani::Arbitrary));
type_param.bounds.push(parse_quote!(#kani_path::Arbitrary));
}
});
generics
Expand Down Expand Up @@ -222,8 +250,10 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
// Expands to an expression like
// Self(kani::any(), kani::any(), ..., kani::any());
let init = fields.unnamed.iter().map(|field| {
quote_spanned! {field.span()=>
kani::any()
let span = field.span();
let kani_path = kani_path!(span);
quote_spanned! {span=>
#kani_path::any()
}
});
quote! {
Expand Down Expand Up @@ -349,8 +379,9 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream {
}
});

let kani_path = kani_path!();
quote! {
match kani::any() {
match #kani_path::any() {
#(#arms)*
}
}
Expand All @@ -376,6 +407,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok
let trait_name = "Invariant";
let derive_item = parse_macro_input!(item as DeriveInput);
let item_name = &derive_item.ident;
let kani_path = kani_path!();

let safe_body = safe_body_with_calls(&item_name, &derive_item, trait_name);
let field_refs = field_refs(&item_name, &derive_item.data);
Expand All @@ -387,7 +419,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok

let expanded = quote! {
// The generated implementation.
impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause {
impl #impl_generics #kani_path::Invariant for #item_name #ty_generics #where_clause {
fn is_safe(&self) -> bool {
let obj = self;
#field_refs
Expand Down Expand Up @@ -463,9 +495,10 @@ fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool {

/// Add a bound `T: Invariant` to every type parameter T.
pub fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
let kani_path = kani_path!();
generics.params.iter_mut().for_each(|param| {
if let GenericParam::Type(type_param) = param {
type_param.bounds.push(parse_quote!(kani::Invariant));
type_param.bounds.push(parse_quote!(#kani_path::Invariant));
}
});
generics
Expand Down
21 changes: 21 additions & 0 deletions tests/expected/arbitrary/ptrs/pointer_generator.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
Checking harness check_arbitrary_ptr...

Status: SUCCESS\
Description: ""OutOfBounds""

Status: SUCCESS\
Description: ""InBounds""

Status: SUCCESS\
Description: ""NullPtr""

Status: FAILURE\
Description: ""DeadObject""

Status: SATISFIED\
Description: "Dangling"

Status: UNREACHABLE\
celinval marked this conversation as resolved.
Show resolved Hide resolved
Description: ""Dangling write""

Verification failed for - check_arbitrary_ptr
38 changes: 38 additions & 0 deletions tests/expected/arbitrary/ptrs/pointer_generator.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// kani-flags: -Z mem-predicates
//! Check the behavior of the new `PointerGenerator`.
extern crate kani;

use kani::{AllocationStatus, PointerGenerator, cover};

/// Harness that checks that all cases are covered and the code behaves as expected.
///
/// Note that for `DeadObject`, `Dangling`, and `OutOfBounds` the predicate will fail due to demonic non-determinism.
#[kani::proof]
fn check_arbitrary_ptr() {
let mut generator = PointerGenerator::<10>::new();
let arbitrary = generator.any_alloc_status::<char>();
let ptr = arbitrary.ptr;
match arbitrary.status {
AllocationStatus::Dangling => {
cover!(true, "Dangling");
assert!(!kani::mem::can_write_unaligned(ptr), "Dangling write");
}
AllocationStatus::Null => {
assert!(!kani::mem::can_write_unaligned(ptr), "NullPtr");
}
AllocationStatus::DeadObject => {
// Due to demonic non-determinism, the API will trigger an error.
assert!(!kani::mem::can_write_unaligned(ptr), "DeadObject");
}
AllocationStatus::OutOfBounds => {
assert!(!kani::mem::can_write_unaligned(ptr), "OutOfBounds");
}
AllocationStatus::InBounds => {
// This should always succeed
assert!(kani::mem::can_write_unaligned(ptr), "InBounds");
}
};
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\

the evaluated program panicked at 'PointerGenerator requires at least one byte.'

note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\
pointer_generator_error.rs\
|\
| let _generator = PointerGenerator::<0>::new();\
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12 changes: 12 additions & 0 deletions tests/expected/arbitrary/ptrs/pointer_generator_error.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// kani-flags: -Z mem-predicates
//! Check misusage of pointer generator fails compilation.
extern crate kani;

use kani::PointerGenerator;

pub fn check_invalid_generator() {
let _generator = PointerGenerator::<0>::new();
}
39 changes: 39 additions & 0 deletions tests/expected/arbitrary/ptrs/pointer_inbounds.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
Checking harness check_overlap...

Status: SATISFIED\
Description: "Same"

Status: SATISFIED\
Description: "Overlap"

Status: SATISFIED\
Description: "Greater"

Status: SATISFIED\
Description: "Smaller"

Checking harness check_alignment...

Status: SUCCESS\
Description: ""Aligned""

Status: SUCCESS\
Description: ""Unaligned""

Checking harness check_inbounds_initialized...

Status: SUCCESS\
Description: ""ValidRead""

Checking harness check_inbounds...

Status: SATISFIED\
Description: "Uninitialized"

Status: SATISFIED\
Description: "Initialized"

Status: SUCCESS\
Description: ""ValidWrite""

Complete - 4 successfully verified harnesses, 0 failures, 4 total.
56 changes: 56 additions & 0 deletions tests/expected/arbitrary/ptrs/pointer_inbounds.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// kani-flags: -Z mem-predicates
//! Check different cases for `PointerGenerator` for in-bounds pointers.
//! TODO: Enable initialization checks (`-Z uninit-checks`) once we add support to unions.
//! The current instrumentation does not work in the presence of MaybeUninit which we use
//! to implement PointerGenerator.
//! Kani will detect the usage of MaybeUninit and fail the verification.
extern crate kani;

use kani::PointerGenerator;

#[kani::proof]
fn check_inbounds() {
let mut generator = kani::pointer_generator::<char, 3>();
let ptr = generator.any_in_bounds::<char>().ptr;
kani::cover!(!kani::mem::can_read_unaligned(ptr), "Uninitialized");
kani::cover!(kani::mem::can_read_unaligned(ptr), "Initialized");
assert!(kani::mem::can_write_unaligned(ptr), "ValidWrite");
}

#[kani::proof]
fn check_inbounds_initialized() {
let mut generator = kani::pointer_generator::<char, 3>();
let arbitrary = generator.any_in_bounds::<char>();
kani::assume(arbitrary.is_initialized);
assert!(kani::mem::can_read_unaligned(arbitrary.ptr), "ValidRead");
}

#[kani::proof]
fn check_alignment() {
let mut generator = kani::pointer_generator::<char, 2>();
let ptr: *mut char = generator.any_in_bounds().ptr;
if ptr.is_aligned() {
assert!(kani::mem::can_write(ptr), "Aligned");
} else {
assert!(!kani::mem::can_write(ptr), "Not aligned");
assert!(kani::mem::can_write_unaligned(ptr), "Unaligned");
}
}

#[kani::proof]
fn check_overlap() {
let mut generator = kani::pointer_generator::<u16, 5>();
let ptr_1 = generator.any_in_bounds::<u16>().ptr;
let ptr_2 = generator.any_in_bounds::<u16>().ptr;
kani::cover!(ptr_1 == ptr_2, "Same");
kani::cover!(ptr_1 == unsafe { ptr_2.byte_add(1) }, "Overlap");

let distance = unsafe { ptr_1.offset_from(ptr_2) };
kani::cover!(distance > 0, "Greater");
kani::cover!(distance < 0, "Smaller");

assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements");
}
11 changes: 11 additions & 0 deletions tests/script-based-pre/verify_std_cmd/verify_core.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,4 +76,15 @@ pub mod verify {
unsafe fn add_one(inout: *mut [u32]) {
inout.as_mut_unchecked().iter_mut().for_each(|e| *e += 1)
}

/// Test that arbitrary pointer works as expected.
/// Disable it for uninit checks, since these checks do not support `MaybeUninit` which is used
/// by the pointer generator.
#[kani::proof]
#[cfg(not(uninit_checks))]
fn check_any_ptr() {
let mut generator = kani::PointerGenerator::<8>::new();
let ptr = generator.any_in_bounds::<i32>().ptr;
assert!(kani::mem::can_write_unaligned(ptr));
}
}
5 changes: 4 additions & 1 deletion tests/script-based-pre/verify_std_cmd/verify_std.expected
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,13 @@ VERIFICATION:- SUCCESSFUL
Checking harness verify::check_swap_tuple...
VERIFICATION:- SUCCESSFUL

Checking harness verify::check_any_ptr...
VERIFICATION:- SUCCESSFUL

Checking harness num::verify::check_non_zero...
VERIFICATION:- SUCCESSFUL

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
Complete - 7 successfully verified harnesses, 0 failures, 7 total.

[TEST] Run kani verify-std -Z uninit-checks

Expand Down
Loading
Loading