diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 1c8cd119c393..5892ba13d26a 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -70,6 +70,23 @@ jobs: env: RUST_TEST_THREADS: 1 + llbc-regression: + runs-on: ubuntu-24.04 + steps: + - name: Checkout Kani + uses: actions/checkout@v4 + + - 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: diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index f11932a7387e..dee27579e220 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -31,7 +31,7 @@ tracing-tree = "0.4.0" # Future proofing: enable backend dependencies using feature. [features] -default = ['cprover', 'llbc'] +default = ['cprover'] llbc = ['charon'] cprover = ['cbmc', 'num', 'serde'] diff --git a/scripts/kani-llbc-regression.sh b/scripts/kani-llbc-regression.sh new file mode 100755 index 000000000000..9d07814e4ab3 --- /dev/null +++ b/scripts/kani-llbc-regression.sh @@ -0,0 +1,33 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +if [[ -z $KANI_REGRESSION_KEEP_GOING ]]; then + set -o errexit +fi +set -o pipefail +set -o nounset + +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +export PATH=$SCRIPT_DIR:$PATH + +# Formatting check +${SCRIPT_DIR}/kani-fmt.sh --check + +# Build kani +cargo build-dev -- --features cprover --features llbc + +# Build compiletest and print configuration. We pick suite / mode combo so there's no test. +echo "--- Compiletest configuration" +cargo run -p compiletest --quiet -- --suite kani --mode cargo-kani --dry-run --verbose +echo "-----------------------------" + +suite="llbc" +mode="expected" +echo "Check compiletest suite=$suite mode=$mode" +cargo run -p compiletest --quiet -- --suite $suite --mode $mode \ + --quiet --no-fail-fast + +echo +echo "All Kani llbc regression tests completed successfully." +echo diff --git a/tests/expected/llbc/basic0/expected b/tests/llbc/basic0/expected similarity index 100% rename from tests/expected/llbc/basic0/expected rename to tests/llbc/basic0/expected diff --git a/tests/expected/llbc/basic0/test.rs b/tests/llbc/basic0/test.rs similarity index 100% rename from tests/expected/llbc/basic0/test.rs rename to tests/llbc/basic0/test.rs diff --git a/tests/expected/llbc/basic1/expected b/tests/llbc/basic1/expected similarity index 100% rename from tests/expected/llbc/basic1/expected rename to tests/llbc/basic1/expected diff --git a/tests/expected/llbc/basic1/test.rs b/tests/llbc/basic1/test.rs similarity index 100% rename from tests/expected/llbc/basic1/test.rs rename to tests/llbc/basic1/test.rs diff --git a/tests/expected/llbc/enum/expected b/tests/llbc/enum/expected similarity index 100% rename from tests/expected/llbc/enum/expected rename to tests/llbc/enum/expected diff --git a/tests/expected/llbc/enum/test.rs b/tests/llbc/enum/test.rs similarity index 100% rename from tests/expected/llbc/enum/test.rs rename to tests/llbc/enum/test.rs diff --git a/tests/expected/llbc/generic/expected b/tests/llbc/generic/expected similarity index 100% rename from tests/expected/llbc/generic/expected rename to tests/llbc/generic/expected diff --git a/tests/expected/llbc/generic/test.rs b/tests/llbc/generic/test.rs similarity index 100% rename from tests/expected/llbc/generic/test.rs rename to tests/llbc/generic/test.rs diff --git a/tests/expected/llbc/option/expected b/tests/llbc/option/expected similarity index 100% rename from tests/expected/llbc/option/expected rename to tests/llbc/option/expected diff --git a/tests/expected/llbc/option/test.rs b/tests/llbc/option/test.rs similarity index 100% rename from tests/expected/llbc/option/test.rs rename to tests/llbc/option/test.rs diff --git a/tests/expected/llbc/projection/expected b/tests/llbc/projection/expected similarity index 100% rename from tests/expected/llbc/projection/expected rename to tests/llbc/projection/expected diff --git a/tests/expected/llbc/projection/test.rs b/tests/llbc/projection/test.rs similarity index 100% rename from tests/expected/llbc/projection/test.rs rename to tests/llbc/projection/test.rs diff --git a/tests/expected/llbc/struct/expected b/tests/llbc/struct/expected similarity index 100% rename from tests/expected/llbc/struct/expected rename to tests/llbc/struct/expected diff --git a/tests/expected/llbc/struct/test.rs b/tests/llbc/struct/test.rs similarity index 100% rename from tests/expected/llbc/struct/test.rs rename to tests/llbc/struct/test.rs diff --git a/tests/expected/llbc/traitimpl/expected b/tests/llbc/traitimpl/expected similarity index 100% rename from tests/expected/llbc/traitimpl/expected rename to tests/llbc/traitimpl/expected diff --git a/tests/expected/llbc/traitimpl/test.rs b/tests/llbc/traitimpl/test.rs similarity index 100% rename from tests/expected/llbc/traitimpl/test.rs rename to tests/llbc/traitimpl/test.rs diff --git a/tests/expected/llbc/tuple/expected b/tests/llbc/tuple/expected similarity index 100% rename from tests/expected/llbc/tuple/expected rename to tests/llbc/tuple/expected diff --git a/tests/expected/llbc/tuple/test.rs b/tests/llbc/tuple/test.rs similarity index 100% rename from tests/expected/llbc/tuple/test.rs rename to tests/llbc/tuple/test.rs