List Workflow Demo

.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```'
+            });

scripts/run-kani.sh

@@ -3,17 +3,19 @@
 set -e
 
 usage() {
-    echo "Usage: $0 [options] [-p <path>] [--kani-args <command arguments>]"
+    echo "Usage: $0 [options] [-p <path>] [--run <verify-std|list>] [--kani-args <command arguments>]"
     echo "Options:"
     echo "  -h, --help         Show this help message"
     echo "  -p, --path <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 <verify-std|list>  Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified."
     echo "  --kani-args  <command arguments to kani>  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
 }
 
 # 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