Add autoharness-analyzer CI job (model-checking#344)

Run https://github.com/carolynzech/autoharness_analyzer and push its
results to the job summary.

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

Author: tautschnig

.github/workflows/kani.yml

@@ -79,3 +79,30 @@ jobs:
               .addHeading('Kani List Output', 2)
               .addRaw(kaniOutput, false)
               .write();
+
+  run-autoharness-analyzer:
+    name: Kani Autoharness Analyzer
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run autoharness analyzer on the std library
+      - name: Run Autoharness Analyzer
+        run: scripts/run-kani.sh --run autoharness-analyzer
+
+      # Step 3: Add output to job summary
+      - name: Add Autoharness Analyzer output to job summary
+        run: |
+          echo "# Autoharness Failure Summary" >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate core, all functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate core, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate std, all functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate std, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"

scripts/run-kani.sh

@@ -7,7 +7,7 @@ usage() {
     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|metrics>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, or collect Kani-specific metrics. Defaults to 'verify-std' if not specified."
+    echo "  --run <verify-std|list|metrics|autoharness-analyzer>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, collect Kani-specific metrics, or summarize autoharness failure reasons. 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
 }
@@ -34,7 +34,7 @@ while [[ $# -gt 0 ]]; do
             fi
             ;;
         --run)
-            if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics") ]]; then
+            if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics" || $2 == "autoharness-analyzer") ]]; then
                 run_command=$2
                 shift 2
             else
@@ -317,6 +317,31 @@ main() {
           --metrics-file metrics-data-std.json
         popd
         rm kani-list.json
+    elif [[ "$run_command" == "autoharness-analyzer" ]]; then
+        echo "Running Kani autoharness codegen command..."
+        "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \
+            --only-codegen -j --output-format=terse \
+            $unstable_args \
+            --no-assert-contracts \
+            $command_args \
+            --enable-unstable \
+            --cbmc-args --object-bits 12
+        # remove metadata file for Kani-generated "dummy" crate that we won't
+        # get scanner data for
+        rm target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/dummy-*
+        echo "Running Kani's std-analysis command..."
+        pushd scripts/kani-std-analysis
+        ./std-analysis.sh $build_dir
+        popd
+        echo "Running autoharness-analyzer command..."
+        git clone --depth 1 https://github.com/carolynzech/autoharness_analyzer
+        cd autoharness_analyzer
+        cargo run -- --per-crate \
+          ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \
+          /tmp/std_lib_analysis/results/
+        cargo run -- --per-crate --unsafe-fns-only \
+          ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \
+          /tmp/std_lib_analysis/results/
     fi
 }