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

Generate non-deterministic pointer variables #3696

Open
stogaru opened this issue Nov 8, 2024 · 0 comments
Open

Generate non-deterministic pointer variables #3696

stogaru opened this issue Nov 8, 2024 · 0 comments
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@stogaru
Copy link

stogaru commented Nov 8, 2024

Requested feature: API to generate pointers non-deterministically

Use case: Currently, to generate arbitrary pointers we are either using the PointerGenerator API or generating a non-deterministic variable and getting a reference to that. For example we are doing one of the following:

let mut generator = PointerGenerator::<4>::new();
let ptr1: *const u32 = generator.any_in_bounds::<u32>().ptr;

OR

let val: u32 = kani::any();
let ptr: *const u32 = &val;

But both of these do not cover the entire address space that a pointer can take. This is important for functions concerned with pointer arithmetic as they do not care about the values within. So, we can have something like:

let ptr: *const u32 = kani::any_alloc_status()

Right now, one way I can think of generating an allocated ptr that can cover the entire address space in the harness is by doing the following:

 let val: $type = kani::any::<$type>();

// pointer can be of any address
let ptr1 = kani::any::<usize>() as *mut $type;

// write_unaligned requires non-overlapping src and dest
// val's address should not overlap with the object ptr1 is pointing to 
kani::assume((ptr1 as usize) > (&val as *const $type as usize));
kani::assume((ptr1 as usize).checked_add(size_of::<$type>()).is_some());
kani::assume((ptr1 as usize + size_of::<$type>()) < (&val as *const $type as usize));

unsafe { ptr1.write_unaligned(val) }

@feliperodri

@stogaru stogaru added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

No branches or pull requests

1 participant