Skip to content
Test

Fix encoding of signed integer divisions #13

Sign in to view logs

Fix encoding of signed integer divisions

Fix encoding of signed integer divisions #13

Workflow file for this run

.github/workflows/test.yml at 42e91b3
name: Test
on:
push:
branches: [master, staging, trying]
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@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@0.5.22
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 --all
- name: Check prusti-contracts
run: |
cd prusti-contracts/prusti-contracts-test/
cargo +stable build
# 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@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 --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-20.04
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 --all
- name: Test Prusti on a collection of crates
run: ./target/release/test-crates --fail-fast --num-shards=4 --shard-index=${{ matrix.shard_index }}