Merge branch 'main' into clone-transformer

Author: AlexanderPortland

Cargo.lock

@@ -249,25 +249,25 @@ dependencies = [
 
 [[package]]
 name = "cargo-util-schemas"
-version = "0.2.0"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e63d2780ac94487eb9f1fea7b0d56300abc9eb488800854ca217f102f5caccca"
+checksum = "7dc1a6f7b5651af85774ae5a34b4e8be397d9cf4bc063b7e6dbd99a841837830"
 dependencies = [
  "semver",
  "serde",
  "serde-untagged",
  "serde-value",
- "thiserror 1.0.69",
+ "thiserror 2.0.12",
  "toml",
  "unicode-xid",
  "url",
 ]
 
 [[package]]
 name = "cargo_metadata"
-version = "0.20.0"
+version = "0.21.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4f7835cfc6135093070e95eb2b53e5d9b5c403dc3a6be6040ee026270aa82502"
+checksum = "5cfca2aaa699835ba88faf58a06342a314a950d2b9686165e038286c30316868"
 dependencies = [
  "camino",
  "cargo-platform",
@@ -280,9 +280,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.2.30"
+version = "1.2.31"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "deec109607ca693028562ed836a5f1c4b8bd77755c4e132fc5ce11b0b6211ae7"
+checksum = "c3a42d84bb6b69d3a8b3eaacf0d88f179e1929695e1ad012b6cf64d9caaa5fd2"
 dependencies = [
  "shlex",
 ]
@@ -344,19 +344,19 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.41"
+version = "4.5.42"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "be92d32e80243a54711e5d7ce823c35c41c9d929dc4ab58e1276f625841aadf9"
+checksum = "ed87a9d530bb41a67537289bafcac159cb3ee28460e0a4571123d2a778a6a882"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.41"
+version = "4.5.42"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "707eab41e9622f9139419d573eca0900137718000c517d47da73045f54331c3d"
+checksum = "64f4f3f3c77c94aff3c7e9aac9a2ca1974a5adf392a8bb751e827d6d127ab966"
 dependencies = [
  "anstream",
  "anstyle",
@@ -436,15 +436,15 @@ dependencies = [
 
 [[package]]
 name = "console"
-version = "0.15.11"
+version = "0.16.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "054ccb5b10f9f2cbf51eb355ca1d05c2d279ce1804688d0db74b4733a5aeafd8"
+checksum = "2e09ced7ebbccb63b4c65413d821f2e00ce54c5ca4514ddc6b3c892fdbcbc69d"
 dependencies = [
  "encode_unicode",
  "libc",
  "once_cell",
  "unicode-width",
- "windows-sys 0.59.0",
+ "windows-sys 0.60.2",
 ]
 
 [[package]]
@@ -1187,6 +1187,8 @@ dependencies = [
  "proc-macro-error2",
  "proc-macro2",
  "quote",
+ "strum",
+ "strum_macros",
  "syn",
 ]
 
@@ -1666,9 +1668,9 @@ dependencies = [
 
 [[package]]
 name = "quick-xml"
-version = "0.38.0"
+version = "0.38.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8927b0664f5c5a98265138b7e3f90aa19a6b21353182469ace36d4ac527b7b1b"
+checksum = "9845d9dccf565065824e69f9f235fafba1587031eda353c1f1561cd6a6be78f4"
 dependencies = [
  "memchr",
 ]
@@ -1710,9 +1712,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.16"
+version = "0.5.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7251471db004e509f4e75a62cca9435365b5ec7bcdff530d612ac7c87c44a792"
+checksum = "5407465600fb0548f1442edf71dd20683c6ed326200ace4b1ef0763521bb3b77"
 dependencies = [
  "bitflags",
 ]
@@ -1902,9 +1904,9 @@ dependencies = [
 
 [[package]]
 name = "serde_json"
-version = "1.0.141"
+version = "1.0.142"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "30b9eff21ebe718216c6ec64e1d9ac57087aad11efc64e32002bce4a0d4c03d3"
+checksum = "030fedb782600dcbd6f02d479bf0d817ac3bb40d644745b769d6a96bc3afc5a7"
 dependencies = [
  "indexmap",
  "itoa",
@@ -1971,9 +1973,9 @@ checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
 
 [[package]]
 name = "signal-hook-registry"
-version = "1.4.5"
+version = "1.4.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9203b8055f63a2a00e2f593bb0510367fe707d7ff1e5c872de2f537b339e5410"
+checksum = "b2a4719bff48cee6b39d12c020eeb490953ad2443b7055bd0b21fca26bd8c28b"
 dependencies = [
  "libc",
 ]
@@ -2206,9 +2208,9 @@ dependencies = [
 
 [[package]]
 name = "tokio"
-version = "1.47.0"
+version = "1.47.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "43864ed400b6043a4757a25c7a64a8efde741aed79a056a2fb348a406701bb35"
+checksum = "89e49afdadebb872d3145a5638b59eb0691ea23e46ca484037cfab3b76b95038"
 dependencies = [
  "backtrace",
  "bytes",
@@ -2691,7 +2693,7 @@ version = "0.60.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f2f500e4d28234f72040990ec9d39e3a6b950f9f22d3dba18416c35882612bcb"
 dependencies = [
- "windows-targets 0.53.2",
+ "windows-targets 0.53.3",
 ]
 
 [[package]]
@@ -2712,10 +2714,11 @@ dependencies = [
 
 [[package]]
 name = "windows-targets"
-version = "0.53.2"
+version = "0.53.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c66f69fcc9ce11da9966ddb31a40968cad001c5bedeb5c2b82ede4253ab48aef"
+checksum = "d5fe6031c4041849d7c496a8ded650796e7b6ecc19df1a431c1a363342e5dc91"
 dependencies = [
+ "windows-link",
  "windows_aarch64_gnullvm 0.53.0",
  "windows_aarch64_msvc 0.53.0",
  "windows_i686_gnu 0.53.0",

cprover_bindings/src/cbmc_string.rs

@@ -1,8 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use lazy_static::lazy_static;
-use std::sync::Mutex;
+use std::cell::RefCell;
 use string_interner::StringInterner;
 use string_interner::backend::StringBackend;
 use string_interner::symbol::SymbolU32;
@@ -23,10 +22,11 @@ use string_interner::symbol::SymbolU32;
 #[derive(Clone, Hash, Copy, PartialEq, Eq, PartialOrd, Ord)]
 pub struct InternedString(SymbolU32);
 
-// Use a `Mutex` to make this thread safe.
-lazy_static! {
-    static ref INTERNER: Mutex<StringInterner<StringBackend>> =
-        Mutex::new(StringInterner::default());
+// This [StringInterner] is a thread local, letting us get away with less synchronization.
+// See the `sync` module below for a full explanation of this choice's consequences.
+thread_local! {
+    static INTERNER: RefCell<StringInterner<StringBackend>> =
+        RefCell::new(StringInterner::default());
 }
 
 impl InternedString {
@@ -42,7 +42,7 @@ impl InternedString {
     /// Needed because exporting the &str backing the InternedString is blocked by lifetime rules.
     /// Instead, this allows users to operate on the &str when needed.
     pub fn map<T, F: FnOnce(&str) -> T>(&self, f: F) -> T {
-        f(INTERNER.lock().unwrap().resolve(self.0).unwrap())
+        INTERNER.with_borrow(|i| f(i.resolve(self.0).unwrap()))
     }
 
     pub fn starts_with(&self, pattern: &str) -> bool {
@@ -52,13 +52,13 @@ impl InternedString {
 
 impl std::fmt::Display for InternedString {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> {
-        write!(fmt, "{}", INTERNER.lock().unwrap().resolve(self.0).unwrap())
+        INTERNER.with_borrow(|i| write!(fmt, "{}", i.resolve(self.0).unwrap()))
     }
 }
 /// Custom-implement Debug, so our debug logging contains meaningful strings, not numbers
 impl std::fmt::Debug for InternedString {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> Result<(), std::fmt::Error> {
-        write!(fmt, "{:?}", INTERNER.lock().unwrap().resolve(self.0).unwrap())
+        INTERNER.with_borrow(|i| write!(fmt, "{:?}", i.resolve(self.0).unwrap()))
     }
 }
 
@@ -67,7 +67,7 @@ where
     T: AsRef<str>,
 {
     fn from(s: T) -> InternedString {
-        InternedString(INTERNER.lock().unwrap().get_or_intern(s))
+        InternedString(INTERNER.with_borrow_mut(|i| i.get_or_intern(s)))
     }
 }
 
@@ -76,7 +76,7 @@ where
     T: AsRef<str>,
 {
     fn eq(&self, other: &T) -> bool {
-        INTERNER.lock().unwrap().resolve(self.0).unwrap() == other.as_ref()
+        INTERNER.with_borrow(|i| i.resolve(self.0).unwrap() == other.as_ref())
     }
 }
 
@@ -105,6 +105,68 @@ where
     }
 }
 
+/// At a high level, the key design choice here is to keep our [StringInterner]s as thread locals.
+/// This works because whichever thread is generating `SymbolTable`s will be updating the interner in a way that
+/// affects serialization, but the serialization doesn't affect the interner in a way that affects generating
+/// `SymbolTable`s.
+///
+/// Thus, it makes a lot of sense to have threads each maintain their own copy of a [StringInterner]. Then, when the main
+/// codegen thread wants to tell another thread to write a new `SymbolTable` to disk, it can just send along
+/// its master copy of the [StringInterner] that they can use to update theirs.
+///
+/// To enforce this, [InternedString] is marked `!Send`--preventing them from being sent between threads
+/// unless they're wrapped in a [WithInterner](sync::WithInterner) type that will ensure the recieving thread updates
+/// its local interner to match the sending thread's.
+pub(crate) mod sync {
+    use string_interner::{StringInterner, backend::StringBackend};
+
+    use crate::{InternedString, cbmc_string::INTERNER};
+
+    /// The value of an [InternedString] is defined based on a thread local [INTERNER] so they cannot safely
+    /// be sent between threads.
+    impl !Send for InternedString {}
+
+    /// A type that is only `!Send` because it contains types specific to a thread local [INTERNER]
+    /// (e.g. [InternedString]s). This forces users to annotate that the types they want to wrap in [WithInterner]
+    /// are `!Send` just for that specific reason rather than using it to make arbitrary types `Send`.
+    ///
+    /// # Safety
+    ///
+    /// Should only be implemented for types which are `!Send` **solely** because they contain information specific
+    /// to their thread local [INTERNER] (e.g. by containing [InternedString]s).
+    pub unsafe trait InternerSpecific {}
+
+    /// Since [WithInterner<T>] guarantees that the inner `T` cannot be accessed without updating the
+    /// thread local [INTERNER] to a copy of what was used to generate `T`, it is safe to send between threads,
+    /// even if the inner `T` contains [InternedString]s which are not [Send] on their own.
+    unsafe impl<T: InternerSpecific> Send for WithInterner<T> {}
+
+    /// A type `T` bundled with the [StringInterner] that was used to generate it.
+    ///
+    /// The only way to access the inner `T` is by calling `into_inner()`, which will automatically
+    /// update the current thread's interner to the interner used the generate `T`,
+    /// ensuring interner coherence between the sending & receiving threads.
+    pub struct WithInterner<T> {
+        interner: StringInterner<StringBackend>,
+        inner: T,
+    }
+
+    impl<T> WithInterner<T> {
+        /// Create a new wrapper of `inner` with a clone of the current thread local [INTERNER].
+        pub fn new_with_current(inner: T) -> Self {
+            let interner = INTERNER.with_borrow(|i| i.clone());
+            WithInterner { interner, inner }
+        }
+
+        /// Get the inner wrapped `T` and implicitly update the current thread local [INTERNER] with a
+        /// copy of the one used to generate `T`.
+        pub fn into_inner(self) -> T {
+            INTERNER.with_borrow_mut(|i| *i = self.interner);
+            self.inner
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use crate::cbmc_string::InternedString;

cprover_bindings/src/lib.rs

@@ -31,6 +31,7 @@
 
 #![feature(f128)]
 #![feature(f16)]
+#![feature(negative_impls)]
 
 mod env;
 pub use env::global_dead_object;
@@ -41,4 +42,5 @@ pub mod utils;
 pub use irep::serialize;
 pub use machine_model::{MachineModel, RoundingMode};
 mod cbmc_string;
+pub use cbmc_string::sync::{InternerSpecific, WithInterner};
 pub use cbmc_string::{InternString, InternStringOption, InternedString};

docs/src/reference/experimental/autoharness.md

@@ -104,7 +104,9 @@ please add them to [this GitHub issue](https://github.com/model-checking/kani/is
 ## Limitations
 ### Arguments Implementing Arbitrary
 Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically, without bounds.
-In technical terms, each of the arguments needs to implement the `Arbitrary` trait or be capable of deriving it.
+In technical terms, each of the arguments needs to implement the `Arbitrary`
+trait or be capable of deriving it, or be a reference (mutable or immutable)
+where any of the prior requirements is fulfilled by the referenced type.
 Kani will detect if a struct or enum could implement `Arbitrary` and derive it automatically.
 Note that this automatic derivation feature is only available for autoharness.