From ec6d98ed385dbcdc62c1eba7643c099f13836341 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Mon, 12 Aug 2024 15:50:18 -0400
Subject: [PATCH] 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.
---
 .github/workflows/kani.yml        |  31 +----
 .github/workflows/rustc.yml       |  35 +-----
 scripts/check_kani.sh             |  55 +++++++++
 scripts/check_rustc.sh            |  44 +++++++
 scripts/pull_from_upstream.sh     |  25 ++++
 scripts/run_update_with_checks.sh | 185 ++++++++++++++++++++++++++++++
 scripts/update_toolchain_date.sh  |  31 +++++
 7 files changed, 347 insertions(+), 59 deletions(-)
 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/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 <toolchain_file_path> <new_date>"
+    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