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

@@ -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