From 97dfc23cf647276387daaf8a3041402948fcf9b4 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 26 Jul 2024 16:36:35 +0000 Subject: [PATCH 1/8] test subtree sync workflow add pull_request just for testing add push permission for testing Test without updating subtree Try within kani dir Use kani as workdir Change parsing Parse regex with path Check for toolchain file Get toolchain date Use correct hash and date Use commit hash instead make upstream pull explicit Add origin for pulling set working directory to head Fix working directory Update subtree Add --quiet Update with --quiet Add pull_from_upstream.sh Add scripts -1 Add explicit commit pull Add temp home dir Add clone from temp Add base repo Update comments clone into tempdir Add working tests --- .github/workflows/update-subtree.yml | 137 ++++++++++++++++++++ scripts/check_kani.sh | 42 +++++++ scripts/check_rustc.sh | 42 +++++++ scripts/pull_from_upstream.sh | 23 ++++ scripts/run_update_with_checks.sh | 182 +++++++++++++++++++++++++++ scripts/update_toolchain_date.sh | 31 +++++ 6 files changed, 457 insertions(+) create mode 100644 .github/workflows/update-subtree.yml create mode 100644 scripts/check_kani.sh create mode 100644 scripts/check_rustc.sh create mode 100755 scripts/pull_from_upstream.sh create mode 100755 scripts/run_update_with_checks.sh create mode 100755 scripts/update_toolchain_date.sh diff --git a/.github/workflows/update-subtree.yml b/.github/workflows/update-subtree.yml new file mode 100644 index 0000000000000..ccaf13706359c --- /dev/null +++ b/.github/workflows/update-subtree.yml @@ -0,0 +1,137 @@ +name: Sync Rust STD + +on: + push: + branches: + - '**' + workflow_dispatch: + +env: + REPO_OWNER: model-checking + REPO_NAME: kani + BRANCH_NAME: features/verify-rust-std + +jobs: + prepare: + runs-on: ${{ matrix.os }} + outputs: + commit_hash: ${{ steps.rust-info.outputs.commit_hash }} + commit_date: ${{ steps.rust-info.outputs.commit_date }} + toolchain_date: ${{ steps.toolchain-date.outputs.toolchain_date }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + steps: + - name: Checkout library + uses: actions/checkout@v3 + with: + path: head + + - name: Checkout `features/verify-rust-std` + uses: actions/checkout@v4 + with: + repository: model-checking/kani + path: kani + ref: features/verify-rust-std + + - name: Read date from rust-toolchain.toml + id: toolchain-date + working-directory: kani + run: | + TOOLCHAIN_DATE=$(grep 'channel.*=.*"nightly-' ./rust-toolchain.toml | sed -E 's/.*nightly-([0-9-]+).*/\1/') + if [ -z "$TOOLCHAIN_DATE" ]; then + echo "Error: Could not extract date from rust-toolchain file." + exit 1 + fi + echo "toolchain_date=$TOOLCHAIN_DATE" >> $GITHUB_OUTPUT + + - name: Build `Kani` + working-directory: kani + run: | + cargo build-dev --release + echo "$(pwd)/scripts" >> $GITHUB_PATH + + - name: Get Rust info + working-directory: kani + id: rust-info + run: | + RUSTC_INFO=$(rustc --version --verbose) + COMMIT_HASH=$(echo "$RUSTC_INFO" | grep 'commit-hash' | awk '{print $2}') + COMMIT_DATE=$(echo "$RUSTC_INFO" | grep 'commit-date' | awk '{print $2}') + echo "commit_hash=$COMMIT_HASH" >> $GITHUB_OUTPUT + echo "commit_date=$COMMIT_DATE" >> $GITHUB_OUTPUT + + sanity-check: + needs: prepare + runs-on: ubuntu-latest + steps: + - name: Echo gathered variables + run: | + echo "Commit Hash: ${{ needs.prepare.outputs.commit_hash }}" + echo "Commit Date: ${{ needs.prepare.outputs.commit_date }}" + echo "Toolchain Date: ${{ needs.prepare.outputs.toolchain_date }}" + + sync: + needs: prepare + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + runs-on: ${{ matrix.os }} + steps: + - name: Checkout library + uses: actions/checkout@v3 + with: + path: head + + - name: Add upstream remote and fetch specific commit + working-directory: head + run: | + git remote add upstream https://github.com/rust-lang/rust.git + git remote set-url origin https://github.com/model-checking/verify-rust-std.git + git fetch upstream ${{ needs.prepare.outputs.commit_hash }} + git remote -v + + - name: Prepare sync branch + working-directory: head + run: | + SYNC_BRANCH="sync-${{ needs.prepare.outputs.toolchain_date }}" + echo "SYNC_BRANCH=$SYNC_BRANCH" >> $GITHUB_ENV + echo "--- Fork branch: ${SYNC_BRANCH} ---" + git checkout ${{ needs.prepare.outputs.commit_hash }} + git pull upstream ${{ needs.prepare.outputs.commit_hash }} + + - name: Update and merge subtree + working-directory: head + run: | + git subtree split --prefix=library --onto subtree/library -b subtree/library --quiet + git fetch origin + git checkout -b ${{ env.SYNC_BRANCH }} origin/main + + - name: Attempt subtree merge + working-directory: head + run: | + if ! git subtree merge --prefix=library subtree/library --squash; then + echo "Merge conflict detected. Attempting automatic resolution." + + # Abort the failed merge + git merge --abort + + # Attempt the merge again with the 'ours' strategy + if git subtree merge --prefix=library subtree/library --squash -X ours; then + echo "Merge conflicts automatically resolved using 'ours' strategy." + echo "MERGE_AUTO_RESOLVED=true" >> $GITHUB_ENV + else + echo "Failed to automatically resolve merge conflicts." + echo "MERGE_FAILED=true" >> $GITHUB_ENV + exit 1 + fi + fi + + - name: Check auto-resolved changes + if: env.MERGE_AUTO_RESOLVED == 'true' + run: | + echo "Merge was auto-resolved. Here are the changes:" + git diff --name-status HEAD~1 + + # You might want to run tests or other checks here to ensure + # the auto-resolution didn't break anything diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh new file mode 100644 index 0000000000000..a3a15b27abe86 --- /dev/null +++ b/scripts/check_kani.sh @@ -0,0 +1,42 @@ +#!/bin/bash + +# Set the working directories +VERIFY_RUST_STD_DIR="$1" +KANI_DIR=$(mktemp -d) + +RUNNER_TEMP=$(mktemp -d) + +# 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" + +# Setup dependencies for Kani +echo "Setting up dependencies for Kani..." +echo +cd "$KANI_DIR" +./scripts/setup/ubuntu/install_deps.sh + +# 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 /tmp/verify-rust-std/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 "$VERIFY_RUST_STD_DIR" diff --git a/scripts/check_rustc.sh b/scripts/check_rustc.sh new file mode 100644 index 0000000000000..55ff95b396c24 --- /dev/null +++ b/scripts/check_rustc.sh @@ -0,0 +1,42 @@ +#!/bin/bash + +# 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..54ceeb3293d1e --- /dev/null +++ b/scripts/pull_from_upstream.sh @@ -0,0 +1,23 @@ +#!/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 diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh new file mode 100755 index 0000000000000..d55701a2903e7 --- /dev/null +++ b/scripts/run_update_with_checks.sh @@ -0,0 +1,182 @@ +#!/bin/bash + +set -eux + +BASE_HOME_DIR="$(pwd)" + +# TODO: Remove all relative paths, with that blob that gets the scripts dir + +# Set variables +REPO_OWNER="jaisnan" +REPO_NAME="rust-dev" +BRANCH_NAME="features/verifuy-07-21" +TOOLCHAIN_FILE="rust-toolchain.toml" + +# Set base +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 + +# 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 From 0dd0be7fd33cb887c2a2debf2af6ba64401bdf64 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 30 Jul 2024 15:08:28 +0000 Subject: [PATCH 2/8] Add todo for issuing a PR --- scripts/check_kani.sh | 2 +- scripts/run_update_with_checks.sh | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh index a3a15b27abe86..938aa23b95233 100644 --- a/scripts/check_kani.sh +++ b/scripts/check_kani.sh @@ -39,4 +39,4 @@ echo # Clean up the Kani directory (optional) rm -rf "$KANI_DIR" -rm -rf "$VERIFY_RUST_STD_DIR" +# rm -rf "$VERIFY_RUST_STD_DIR" diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh index d55701a2903e7..b0f283fa67bb5 100755 --- a/scripts/run_update_with_checks.sh +++ b/scripts/run_update_with_checks.sh @@ -4,8 +4,6 @@ set -eux BASE_HOME_DIR="$(pwd)" -# TODO: Remove all relative paths, with that blob that gets the scripts dir - # Set variables REPO_OWNER="jaisnan" REPO_NAME="rust-dev" @@ -178,5 +176,8 @@ 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" From 9ed81c482c777602a6d48003396a343f4727963c Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 30 Jul 2024 15:22:13 +0000 Subject: [PATCH 3/8] Remove timeout workflow --- .github/workflows/update-subtree.yml | 137 --------------------------- 1 file changed, 137 deletions(-) delete mode 100644 .github/workflows/update-subtree.yml diff --git a/.github/workflows/update-subtree.yml b/.github/workflows/update-subtree.yml deleted file mode 100644 index ccaf13706359c..0000000000000 --- a/.github/workflows/update-subtree.yml +++ /dev/null @@ -1,137 +0,0 @@ -name: Sync Rust STD - -on: - push: - branches: - - '**' - workflow_dispatch: - -env: - REPO_OWNER: model-checking - REPO_NAME: kani - BRANCH_NAME: features/verify-rust-std - -jobs: - prepare: - runs-on: ${{ matrix.os }} - outputs: - commit_hash: ${{ steps.rust-info.outputs.commit_hash }} - commit_date: ${{ steps.rust-info.outputs.commit_date }} - toolchain_date: ${{ steps.toolchain-date.outputs.toolchain_date }} - strategy: - matrix: - os: [ubuntu-latest, macos-latest] - steps: - - name: Checkout library - uses: actions/checkout@v3 - with: - path: head - - - name: Checkout `features/verify-rust-std` - uses: actions/checkout@v4 - with: - repository: model-checking/kani - path: kani - ref: features/verify-rust-std - - - name: Read date from rust-toolchain.toml - id: toolchain-date - working-directory: kani - run: | - TOOLCHAIN_DATE=$(grep 'channel.*=.*"nightly-' ./rust-toolchain.toml | sed -E 's/.*nightly-([0-9-]+).*/\1/') - if [ -z "$TOOLCHAIN_DATE" ]; then - echo "Error: Could not extract date from rust-toolchain file." - exit 1 - fi - echo "toolchain_date=$TOOLCHAIN_DATE" >> $GITHUB_OUTPUT - - - name: Build `Kani` - working-directory: kani - run: | - cargo build-dev --release - echo "$(pwd)/scripts" >> $GITHUB_PATH - - - name: Get Rust info - working-directory: kani - id: rust-info - run: | - RUSTC_INFO=$(rustc --version --verbose) - COMMIT_HASH=$(echo "$RUSTC_INFO" | grep 'commit-hash' | awk '{print $2}') - COMMIT_DATE=$(echo "$RUSTC_INFO" | grep 'commit-date' | awk '{print $2}') - echo "commit_hash=$COMMIT_HASH" >> $GITHUB_OUTPUT - echo "commit_date=$COMMIT_DATE" >> $GITHUB_OUTPUT - - sanity-check: - needs: prepare - runs-on: ubuntu-latest - steps: - - name: Echo gathered variables - run: | - echo "Commit Hash: ${{ needs.prepare.outputs.commit_hash }}" - echo "Commit Date: ${{ needs.prepare.outputs.commit_date }}" - echo "Toolchain Date: ${{ needs.prepare.outputs.toolchain_date }}" - - sync: - needs: prepare - strategy: - matrix: - os: [ubuntu-latest, macos-latest] - runs-on: ${{ matrix.os }} - steps: - - name: Checkout library - uses: actions/checkout@v3 - with: - path: head - - - name: Add upstream remote and fetch specific commit - working-directory: head - run: | - git remote add upstream https://github.com/rust-lang/rust.git - git remote set-url origin https://github.com/model-checking/verify-rust-std.git - git fetch upstream ${{ needs.prepare.outputs.commit_hash }} - git remote -v - - - name: Prepare sync branch - working-directory: head - run: | - SYNC_BRANCH="sync-${{ needs.prepare.outputs.toolchain_date }}" - echo "SYNC_BRANCH=$SYNC_BRANCH" >> $GITHUB_ENV - echo "--- Fork branch: ${SYNC_BRANCH} ---" - git checkout ${{ needs.prepare.outputs.commit_hash }} - git pull upstream ${{ needs.prepare.outputs.commit_hash }} - - - name: Update and merge subtree - working-directory: head - run: | - git subtree split --prefix=library --onto subtree/library -b subtree/library --quiet - git fetch origin - git checkout -b ${{ env.SYNC_BRANCH }} origin/main - - - name: Attempt subtree merge - working-directory: head - run: | - if ! git subtree merge --prefix=library subtree/library --squash; then - echo "Merge conflict detected. Attempting automatic resolution." - - # Abort the failed merge - git merge --abort - - # Attempt the merge again with the 'ours' strategy - if git subtree merge --prefix=library subtree/library --squash -X ours; then - echo "Merge conflicts automatically resolved using 'ours' strategy." - echo "MERGE_AUTO_RESOLVED=true" >> $GITHUB_ENV - else - echo "Failed to automatically resolve merge conflicts." - echo "MERGE_FAILED=true" >> $GITHUB_ENV - exit 1 - fi - fi - - - name: Check auto-resolved changes - if: env.MERGE_AUTO_RESOLVED == 'true' - run: | - echo "Merge was auto-resolved. Here are the changes:" - git diff --name-status HEAD~1 - - # You might want to run tests or other checks here to ensure - # the auto-resolution didn't break anything From dd11ad5364110ce897d4e1c5afe4d0a9c121b109 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 30 Jul 2024 15:25:53 +0000 Subject: [PATCH 4/8] Add clarifying comments, and update Global Constants --- scripts/pull_from_upstream.sh | 2 ++ scripts/run_update_with_checks.sh | 12 +++++++----- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/scripts/pull_from_upstream.sh b/scripts/pull_from_upstream.sh index 54ceeb3293d1e..183d258837eb8 100755 --- a/scripts/pull_from_upstream.sh +++ b/scripts/pull_from_upstream.sh @@ -21,3 +21,5 @@ git subtree split --prefix=library --onto subtree/library -b subtree/library 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 index b0f283fa67bb5..e7419f34d4901 100755 --- a/scripts/run_update_with_checks.sh +++ b/scripts/run_update_with_checks.sh @@ -4,13 +4,15 @@ set -eux BASE_HOME_DIR="$(pwd)" -# Set variables -REPO_OWNER="jaisnan" -REPO_NAME="rust-dev" -BRANCH_NAME="features/verifuy-07-21" +# 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 +# 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 From 016b92635e533a09b78cc84f39c7ed738d311a0e Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 30 Jul 2024 15:26:39 +0000 Subject: [PATCH 5/8] Delete runner temp --- scripts/check_kani.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh index 938aa23b95233..d760c2aebaf95 100644 --- a/scripts/check_kani.sh +++ b/scripts/check_kani.sh @@ -39,4 +39,5 @@ echo # Clean up the Kani directory (optional) rm -rf "$KANI_DIR" +rm -rf "$RUNNER_TEMP" # rm -rf "$VERIFY_RUST_STD_DIR" From ff7f6d257d3de60110650ccc4ea57468f88a6a4b Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 30 Jul 2024 22:48:04 +0000 Subject: [PATCH 6/8] test CI with scripts Test with github workspace Try with bash Run ls Try with path expanded Fix path to script Fix path to library Fix script Check with verify-rst-std Check workflow Check path Fix path change path to head --- .github/workflows/kani.yml | 31 ++++--------------------------- .github/workflows/rustc.yml | 35 +++-------------------------------- scripts/check_kani.sh | 2 +- 3 files changed, 8 insertions(+), 60 deletions(-) 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 index d760c2aebaf95..898dd9393ba5b 100644 --- a/scripts/check_kani.sh +++ b/scripts/check_kani.sh @@ -32,7 +32,7 @@ cargo build-dev --release echo "Running tests..." echo cd "$VERIFY_RUST_STD_DIR" -$KANI_DIR/scripts/kani verify-std -Z unstable-options /tmp/verify-rust-std/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates -Z ptr-to-ref-cast-checks +$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 From 8935fad0ac465514ce00026c0e83c425f2506f20 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 31 Jul 2024 00:14:06 +0000 Subject: [PATCH 7/8] Check OS for kani --- scripts/check_kani.sh | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh index 898dd9393ba5b..03861ea03bf26 100644 --- a/scripts/check_kani.sh +++ b/scripts/check_kani.sh @@ -6,6 +6,9 @@ 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 @@ -16,11 +19,18 @@ 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" -./scripts/setup/ubuntu/install_deps.sh +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..." From 9011191a700366a72ce2c66867973ef7446db61a Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Wed, 31 Jul 2024 01:20:00 +0000 Subject: [PATCH 8/8] Add `set -e` to ensure that CI breaks if scripts break --- scripts/check_kani.sh | 2 ++ scripts/check_rustc.sh | 2 ++ 2 files changed, 4 insertions(+) diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh index 03861ea03bf26..f381c1a376c83 100644 --- a/scripts/check_kani.sh +++ b/scripts/check_kani.sh @@ -1,5 +1,7 @@ #!/bin/bash +set -e + # Set the working directories VERIFY_RUST_STD_DIR="$1" KANI_DIR=$(mktemp -d) diff --git a/scripts/check_rustc.sh b/scripts/check_rustc.sh index 55ff95b396c24..610f6157b20ce 100644 --- a/scripts/check_rustc.sh +++ b/scripts/check_rustc.sh @@ -1,5 +1,7 @@ #!/bin/bash +set -e + # Set the working directory for your local repository HEAD_DIR=$1