Merge branch 'model-checking:main' into complete-transmute

Author: AlexLB99

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "f6bdf90c54ad6eed51b25c125f251cac01cfe170"
+  FLUX_VERSION: "ebafb8d0ca32d8c0fcd2a0cfef6b1b4bd4dc4a6f"
 
 jobs:
   check-flux-on-core:

library/Cargo.lock

@@ -22,9 +22,7 @@ safety = { path = "../contracts/safety" }
 [features]
 compiler-builtins-mem = ['compiler_builtins/mem']
 compiler-builtins-c = ["compiler_builtins/c"]
-compiler-builtins-no-asm = ["compiler_builtins/no-asm"]
 compiler-builtins-no-f16-f128 = ["compiler_builtins/no-f16-f128"]
-compiler-builtins-mangled-names = ["compiler_builtins/mangled-names"]
 # Make panics and failed asserts immediately abort without formatting any message
 panic_immediate_abort = ["core/panic_immediate_abort"]
 # Choose algorithms that are optimized for binary size instead of runtime performance

library/alloc/Cargo.toml

@@ -5,7 +5,7 @@
 use core::error::Error;
 use core::fmt::{self, Debug, Display, Formatter};
 #[cfg(not(no_global_oom_handling))]
-use core::intrinsics::const_allocate;
+use core::intrinsics::{const_allocate, const_make_global};
 use core::marker::PhantomData;
 #[cfg(not(no_global_oom_handling))]
 use core::marker::Unsize;
@@ -340,9 +340,10 @@ impl<H> WithHeader<H> {
                     alloc.add(metadata_offset).cast();
                 // SAFETY: `*metadata_ptr` is within the allocation.
                 metadata_ptr.write(ptr::metadata::<Dyn>(ptr::dangling::<T>() as *const Dyn));
-
+                // SAFETY: valid heap allocation
+                const_make_global(alloc);
                 // SAFETY: we have just written the metadata.
-                &*(metadata_ptr)
+                &*metadata_ptr
             }
         };
 

library/alloc/src/boxed/thin.rs

@@ -192,7 +192,7 @@ impl<T, A: Allocator> Drop for Drain<'_, T, A> {
                     // this branch is never taken.
                     // We use `#[cold]` instead of `#[inline(never)]`, because inlining this
                     // function into the general case (`.drain(n..m)`) is fine.
-                    // See `tests/codegen/vecdeque-drain.rs` for a test.
+                    // See `tests/codegen-llvm/vecdeque-drain.rs` for a test.
                     #[cold]
                     fn join_head_and_tail_wrapping<T, A: Allocator>(
                         source_deque: &mut VecDeque<T, A>,

library/alloc/src/collections/vec_deque/drain.rs

@@ -348,13 +348,13 @@
 //! format := '{' [ argument ] [ ':' format_spec ] [ ws ] * '}'
 //! argument := integer | identifier
 //!
-//! format_spec := [[fill]align][sign]['#']['0'][width]['.' precision]type
+//! format_spec := [[fill]align][sign]['#']['0'][width]['.' precision][type]
 //! fill := character
 //! align := '<' | '^' | '>'
 //! sign := '+' | '-'
 //! width := count
 //! precision := count | '*'
-//! type := '' | '?' | 'x?' | 'X?' | identifier
+//! type := '?' | 'x?' | 'X?' | identifier
 //! count := parameter | integer
 //! parameter := argument '$'
 //! ```

library/alloc/src/fmt.rs

@@ -95,7 +95,6 @@
 #![cfg_attr(kani, feature(kani))]
 #![feature(alloc_layout_extra)]
 #![feature(allocator_api)]
-#![feature(array_chunks)]
 #![feature(array_into_iter_constructors)]
 #![feature(array_windows)]
 #![feature(ascii_char)]
@@ -156,6 +155,7 @@
 #![feature(try_trait_v2)]
 #![feature(try_with_capacity)]
 #![feature(tuple_trait)]
+#![feature(ub_checks)]
 #![feature(unicode_internals)]
 #![feature(unsize)]
 #![feature(unwrap_infallible)]

library/alloc/src/lib.rs

@@ -761,7 +761,7 @@ impl<A: Allocator> RawVecInner<A> {
 }
 
 // not marked inline(never) since we want optimizers to be able to observe the specifics of this
-// function, see tests/codegen/vec-reserve-extend.rs.
+// function, see tests/codegen-llvm/vec-reserve-extend.rs.
 #[cold]
 fn finish_grow<A>(
     new_layout: Layout,

library/alloc/src/raw_vec/mod.rs

@@ -16,10 +16,6 @@ use core::cmp::Ordering::{self, Less};
 use core::mem::MaybeUninit;
 #[cfg(not(no_global_oom_handling))]
 use core::ptr;
-#[unstable(feature = "array_chunks", issue = "74985")]
-pub use core::slice::ArrayChunks;
-#[unstable(feature = "array_chunks", issue = "74985")]
-pub use core::slice::ArrayChunksMut;
 #[unstable(feature = "array_windows", issue = "75027")]
 pub use core::slice::ArrayWindows;
 #[stable(feature = "inherent_ascii_escape", since = "1.60.0")]

library/alloc/src/slice.rs

@@ -787,12 +787,12 @@ impl String {
     #[cfg(not(no_global_oom_handling))]
     #[unstable(feature = "str_from_utf16_endian", issue = "116258")]
     pub fn from_utf16le(v: &[u8]) -> Result<String, FromUtf16Error> {
-        if v.len() % 2 != 0 {
+        let (chunks, []) = v.as_chunks::<2>() else {
             return Err(FromUtf16Error(()));
-        }
+        };
         match (cfg!(target_endian = "little"), unsafe { v.align_to::<u16>() }) {
             (true, ([], v, [])) => Self::from_utf16(v),
-            _ => char::decode_utf16(v.array_chunks::<2>().copied().map(u16::from_le_bytes))
+            _ => char::decode_utf16(chunks.iter().copied().map(u16::from_le_bytes))
                 .collect::<Result<_, _>>()
                 .map_err(|_| FromUtf16Error(())),
         }
@@ -830,11 +830,11 @@ impl String {
             (true, ([], v, [])) => Self::from_utf16_lossy(v),
             (true, ([], v, [_remainder])) => Self::from_utf16_lossy(v) + "\u{FFFD}",
             _ => {
-                let mut iter = v.array_chunks::<2>();
-                let string = char::decode_utf16(iter.by_ref().copied().map(u16::from_le_bytes))
+                let (chunks, remainder) = v.as_chunks::<2>();
+                let string = char::decode_utf16(chunks.iter().copied().map(u16::from_le_bytes))
                     .map(|r| r.unwrap_or(char::REPLACEMENT_CHARACTER))
                     .collect();
-                if iter.remainder().is_empty() { string } else { string + "\u{FFFD}" }
+                if remainder.is_empty() { string } else { string + "\u{FFFD}" }
             }
         }
     }
@@ -862,12 +862,12 @@ impl String {
     #[cfg(not(no_global_oom_handling))]
     #[unstable(feature = "str_from_utf16_endian", issue = "116258")]
     pub fn from_utf16be(v: &[u8]) -> Result<String, FromUtf16Error> {
-        if v.len() % 2 != 0 {
+        let (chunks, []) = v.as_chunks::<2>() else {
             return Err(FromUtf16Error(()));
-        }
+        };
         match (cfg!(target_endian = "big"), unsafe { v.align_to::<u16>() }) {
             (true, ([], v, [])) => Self::from_utf16(v),
-            _ => char::decode_utf16(v.array_chunks::<2>().copied().map(u16::from_be_bytes))
+            _ => char::decode_utf16(chunks.iter().copied().map(u16::from_be_bytes))
                 .collect::<Result<_, _>>()
                 .map_err(|_| FromUtf16Error(())),
         }
@@ -905,11 +905,11 @@ impl String {
             (true, ([], v, [])) => Self::from_utf16_lossy(v),
             (true, ([], v, [_remainder])) => Self::from_utf16_lossy(v) + "\u{FFFD}",
             _ => {
-                let mut iter = v.array_chunks::<2>();
-                let string = char::decode_utf16(iter.by_ref().copied().map(u16::from_be_bytes))
+                let (chunks, remainder) = v.as_chunks::<2>();
+                let string = char::decode_utf16(chunks.iter().copied().map(u16::from_be_bytes))
                     .map(|r| r.unwrap_or(char::REPLACEMENT_CHARACTER))
                     .collect();
-                if iter.remainder().is_empty() { string } else { string + "\u{FFFD}" }
+                if remainder.is_empty() { string } else { string + "\u{FFFD}" }
             }
         }
     }
@@ -2611,7 +2611,7 @@ impl_eq! { Cow<'a, str>, &'b str }
 impl_eq! { Cow<'a, str>, String }
 
 #[stable(feature = "rust1", since = "1.0.0")]
-#[rustc_const_unstable(feature = "const_default", issue = "67792")]
+#[rustc_const_unstable(feature = "const_default", issue = "143894")]
 impl const Default for String {
     /// Creates an empty `String`.
     #[inline]