From d61e84717470090c97ea56d6054d525dc49b23f5 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 13:11:50 -0700 Subject: [PATCH 1/6] Add a new workflow to check std verification --- .github/workflows/check-verify-std.yml | 84 ++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 .github/workflows/check-verify-std.yml diff --git a/.github/workflows/check-verify-std.yml b/.github/workflows/check-verify-std.yml new file mode 100644 index 000000000000..50ce357dfdb2 --- /dev/null +++ b/.github/workflows/check-verify-std.yml @@ -0,0 +1,84 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to build and run the `verify-rust-std` repository. +# +# This check should be optional, but it has been added to help provide +# visibility to when a PR may break the `verify-rust-std` repository. +# +# We expect toolchain updates to potentially break this workflow in cases where +# the version tracked in the `verify-rust-std` is not compatible with newer +# versions of the Rust toolchain. +# +# Changes unrelated to the toolchain should match the current status of main. + +name: Check Std Verification +on: pull_request + +env: + RUST_BACKTRACE: 1 + +jobs: + build: + runs-on: ${{ matrix.os }} + strategy: + matrix: + # Kani does not support windows. + os: [ ubuntu-22.04, macos-14 ] + steps: + - name: Checkout Library + uses: actions/checkout@v4 + with: + repository: model-checking/verify-rust-std + path: verify-rust-std + submodules: true + + - name: Checkout `Kani` + uses: actions/checkout@v4 + with: + path: kani + + - name: Setup Kani Dependencies + uses: ./.github/actions/setup + with: + os: ${{ matrix.os }} + kani_dir: kani + + - name: Build Kani + working-directory: kani + run: | + cargo build-dev + echo "$(pwd)/scripts" >> $GITHUB_PATH + + - name: Run verification with HEAD + id: check-head + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks + + # If the head failed, check if it's a new failure. + - name: Checkout base + working-directory: kani + if: steps.check-head.outcome != 'success' + run: | + BASE_REF=${{ github.event.pull_request.base.sha }} + git checkout ${BASE_REF} + cargo build-dev + + - name: Run verification with BASE + id: check-base + if: steps.check-head.outcome != 'success' + working-directory: verify-rust-std + continue-on-error: true + 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: Compare results + if: steps.check-head.outcome != 'success' && steps.check-base.output == 'success' + run: | + echo "New failure introduced by this change" + exit 1 + From 5eee254ec0364ded78810e2bcbaa59054d986be7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 13:32:31 -0700 Subject: [PATCH 2/6] Fix top job name --- .github/workflows/check-verify-std.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/check-verify-std.yml b/.github/workflows/check-verify-std.yml index 50ce357dfdb2..af9763713b97 100644 --- a/.github/workflows/check-verify-std.yml +++ b/.github/workflows/check-verify-std.yml @@ -19,7 +19,7 @@ env: RUST_BACKTRACE: 1 jobs: - build: + verify-std: runs-on: ${{ matrix.os }} strategy: matrix: From b85323f2747b1f543d5dc1025645cea1a6c9157c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 13:36:24 -0700 Subject: [PATCH 3/6] Fix setup step --- .github/workflows/check-verify-std.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/check-verify-std.yml b/.github/workflows/check-verify-std.yml index af9763713b97..77d2aa6e3de7 100644 --- a/.github/workflows/check-verify-std.yml +++ b/.github/workflows/check-verify-std.yml @@ -39,7 +39,7 @@ jobs: path: kani - name: Setup Kani Dependencies - uses: ./.github/actions/setup + uses: ./kani/.github/actions/setup with: os: ${{ matrix.os }} kani_dir: kani From 185e28fb2a735df5726b88ad9a70a59682bcbb2a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 13:45:24 -0700 Subject: [PATCH 4/6] Rename file --- .github/workflows/{check-verify-std.yml => verify-std-check.yml} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename .github/workflows/{check-verify-std.yml => verify-std-check.yml} (100%) diff --git a/.github/workflows/check-verify-std.yml b/.github/workflows/verify-std-check.yml similarity index 100% rename from .github/workflows/check-verify-std.yml rename to .github/workflows/verify-std-check.yml From e21e5f6ac63be7e99e831ecd456bfb953cb4075d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 13:59:39 -0700 Subject: [PATCH 5/6] Make workflow reusable --- .github/workflows/verify-std-check.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml index 77d2aa6e3de7..667be6b340c5 100644 --- a/.github/workflows/verify-std-check.yml +++ b/.github/workflows/verify-std-check.yml @@ -13,7 +13,9 @@ # Changes unrelated to the toolchain should match the current status of main. name: Check Std Verification -on: pull_request +on: + pull_request: + workflow_call: env: RUST_BACKTRACE: 1 @@ -61,7 +63,7 @@ jobs: # If the head failed, check if it's a new failure. - name: Checkout base working-directory: kani - if: steps.check-head.outcome != 'success' + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' run: | BASE_REF=${{ github.event.pull_request.base.sha }} git checkout ${BASE_REF} @@ -69,15 +71,15 @@ jobs: - name: Run verification with BASE id: check-base - if: steps.check-head.outcome != 'success' + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' working-directory: verify-rust-std continue-on-error: true 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: Compare results - if: steps.check-head.outcome != 'success' && steps.check-base.output == 'success' + - name: Compare PR results + if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output run: | echo "New failure introduced by this change" exit 1 From 3b97847073ba7e4d2363befcf85f1af1c4c8a7dc Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 14:05:32 -0700 Subject: [PATCH 6/6] Add a workflow to update `features/verify-rust-std` --- .github/workflows/verify-std-update.yml | 35 +++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 .github/workflows/verify-std-update.yml diff --git a/.github/workflows/verify-std-update.yml b/.github/workflows/verify-std-update.yml new file mode 100644 index 000000000000..518f80ecd1b8 --- /dev/null +++ b/.github/workflows/verify-std-update.yml @@ -0,0 +1,35 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to update the verify std branch. + +name: Update "features/verify-rust-std" +on: + schedule: + - cron: "30 3 * * *" # Run this every day at 03:30 UTC + workflow_dispatch: # Allow manual dispatching. + +env: + RUST_BACKTRACE: 1 + +jobs: + # First ensure the HEAD is compatible with the `verify-rust-std` repository. + verify-std: + name: Verify Std + permissions: { } + uses: ./.github/workflows/verify-std-check.yml + + # Push changes to the features branch. + update-branch: + needs: verify-std + permissions: + contents: write + runs-on: ubuntu-latest + steps: + - name: Checkout Kani + uses: actions/checkout@v4 + + - name: Update feature branch + run: | + git push origin HEAD:features/verify-rust-std +