Skip to content

Commit ec6d98e

Browse files
jaisnanjaisnan
authored
Add scripts for local subtree update (#46)
The CI job for subtree update timesout because it takes more than 6hrs. While we figure out how to solve that problem, this process makes sure there's an automated way for anyone to update the repo's subtree hosted library, with a one click script/command. The structure of this process follows the (would-be) CI workflow closely i.e 1. Call `scripts/run_update_with_checks.sh` 2. This script in turn calls the other scripts in order 3. Pull and update local `subtree/library` with updates from [rust-lang](https://github.com/rust-lang/rust) 4. Merge `subtree/library` onto local `SYNC-{DATE}` where {DATE} is the date tracked by Kani's `features/verify-rust-std` branch. 5. Update toolchain to the date tracked by kani's `features/verify-rust-std` branch and commit. 6. Test this branch with `check_rustc` which checks for compilation compatibility of the updated library and `check_kani` which checks that Kani's injected harnesses verify as expected. ## Call-out This currently only automates the process of updating the subtree and running all checks on it. After that, the process of issuing a PR from the SYNC-DATE branch of the local repo is still in the responsibility of the dev running the script. There is ongoing work to automate the process of writing/pushing branches as well. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 0be79d6 commit ec6d98e

File tree

7 files changed

+347
-59
lines changed

7 files changed

+347
-59
lines changed

‎.github/workflows/kani.yml

+4-27
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ on:
99
paths:
1010
- 'library/**'
1111
- '.github/workflows/kani.yml'
12+
- 'scripts/check_kani.sh'
1213

1314
defaults:
1415
run:
@@ -30,32 +31,8 @@ jobs:
3031
- name: Checkout Library
3132
uses: actions/checkout@v4
3233
with:
33-
path: verify-rust-std
34+
path: head
3435
submodules: true
3536

36-
# We currently build Kani from a branch that tracks a rustc version compatible with this library version.
37-
- name: Checkout `Kani`
38-
uses: actions/checkout@v4
39-
with:
40-
repository: model-checking/kani
41-
path: kani
42-
ref: features/verify-rust-std
43-
44-
- name: Setup Dependencies
45-
working-directory: kani
46-
run: |
47-
./scripts/setup/${{ matrix.base }}/install_deps.sh
48-
49-
- name: Build `Kani`
50-
working-directory: kani
51-
run: |
52-
cargo build-dev --release
53-
echo "$(pwd)/scripts" >> $GITHUB_PATH
54-
55-
- name: Run tests
56-
working-directory: verify-rust-std
57-
env:
58-
RUST_BACKTRACE: 1
59-
run: |
60-
kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
61-
-Z mem-predicates -Z ptr-to-ref-cast-checks
37+
- name: Run Kani Script
38+
run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head

‎.github/workflows/rustc.yml

+3-32
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ on:
1111
- 'library/**'
1212
- 'rust-toolchain.toml'
1313
- '.github/workflows/rustc.yml'
14+
- 'scripts/check_rustc.sh'
1415

1516
defaults:
1617
run:
@@ -29,35 +30,5 @@ jobs:
2930
with:
3031
path: head
3132

32-
- name: Checkout `upstream/master`
33-
uses: actions/checkout@v4
34-
with:
35-
repository: rust-lang/rust
36-
path: upstream
37-
fetch-depth: 0
38-
submodules: true
39-
40-
# Run rustc twice in case the toolchain needs to be installed.
41-
# Retrieve the commit id from the `rustc --version`. Output looks like:
42-
# `rustc 1.80.0-nightly (84b40fc90 2024-05-27)`
43-
- name: Checkout matching commit
44-
run: |
45-
cd head
46-
rustc --version
47-
COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
48-
cd ../upstream
49-
git checkout ${COMMIT_ID}
50-
51-
- name: Copy Library
52-
run: |
53-
rm -rf upstream/library
54-
cp -r head/library upstream
55-
56-
- name: Run tests
57-
working-directory: upstream
58-
env:
59-
# Avoid error due to unexpected `cfg`.
60-
RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
61-
run: |
62-
./configure --set=llvm.download-ci-llvm=true
63-
./x test --stage 0 library/std
33+
- name: Run rustc script
34+
run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head

‎scripts/check_kani.sh

+55
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
# Set the working directories
6+
VERIFY_RUST_STD_DIR="$1"
7+
KANI_DIR=$(mktemp -d)
8+
9+
RUNNER_TEMP=$(mktemp -d)
10+
11+
# Get the OS name
12+
os_name=$(uname -s)
13+
14+
# Checkout your local repository
15+
echo "Checking out local repository..."
16+
echo
17+
cd "$VERIFY_RUST_STD_DIR"
18+
19+
# Checkout the Kani repository
20+
echo "Checking out Kani repository..."
21+
echo
22+
git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR"
23+
24+
# Check the OS and
25+
# Setup dependencies for Kani
26+
echo "Setting up dependencies for Kani..."
27+
echo
28+
cd "$KANI_DIR"
29+
if [ "$os_name" == "Linux" ]; then
30+
./scripts/setup/ubuntu/install_deps.sh
31+
elif [ "$os_name" == "Darwin" ]; then
32+
./scripts/setup/macos/install_deps.sh
33+
else
34+
echo "Unknown operating system"
35+
fi
36+
37+
# Build Kani
38+
echo "Building Kani..."
39+
echo
40+
cargo build-dev --release
41+
# echo "$(pwd)/scripts" >> $PATH
42+
43+
# Run tests
44+
echo "Running tests..."
45+
echo
46+
cd "$VERIFY_RUST_STD_DIR"
47+
$KANI_DIR/scripts/kani verify-std -Z unstable-options $VERIFY_RUST_STD_DIR/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates -Z ptr-to-ref-cast-checks
48+
49+
echo "Tests completed."
50+
echo
51+
52+
# Clean up the Kani directory (optional)
53+
rm -rf "$KANI_DIR"
54+
rm -rf "$RUNNER_TEMP"
55+
# rm -rf "$VERIFY_RUST_STD_DIR"

‎scripts/check_rustc.sh

+44
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
# Set the working directory for your local repository
6+
HEAD_DIR=$1
7+
8+
# Temporary directory for upstream repository
9+
TEMP_DIR=$(mktemp -d)
10+
11+
# Checkout your local repository
12+
echo "Checking out local repository..."
13+
cd "$HEAD_DIR"
14+
15+
# Get the commit ID from rustc --version
16+
echo "Retrieving commit ID..."
17+
COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
18+
echo "$COMMIT_ID for rustc is"
19+
20+
# Clone the rust-lang/rust repository
21+
echo "Cloning rust-lang/rust repository..."
22+
git clone https://github.com/rust-lang/rust.git "$TEMP_DIR/upstream"
23+
24+
# Checkout the specific commit
25+
echo "Checking out commit $COMMIT_ID..."
26+
cd "$TEMP_DIR/upstream"
27+
git checkout "$COMMIT_ID"
28+
29+
# Copy your library to the upstream directory
30+
echo "Copying library to upstream directory..."
31+
rm -rf "$TEMP_DIR/upstream/library"
32+
cp -r "$HEAD_DIR/library" "$TEMP_DIR/upstream"
33+
34+
# Run the tests
35+
cd "$TEMP_DIR/upstream"
36+
export RUSTFLAGS="--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
37+
echo "Running tests..."
38+
./configure --set=llvm.download-ci-llvm=true
39+
./x test --stage 0 library/std
40+
41+
echo "Tests completed."
42+
43+
# Clean up the temporary directory
44+
rm -rf "$TEMP_DIR"

‎scripts/pull_from_upstream.sh

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#!/bin/bash
2+
3+
set -eux
4+
5+
cd $1
6+
7+
TOOLCHAIN_DATE=$2
8+
COMMIT_HASH=$3
9+
10+
# The checkout and pull itself needs to happen in sync with features/verify-rust-std
11+
# Often times rust is going to be ahead of kani in terms of the toolchain, and both need to point to
12+
# the same commit
13+
SYNC_BRANCH="sync-$TOOLCHAIN_DATE" && echo "--- Fork branch: ${SYNC_BRANCH} ---"
14+
# # 1. Update the upstream/master branch with the latest changes
15+
git fetch upstream
16+
git checkout $COMMIT_HASH
17+
18+
# # 2. Update the subtree branch
19+
git subtree split --prefix=library --onto subtree/library -b subtree/library
20+
# 3. Update main
21+
git fetch origin
22+
git checkout -b ${SYNC_BRANCH} origin/main
23+
git subtree merge --prefix=library subtree/library --squash
24+
25+
# TODO: Update origin/subtree/library as well after the process by pushing to it

0 commit comments

Comments
 (0)