Merge branch 'main' into kanicov-tool

adpaco-aws · Oct 7, 2024 · cb123e5 · cb123e5
2 parents c7606f3 + 1c38609
commit cb123e5
Show file tree

Hide file tree

Showing 16 changed files with 762 additions and 34 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -156,19 +156,19 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clap"
-version = "4.5.18"
+version = "4.5.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b0956a43b323ac1afaffc053ed5c4b7c1f1800bacd1683c353aabbb752515dd3"
+checksum = "7be5744db7978a28d9df86a214130d106a89ce49644cbc4e3f0c22c3fba30615"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.18"
+version = "4.5.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4d72166dd41634086d5803a47eb71ae740e61d84709c36f3c34110173db3961b"
+checksum = "a5fbc17d3ef8278f55b282b2a2e75ae6f6c7d4bb70ed3d0382375104bfafdb4b"
 dependencies = [
  "anstream",
  "anstyle",
@@ -420,6 +420,12 @@ dependencies = [
  "ahash",
 ]
 
+[[package]]
+name = "hashbrown"
+version = "0.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb"
+
 [[package]]
 name = "heck"
 version = "0.5.0"
@@ -437,12 +443,12 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "2.5.0"
+version = "2.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68b900aa2f7301e21c36462b170ee99994de34dff39a4a6a528e80e7376d07e5"
+checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da"
 dependencies = [
  "equivalent",
- "hashbrown",
+ "hashbrown 0.15.0",
 ]
 
 [[package]]
@@ -743,12 +749,9 @@ dependencies = [
 
 [[package]]
 name = "once_cell"
-version = "1.20.1"
+version = "1.20.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "82881c4be219ab5faaf2ad5e5e5ecdff8c66bd7402ca3160975c93b24961afd1"
-dependencies = [
- "portable-atomic",
-]
+checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775"
 
 [[package]]
 name = "os_info"
@@ -811,12 +814,6 @@ version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02"
 
-[[package]]
-name = "portable-atomic"
-version = "1.9.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cc9c68a3f6da06753e9335d63e27f6b9754dd1920d941135b7ea8224f141adb2"
-
 [[package]]
 name = "powerfmt"
 version = "0.2.0"
@@ -924,9 +921,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.6"
+version = "0.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "355ae415ccd3a04315d3f8246e86d67689ea74d88d915576e1589a351062a13b"
+checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f"
 dependencies = [
  "bitflags",
 ]
@@ -1146,7 +1143,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e"
 dependencies = [
  "cfg-if",
- "hashbrown",
+ "hashbrown 0.14.5",
  "serde",
 ]
 

diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
@@ -7,11 +7,16 @@
 //! by an unconstrained symbolic value of their size (e.g., `u8`, `u16`, `u32`, etc.).
 //!
 //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
+
+mod pointer;
+
 #[macro_export]
 #[allow(clippy::crate_in_macro_def)]
 macro_rules! generate_arbitrary {
     ($core:path) => {
         use core_path::marker::{PhantomData, PhantomPinned};
+        use core_path::mem::MaybeUninit;
+        use core_path::ptr::{self, addr_of_mut};
         use $core as core_path;
 
         pub trait Arbitrary
@@ -157,6 +162,15 @@ macro_rules! generate_arbitrary {
             }
         }
 
+        impl<T> Arbitrary for MaybeUninit<T>
+        where
+            T: Arbitrary,
+        {
+            fn any() -> Self {
+                if crate::kani::any() { MaybeUninit::new(T::any()) } else { MaybeUninit::uninit() }
+            }
+        }
+
         arbitrary_tuple!(A);
         arbitrary_tuple!(A, B);
         arbitrary_tuple!(A, B, C);
@@ -169,6 +183,11 @@ macro_rules! generate_arbitrary {
         arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J);
         arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K);
         arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L);
+
+        pub use self::arbitrary_ptr::*;
+        mod arbitrary_ptr {
+            kani_core::ptr_generator!();
+        }
     };
 }