kani list Workflow (#146)

Adds a workflow that runs `kani list` on the standard library and posts
the results in a comment on the pull request. This workflow runs iff a
pull request is merged, so that we have one comment at the end of a PR
with the most up-to-date list results. (I considered other approaches,
like running it on opening the PR or with every commit, but decided
having one single comment with the final changes was best for
brevity/clarity).

See this [test
PR](carolynzech#10) on my fork
as a demo of how it would work.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <[email protected]>

.github/workflows/kani.yml

@@ -65,3 +65,17 @@ jobs:
       - name: Test Kani script (In Repo Directory)
         working-directory: ${{github.workspace}}/head
         run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
+
+      # Step 4: Run list on the std library and add output to job summary
+      - name: Run Kani List
+        run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
+
+      - name: Add Kani List output to job summary
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const fs = require('fs');
+            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
+            await core.summary
+              .addRaw(kaniOutput)
+              .write();

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,20 @@ 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 -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12
+    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 \
+            -Z loop-contracts \
+            --output-format=terse \
+            $command_args \
+            --enable-unstable \
+            --cbmc-args --object-bits 12
+    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