-
Notifications
You must be signed in to change notification settings - Fork 84
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into reset-mem-init
- Loading branch information
Showing
90 changed files
with
2,255 additions
and
588 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,86 @@ | ||
| # 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: | ||
| workflow_call: | ||
|
|
||
| env: | ||
| RUST_BACKTRACE: 1 | ||
|
|
||
| jobs: | ||
| verify-std: | ||
| 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: ./kani/.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' && github.event_name == 'pull_request' | ||
| 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' && 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 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 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.