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.

Sign up for GitHub

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

Jump to bottom

Avoid global path conditions in Kani's library #2394

Draft
wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

Avoid global path conditions in Kani's library #2394

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4bb9295
Avoid global path conditions in Kani's library
tautschnig Apr 20, 2023
360e406
Fix slice length setting in case of null pointer
tautschnig Apr 27, 2023
aec5fb5
Merge branch 'main' into no-assume
tautschnig Apr 27, 2023
be11b58
Merge branch 'main' into no-assume
tautschnig Sep 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 13 additions & 7 deletions library/kani/src/arbitrary.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,8 +76,7 @@ trivial_arbitrary!(());
impl Arbitrary for bool {
#[inline(always)]
fn any() -> Self {
let byte = u8::any();
crate::assume(byte < 2);
let byte = u8::any() & 0x1;
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
byte == 1
}
}
Expand All @@ -88,9 +87,13 @@ 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) }
let val = u32::any() & 0x0FFFFF;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Doesn't this eliminate valid char values like 0x10FFFE?

Copy link
Contributor

@celinval celinval Apr 27, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You could add a harness that this logic covers all valid char values and that it doesn't produce any invalid ones. For example, I wrote a harness that uses the same logic here, but add two assertions (if I understood this correctly):

#[kani::proof]
fn any() -> char {
    // Generate an arbitrary u32 and constrain it to make it a valid representation of char.
    let val = kani::any::<u32>() & 0x0FFFFF;
    if val & 0xD800 != 0 {
        // val > 0xD7FF && val < 0xE000
        // This branch should only cover values that cannot be converted to UTF-8.
        assert!(char::from_u32(val).is_none());
        unsafe { char::from_u32_unchecked(0x10FFFF) }
    } else {
        // This branch should only convert valid values.
        assert!(char::from_u32(val).is_some());
        unsafe { char::from_u32_unchecked(val) }
    }
}

The assertion of the if branch fails. The CEX I got was for 69632.

Copy link
Contributor

@celinval celinval Apr 27, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The following harness uses cover to check if our logic covers all characters:

/// Same logic as `kani::any::<char>()` but that takes the u32 as input.
fn any_char(input: u32) -> char {
    let val = input & 0x0FFFFF;
    if val & 0xD800 != 0 {
        // val > 0xD7FF && val < 0xE000
        unsafe { char::from_u32_unchecked(0x10FFFF) }
    } else {
        unsafe { char::from_u32_unchecked(val) }
    }
}

/// Checks that we generate all possible valid characters.
#[kani::proof]
fn check_all_valid_char() {
    let input: u32 = kani::any();
    if let Some(valid) = char::from_u32(input) {
        if valid != any_char(input) {
            // If this is unreachable, we produce all valid characters.
            // If this is satisfiable, we may produce all valid characters.
            // If this is unsat, we do not produce value for all valid characters.
            kani::cover!(any_char(kani::any()) == valid)
        }
    }
}

This cover is unsatisfiable.

if val & 0xD800 != 0 {
// val > 0xD7FF && val < 0xE000
unsafe { char::from_u32_unchecked(0x10FFFF) }
} else {
unsafe { char::from_u32_unchecked(val) }
}
}
}

Expand All @@ -100,8 +103,11 @@ macro_rules! nonzero_arbitrary {
#[inline(always)]
fn any() -> Self {
let val = <$base>::any();
crate::assume(val != 0);
unsafe { <$type>::new_unchecked(val) }
if val == 0 {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it useful to eliminate branches like you did in the bool case? If so, we can use:

   let val = val | (((val == 0) as $base) & 0x1);

or something simpler (if possible). This sets the last bit only if the value is 0.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this will do it, right?

   let val = val | (val == 0) as $base;

unsafe { <$type>::new_unchecked(1) }
} else {
unsafe { <$type>::new_unchecked(val) }
}
}
}
};
Expand Down
19 changes: 11 additions & 8 deletions library/kani/src/slice.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
use crate::{any, assume, Arbitrary};
use crate::{any, Arbitrary};
use std::alloc::{alloc, dealloc, Layout};
use std::ops::{Deref, DerefMut};

Expand Down Expand Up @@ -30,9 +30,7 @@ pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) ->
fn any_range<const LENGTH: usize>() -> (usize, usize) {
let from: usize = any();
let to: usize = any();
assume(to <= LENGTH);
assume(from <= to);
(from, to)
if to > LENGTH || to < from { (0, 0) } else { (from, to) }
}

/// A struct that stores a slice of type `T` with a non-deterministic length
Expand Down Expand Up @@ -80,10 +78,15 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {

fn alloc_slice() -> Self {
let slice_len = any();
assume(slice_len <= MAX_SLICE_LENGTH);
let layout = Layout::array::<T>(slice_len).unwrap();
let ptr = if slice_len == 0 { std::ptr::null() } else { unsafe { alloc(layout) } };
Self { layout, ptr: ptr as *mut T, slice_len }
if slice_len <= MAX_SLICE_LENGTH {
let layout = Layout::array::<T>(slice_len).unwrap();
let ptr = if slice_len == 0 { std::ptr::null() } else { unsafe { alloc(layout) } };
Self { layout, ptr: ptr as *mut T, slice_len }
} else {
let layout = Layout::array::<T>(0).unwrap();
let ptr: *const T = std::ptr::null();
Self { layout, ptr: ptr as *mut T, slice_len }
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
}
}

pub fn get_slice(&self) -> &[T] {
Expand Down
7 changes: 4 additions & 3 deletions library/kani/src/vec.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
use crate::{any, assume, Arbitrary};
use crate::{any, Arbitrary};

/// Generates an arbitrary vector whose length is at most MAX_LENGTH.
pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
Expand All @@ -10,8 +10,9 @@ where
{
let mut v = exact_vec::<T, MAX_LENGTH>();
let real_length: usize = any();
assume(real_length <= MAX_LENGTH);
unsafe { v.set_len(real_length) };
if real_length <= MAX_LENGTH {
unsafe { v.set_len(real_length) };
}

v
}
Expand Down