test.yml

name: Test

on:
  push:
    branches: [master, rewrite-2023, staging, trying]
    paths-ignore: 'docs/**'
  pull_request:
    branches: [master, rewrite-2023]
    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@v2
      - 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@v2
      - name: Set up Java
        uses: actions/setup-java@v1
        with:
          java-version: '15'
      - 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@v2
      - name: Set up Java
        uses: actions/setup-java@v1
        with:
          java-version: '15'
      - 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@v2
      - 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@v2
  #    - name: Set up Java
  #      uses: actions/setup-java@v1
  #      with:
  #        java-version: '15'
  #    - 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 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@v2
      - name: Set up Python 3
        uses: actions/setup-python@v2
        with:
          python-version: '3.x'
      - name: Set up Java
        uses: actions/setup-java@v1
        with:
          java-version: '15'
      - 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 cargo tests
        run: python x.py test -p prusti-tests
        #run: python x.py test --all
      - name: Check prusti-contracts
        run: |
          cd prusti-contracts/prusti-contracts-test/
          cargo +stable build

  # 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
  #  if: false # disabled for v2 for now
  #  strategy:
  #    matrix:
  #      shard_index: [0, 1, 2, 3]
  #  steps:
  #    - name: Check out the repo
  #      uses: actions/checkout@v2
  #    - name: Setup Python 3
  #      uses: actions/setup-python@v2
  #      with:
  #        python-version: '3.x'
  #    - name: Set up Java
  #      uses: actions/setup-java@v1
  #      with:
  #        java-version: '15'
  #    - 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] #, 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) }}