Repository navigation
Fix codegen crashes on SVE tuples and non-power-of-two Simd on aarc…
#14247
This file contains hidden or 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
| # Copyright Kani Contributors | |
| # SPDX-License-Identifier: Apache-2.0 OR MIT | |
| name: Kani CI | |
| on: | |
| pull_request: | |
| merge_group: | |
| push: | |
| # Not just any push, as that includes tags. | |
| # We don't want to re-trigger this workflow when tagging an existing commit. | |
| branches: | |
| - '**' | |
| env: | |
| RUST_BACKTRACE: 1 | |
| jobs: | |
| regression: | |
| runs-on: ${{ matrix.os }} | |
| permissions: | |
| contents: read | |
| strategy: | |
| matrix: | |
| os: [macos-15-intel, ubuntu-22.04, ubuntu-24.04, macos-14, ubuntu-24.04-arm] | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v6 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ${{ matrix.os }} | |
| - name: Execute Kani regression | |
| run: ./scripts/kani-regression.sh | |
| benchcomp-tests: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v6 | |
| - name: Install benchcomp dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y python3-pip | |
| pushd tools/benchcomp && pip3 install -r requirements.txt | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-24.04 | |
| - name: Build Kani using release mode | |
| run: cargo build-dev -- --release | |
| - name: Run benchcomp unit and regression tests | |
| run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run | |
| perf: | |
| runs-on: ubuntu-24.04 | |
| # The full perf suite runs in ~45 min (matching main): most cases finish in | |
| # seconds; the heaviest, s2n-quic-core, runs 34 harnesses in ~1500s. The | |
| # per-test guardrail in scripts/kani-perf.sh (2400s) sits above that. The | |
| # 180-min step timeout leaves ample headroom over that realistic runtime, | |
| # and the job timeout sits above (step timeout) x (max_attempts) so a retry | |
| # can still land. | |
| timeout-minutes: 380 | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v6 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-24.04 | |
| - name: Execute Kani performance tests | |
| # Retry on infra-driven failures (spot preemption / runner shutdown). | |
| # The script itself bounds per-test wall time, so functional regressions | |
| # surface as normal test failures and are not retried indefinitely. | |
| uses: nick-fields/retry@v4 | |
| with: | |
| timeout_minutes: 180 | |
| max_attempts: 2 | |
| command: ./scripts/kani-perf.sh | |
| env: | |
| RUST_TEST_THREADS: 1 | |
| llbc-regression: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v6 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-24.04 | |
| - name: Build Kani with Charon | |
| run: cargo build-dev -- --features cprover --features llbc | |
| - name: Run tests | |
| run: ./scripts/kani-llbc-regression.sh | |
| documentation: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - name: Install book dependencies | |
| run: ./scripts/setup/ubuntu/install_doc_deps.sh | |
| # On one OS only, build the documentation, too. | |
| - name: Build Documentation | |
| run: ./scripts/build-docs.sh | |
| # When we're pushed to main branch, only then actually publish the docs. | |
| - name: Publish Documentation | |
| if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }} | |
| uses: JamesIves/github-pages-deploy-action@v4 | |
| with: | |
| branch: gh-pages | |
| folder: docs/book/ | |
| single-commit: true |