Merge branch 'main' into repeatinvariant

Author: thanhnguyen-aws

doc/src/challenges/0005-linked-list.md

@@ -1,10 +1,11 @@
 # Challenge 5: Verify functions iterating over inductive data type: `linked_list`
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *2024/07/01*
-- **End date:** *2025/04/10*
+- **End date:** *2025/08/12*
 - **Reward:** *5,000 USD*
+- **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------
 

library/Cargo.lock

@@ -14,6 +14,7 @@ crate-type = ["dylib", "rlib"]
 
 [dependencies]
 alloc = { path = "../alloc", public = true }
+# std no longer uses cfg-if directly, but the included copy of backtrace does.
 cfg-if = { version = "1.0", features = ['rustc-dep-of-std'] }
 panic_unwind = { path = "../panic_unwind", optional = true }
 panic_abort = { path = "../panic_abort" }

library/std/Cargo.toml

@@ -3119,7 +3119,7 @@ pub fn read_dir<P: AsRef<Path>>(path: P) -> io::Result<ReadDir> {
 /// On UNIX-like systems, this function will update the permission bits
 /// of the file pointed to by the symlink.
 ///
-/// Note that this behavior can lead to privalage escalation vulnerabilities,
+/// Note that this behavior can lead to privilege escalation vulnerabilities,
 /// where the ability to create a symlink in one directory allows you to
 /// cause the permissions of another file or directory to be modified.
 ///

library/std/src/fs.rs

@@ -63,10 +63,11 @@ where
     R: Read,
     W: Write,
 {
-    cfg_if::cfg_if! {
-        if #[cfg(any(target_os = "linux", target_os = "android"))] {
+    cfg_select! {
+        any(target_os = "linux", target_os = "android") => {
             crate::sys::kernel_copy::copy_spec(reader, writer)
-        } else {
+        }
+        _ => {
             generic_copy(reader, writer)
         }
     }

library/std/src/io/copy.rs

@@ -331,6 +331,7 @@
 #![feature(bstr)]
 #![feature(bstr_internals)]
 #![feature(cast_maybe_uninit)]
+#![feature(cfg_select)]
 #![feature(char_internals)]
 #![feature(clone_to_uninit)]
 #![feature(const_cmp)]

library/std/src/lib.rs

@@ -1,14 +1,16 @@
-cfg_if::cfg_if! {
-    if #[cfg(any(
+cfg_select! {
+    any(
         target_os = "linux", target_os = "android",
         target_os = "hurd",
         target_os = "dragonfly", target_os = "freebsd",
         target_os = "openbsd", target_os = "netbsd",
         target_os = "solaris", target_os = "illumos",
         target_os = "haiku", target_os = "nto",
-        target_os = "cygwin"))] {
+        target_os = "cygwin",
+    ) => {
         use libc::MSG_NOSIGNAL;
-    } else {
+    }
+    _ => {
         const MSG_NOSIGNAL: core::ffi::c_int = 0x0;
     }
 }

library/std/src/os/unix/net/stream.rs

@@ -4,26 +4,26 @@
 
 #![stable(feature = "rust1", since = "1.0.0")]
 
-use cfg_if::cfg_if;
-
 use crate::ffi::OsStr;
 use crate::os::unix::io::{AsFd, AsRawFd, BorrowedFd, FromRawFd, IntoRawFd, OwnedFd, RawFd};
 use crate::path::Path;
 use crate::sealed::Sealed;
 use crate::sys_common::{AsInner, AsInnerMut, FromInner, IntoInner};
 use crate::{io, process, sys};
 
-cfg_if! {
-    if #[cfg(any(target_os = "vxworks", target_os = "espidf", target_os = "horizon", target_os = "vita"))] {
+cfg_select! {
+    any(target_os = "vxworks", target_os = "espidf", target_os = "horizon", target_os = "vita") => {
         type UserId = u16;
         type GroupId = u16;
-    } else if #[cfg(target_os = "nto")] {
+    }
+    target_os = "nto" => {
         // Both IDs are signed, see `sys/target_nto.h` of the QNX Neutrino SDP.
         // Only positive values should be used, see e.g.
         // https://www.qnx.com/developers/docs/7.1/#com.qnx.doc.neutrino.lib_ref/topic/s/setuid.html
         type UserId = i32;
         type GroupId = i32;
-    } else {
+    }
+    _ => {
         type UserId = u32;
         type GroupId = u32;
     }

library/std/src/os/unix/process.rs

@@ -1,5 +1,3 @@
-use cfg_if::cfg_if;
-
 use crate::cell::UnsafeCell;
 use crate::fmt;
 use crate::ops::Deref;
@@ -87,8 +85,8 @@ pub struct ReentrantLock<T: ?Sized> {
     data: T,
 }
 
-cfg_if!(
-    if #[cfg(target_has_atomic = "64")] {
+cfg_select!(
+    target_has_atomic = "64" => {
         use crate::sync::atomic::{Atomic, AtomicU64, Ordering::Relaxed};
 
         struct Tid(Atomic<u64>);
@@ -110,7 +108,8 @@ cfg_if!(
                 self.0.store(value, Relaxed);
             }
         }
-    } else {
+    }
+    _ => {
         /// Returns the address of a TLS variable. This is guaranteed to
         /// be unique across all currently alive threads.
         fn tls_addr() -> usize {

library/std/src/sync/reentrant_lock.rs

@@ -68,29 +68,37 @@ unsafe fn realloc_fallback(
     }
 }
 
-cfg_if::cfg_if! {
-    if #[cfg(any(
+cfg_select! {
+    any(
         target_family = "unix",
         target_os = "wasi",
         target_os = "teeos",
         target_os = "trusty",
-    ))] {
+    ) => {
         mod unix;
-    } else if #[cfg(target_os = "windows")] {
+    }
+    target_os = "windows" => {
         mod windows;
-    } else if #[cfg(target_os = "hermit")] {
+    }
+    target_os = "hermit" => {
         mod hermit;
-    } else if #[cfg(all(target_vendor = "fortanix", target_env = "sgx"))] {
+    }
+    all(target_vendor = "fortanix", target_env = "sgx") => {
         mod sgx;
-    } else if #[cfg(target_os = "solid_asp3")] {
+    }
+    target_os = "solid_asp3" => {
         mod solid;
-    } else if #[cfg(target_os = "uefi")] {
+    }
+    target_os = "uefi" => {
         mod uefi;
-    } else if #[cfg(target_family = "wasm")] {
+    }
+    target_family = "wasm" => {
         mod wasm;
-    } else if #[cfg(target_os = "xous")] {
+    }
+    target_os = "xous" => {
         mod xous;
-    } else if #[cfg(target_os = "zkvm")] {
+    }
+    target_os = "zkvm" => {
         mod zkvm;
     }
 }