Skip to content

Commit 7437d1e

Browse files
thanhnguyen-awsthanhnguyen-aws
authored
Merge branch 'model-checking:main' into morechallenges
2 parents 4a3a0e6 + eef04d8 commit 7437d1e

File tree

23 files changed

+9940
-0
lines changed

23 files changed

+9940
-0
lines changed

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

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
name: Subtree Update
2+
3+
on:
4+
schedule:
5+
- cron: '0 14 * * *' # Run at 14:00 UTC every day
6+
workflow_dispatch:
7+
8+
defaults:
9+
run:
10+
shell: bash
11+
12+
jobs:
13+
update-subtree-library:
14+
runs-on: ubuntu-latest
15+
16+
steps:
17+
- name: Checkout Repository
18+
uses: actions/checkout@v4
19+
with:
20+
fetch-depth: 0
21+
path: verify-rust-std
22+
submodules: true
23+
24+
- name: Checkout Kani
25+
uses: actions/checkout@v4
26+
with:
27+
repository: model-checking/kani
28+
path: kani-tmp
29+
30+
- name: Checkout Rust
31+
uses: actions/checkout@v4
32+
with:
33+
repository: rust-lang/rust
34+
fetch-depth: 0
35+
path: rust-tmp
36+
37+
- name: Checkout git-filter-repo
38+
uses: actions/checkout@v4
39+
with:
40+
repository: newren/git-filter-repo
41+
path: git-filter-repo
42+
43+
- name: Fetch toolchain versions
44+
run: |
45+
CURRENT_TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' verify-rust-std/rust-toolchain.toml)
46+
NEXT_TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' kani-tmp/rust-toolchain.toml)
47+
CURRENT_COMMIT_HASH=$(curl https://static.rust-lang.org/dist/$CURRENT_TOOLCHAIN_DATE/channel-rust-nightly-git-commit-hash.txt)
48+
NEXT_COMMIT_HASH=$(curl https://static.rust-lang.org/dist/$NEXT_TOOLCHAIN_DATE/channel-rust-nightly-git-commit-hash.txt)
49+
if [ -z "$CURRENT_COMMIT_HASH" ]; then
50+
echo "Could not find current commit hash on static.rust-lang.org"
51+
exit 1
52+
fi
53+
if [ -z "$NEXT_COMMIT_HASH" ]; then
54+
echo "Could not find next commit hash on static.rust-lang.org"
55+
exit 1
56+
fi
57+
echo "CURRENT_TOOLCHAIN_DATE=${CURRENT_TOOLCHAIN_DATE}" >> $GITHUB_ENV
58+
echo "NEXT_TOOLCHAIN_DATE=${NEXT_TOOLCHAIN_DATE}" >> $GITHUB_ENV
59+
echo "CURRENT_COMMIT_HASH=${CURRENT_COMMIT_HASH}" >> $GITHUB_ENV
60+
echo "NEXT_COMMIT_HASH=${NEXT_COMMIT_HASH}" >> $GITHUB_ENV
61+
62+
- name: Update subtree/library locally
63+
run: |
64+
cd rust-tmp
65+
66+
# Ensure "upstream/master" branch contains the target commit
67+
if ! git show ${NEXT_COMMIT_HASH} --oneline --no-patch; then
68+
echo "Rust commit ${NEXT_COMMIT_HASH} cannot be found."
69+
exit 1
70+
fi
71+
72+
git checkout ${NEXT_COMMIT_HASH}
73+
../git-filter-repo/git-filter-repo --subdirectory-filter library --force
74+
git checkout -b subtree/library
75+
76+
cd ../verify-rust-std
77+
git remote add rust-filtered ../rust-tmp/
78+
git fetch rust-filtered
79+
git checkout -b subtree/library rust-filtered/subtree/library
80+
SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
81+
UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
82+
UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
83+
if [ "${UPSTREAM_HEAD}" = "${UPSTREAM_FROM}" ]; then
84+
echo "Nothing to do, ${UPSTREAM_FROM} matches ${UPSTREAM_HEAD} (${SUBTREE_HEAD_MSG})"
85+
echo "MERGE_CONFLICTS=noop" >> $GITHUB_ENV
86+
else
87+
git branch --set-upstream-to=origin/subtree/library
88+
git -c user.name=gitbot -c user.email=git@bot rebase
89+
echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
90+
fi
91+
92+
- name: Create Pull Request
93+
if: ${{ env.MERGE_CONFLICTS != 'noop' }}
94+
uses: peter-evans/create-pull-request@v7
95+
with:
96+
title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
97+
body: |
98+
This is an automated PR to update the subtree/library branch to the changes
99+
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
100+
to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
101+
branch: update-subtree/library
102+
delete-branch: true
103+
base: subtree/library
104+
path: verify-rust-std
105+
106+
- name: Merge subtree/library changes
107+
if: ${{ env.MERGE_CONFLICTS != 'noop' }}
108+
run: |
109+
cd verify-rust-std
110+
git checkout main
111+
112+
# This command may fail, which will require human intervention.
113+
if ! git \
114+
-c user.name=gitbot -c user.email=git@bot \
115+
subtree merge --prefix=library update-subtree/library --squash; then
116+
echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
117+
git -c user.name=gitbot -c user.email=git@bot commit -a -m "Merge from $NEXT_COMMIT_HASH with conflicts"
118+
else
119+
echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
120+
fi
121+
122+
sed -i "s/^channel = \"nightly-.*\"/channel = \"${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
123+
git -c user.name=gitbot -c user.email=git@bot \
124+
commit -m "Update toolchain to ${NEXT_TOOLCHAIN_DATE}" rust-toolchain.toml
125+
126+
- name: Create Pull Request without conflicts
127+
if: ${{ env.MERGE_CONFLICTS == 'no' }}
128+
uses: peter-evans/create-pull-request@v7
129+
with:
130+
title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
131+
body: |
132+
This is an automated PR to merge library subtree updates
133+
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
134+
to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
135+
This is a clean merge, no conflicts were detected.
136+
branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
137+
delete-branch: true
138+
base: main
139+
path: verify-rust-std
140+
141+
- name: Create Pull Request with conflicts
142+
if: ${{ env.MERGE_CONFLICTS == 'yes' }}
143+
uses: peter-evans/create-pull-request@v7
144+
with:
145+
title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
146+
body: |
147+
This is an automated PR to merge library subtree updates
148+
from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
149+
to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}) (inclusive)
150+
into main. `git merge` resulted in conflicts, which require manual resolution.
151+
Files were commited with merge conflict markers.
152+
branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
153+
delete-branch: true
154+
base: main
155+
path: verify-rust-std

‎.github/workflows/verifast-negative.yml‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
# This workflow runs some negative VeriFast test cases, to ensure
2+
# that VeriFast actually catches bugs.
3+
4+
name: VeriFast (negative)
5+
6+
on:
7+
workflow_dispatch:
8+
merge_group:
9+
pull_request:
10+
branches: [ main ]
11+
push:
12+
paths:
13+
- 'library/**'
14+
- '.github/workflows/verifast.yml'
15+
- 'verifast-proofs/**'
16+
17+
defaults:
18+
run:
19+
shell: bash
20+
21+
jobs:
22+
check-verifast-on-std:
23+
name: Verify std library
24+
runs-on: ubuntu-latest
25+
26+
steps:
27+
- name: Checkout Repository
28+
uses: actions/checkout@v4
29+
30+
- name: Install VeriFast
31+
run: |
32+
cd ~
33+
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
34+
# https://github.com/verifast/verifast/attestations/4911733
35+
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
36+
tar xf verifast-25.02-linux.tar.gz
37+
38+
- name: Install the Rust toolchain used by VeriFast
39+
run: rustup toolchain install nightly-2024-11-23
40+
41+
- name: Run VeriFast Verification
42+
run: |
43+
export PATH=~/verifast-25.02/bin:$PATH
44+
cd verifast-proofs
45+
mysh check-verifast-proofs-negative.mysh

‎.github/workflows/verifast.yml‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
name: VeriFast
2+
3+
on:
4+
workflow_dispatch:
5+
merge_group:
6+
pull_request:
7+
branches: [ main ]
8+
push:
9+
paths:
10+
- 'library/**'
11+
- '.github/workflows/verifast.yml'
12+
- 'verifast-proofs/**'
13+
14+
defaults:
15+
run:
16+
shell: bash
17+
18+
jobs:
19+
check-verifast-on-std:
20+
name: Verify std library
21+
runs-on: ubuntu-latest
22+
23+
steps:
24+
- name: Checkout Repository
25+
uses: actions/checkout@v4
26+
27+
- name: Install VeriFast
28+
run: |
29+
cd ~
30+
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
31+
# https://github.com/verifast/verifast/attestations/4911733
32+
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
33+
tar xf verifast-25.02-linux.tar.gz
34+
35+
- name: Install the Rust toolchain used by VeriFast
36+
run: rustup toolchain install nightly-2024-11-23
37+
38+
- name: Run VeriFast Verification
39+
run: |
40+
export PATH=~/verifast-25.02/bin:$PATH
41+
cd verifast-proofs
42+
mysh check-verifast-proofs.mysh

‎doc/src/SUMMARY.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
- [Verification Tools](./tools.md)
1010
- [Kani](./tools/kani.md)
1111
- [GOTO Transcoder](./tools/goto-transcoder.md)
12+
- [VeriFast](./tools/verifast.md)
1213

1314
---
1415

‎doc/src/tools.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
1313
|---------------------|-------|
1414
| Kani Rust Verifier | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml) |
1515
| GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml) |
16+
| VeriFast for Rust | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml) |
1617

1718

1819

0 commit comments

Comments
 (0)