diff --git a/.github/workflows/list.yml b/.github/workflows/list.yml new file mode 100644 index 0000000000000..06ed7ceff0422 --- /dev/null +++ b/.github/workflows/list.yml @@ -0,0 +1,54 @@ +name: Kani List + +on: + workflow_dispatch: + pull_request: + branches: [ main ] + types: [ closed ] + +permissions: + pull-requests: write + +defaults: + run: + shell: bash + +jobs: + run-kani-list-on-std: + name: List Kani harnesses and contracts on std library + runs-on: ${{ matrix.os }} + # Only run this job if the pull request was merged + if: github.event.pull_request.merged == true + strategy: + matrix: + os: [ubuntu-latest] + include: + - os: ubuntu-latest + base: ubuntu + steps: + # Step 1: Check out the repository + - name: Checkout Repository + uses: actions/checkout@v4 + with: + path: head + submodules: true + + # Step 2: Run list on the std library (assumes it creates kani_list.txt) + - name: Run Kani List + run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head + + # Step 3: Read kani_list.txt and post comment on PR + - name: Comment Results on PR + uses: actions/github-script@v6 + with: + github-token: ${{secrets.GITHUB_TOKEN}} + script: | + const fs = require('fs'); + const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8'); + + await github.rest.issues.createComment({ + issue_number: ${{ github.event.pull_request.number }}, + owner: context.repo.owner, + repo: context.repo.repo, + body: 'Kani List Results:\n```\n' + kaniOutput + '\n```' + }); diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 8ce27dac5d207..a4f6b46a825bb 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -3,10 +3,11 @@ set -e usage() { - echo "Usage: $0 [options] [-p ] [--kani-args ]" + echo "Usage: $0 [options] [-p ] [--run ] [--kani-args ]" echo "Options:" echo " -h, --help Show this help message" echo " -p, --path Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory." + echo " --run Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified." echo " --kani-args Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument." exit 1 } @@ -14,6 +15,7 @@ usage() { # Initialize variables command_args="" path="" +run_command="verify-std" # Parse command line arguments # TODO: Improve parsing with getopts @@ -31,13 +33,23 @@ while [[ $# -gt 0 ]]; do usage fi ;; + --run) + if [[ -n $2 && ($2 == "verify-std" || $2 == "list") ]]; then + run_command=$2 + shift 2 + else + echo "Error: Invalid run command. Must be 'verify-std' or 'list'." + usage + fi + ;; --kani-args) shift command_args="$@" break ;; *) - break + echo "Error: Unknown option $1" + usage ;; esac done @@ -181,9 +193,13 @@ main() { echo "Running Kani command..." "$kani_path" --version - echo "Running Kani verify-std command..." - - "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args + if [[ "$run_command" == "verify-std" ]]; then + echo "Running Kani verify-std command..." + "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args + elif [[ "$run_command" == "list" ]]; then + echo "Running Kani list command..." + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates ./library --std > $path/kani_list.txt + fi } main