diff --git a/.github/workflows/test-action.yml b/.github/workflows/test-action.yml index d78ee5a..e59861e 100644 --- a/.github/workflows/test-action.yml +++ b/.github/workflows/test-action.yml @@ -12,10 +12,63 @@ jobs: # you must check out the repository - name: Checkout uses: actions/checkout@v3 - - name: Run Kani + + - name: Run Kani with invalid version + id: set_error + uses: ./ + with: + working-directory: tests/cargo-kani/simple-lib + kani-version: '0.1.10' + continue-on-error: true + + - name: Check previous step outcome + id: get_error + run: | + # Check the outcome of "Run Kani with invalid version" + if [[ "${{ steps.set_error.outcome }}" == "failure" ]]; then + echo "Running Kani with invalid version "0.1.10" failed." + else + echo "::error::Running Kani with invalid version succeeded incorrectly or was skipped." + exit 1 + fi + + - name: Run Kani with older version + uses: ./ # Uses the action in the root directory + with: + working-directory: tests/cargo-kani/simple-lib + kani-version: '0.33.0' + + - name: Test run Kani with older version + run: | + installed_version=$(kani --version | awk '{print $2}') + expected_version='0.33.0' + + if [[ "$installed_version" == "$expected_version" ]]; then + echo "The installed version ($installed_version) matches the expected version ($expected_version)." + else + echo "::error::The installed version ($installed_version) does not match the expected version ($expected_version)." + exit 1 + fi + + - name: Run Kani with latest version uses: ./ # Uses the action in the root directory with: working-directory: tests/cargo-kani/simple-lib + + - name: Test run Kani with latest version + run: | + installed_version=$(kani --version | awk '{print $2}') + expected_version=$(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g') + + echo "version online is $(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g')." + + if [[ "$installed_version" == "$expected_version" ]]; then + echo "The installed version ($installed_version) matches the latest version ($expected_version)" + else + echo "::error::The installed version ($installed_version) does not match the latest version ($expected_version)." + exit 1 + fi + - name: Test ProfProof within Kani Action uses: ./ with: diff --git a/README.md b/README.md index 13d74b9..cdf8f47 100644 --- a/README.md +++ b/README.md @@ -2,6 +2,65 @@ This repository provides a GitHub Action for running the [Kani Rust Verifier](https://github.com/model-checking/kani) in CI. +## GitHub Action Parameters + +The following parameters can be used to configure and customize the behavior of this GitHub Action: + +NOTE: All the fields provided are optional and have default behaviors when not specified. + +`kani-version` + +- **Description**: Specifies the Kani version number to use. +- **Default**: 'latest' +- **Usage**: You can provide a specific version of Kani to use. If omitted, the latest version will be installed and used. + +`command` + +- **Description**: Specifies the command to run Kani. +- **Default**: 'cargo-kani' +- **Usage**: You can set a custom command to run Kani. For example, this allows you to use a different binary or script for Kani, if needed. + +`working-directory` + +- **Description**: Specifies the directory in which Kani should be run. +- **Default**: '.' +- **Usage**: Kani will be executed within this directory. + +`args` + +- **Description**: Specifies additional arguments to pass to Kani. +- **Default**: '' +- **Usage**: You can provide any additional command-line arguments to Kani using this parameter. These arguments will be appended to the Kani command. + +`enable-propproof` + +- **Description**: Experimental feature that allows Kani to verify proptest harnesses using the PropProof feature. +- **Default**: false +- **Usage**: If set to `true`, Kani will enable the experimental PropProof feature for verifying proptest harnesses. + +## Kani-version default behavior + +Please note that since providing `kani-version` is optional, if the user doesn't provide the version, the action will install the latest version of `Kani` on `crates.io`. + +## Example usage in a workflow YAML file: + +Here is an example of a workflow YAML file for the Kani Github Action + +```yaml +jobs: + kani: + runs-on: ubuntu-latest + steps: + - name: Run Kani + uses: model-checking/kani-github-action@v0.37 + with: + kani-version: '0.35.0' + command: 'cargo-kani' + working-directory: './path/to/project' + args: '--tests' + enable-propproof: true +``` + ## Security See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information. @@ -10,4 +69,3 @@ See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more inform This code is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT) for details. - diff --git a/action.yml b/action.yml index 688c0d6..664f6ae 100644 --- a/action.yml +++ b/action.yml @@ -10,6 +10,10 @@ branding: color: 'orange' inputs: + kani-version: + description: 'Kani Version number' + required: false + default: 'latest' command: description: 'Command to run.' required: false @@ -34,11 +38,8 @@ runs: uses: dtolnay/rust-toolchain@stable - name: Install Kani + run: ${{ github.action_path }}/src/install-kani.sh ${{ inputs.kani-version }} shell: bash - run: | - export KANI_VERSION="0.36.0"; - cargo install --version $KANI_VERSION --locked kani-verifier; - cargo-kani setup; - name: Install PropProof if: ${{ inputs.enable-propproof == 'true' }} diff --git a/src/install-kani.sh b/src/install-kani.sh new file mode 100755 index 0000000..7f5406d --- /dev/null +++ b/src/install-kani.sh @@ -0,0 +1,39 @@ +#!/bin/bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# If version is latest, install directly from cargo +if [ "$1" == "latest" ]; then + cargo install --locked kani-verifier; +else + VERSION=$1 + cargo install --version $VERSION --locked kani-verifier; +fi + +# Check exit status for error handling +if [ $? -eq 0 ]; then + echo "Installed Kani $VERSION successfully" +else + echo "::error::Could not install Kani. Please check if the provided version is correct" + exit 1 +fi + +# Setup kani in ci +cargo-kani setup; + +# Get the current installed version of kani and check it against the latest version +installed_version=$(kani --version | awk '{print $2}') + +if [$? -eq 0]; then + if [ "$1" == "latest" ]; then + # Cargo search returns version number as string + requested_version=$(cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}') + else + requested_version=$1 + fi + + if ["$installed_version" != "$requested_version"]; then + echo "::error::The version of Kani installed was different than the one requested" + exit 1 + fi +fi