From 031d51b78a4ed5504e75587816e8b04b385769fa Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Mon, 18 Nov 2024 16:13:14 -0500
Subject: [PATCH 1/2] kani list workflow step

---
 .github/workflows/kani.yml | 10 ++++++++++
 scripts/run-kani.sh        | 26 +++++++++++++++++++++-----
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 6dec32c..3e56fe0 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -65,3 +65,13 @@ 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 3: Run list on the std library (assumes it creates kani_list.txt)
+      - name: Run Kani List
+        uses: actions/github-script@v6
+        with:
+          script: |
+            head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head;
+            const fs = require('fs');
+            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
+            kaniOutput >> "$GITHUB_STEP_SUMMARY";
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 8ce27da..a4f6b46 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -3,10 +3,11 @@
 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
 }
@@ -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

From ec4d90932ad46076baf5d1c0c8615f5c8b50a504 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Mon, 18 Nov 2024 21:40:34 -0500
Subject: [PATCH 2/2] fix run error

---
 .github/workflows/kani.yml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 3e56fe0..b3c8aa3 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -66,12 +66,16 @@ jobs:
         working-directory: ${{github.workspace}}/head
         run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
       
-      # Step 3: Run list on the std library (assumes it creates kani_list.txt)
+      # 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: |
-            head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head;
             const fs = require('fs');
             const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
-            kaniOutput >> "$GITHUB_STEP_SUMMARY";
+            await core.summary
+              .addRaw(kaniOutput)
+              .write();
\ No newline at end of file