-
Notifications
You must be signed in to change notification settings - Fork 92
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
21 changed files
with
399 additions
and
41 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,89 @@ | ||
| # 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 | ||
| fetch-depth: 0 | ||
|
|
||
| - 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.outcome != steps.check-base.outcome | ||
| run: | | ||
| echo "New failure introduced by this change" | ||
| echo "HEAD: ${{ steps.check-head.outcome }}" | ||
| echo "BASE: ${{ steps.check-base.outcome }}" | ||
| 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
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
6 changes: 6 additions & 0 deletions
6
tests/expected/function-contract/interior-mutability/api/cell.expected
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,6 @@ | ||
| assertion\ | ||
| - Status: SUCCESS\ | ||
| - Description: "|_| im.x.get() < 101"\ | ||
| in function modify | ||
|
|
||
| VERIFICATION:- SUCCESSFUL |
25 changes: 25 additions & 0 deletions
25
tests/expected/function-contract/interior-mutability/api/cell.rs
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,25 @@ | ||
| // Copyright Kani Contributors | ||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
| // kani-flags: -Zfunction-contracts | ||
|
|
||
| /// Mutating Cell via `as_ptr` in contracts | ||
| use std::cell::Cell; | ||
|
|
||
| /// This struct contains Cell which can be mutated | ||
| struct InteriorMutability { | ||
| x: Cell<u32>, | ||
| } | ||
|
|
||
| #[kani::requires(im.x.get() < 100)] | ||
| #[kani::modifies(im.x.as_ptr())] | ||
| #[kani::ensures(|_| im.x.get() < 101)] | ||
| ///im is an immutable reference with interior mutability | ||
| fn modify(im: &InteriorMutability) { | ||
| im.x.set(im.x.get() + 1) | ||
| } | ||
|
|
||
| #[kani::proof_for_contract(modify)] | ||
| fn harness_for_modify() { | ||
| let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; | ||
| modify(&im) | ||
| } |
Oops, something went wrong.