Decouple kani version from kani-github-action version

.github/workflows/test-action.yml

@@ -12,10 +12,61 @@ 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: Ensure "Run Kani with invalid version" fails
+ 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')
+
+ 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:

README.md

@@ -2,6 +2,94 @@
 
 This repository provides a GitHub Action for running the [Kani Rust Verifier](https://github.com/model-checking/kani) in CI.
 
+## Kani 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. [Cargo's version specific format is expected for specific versions](https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html).
+If omitted, the latest version of `Kani` hosted on [`Kani's crates.io page`](https://crates.io/crates/kani-verifier) 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 are a few examples of workflow YAML files for the Kani Github Action
+
+#### Default config which uses the latest version of kani on project
+```yaml
+jobs:
+ kani:
+ runs-on: ubuntu-latest
+ steps:
+ - name: Run Kani
+ uses: model-checking/kani-github-action@v1.0
+ with:
+ command: 'cargo-kani'
+ working-directory: './path/to/project'
+```
+
+#### Use a specific version of kani, version `0.35.0` on project
+```yaml
+jobs:
+ kani:
+ runs-on: ubuntu-latest
+ steps:
+ - name: Run Kani
+ uses: model-checking/kani-github-action@v1.0
+ with:
+ kani-version: '0.35.0'
+ command: 'cargo-kani'
+ working-directory: './path/to/project'
+```
+
+#### Use pinned version of kani, version `0.35.0` on project with `--tests`
+```yaml
+jobs:
+ kani:
+ runs-on: ubuntu-latest
+ steps:
+ - name: Run Kani
+ uses: model-checking/kani-github-action@v1.0
+ 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 +98,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.
-

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.37.0";
- cargo install --version $KANI_VERSION --locked kani-verifier;
- cargo-kani setup;
 
  - name: Install PropProof
  if: ${{ inputs.enable-propproof == 'true' }}

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