Merge remote-tracking branch 'origin/main' into align-harness

.github/workflows/kani.yml

@@ -9,6 +9,7 @@ on:
  paths:
  - 'library/**'
  - '.github/workflows/kani.yml'
+ - 'scripts/check_kani.sh'
 
 defaults:
  run:
@@ -30,32 +31,8 @@ jobs:
  - name: Checkout Library
  uses: actions/checkout@v4
  with:
- path: verify-rust-std
+ path: head
  submodules: true
 
- # We currently build Kani from a branch that tracks a rustc version compatible with this library version.
- - name: Checkout `Kani`
- uses: actions/checkout@v4
- with:
- repository: model-checking/kani
- path: kani
- ref: features/verify-rust-std
-
- - name: Setup Dependencies
- working-directory: kani
- run: |
- ./scripts/setup/${{ matrix.base }}/install_deps.sh
-
- - name: Build `Kani`
- working-directory: kani
- run: |
- cargo build-dev --release
- echo "$(pwd)/scripts" >> $GITHUB_PATH
-
- - name: Run tests
- working-directory: verify-rust-std
- env:
- RUST_BACKTRACE: 1
- run: |
- kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
- -Z mem-predicates -Z ptr-to-ref-cast-checks
+ - name: Run Kani Script
+ run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head

.github/workflows/rustc.yml

@@ -11,6 +11,7 @@ on:
  - 'library/**'
  - 'rust-toolchain.toml'
  - '.github/workflows/rustc.yml'
+ - 'scripts/check_rustc.sh'
 
 defaults:
  run:
@@ -29,35 +30,5 @@ jobs:
  with:
  path: head
 
- - name: Checkout `upstream/master`
- uses: actions/checkout@v4
- with:
- repository: rust-lang/rust
- path: upstream
- fetch-depth: 0
- submodules: true
-
- # Run rustc twice in case the toolchain needs to be installed.
- # Retrieve the commit id from the `rustc --version`. Output looks like:
- # `rustc 1.80.0-nightly (84b40fc90 2024-05-27)`
- - name: Checkout matching commit
- run: |
- cd head
- rustc --version
- COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
- cd ../upstream
- git checkout ${COMMIT_ID}
-
- - name: Copy Library
- run: |
- rm -rf upstream/library
- cp -r head/library upstream
-
- - name: Run tests
- working-directory: upstream
- env:
- # Avoid error due to unexpected `cfg`.
- RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
- run: |
- ./configure --set=llvm.download-ci-llvm=true
- ./x test --stage 0 library/std
+ - name: Run rustc script
+ run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head

scripts/check_kani.sh

@@ -0,0 +1,55 @@
+#!/bin/bash
+
+set -e
+
+# Set the working directories
+VERIFY_RUST_STD_DIR="$1"
+KANI_DIR=$(mktemp -d)
+
+RUNNER_TEMP=$(mktemp -d)
+
+# Get the OS name
+os_name=$(uname -s)
+
+# Checkout your local repository
+echo "Checking out local repository..."
+echo
+cd "$VERIFY_RUST_STD_DIR"
+
+# Checkout the Kani repository
+echo "Checking out Kani repository..."
+echo
+git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR"
+
+# Check the OS and
+# Setup dependencies for Kani
+echo "Setting up dependencies for Kani..."
+echo
+cd "$KANI_DIR"
+if [ "$os_name" == "Linux" ]; then
+ ./scripts/setup/ubuntu/install_deps.sh
+elif [ "$os_name" == "Darwin" ]; then
+ ./scripts/setup/macos/install_deps.sh
+else
+ echo "Unknown operating system"
+fi
+
+# Build Kani
+echo "Building Kani..."
+echo
+cargo build-dev --release
+# echo "$(pwd)/scripts" >> $PATH
+
+# Run tests
+echo "Running tests..."
+echo
+cd "$VERIFY_RUST_STD_DIR"
+$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
+
+echo "Tests completed."
+echo
+
+# Clean up the Kani directory (optional)
+rm -rf "$KANI_DIR"
+rm -rf "$RUNNER_TEMP"
+# rm -rf "$VERIFY_RUST_STD_DIR"

scripts/check_rustc.sh

@@ -0,0 +1,44 @@
+#!/bin/bash
+
+set -e
+
+# Set the working directory for your local repository
+HEAD_DIR=$1
+
+# Temporary directory for upstream repository
+TEMP_DIR=$(mktemp -d)
+
+# Checkout your local repository
+echo "Checking out local repository..."
+cd "$HEAD_DIR"
+
+# Get the commit ID from rustc --version
+echo "Retrieving commit ID..."
+COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
+echo "$COMMIT_ID for rustc is"
+
+# Clone the rust-lang/rust repository
+echo "Cloning rust-lang/rust repository..."
+git clone https://github.com/rust-lang/rust.git "$TEMP_DIR/upstream"
+
+# Checkout the specific commit
+echo "Checking out commit $COMMIT_ID..."
+cd "$TEMP_DIR/upstream"
+git checkout "$COMMIT_ID"
+
+# Copy your library to the upstream directory
+echo "Copying library to upstream directory..."
+rm -rf "$TEMP_DIR/upstream/library"
+cp -r "$HEAD_DIR/library" "$TEMP_DIR/upstream"
+
+# Run the tests
+cd "$TEMP_DIR/upstream"
+export RUSTFLAGS="--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
+echo "Running tests..."
+./configure --set=llvm.download-ci-llvm=true
+./x test --stage 0 library/std
+
+echo "Tests completed."
+
+# Clean up the temporary directory
+rm -rf "$TEMP_DIR"

scripts/pull_from_upstream.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -eux
+
+cd $1
+
+TOOLCHAIN_DATE=$2
+COMMIT_HASH=$3
+
+# The checkout and pull itself needs to happen in sync with features/verify-rust-std
+# Often times rust is going to be ahead of kani in terms of the toolchain, and both need to point to
+# the same commit
+SYNC_BRANCH="sync-$TOOLCHAIN_DATE" && echo "--- Fork branch: ${SYNC_BRANCH} ---"
+# # 1. Update the upstream/master branch with the latest changes
+git fetch upstream
+git checkout $COMMIT_HASH
+
+# # 2. Update the subtree branch
+git subtree split --prefix=library --onto subtree/library -b subtree/library
+# 3. Update main
+git fetch origin
+git checkout -b ${SYNC_BRANCH} origin/main
+git subtree merge --prefix=library subtree/library --squash
+
+# TODO: Update origin/subtree/library as well after the process by pushing to it