Merge remote-tracking branch 'origin/main' into autoharness-support

Author: tautschnig

.github/workflows/kani.yml

@@ -158,3 +158,30 @@ jobs:
               .addHeading('Kani List Output', 2)
               .addRaw(kaniOutput, false)
               .write();
+
+  run-autoharness-analyzer:
+    name: Kani Autoharness Analyzer
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run autoharness analyzer on the std library
+      - name: Run Autoharness Analyzer
+        run: scripts/run-kani.sh --run autoharness-analyzer
+
+      # Step 3: Add output to job summary
+      - name: Add Autoharness Analyzer output to job summary
+        run: |
+          echo "# Autoharness Failure Summary" >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate core, all functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate core, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate std, all functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate std, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"

doc/src/SUMMARY.md

@@ -31,4 +31,4 @@
   - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)
   - [16: Verify the safety of Iterator functions](./challenges/0016-iter.md)
   - [17: Verify the safety of slice functions](./challenges/0017-slice.md)
-  - [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter-pt1.md)
+  - [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter.md)

library/Cargo.lock

@@ -16,8 +16,8 @@ bench = false
 
 [dependencies]
 core = { path = "../core", public = true }
-compiler_builtins = { version = "=0.1.155", features = ['rustc-dep-of-std'] }
 safety = { path = "../contracts/safety" }
+compiler_builtins = { version = "=0.1.156", features = ['rustc-dep-of-std'] }
 
 [features]
 compiler-builtins-mem = ['compiler_builtins/mem']

library/alloc/Cargo.toml

@@ -574,7 +574,7 @@ impl CString {
     #[stable(feature = "as_c_str", since = "1.20.0")]
     #[rustc_diagnostic_item = "cstring_as_c_str"]
     pub fn as_c_str(&self) -> &CStr {
-        &*self
+        unsafe { CStr::from_bytes_with_nul_unchecked(self.as_bytes_with_nul()) }
     }
 
     /// Converts this `CString` into a boxed [`CStr`].
@@ -705,14 +705,14 @@ impl ops::Deref for CString {
 
     #[inline]
     fn deref(&self) -> &CStr {
-        unsafe { CStr::from_bytes_with_nul_unchecked(self.as_bytes_with_nul()) }
+        self.as_c_str()
     }
 }
 
 #[stable(feature = "rust1", since = "1.0.0")]
 impl fmt::Debug for CString {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        fmt::Debug::fmt(&**self, f)
+        fmt::Debug::fmt(self.as_c_str(), f)
     }
 }
 

library/alloc/src/ffi/c_str.rs

@@ -33,12 +33,6 @@ fn build_with_zero2() {
     assert!(CString::new(vec![0]).is_err());
 }
 
-#[test]
-fn formatted() {
-    let s = CString::new(&b"abc\x01\x02\n\xE2\x80\xA6\xFF"[..]).unwrap();
-    assert_eq!(format!("{s:?}"), r#""abc\x01\x02\n\xe2\x80\xa6\xff""#);
-}
-
 #[test]
 fn borrowed() {
     unsafe {

library/alloctests/tests/c_str2.rs

@@ -772,8 +772,8 @@ impl hash::Hash for TypeId {
         //   (especially given the previous point about the lower 64 bits being
         //   high quality on their own).
         // - It is correct to do so -- only hashing a subset of `self` is still
-        //   with an `Eq` implementation that considers the entire value, as
-        //   ours does.
+        //   compatible with an `Eq` implementation that considers the entire
+        //   value, as ours does.
         self.t.1.hash(state);
     }
 }

library/core/src/any.rs

@@ -32,7 +32,7 @@ pub macro asm("assembly template", $(operands,)* $(options($(option),*))?) {
 ///
 /// [Rust By Example]: https://doc.rust-lang.org/nightly/rust-by-example/unsafe/asm.html
 /// [reference]: https://doc.rust-lang.org/nightly/reference/inline-assembly.html
-#[unstable(feature = "naked_functions", issue = "90957")]
+#[stable(feature = "naked_functions", since = "CURRENT_RUSTC_VERSION")]
 #[rustc_builtin_macro]
 pub macro naked_asm("assembly template", $(operands,)* $(options($(option),*))?) {
     /* compiler built-in */

library/core/src/arch.rs

@@ -36,8 +36,7 @@ use crate::ops::{Deref, DerefMut, DerefPure};
 /// presented as hex escape sequences.
 ///
 /// The `Display` implementation behaves as if the `ByteStr` were first lossily converted to a
-/// `str`, with invalid UTF-8 presented as the Unicode replacement character: �
-///
+/// `str`, with invalid UTF-8 presented as the Unicode replacement character (�).
 #[unstable(feature = "bstr", issue = "134915")]
 #[repr(transparent)]
 #[doc(alias = "BStr")]

library/core/src/bstr/mod.rs

@@ -157,7 +157,6 @@ impl Error for FromBytesWithNulError {
 /// within the slice.
 ///
 /// This error is created by the [`CStr::from_bytes_until_nul`] method.
-///
 #[derive(Clone, PartialEq, Eq, Debug)]
 #[stable(feature = "cstr_from_bytes_until_nul", since = "1.69.0")]
 pub struct FromBytesUntilNulError(());

library/core/src/ffi/c_str.rs

@@ -304,7 +304,7 @@ pub unsafe fn simd_shuffle<T, U, V>(x: T, y: T, idx: U) -> V;
 ///
 /// `U` must be a vector of pointers to the element type of `T`, with the same length as `T`.
 ///
-/// `V` must be a vector of signed integers with the same length as `T` (but any element size).
+/// `V` must be a vector of integers with the same length as `T` (but any element size).
 ///
 /// For each pointer in `ptr`, if the corresponding value in `mask` is `!0`, read the pointer.
 /// Otherwise if the corresponding value in `mask` is `0`, return the corresponding value from
@@ -325,7 +325,7 @@ pub unsafe fn simd_gather<T, U, V>(val: T, ptr: U, mask: V) -> T;
 ///
 /// `U` must be a vector of pointers to the element type of `T`, with the same length as `T`.
 ///
-/// `V` must be a vector of signed integers with the same length as `T` (but any element size).
+/// `V` must be a vector of integers with the same length as `T` (but any element size).
 ///
 /// For each pointer in `ptr`, if the corresponding value in `mask` is `!0`, write the
 /// corresponding value in `val` to the pointer.
@@ -349,7 +349,7 @@ pub unsafe fn simd_scatter<T, U, V>(val: T, ptr: U, mask: V);
 ///
 /// `U` must be a pointer to the element type of `T`
 ///
-/// `V` must be a vector of signed integers with the same length as `T` (but any element size).
+/// `V` must be a vector of integers with the same length as `T` (but any element size).
 ///
 /// For each element, if the corresponding value in `mask` is `!0`, read the corresponding
 /// pointer offset from `ptr`.
@@ -372,7 +372,7 @@ pub unsafe fn simd_masked_load<V, U, T>(mask: V, ptr: U, val: T) -> T;
 ///
 /// `U` must be a pointer to the element type of `T`
 ///
-/// `V` must be a vector of signed integers with the same length as `T` (but any element size).
+/// `V` must be a vector of integers with the same length as `T` (but any element size).
 ///
 /// For each element, if the corresponding value in `mask` is `!0`, write the corresponding
 /// value in `val` to the pointer offset from `ptr`.
@@ -556,7 +556,7 @@ pub unsafe fn simd_bitmask<T, U>(x: T) -> U;
 ///
 /// `T` must be a vector.
 ///
-/// `M` must be a signed integer vector with the same length as `T` (but any element size).
+/// `M` must be an integer vector with the same length as `T` (but any element size).
 ///
 /// For each element, if the corresponding value in `mask` is `!0`, select the element from
 /// `if_true`.  If the corresponding value in `mask` is `0`, select the element from

library/core/src/intrinsics/simd.rs

@@ -151,6 +151,9 @@ impl f128 {
     pub const RADIX: u32 = 2;
 
     /// Number of significant digits in base 2.
+    ///
+    /// Note that the size of the mantissa in the bitwise representation is one
+    /// smaller than this since the leading 1 is not stored explicitly.
     #[unstable(feature = "f128", issue = "116909")]
     pub const MANTISSA_DIGITS: u32 = 113;
 

library/core/src/num/f128.rs

@@ -146,6 +146,9 @@ impl f16 {
     pub const RADIX: u32 = 2;
 
     /// Number of significant digits in base 2.
+    ///
+    /// Note that the size of the mantissa in the bitwise representation is one
+    /// smaller than this since the leading 1 is not stored explicitly.
     #[unstable(feature = "f16", issue = "116909")]
     pub const MANTISSA_DIGITS: u32 = 11;
 

library/core/src/num/f16.rs

@@ -396,6 +396,9 @@ impl f32 {
     pub const RADIX: u32 = 2;
 
     /// Number of significant digits in base 2.
+    ///
+    /// Note that the size of the mantissa in the bitwise representation is one
+    /// smaller than this since the leading 1 is not stored explicitly.
     #[stable(feature = "assoc_int_consts", since = "1.43.0")]
     pub const MANTISSA_DIGITS: u32 = 24;
 

library/core/src/num/f32.rs

@@ -396,6 +396,9 @@ impl f64 {
     pub const RADIX: u32 = 2;
 
     /// Number of significant digits in base 2.
+    ///
+    /// Note that the size of the mantissa in the bitwise representation is one
+    /// smaller than this since the leading 1 is not stored explicitly.
     #[stable(feature = "assoc_int_consts", since = "1.43.0")]
     pub const MANTISSA_DIGITS: u32 = 53;
     /// Approximate number of significant digits in base 10.

library/core/src/num/f64.rs

@@ -1589,6 +1589,7 @@ macro_rules! int_impl {
             let mut base = self;
             let mut acc: Self = 1;
 
+            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     acc = try_opt!(acc.checked_mul(base));
@@ -2299,6 +2300,7 @@ macro_rules! int_impl {
             let mut acc: Self = 1;
 
             if intrinsics::is_val_statically_known(exp) {
+                #[safety::loop_invariant(exp>=1)]
                 while exp > 1 {
                     if (exp & 1) == 1 {
                         acc = acc.wrapping_mul(base);
@@ -2316,6 +2318,7 @@ macro_rules! int_impl {
                 // at compile time. We can't use the same code for the constant
                 // exponent case because LLVM is currently unable to unroll
                 // this loop.
+                #[safety::loop_invariant(true)]
                 loop {
                     if (exp & 1) == 1 {
                         acc = acc.wrapping_mul(base);

library/core/src/num/int_macros.rs

@@ -1,6 +1,8 @@
 //! Definitions of `Saturating<T>`.
 
 use crate::fmt;
+#[cfg(kani)]
+use crate::kani;
 use crate::ops::{
     Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign,
     Mul, MulAssign, Neg, Not, Rem, RemAssign, Sub, SubAssign,
@@ -37,6 +39,14 @@ use crate::ops::{
 #[rustc_diagnostic_item = "Saturating"]
 pub struct Saturating<T>(#[stable(feature = "saturating_int_impl", since = "1.74.0")] pub T);
 
+#[cfg(kani)]
+#[stable(feature = "saturating_int_impl", since = "1.74.0")]
+impl<T: kani::Arbitrary> kani::Arbitrary for Saturating<T> {
+    fn any() -> Self {
+        Self { 0: kani::any() }
+    }
+}
+
 #[stable(feature = "saturating_int_impl", since = "1.74.0")]
 impl<T: fmt::Debug> fmt::Debug for Saturating<T> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

library/core/src/num/saturating.rs

@@ -1780,6 +1780,7 @@ macro_rules! uint_impl {
             let mut base = self;
             let mut acc: Self = 1;
 
+            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     acc = try_opt!(acc.checked_mul(base));
@@ -2349,6 +2350,7 @@ macro_rules! uint_impl {
             let mut acc: Self = 1;
 
             if intrinsics::is_val_statically_known(exp) {
+                #[safety::loop_invariant(exp>=1)]
                 while exp > 1 {
                     if (exp & 1) == 1 {
                         acc = acc.wrapping_mul(base);
@@ -2366,6 +2368,7 @@ macro_rules! uint_impl {
                 // at compile time. We can't use the same code for the constant
                 // exponent case because LLVM is currently unable to unroll
                 // this loop.
+                #[safety::loop_invariant(true)]
                 loop {
                     if (exp & 1) == 1 {
                         acc = acc.wrapping_mul(base);
@@ -3044,6 +3047,7 @@ macro_rules! uint_impl {
             // Scratch space for storing results of overflowing_mul.
             let mut r;
 
+            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     r = acc.overflowing_mul(base);

library/core/src/num/uint_macros.rs

@@ -1,6 +1,8 @@
 //! Definitions of `Wrapping<T>`.
 
 use crate::fmt;
+#[cfg(kani)]
+use crate::kani;
 use crate::ops::{
     Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign,
     Mul, MulAssign, Neg, Not, Rem, RemAssign, Shl, ShlAssign, Shr, ShrAssign, Sub, SubAssign,
@@ -42,6 +44,14 @@ use crate::ops::{
 #[rustc_diagnostic_item = "Wrapping"]
 pub struct Wrapping<T>(#[stable(feature = "rust1", since = "1.0.0")] pub T);
 
+#[cfg(kani)]
+#[stable(feature = "rust1", since = "1.0.0")]
+impl<T: kani::Arbitrary> kani::Arbitrary for Wrapping<T> {
+    fn any() -> Self {
+        Self { 0: kani::any() }
+    }
+}
+
 #[stable(feature = "rust1", since = "1.0.0")]
 impl<T: fmt::Debug> fmt::Debug for Wrapping<T> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

library/core/src/num/wrapping.rs

@@ -2814,7 +2814,7 @@ impl<T> [T] {
             let half = size / 2;
             let mid = base + half;
 
-            // SAFETY: the call is made safe by the following inconstants:
+            // SAFETY: the call is made safe by the following invariants:
             // - `mid >= 0`: by definition
             // - `mid < size`: `mid = size / 2 + size / 4 + size / 8 ...`
             let cmp = f(unsafe { self.get_unchecked(mid) });

library/core/src/slice/mod.rs

@@ -13,3 +13,9 @@ fn compares_as_u8s() {
     assert_eq!(Ord::cmp(a, b), Ord::cmp(a_bytes, b_bytes));
     assert_eq!(PartialOrd::partial_cmp(a, b), PartialOrd::partial_cmp(a_bytes, b_bytes));
 }
+
+#[test]
+fn debug() {
+    let s = c"abc\x01\x02\n\xE2\x80\xA6\xFF";
+    assert_eq!(format!("{s:?}"), r#""abc\x01\x02\n\xe2\x80\xa6\xff""#);
+}

library/coretests/tests/ffi/cstr.rs

@@ -5,6 +5,9 @@ use crate::simd::{
     ptr::{SimdConstPtr, SimdMutPtr},
 };
 
+#[cfg(kani)]
+use crate::kani;
+
 /// A SIMD vector with the shape of `[T; N]` but the operations of `T`.
 ///
 /// `Simd<T, N>` supports the operators (+, *, etc.) that `T` does in "elementwise" fashion.
@@ -100,6 +103,7 @@ use crate::simd::{
 // avoided, as it will likely become illegal on `#[repr(simd)]` structs in the future. It also
 // causes rustc to emit illegal LLVM IR in some cases.
 #[repr(simd, packed)]
+#[cfg_attr(kani, derive(kani::Arbitrary))]
 pub struct Simd<T, const N: usize>([T; N])
 where
     LaneCount<N>: SupportedLaneCount,

library/portable-simd/crates/core_simd/src/vector.rs

@@ -18,7 +18,7 @@ cfg-if = { version = "1.0", features = ['rustc-dep-of-std'] }
 panic_unwind = { path = "../panic_unwind", optional = true }
 panic_abort = { path = "../panic_abort" }
 core = { path = "../core", public = true }
-compiler_builtins = { version = "=0.1.155" }
+compiler_builtins = { version = "=0.1.156" }
 unwind = { path = "../unwind" }
 hashbrown = { version = "0.15", default-features = false, features = [
     'rustc-dep-of-std',
@@ -36,7 +36,7 @@ miniz_oxide = { version = "0.8.0", optional = true, default-features = false }
 addr2line = { version = "0.24.0", optional = true, default-features = false }
 
 [target.'cfg(not(all(windows, target_env = "msvc")))'.dependencies]
-libc = { version = "0.2.171", default-features = false, features = [
+libc = { version = "0.2.172", default-features = false, features = [
     'rustc-dep-of-std',
 ], public = true }