diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index e2783264cf81a..da0928998976c 100644 --- a/.github/workflows/kani.yml +++ b/.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 diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml index 1903dd98e5b2c..112c1f58f7ce8 100644 --- a/.github/workflows/rustc.yml +++ b/.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 diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh new file mode 100644 index 0000000000000..f381c1a376c83 --- /dev/null +++ b/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" diff --git a/scripts/check_rustc.sh b/scripts/check_rustc.sh new file mode 100644 index 0000000000000..610f6157b20ce --- /dev/null +++ b/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" diff --git a/scripts/pull_from_upstream.sh b/scripts/pull_from_upstream.sh new file mode 100755 index 0000000000000..183d258837eb8 --- /dev/null +++ b/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 diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh new file mode 100755 index 0000000000000..e7419f34d4901 --- /dev/null +++ b/scripts/run_update_with_checks.sh @@ -0,0 +1,185 @@ +#!/bin/bash + +set -eux + +BASE_HOME_DIR="$(pwd)" + +# Set variables for verify-rust-std +# NOTE: This process assumes that verify-rust-std is updated automatically +# and independently +REPO_OWNER="model-checking" +REPO_NAME="kani" +BRANCH_NAME="features/verify-rust-std" +TOOLCHAIN_FILE="rust-toolchain.toml" + +# Set base as verify-rust-std's origin/main branch +BASE_REPO="https://github.com/model-checking/verify-rust-std.git" + +# Create a temporary directory +TEMP_HOME_DIR=$(mktemp -d) + +# Clone the repository into the temporary directory +git clone "$BASE_REPO" "$TEMP_HOME_DIR" +cd $TEMP_HOME_DIR + +# Function to extract commit hash and date from rustc version +get_rustc_info() { + local rustc_output=$(rustc --version --verbose) + local commit_hash=$(echo "$rustc_output" | grep 'commit-hash' | awk '{print $2}') + local commit_date=$(echo "$rustc_output" | grep 'commit-date' | awk '{print $2}') + + if [ -z "$commit_hash" ] || [ -z "$commit_date" ]; then + echo "Error: Could not extract commit hash or date from rustc output." + exit 1 + fi + + echo "$commit_hash:$commit_date" +} + +# Read the toolchain date from the rust-toolchain.toml file +read_toolchain_date() { + local toolchain_file=$TOOLCHAIN_FILE + + if [ ! -f "$toolchain_file" ]; then + echo "Error: $toolchain_file not found in the working directory." >&2 + return 1 + fi + + local toolchain_date + toolchain_date=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' ./rust-toolchain.toml) + + if [ -z "$toolchain_date" ]; then + echo "Error: Could not extract date from $toolchain_file" >&2 + return 1 + fi + + echo "$toolchain_date" +} + +# Check if a path is provided as an argument +# This is useful for local processing and debugging +if [ $# -eq 1 ]; then + REPO_PATH="$1" + echo "Using provided repository path: $REPO_PATH" + + # Ensure the provided path exists and is a git repository + if [ ! -d "$REPO_PATH/.git" ]; then + echo "Error: Provided path is not a git repository." + exit 1 + fi + + pushd $REPO_PATH + git switch $BRANCH_NAME + + # Get rustc info + RUSTC_INFO=$(get_rustc_info) + TOOLCHAIN_DATE=$(read_toolchain_date) + + if [ $? -ne 0 ]; then + exit 1 + fi + COMMIT_HASH=$(echo $RUSTC_INFO | cut -d':' -f1) + RUST_DATE=$(echo $RUSTC_INFO | cut -d':' -f2) + popd +else + # Create a temporary directory + TEMP_KANI_DIR=$(mktemp -d) + echo "Created temporary directory: $TEMP_KANI_DIR" + + # Clone the repository into the temporary directory + echo "Cloning repository..." + git clone --branch "$BRANCH_NAME" --depth 1 "https://github.com/$REPO_OWNER/$REPO_NAME.git" "$TEMP_KANI_DIR" + + # Move into this temp dir to read the toolchain + cd $TEMP_KANI_DIR + + if [ $? -ne 0 ]; then + echo "Error: Failed to clone the repository." + rm -rf "$TEMP_KANI_DIR" + exit 1 + fi + + # Get rustc info + RUSTC_INFO=$(get_rustc_info) + TOOLCHAIN_DATE=$(read_toolchain_date) + + COMMIT_HASH=$(echo $RUSTC_INFO | cut -d':' -f1) + RUST_DATE=$(echo $RUSTC_INFO | cut -d':' -f2) + + # Clean up the temporary directory + rm -rf "$TEMP_KANI_DIR" +fi + +if [ -z "$COMMIT_HASH" ]; then + echo "Could not find commit hash in rust-toolchain.toml" + exit 1 +fi + +if [ -z "$RUST_DATE" ]; then + echo "Could not find date in rust-toolchain.toml" + exit 1 +fi + +# Go to temp dir +cd $TEMP_HOME_DIR + +echo "Rust commit hash found: $COMMIT_HASH" +echo "Rust date found: $TOOLCHAIN_DATE" + +# Ensure we have the rust-lang/rust repository as a remote named "upstream" +if ! git remote | grep -q '^upstream$'; then + echo "Adding rust-lang/rust as upstream remote" + git remote add upstream https://github.com/rust-lang/rust.git +fi + + +echo "------------------------------------" +# Call the first script to update the subtree +echo "Update subtree in Main" +source $BASE_HOME_DIR/scripts/pull_from_upstream.sh "$TEMP_HOME_DIR" $TOOLCHAIN_DATE $COMMIT_HASH +OUTPUT_SCRIPT1=("$?") +if [ "${#OUTPUT_SCRIPT1[@]}" -eq 0 ]; then + echo "script1.sh failed to run." + exit 1 +else + echo "script1.sh completed successfully." +fi + +# Call the second script +echo "Running script2.sh..." +source $BASE_HOME_DIR/scripts/update_toolchain_date.sh "$TEMP_HOME_DIR" "$TOOLCHAIN_DATE" +OUTPUT_SCRIPT2=("$?") +if [ "${#OUTPUT_SCRIPT2[@]}" -eq 0 ]; then + echo "script2.sh failed to run." + exit 1 +else + echo "Update toolchain ran successfully." +fi + +# Call the third script +echo "Running script3.sh..." +source $BASE_HOME_DIR/scripts/check_rustc.sh "$TEMP_HOME_DIR" +OUTPUT_SCRIPT3=("$?") +if [ "${#OUTPUT_SCRIPT3[@]}" -eq 0 ]; then + echo "script3.sh failed to run." + exit 1 +else + echo "script3.sh completed successfully." +fi + +# Call the fourth script +echo "Running script4.sh..." +source $BASE_HOME_DIR/scripts/check_kani.sh "$TEMP_HOME_DIR" +OUTPUT_SCRIPT4=("$?") +if [ "${#OUTPUT_SCRIPT4[@]}" -eq 0 ]; then + echo "script4.sh failed to run." + exit 1 +else + echo "script4.sh completed successfully." +fi + +# TODO: Issue a Pull Request from the sync branch of the temp repo +# cd $TEMP_HOME_DIR + +# Remove the temporary directory +# rm -rf "$TEMP_DIR" diff --git a/scripts/update_toolchain_date.sh b/scripts/update_toolchain_date.sh new file mode 100755 index 0000000000000..21798932dfd3f --- /dev/null +++ b/scripts/update_toolchain_date.sh @@ -0,0 +1,31 @@ +#!/bin/bash + +# Check if the correct number of args +if [[ $# -ne 2 ]]; then + echo "Usage: $0 " + echo "$#" + exit 1 +fi + +toolchain_file="$1/rust-toolchain.toml" +new_date="$2" + +# Check if the toolchain file exists +if [[ ! -f "$toolchain_file" ]]; then + echo "Error: Toolchain file does not exist." + exit 1 +fi + +# Use sed to replace the date +sed -i.bak -E 's/^channel = "nightly-[0-9]{4}-[0-9]{2}-[0-9]{2}"$/channel = "nightly-'"$new_date"'"/' "$toolchain_file" + +# Check if the replacement was succesful +if [[ $? -eq 0 ]]; then + echo "Date succesfully updated in $toolchain_file" + rm "${toolchain_file}.bak" + + git commit -am "Update toolchain to $new_date" +else + echo "Error: Failed to update the file in $toolchain_file" + exit 1 +fi