kani: remove use of kani::vec::any_vec (#231)

camshaft · Jun 10, 2024 · ab92799 · ab92799
1 parent 004acbf
commit ab92799
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 13 deletions.
diff --git a/lib/bolero-kani/Cargo.toml b/lib/bolero-kani/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "bolero-kani"
-version = "0.11.1"
+version = "0.11.2"
 authors = ["Cameron Bytheway <[email protected]>"]
 description = "kani plugin for bolero"
 homepage = "https://github.com/camshaft/bolero"

diff --git a/lib/bolero-kani/src/lib.rs b/lib/bolero-kani/src/lib.rs
@@ -15,12 +15,6 @@ mod kani {
         // no-op
         let _ = cond;
     }
-
-    pub mod vec {
-        pub fn any_vec<T, const N: usize>() -> Vec<T> {
-            todo!()
-        }
-    }
 }
 
 #[doc(hidden)]
@@ -78,11 +72,12 @@ pub mod lib {
             // TODO make this configurable
             const MAX_LEN: usize = 256;
 
-            let bytes = kani::vec::any_vec::<u8, MAX_LEN>();
-            let len = self.options.max_len_or_default().min(MAX_LEN);
-            kani::assume(bytes.len() <= len);
+            let bytes = kani::any::<[u8; MAX_LEN]>();
+            let len = kani::any::<usize>();
+            let max_len = self.options.max_len_or_default().min(MAX_LEN);
+            kani::assume(len <= max_len);
 
-            f(&bytes)
+            f(&bytes[..len])
         }
 
         fn with_driver<F: FnMut(&mut Self::Driver) -> Output>(&mut self, f: &mut F) -> Output {
@@ -160,8 +155,14 @@ pub mod lib {
             Hint: FnOnce() -> (usize, Option<usize>),
             Gen: FnMut(&[u8]) -> Option<(usize, T)>,
         {
-            let bytes = kani::vec::any_vec::<u8, 256>();
-            let value = gen(&bytes).map(|v| v.1);
+            // TODO make this configurable
+            const MAX_LEN: usize = 256;
+
+            let bytes = kani::any::<[u8; MAX_LEN]>();
+            let len = kani::any::<usize>();
+            kani::assume(len <= MAX_LEN);
+
+            let value = gen(&bytes[..len]).map(|v| v.1);
             kani::assume(value.is_some());
             value
         }