Avoid global path conditions in Kani's library

There is no need to maintain global path conditions in order to
constrain non-deterministic data: we can locally pick an arbitrary one
of the permitted values. This avoids propagating guards on input data
across all properties subsequently seen in symbolic execution.

Author: tautschnig

library/kani/src/arbitrary.rs

@@ -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;
         byte == 1
     }
 }
@@ -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;
+        if val & 0xD800 != 0 {
+            // val > 0xD7FF && val < 0xE000
+            unsafe { char::from_u32_unchecked(0x10FFFF) }
+        } else {
+            unsafe { char::from_u32_unchecked(val) }
+        }
     }
 }
 
@@ -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 {
+                    unsafe { <$type>::new_unchecked(1) }
+                } else {
+                    unsafe { <$type>::new_unchecked(val) }
+                }
             }
         }
     };

library/kani/src/slice.rs

@@ -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};
 
@@ -30,9 +30,13 @@ 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 {
+        (0, 0)
+    } else if to < from {
+        (0, 0)
+    } else {
+        (from, to)
+    }
 }
 
 /// A struct that stores a slice of type `T` with a non-deterministic length
@@ -80,10 +84,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 }
+        }
     }
 
     pub fn get_slice(&self) -> &[T] {

library/kani/src/vec.rs

@@ -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>
@@ -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
 }