Skip to content

Commit b540e67

Browse files
thanhnguyen-awsthanhnguyen-aws
authored
Merge branch 'main' into vecchallenge
2 parents 73a6f27 + b152f68 commit b540e67

158 files changed

Lines changed: 3370 additions & 1327 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/update-subtree.yml‎

Lines changed: 42 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -137,11 +137,14 @@ jobs:
137137
uses: peter-evans/create-pull-request@v7
138138
with:
139139
title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
140-
body: |
140+
body: >
141141
This is an automated PR to update the subtree/library branch to the changes
142-
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
143-
to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
144-
**Do not merge this PR using the merge queue. Instead, use the rebase strategy.**
142+
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.CURRENT_COMMIT_HASH }})
143+
to ${{ env.NEXT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.NEXT_COMMIT_HASH }}), inclusive.
144+
145+
**Review this PR as usual, but do not merge this PR using the GitHub web interface.
146+
Instead, once it is approved, use `git push` to literally push the changes to `subtree/library`
147+
without any rebase or merge.**
145148
branch: update-subtree/library
146149
delete-branch: true
147150
base: subtree/library
@@ -151,20 +154,36 @@ jobs:
151154
if: ${{ env.MERGE_CONFLICTS != 'noop' && env.MERGE_PR_EXISTS == 'no' }}
152155
run: |
153156
cd verify-rust-std
154-
if ! git rev-parse --verify subtree/library; then
157+
# create-pull-request resets branches locally, implying that
158+
# `subtree/library` no longer is what the above instructions created.
159+
if [ "${SUBTREE_PR_EXISTS}" = "yes" ]; then
155160
git checkout -t -b subtree/library origin/update-subtree/library
161+
else
162+
git checkout subtree/library
163+
git reset --hard origin/update-subtree/library
156164
fi
157165
git checkout main
158166
167+
# Tell git about the correct merge base to use, which is the subtree
168+
# head that we last merged from.
169+
PREV_SUBTREE_HEAD=$(git log --grep="^git-subtree-split:" | egrep '^[[:space:]]+git-subtree-split:' | awk '{print $2;exit}')
170+
echo "Previous subtree head: ${PREV_SUBTREE_HEAD}"
171+
git replace --graft subtree/library ${PREV_SUBTREE_HEAD}
172+
git replace --graft main ${PREV_SUBTREE_HEAD}
173+
159174
# This command may fail, which will require human intervention.
160175
if ! git \
161176
-c user.name=gitbot -c user.email=git@bot \
162-
subtree merge --prefix=library subtree/library --squash; then
177+
merge -Xsubtree=library subtree/library; then
163178
echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
164179
git -c user.name=gitbot -c user.email=git@bot commit -a -m "Merge from $NEXT_COMMIT_HASH with conflicts"
165180
else
166181
echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
167182
fi
183+
git replace -d subtree/library
184+
git replace -d main~1
185+
NEW_SUBTREE_HEAD=$(git rev-parse subtree/library)
186+
echo "NEW_SUBTREE_HEAD=${NEW_SUBTREE_HEAD}" >> $GITHUB_ENV
168187
169188
sed -i "s/^channel = \"nightly-.*\"/channel = \"nightly-${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
170189
git -c user.name=gitbot -c user.email=git@bot \
@@ -173,16 +192,22 @@ jobs:
173192
sed -i "s/commit = .*/commit = \"${KANI_COMMIT_HASH}\"/" tool_config/kani-version.toml
174193
git -c user.name=gitbot -c user.email=git@bot \
175194
commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
195+
176196
- name: Create Pull Request without conflicts
177197
if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}
178198
uses: peter-evans/create-pull-request@v7
179199
with:
180200
title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
181-
body: |
201+
body: >
182202
This is an automated PR to merge library subtree updates
183-
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
184-
to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
203+
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.CURRENT_COMMIT_HASH }})
204+
to ${{ env.NEXT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.NEXT_COMMIT_HASH }}), inclusive.
185205
This is a clean merge, no conflicts were detected.
206+
**Do not remove or edit the following annotations:**
207+
208+
git-subtree-dir: library
209+
210+
git-subtree-split: ${{ env.NEW_SUBTREE_HEAD }}
186211
branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
187212
delete-branch: true
188213
base: main
@@ -193,12 +218,17 @@ jobs:
193218
uses: peter-evans/create-pull-request@v7
194219
with:
195220
title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
196-
body: |
221+
body: >
197222
This is an automated PR to merge library subtree updates
198-
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
199-
to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}) (inclusive)
223+
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.CURRENT_COMMIT_HASH }})
224+
to ${{ env.NEXT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.NEXT_COMMIT_HASH }}) (inclusive)
200225
into main. `git merge` resulted in conflicts, which require manual resolution.
201226
Files were commited with merge conflict markers.
227+
**Do not remove or edit the following annotations:**
228+
229+
git-subtree-dir: library
230+
231+
git-subtree-split: ${{ env.NEW_SUBTREE_HEAD }}
202232
branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
203233
delete-branch: true
204234
base: main

‎doc/mdbook-metrics/src/main.rs‎

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,25 @@ fn run_kani_metrics_script() -> Result<(), Error> {
4444
Command::new("python")
4545
.args(&[
4646
"kani_std_analysis.py",
47+
"--crate",
48+
"core",
49+
"--metrics-file",
50+
"metrics-data-core.json",
51+
"--plot-only",
52+
"--plot-dir",
53+
&tools_path.to_string_lossy(),
54+
])
55+
.stdout(std::process::Stdio::null())
56+
.stderr(std::process::Stdio::null())
57+
.status()?;
58+
59+
Command::new("python")
60+
.args(&[
61+
"kani_std_analysis.py",
62+
"--crate",
63+
"std",
64+
"--metrics-file",
65+
"metrics-data-std.json",
4766
"--plot-only",
4867
"--plot-dir",
4968
&tools_path.to_string_lossy(),
@@ -83,12 +102,19 @@ fn add_graphs(chapter: &mut Chapter) {
83102
84103
Note that these metrics are for x86-64 architectures.
85104
86-
## `core`
105+
### `core`
87106
![Unsafe Metrics](core_unsafe_metrics.png)
88107
89108
![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
90109
91110
![Safe Metrics](core_safe_metrics.png)
111+
112+
### `std`
113+
![Unsafe Metrics](std_unsafe_metrics.png)
114+
115+
![Safe Abstractions Metrics](std_safe_abstractions_metrics.png)
116+
117+
![Safe Metrics](std_safe_metrics.png)
92118
"#;
93119

94120
chapter.content.push_str(new_content);

‎doc/src/challenges/0006-nonnull.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
# Challenge 6: Safety of NonNull
22

3-
- **Status:** Open
3+
- **Status:** Resolved
44
- **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
55
- **Start date:** *2024/08/16*
66
- **End date:** *2025/04/10*
77
- **Reward:** *N/A*
8-
8+
- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), [Dhvani Kapadia](https://github.com/Dhvani-Kapadia) and [Jiun Chi Yang](https://github.com/Jimmycreative)
99
-------------------
1010

1111

‎doc/src/challenges/0008-smallsort.md‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,7 @@
1111

1212
## Goal
1313

14-
The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting
15-
algorithms optimized for slices with small lengths.
14+
The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting algorithms with optimized implementations for slices with small lengths.
1615
In this challenge, the goal is to, first prove the memory safety of the public functions in the `smallsort` module, and, second, write contracts for them to
1716
show that the sorting algorithms actually sort the slices.
1817

‎doc/src/challenges/0012-nonzero.md‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,6 @@ Verify the safety of the following functions and methods (all located within `co
7373
| `from_mut` |
7474
| `from_mut_unchecked` |
7575

76-
You are not required to write correctness contracts for these methods (e.g., for `max`, ensuring that the `result` is indeed the maximum of the inputs), but it would be great to do so!
7776

7877
### List of UBs
7978

‎doc/src/challenges/0014-convert-num.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
# Challenge 14: Safety of Primitive Conversions
22

3-
- **Status:** Open
4-
- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220
3+
- **Status:** Resolved
4+
- **Tracking Issue:** [#220](https://github.com/model-checking/verify-rust-std/issues/220)
55
- **Start date:** 2024/12/15
66
- **End date:** 2025/2/28
77
- **Prize:** *TBD*
8-
8+
- **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
99
-------------------
1010

1111
## Goal

‎doc/src/challenges/0015-intrinsics-simd.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
- **Status:** Open
44
- **Reward:**
55
- **Solution:**
6-
- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/173
6+
- **Tracking Issue:** [#173](https://github.com/model-checking/verify-rust-std/issues/173)
77
- **Start date:** 2025/02/01
88
- **End date:** 2025/08/01
99

‎library/Cargo.lock‎

Lines changed: 36 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎library/Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ members = [
88
]
99

1010
exclude = [
11+
"literal-escaper",
1112
# stdarch has its own Cargo workspace
1213
"stdarch",
1314
"windows_targets"

‎library/alloc/Cargo.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ repository = "https://github.com/rust-lang/rust.git"
88
description = "The Rust core allocation and collections library"
99
autotests = false
1010
autobenches = false
11-
edition = "2021"
11+
edition = "2024"
1212

1313
[lib]
1414
test = false

0 commit comments

Comments
 (0)