Runtime checks #7177
Workflow file for this run
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
| name: Test | |
| on: | |
| push: | |
| branches: 'master' | |
| paths-ignore: 'docs/**' | |
| pull_request: | |
| branches: 'master' | |
| paths-ignore: 'docs/**' | |
| # Cancel previous runs in a PR when pushing new commits | |
| concurrency: | |
| group: worflow-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | |
| # Do not cancel when testing the master branch | |
| cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }} | |
| env: | |
| RUST_BACKTRACE: 1 | |
| PRUSTI_ASSERT_TIMEOUT: 60000 | |
| jobs: | |
| # Check formatting | |
| fmt-check: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Check formatting | |
| run: | | |
| rustup component add rustfmt | |
| python ./x.py fmt-check-all | |
| # Run clippy checks | |
| clippy-check: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Check and report Clippy errors | |
| run: | | |
| python ./x.py clippy -- -D warnings | |
| # Detect missing dependencies in workspace packages | |
| # See: https://stackoverflow.com/a/74293494/2491528 | |
| check-deps: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Compile each workspace package individually | |
| run: | | |
| cargo install cargo-hack | |
| python ./x.py hack build --workspace | |
| # Check that we depend on the compiler only through SMIR. | |
| smir-check: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Check and report illegal extern crate. | |
| run: | | |
| python ./x.py check-smir | |
| # Run a subset of the tests that used to fail often. | |
| # The goal here is to fail fast and give quick feedback to the developers. | |
| # This job intentionally doesn't use the verification cache. | |
| quick-tests: | |
| runs-on: ubuntu-latest | |
| env: | |
| PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Build with cargo | |
| run: python x.py build --all | |
| - name: Run quick tests | |
| run: python x.py test --all quick | |
| # Run a subset of the tests with the purification optimization enabled | |
| # to ensure that we do not introduce regressions. | |
| purification-tests: | |
| needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests] | |
| runs-on: ubuntu-latest | |
| env: | |
| PRUSTI_ENABLE_PURIFICATION_OPTIMIZATION: true | |
| PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Prepare verification cache keys | |
| shell: bash | |
| run: | | |
| VER_CACHE_KEY_SHARED=prusti-cache-$(cat viper-toolchain)-$(date +%Y-%m) | |
| echo "VER_CACHE_KEY_SHARED=$VER_CACHE_KEY_SHARED" >> $GITHUB_ENV | |
| echo "VER_CACHE_KEY_UNIQUE=$VER_CACHE_KEY_SHARED-${RANDOM}${RANDOM}" >> $GITHUB_ENV | |
| - name: Load verification cache | |
| uses: actions/cache@v3 | |
| with: | |
| path: ${{ env.PRUSTI_CACHE_PATH }} | |
| # Use a unique key, so that the job will always store the cache at the end of the run | |
| key: ${{ env.VER_CACHE_KEY_UNIQUE }} | |
| # Restore from the most recent cache that matches a shared prefix of the key | |
| restore-keys: ${{ env.VER_CACHE_KEY_SHARED }} | |
| - name: Build with cargo | |
| run: python x.py build --all | |
| - name: Run quick tests | |
| run: | | |
| python x.py verify-test prusti-tests/tests/verify/pass/rosetta/Knuth_shuffle.rs | |
| # python x.py test --all pass/rosetta/Binary_search_shared.rs | |
| # python x.py test --all pass/demos/account.rs | |
| # python x.py test --all pass/rosetta/Knights_tour.rs | |
| # python x.py test --all pass/quick/fold-unfold.rs | |
| # python x.py test --all pass/quick/moves.rs | |
| # python x.py test --all pass/quick/mut-borrows.rs | |
| # python x.py test --all pass/quick/shared-borrows.rs | |
| # python x.py test --all pass/quick/trait-contracts-refinement.rs | |
| # python x.py test --all pass/quick/fibonacci.rs | |
| # python x.py test --all pass/pure-fn/len-lookup.rs | |
| # python x.py test --all pass/pure-fn/quantifiers.rs | |
| # python x.py test --all pass/pure-fn/recursive-pure-fn.rs | |
| # python x.py test --all pass/pure-fn/ref-mut-arg.rs | |
| # python x.py test --all pass/rosetta/Ackermann_function.rs | |
| # python x.py test --all pass/rosetta/Heapsort.rs | |
| - name: Run with purification. | |
| env: | |
| PRUSTI_VIPER_BACKEND: silicon | |
| PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon | |
| PRUSTI_VERIFY_CORE_PROOF: true | |
| PRUSTI_VERIFY_SPECIFICATIONS: true | |
| PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false | |
| PRUSTI_INLINE_CALLER_FOR: false | |
| run: | | |
| python x.py test core_proof | |
| - name: Run with purification with Carbon. | |
| env: | |
| PRUSTI_VIPER_BACKEND: silicon | |
| PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: carbon | |
| PRUSTI_VERIFY_CORE_PROOF: true | |
| PRUSTI_VERIFY_SPECIFICATIONS: true | |
| PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false | |
| PRUSTI_INLINE_CALLER_FOR: false | |
| run: | | |
| python x.py test core_proof | |
| - name: Run without purification. | |
| env: | |
| PRUSTI_VIPER_BACKEND: silicon | |
| PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon | |
| PRUSTI_VERIFY_CORE_PROOF: true | |
| PRUSTI_VERIFY_SPECIFICATIONS: true | |
| PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: true | |
| PRUSTI_INLINE_CALLER_FOR: false | |
| run: | | |
| python x.py test core_proof | |
| - name: Inline caller for functions | |
| env: | |
| PRUSTI_VIPER_BACKEND: silicon | |
| PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon | |
| PRUSTI_VERIFY_CORE_PROOF: true | |
| PRUSTI_VERIFY_SPECIFICATIONS: true | |
| PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false | |
| PRUSTI_INLINE_CALLER_FOR: true | |
| run: | | |
| python x.py test core_proof | |
| # Run all the tests. | |
| all-tests: | |
| needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests] | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, windows-latest, macos-latest] | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| env: | |
| PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Python 3 | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.x' | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Prepare verification cache keys | |
| shell: bash | |
| run: | | |
| VER_CACHE_KEY_SHARED=prusti-cache-$(cat viper-toolchain)-$(date +%Y-%m) | |
| echo "VER_CACHE_KEY_SHARED=$VER_CACHE_KEY_SHARED" >> $GITHUB_ENV | |
| echo "VER_CACHE_KEY_UNIQUE=$VER_CACHE_KEY_SHARED-${RANDOM}${RANDOM}" >> $GITHUB_ENV | |
| - name: Load verification cache | |
| uses: actions/cache@v3 | |
| with: | |
| path: ${{ env.PRUSTI_CACHE_PATH }} | |
| # Use a unique key, so that the job will always store the cache at the end of the run | |
| key: ${{ env.VER_CACHE_KEY_UNIQUE }} | |
| # Restore from the most recent cache that matches a shared prefix of the key | |
| restore-keys: ${{ env.VER_CACHE_KEY_SHARED }} | |
| - name: Build with cargo | |
| run: python x.py build --all --jobs 1 | |
| - name: Run cargo tests | |
| run: python x.py test --all | |
| - name: Run a subset of tests with Carbon | |
| run: | | |
| python x.py test pass/no-annotation --all --verbose | |
| env: | |
| PRUSTI_VIPER_BACKEND: carbon | |
| - name: Check prusti-contracts | |
| run: | | |
| cd prusti-contracts/prusti-contracts-test/ | |
| cargo +stable build | |
| release-build: | |
| needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests] | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, windows-latest, macos-latest] | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Python 3 | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.x' | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Build with cargo --release | |
| run: python x.py build --release | |
| # Run Prusti on itself. | |
| # Disabled because of a bug when compiling jni-gen | |
| test-on-prusti: | |
| needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests] | |
| runs-on: ubuntu-latest | |
| if: false | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Build with cargo | |
| run: python x.py build --release --all | |
| - name: Run cargo-prusti on Prusti | |
| run: python x.py exec target/release/cargo-prusti | |
| env: | |
| PRUSTI_SKIP_UNSUPPORTED_FEATURES: true | |
| PRUSTI_FULL_COMPILATION: true | |
| PRUSTI_CHECK_PANICS: false | |
| PRUSTI_CHECK_OVERFLOWS: false | |
| PRUSTI_INTERNAL_ERRORS_AS_WARNINGS: true | |
| # Test cargo-prusti on a collection of crates. | |
| test-crates: | |
| needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests] | |
| runs-on: ubuntu-22.04 | |
| strategy: | |
| matrix: | |
| shard_index: [0, 1, 2, 3] | |
| steps: | |
| - name: Check out the repo | |
| uses: actions/checkout@v3 | |
| - name: Setup Python 3 | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.x' | |
| - name: Set up Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| java-version: '15' | |
| distribution: 'zulu' | |
| - name: Set up the environment | |
| run: python x.py setup | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| shared-key: "shared" | |
| - name: Build with cargo --release | |
| run: | | |
| python x.py build --release -p prusti | |
| python x.py build --release -p prusti-launch | |
| python x.py build --release -p test-crates | |
| - name: Test Prusti on a collection of crates | |
| run: ./target/release/test-crates --fail-fast --num-shards=4 --shard-index=${{ matrix.shard_index }} | |
| # Dummy job to specify the jobs that must pass before merging on master | |
| can-merge: | |
| runs-on: ubuntu-latest | |
| needs: [all-tests, purification-tests, release-build, test-crates] | |
| # Always run, even if the workflow was cancelled | |
| if: ${{ always() }} | |
| steps: | |
| - name: Fail if the workflow failed or was cancelled | |
| uses: re-actors/alls-green@release/v1 | |
| with: | |
| jobs: ${{ toJSON(needs) }} |