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