From 4bb9295b5c6a4f0ef0b1ae557674b13ff0f6912a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 20 Apr 2023 11:37:21 +0000
Subject: [PATCH 1/2] 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.
---
 library/kani/src/arbitrary.rs | 20 +++++++++++++-------
 library/kani/src/slice.rs     | 19 +++++++++++--------
 library/kani/src/vec.rs       |  7 ++++---
 3 files changed, 28 insertions(+), 18 deletions(-)

diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index 2e13f90e3aef..fcd154de35ee 100644
--- a/library/kani/src/arbitrary.rs
+++ b/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) }
+                }
             }
         }
     };
diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
index f06118a4b2f5..0ff44eecdb5e 100644
--- a/library/kani/src/slice.rs
+++ b/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,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
@@ -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 }
+        }
     }
 
     pub fn get_slice(&self) -> &[T] {
diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs
index 5deb90d0ec14..331851ea2656 100644
--- a/library/kani/src/vec.rs
+++ b/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
 }

From 360e4067345b41f072e413cf25e4f9e74dae2225 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Thu, 27 Apr 2023 10:10:33 +0200
Subject: [PATCH 2/2] Fix slice length setting in case of null pointer

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
---
 library/kani/src/slice.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
index 0ff44eecdb5e..2b7e6742d21f 100644
--- a/library/kani/src/slice.rs
+++ b/library/kani/src/slice.rs
@@ -85,7 +85,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
         } else {
             let layout = Layout::array::<T>(0).unwrap();
             let ptr: *const T = std::ptr::null();
-            Self { layout, ptr: ptr as *mut T, slice_len }
+            Self { layout, ptr: ptr as *mut T, slice_len: 0 }
         }
     }