Merge branch 'main' into strIterchallenges

Author: thanhnguyen-aws

.github/workflows/update-subtree.yml

@@ -58,8 +58,27 @@ jobs:
         echo "NEXT_TOOLCHAIN_DATE=${NEXT_TOOLCHAIN_DATE}" >> $GITHUB_ENV
         echo "CURRENT_COMMIT_HASH=${CURRENT_COMMIT_HASH}" >> $GITHUB_ENV
         echo "NEXT_COMMIT_HASH=${NEXT_COMMIT_HASH}" >> $GITHUB_ENV
+        KANI_COMMIT_HASH=$(git -C kani-tmp rev-parse HEAD)
+        echo "KANI_COMMIT_HASH=${KANI_COMMIT_HASH}" >> $GITHUB_ENV
+
+    - name: Check for existing pull requests
+      run: |
+        cd verify-rust-std
+        if gh pr list --json title --jq '.[] | select(.title | startswith("Update subtree/library to")) | .title' | grep -q .; then
+          echo "SUBTREE_PR_EXISTS=yes" >> $GITHUB_ENV
+        else
+          echo "SUBTREE_PR_EXISTS=no" >> $GITHUB_ENV
+        fi
+        if gh pr list --json title --jq '.[] | select(.title | startswith("Merge subtree update for toolchain nightly-")) | .title' | grep -q .; then
+          echo "MERGE_PR_EXISTS=yes" >> $GITHUB_ENV
+        else
+          echo "MERGE_PR_EXISTS=no" >> $GITHUB_ENV
+        fi
+      env:
+        GH_TOKEN: ${{ github.token }}
 
     - name: Update subtree/library locally
+      if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
       run: |
         cd rust-tmp
 
@@ -77,6 +96,9 @@ jobs:
         git remote add rust-filtered ../rust-tmp/
         git fetch rust-filtered
         git checkout -b subtree/library rust-filtered/subtree/library
+        # The filter-subtree operation adds an extraneous `library/` folder containing the submodules
+        # (c.f. https://github.com/model-checking/verify-rust-std/issues/249), so remove that before committing.
+        rm -rf library
         SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
         UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
         UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
@@ -89,22 +111,23 @@ jobs:
           echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
         fi
 
-    - name: Create Pull Request
-      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+    - name: Create Pull Request to update subtree/library
+      if: ${{ env.MERGE_CONFLICTS != 'noop' && env.SUBTREE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
         body: |
           This is an automated PR to update the subtree/library branch to the changes
           from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
           to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
+          **Do not merge this PR using the merge queue. Instead, use the rebase strategy.**
         branch: update-subtree/library
         delete-branch: true
         base: subtree/library
         path: verify-rust-std
 
     - name: Merge subtree/library changes
-      if: ${{ env.MERGE_CONFLICTS != 'noop' }}
+      if: ${{ env.MERGE_CONFLICTS != 'noop' && env.MERGE_PR_EXISTS == 'no' }}
       run: |
         cd verify-rust-std
         git checkout main
@@ -119,12 +142,15 @@ jobs:
           echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
         fi
 
-        sed -i "s/^channel = \"nightly-.*\"/channel = \"${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
+        sed -i "s/^channel = \"nightly-.*\"/channel = \"nightly-${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update toolchain to ${NEXT_TOOLCHAIN_DATE}" rust-toolchain.toml
-
+        # Update kani-version.toml with the new Kani commit hash
+        sed -i "s/commit = .*/commit = \"${KANI_COMMIT_HASH}\"/" tool_config/kani-version.toml
+        git -c user.name=gitbot -c user.email=git@bot \
+          commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
     - name: Create Pull Request without conflicts
-      if: ${{ env.MERGE_CONFLICTS == 'no' }}
+      if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
@@ -139,7 +165,7 @@ jobs:
         path: verify-rust-std
 
     - name: Create Pull Request with conflicts
-      if: ${{ env.MERGE_CONFLICTS == 'yes' }}
+      if: ${{ env.MERGE_CONFLICTS == 'yes' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'

library/Cargo.lock

@@ -3,6 +3,7 @@ resolver = "1"
 members = [
   "std",
   "sysroot",
+  "coretests",
 ]
 
 exclude = [
@@ -32,7 +33,7 @@ codegen-units = 10000
 [profile.release.package]
 addr2line.debug = 0
 addr2line.opt-level = "s"
-adler.debug = 0
+adler2.debug = 0
 gimli.debug = 0
 gimli.opt-level = "s"
 miniz_oxide.debug = 0

library/Cargo.toml

@@ -10,7 +10,7 @@ edition = "2021"
 
 [dependencies]
 core = { path = "../core" }
-compiler_builtins = { version = "=0.1.138", features = ['rustc-dep-of-std'] }
+compiler_builtins = { version = "=0.1.145", features = ['rustc-dep-of-std'] }
 safety = { path = "../contracts/safety" }
 
 [dev-dependencies]

library/alloc/Cargo.toml

@@ -353,6 +353,7 @@ pub fn iter_10k(b: &mut Bencher) {
 }
 
 #[bench]
+#[cfg_attr(target_os = "emscripten", ignore)] // hits an OOM
 pub fn iter_1m(b: &mut Bencher) {
     bench_iter(b, 1_000, 1_000_000);
 }

library/alloc/benches/btree/map.rs

@@ -4,8 +4,7 @@
 #![feature(iter_next_chunk)]
 #![feature(repr_simd)]
 #![feature(slice_partition_dedup)]
-#![cfg_attr(bootstrap, feature(strict_provenance))]
-#![cfg_attr(not(bootstrap), feature(strict_provenance_lints))]
+#![feature(strict_provenance_lints)]
 #![feature(test)]
 #![deny(fuzzy_provenance_casts)]
 

library/alloc/benches/lib.rs

@@ -366,14 +366,25 @@ rotate!(rotate_medium_half, gen_random, 9158, 9158 / 2);
 rotate!(rotate_medium_half_plus_one, gen_random, 9158, 9158 / 2 + 1);
 
 // Intended to use more RAM than the machine has cache
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by1, gen_random, 5 * 1024 * 1024, 1);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by9199_u64, gen_random, 5 * 1024 * 1024, 9199);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by9199_bytes, gen_random_bytes, 5 * 1024 * 1024, 9199);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by9199_strings, gen_strings, 5 * 1024 * 1024, 9199);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by9199_big, gen_big_random, 5 * 1024 * 1024, 9199);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by1234577_u64, gen_random, 5 * 1024 * 1024, 1234577);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by1234577_bytes, gen_random_bytes, 5 * 1024 * 1024, 1234577);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by1234577_strings, gen_strings, 5 * 1024 * 1024, 1234577);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_by1234577_big, gen_big_random, 5 * 1024 * 1024, 1234577);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_half, gen_random, 5 * 1024 * 1024, 5 * 1024 * 1024 / 2);
+#[cfg(not(target_os = "emscripten"))] // hits an OOM
 rotate!(rotate_huge_half_plus_one, gen_random, 5 * 1024 * 1024, 5 * 1024 * 1024 / 2 + 1);

library/alloc/benches/slice.rs

@@ -547,6 +547,11 @@ fn bench_in_place_collect_droppable(b: &mut Bencher) {
     })
 }
 
+// node.js gives out of memory error to use with length 1_100_000
+#[cfg(target_os = "emscripten")]
+const LEN: usize = 4096;
+
+#[cfg(not(target_os = "emscripten"))]
 const LEN: usize = 16384;
 
 #[bench]

library/alloc/benches/vec.rs

@@ -10,9 +10,6 @@ use core::hint;
 #[cfg(not(test))]
 use core::ptr::{self, NonNull};
 
-#[cfg(test)]
-mod tests;
-
 extern "Rust" {
     // These are the magic symbols to call the global allocator. rustc generates
     // them to call `__rg_alloc` etc. if there is a `#[global_allocator]` attribute
@@ -342,7 +339,7 @@ unsafe impl Allocator for Global {
     }
 }
 
-/// The allocator for unique pointers.
+/// The allocator for `Box`.
 #[cfg(all(not(no_global_oom_handling), not(test)))]
 #[lang = "exchange_malloc"]
 #[inline]