cbmc-latest.yml

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

# We use block scalar notation to allow us to add ":" to the workflow name.
name: >-
  Nightly: CBMC Latest

on:
  schedule:
    - cron: "0 9 * * *" # Run this every day at 9 AM UTC (4 AM ET/1 AM PT)
  workflow_dispatch:    # Allow manual dispatching for a custom branch / tag.


env:
  RUST_BACKTRACE: 1

jobs:
  regression:
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
    steps:
      - name: Checkout Kani under "kani"
        uses: actions/checkout@v4
        with:
          path: kani

      - name: Setup Kani Dependencies
        uses: ./kani/.github/actions/setup
        with:
          os: ${{ matrix.os }}
          kani_dir: 'kani'

      - name: Checkout CBMC under "cbmc"
        uses: actions/checkout@v4
        with:
          repository: diffblue/cbmc
          path: cbmc

      - name: Build CBMC (Linux)
        if: ${{ startsWith(matrix.os, 'ubuntu') }}
        working-directory: ./cbmc
        run: |
          cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
          cmake --build build -- -j 4
          # Prepend the bin directory to $PATH
          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH

      - name: Build CBMC (macOS)
        if: ${{ startsWith(matrix.os, 'macos') }}
        working-directory: ./cbmc
        run: |
          cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_COMPILER=$(which clang++)
          cmake --build build -- -j 4
          # Prepend the bin directory to $PATH
          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH

      - name: Execute Kani regressions
        working-directory: ./kani
        run: ./scripts/kani-regression.sh

  perf:
    runs-on: ubuntu-20.04
    steps:
      - name: Checkout Kani under "kani"
        uses: actions/checkout@v4
        with:
          path: kani

      - name: Setup Kani Dependencies
        uses: ./kani/.github/actions/setup
        with:
          os: ubuntu-20.04
          kani_dir: 'kani'

      - name: Build Kani using release mode
        working-directory: ./kani
        run: cargo build-dev -- --release

      - name: Checkout CBMC under "cbmc"
        uses: actions/checkout@v4
        with:
          repository: diffblue/cbmc
          path: cbmc

      - name: Build CBMC
        working-directory: ./cbmc
        run: |
          cmake -S . -Bbuild -DWITH_JBMC=OFF
          cmake --build build -- -j 4
          # Prepend the bin directory to $PATH
          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH

      - name: Execute Kani performance tests
        working-directory: ./kani
        run: ./scripts/kani-perf.sh

      - name: Execute Kani performance ignored tests
        working-directory: ./kani
        continue-on-error: true
        run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored --no-fail-fast