test.yml

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) }}