Merge branch 'main' into add-script-to-automate-build

model-checking · Sep 10, 2024 · 5ba1b85 · 5ba1b85
2 parents a181e29 + 149f6dd
commit 5ba1b85
Show file tree

Hide file tree

Showing 259 changed files with 10,650 additions and 3,472 deletions.
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
@@ -13,14 +13,16 @@
 ---
 
 - [Challenges](./challenges.md)
- - [Core Transmutation](./challenges/0001-core-transmutation.md)
- - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
- - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
- - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
- - [Inductive data type](./challenges/0005-linked-list.md)
- - [Safety of NonNull](./challenges/0006-nonnull.md)
- - [Contracts for SmallSort](./challenges/0008-smallsort.md)
- - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)
- - [Memory safety of String](./challenges/0010-string.md)
- - [Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
- - [Safety of NonZero](./challenges/0012-nonzero.md)
+ - [1: Verify core transmuting methods](./challenges/0001-core-transmutation.md)
+ - [2: Verify the memory safery of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md)
+ - [3: Verifying Raw Pointer Arithmetic Operations](./challenges/0003-pointer-arithmentic.md)
+ - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
+ - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md)
+ - [6: Safety of `NonNull`](./challenges/0006-nonnull.md)
+ - [8: Contracts for SmallSort](./challenges/0008-smallsort.md)
+ - [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)
+ - [10: Memory safety of String](./challenges/0010-string.md)
+ - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
+ - [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
+
+
diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md
@@ -1,7 +1,7 @@
 # Challenge 1: Verify `core` transmuting methods
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19)
+- **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
 - **Start date:** 2024-06-12
 - **End date:** 2024-12-10
 

diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md
@@ -1,7 +1,7 @@
 # Challenge 2: Verify the memory safery of core intrinsics using raw pointers
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/16)
+- **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
 - **Start date:** *24/06/12*
 - **End date:** *24/12/10*
 

diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md
@@ -2,7 +2,7 @@
 
 - **Status:** Open
 - **Solution:**
-- **Tracking Issue:** <https://github.com/model-checking/verify-rust-std/issues/21>
+- **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
 - **Start date:** 24/06/24
 - **End date:** 24/12/10
 

diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md
@@ -1,7 +1,7 @@
 # Challenge 4: Memory safety of BTreeMap's `btree::node` module
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
+- **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
 - **Start date:** *2024-07-01*
 - **End date:** *2024-12-10*
 

diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md
@@ -1,7 +1,7 @@
 # Challenge 5: Verify functions iterating over inductive data type: `linked_list`
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29)
+- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *24/07/01*
 - **End date:** *24/12/10*
 

diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md
@@ -1,7 +1,7 @@
 # Challenge 6: Safety of NonNull
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/53)
+- **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
 - **Start date:** *2024-08-16*
 - **End date:** *2024-12-10*
 

diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md
@@ -1,7 +1,7 @@
 # Challenge 8: Contracts for SmallSort
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/56)
+- **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
 - **Start date:** *2024-08-17*
 - **End date:** *2024-12-10*
 

diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md
@@ -1,7 +1,7 @@
 # Challenge 10: Memory safety of String
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61)
+- **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61)
 - **Start date:** *2024-08-19*
 - **End date:** *2024-12-10*
 

diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md
@@ -2,7 +2,7 @@
 
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/59)
+- **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
 - **Start date:** *2024-08-20*
 - **End date:** *2024-12-10*
 

diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md
@@ -1,7 +1,7 @@
 # Challenge 12: Safety of `NonZero`
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/71)
+- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
 - **Start date:** *2024-08-23*
 - **End date:** *2024-12-10*
 

diff --git a/library/Cargo.lock b/library/Cargo.lock
diff --git a/library/Cargo.toml b/library/Cargo.toml
@@ -8,6 +8,7 @@ members = [
 exclude = [
  # stdarch has its own Cargo workspace
  "stdarch",
+ "windows_targets"
 ]
 
 [profile.release.package.compiler_builtins]
@@ -30,8 +31,10 @@ codegen-units = 10000
 # helps to improve link times a little bit.
 [profile.release.package]
 addr2line.debug = 0
+addr2line.opt-level = "s"
 adler.debug = 0
 gimli.debug = 0
+gimli.opt-level = "s"
 miniz_oxide.debug = 0
 object.debug = 0
 rustc-demangle.debug = 0

diff --git a/library/alloc/Cargo.toml b/library/alloc/Cargo.toml
@@ -10,10 +10,7 @@ edition = "2021"
 
 [dependencies]
 core = { path = "../core" }
-compiler_builtins = { version = "0.1.114", features = ['rustc-dep-of-std'] }
-
-[target.'cfg(not(any(target_arch = "aarch64", target_arch = "x86", target_arch = "x86_64")))'.dependencies]
-compiler_builtins = { version = "0.1.114", features = ["no-f16-f128"] }
+compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
 
 [dev-dependencies]
 rand = { version = "0.8.5", default-features = false, features = ["alloc"] }
@@ -55,4 +52,5 @@ check-cfg = [
  'cfg(no_global_oom_handling)',
  'cfg(no_rc)',
  'cfg(no_sync)',
+ 'cfg(randomized_layouts)',
 ]
diff --git a/library/alloc/benches/lib.rs b/library/alloc/benches/lib.rs
@@ -1,6 +1,3 @@
-// Disabling on android for the time being
-// See https://github.com/rust-lang/rust/issues/73535#event-3477699747
-#![cfg(not(target_os = "android"))]
 // Disabling in Miri as these would take too long.
 #![cfg(not(miri))]
 #![feature(btree_extract_if)]

diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs
@@ -372,6 +372,7 @@ extern "Rust" {
 #[rustc_const_unstable(feature = "const_alloc_error", issue = "92523")]
 #[cfg(all(not(no_global_oom_handling), not(test)))]
 #[cold]
+#[optimize(size)]
 pub const fn handle_alloc_error(layout: Layout) -> ! {
  const fn ct_error(_: Layout) -> ! {
  panic!("allocation failed");