Skip to content

Commit 79f2d79

Browse files
tautschnigtautschnig
committed
Merge remote-tracking branch 'origin/main' into align-harness
2 parents a91dcad + ec6d98e commit 79f2d79

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)