Add autoharness to run-kani script and use in CI

For now, do not run any actual harnesses.

Author: tautschnig

.github/workflows/kani.yml

@@ -53,6 +53,36 @@ jobs:
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
+  kani-autoharness:
+    name: Verify std library using autoharness
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: false
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run Kani autoharness on the std library for selected functions.
+      # Uses "--include-pattern no::such::function" to make sure we do not try
+      # to run across all possible functions as that may take a lot longer than
+      # expected
+      - name: Run Kani Verification
+        run: |
+          scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern no:such::function:: \
+            --jobs=3 --output-format=terse
+
   run-kani-list:
     name: Kani List
     runs-on: ubuntu-latest

scripts/run-kani.sh

@@ -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") ]]; then
                 run_command=$2
                 shift 2
             else
@@ -297,13 +297,23 @@ main() {
                 --enable-unstable \
                 --cbmc-args --object-bits 12
         fi
+      elif [[ "$run_command" == "autoharness" ]]; then
+          # Run verification for a subset of automatically generated harnesses
+          # (not in parallel)
+          echo "Running Kani autoharness command..."
+          "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \
+              $unstable_args \
+              --no-assert-contracts \
+              $command_args \
+              --enable-unstable \
+              --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" list -Z list $unstable_args ./library --std --format markdown
+        "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown
     elif [[ "$run_command" == "metrics" ]]; then
         local current_dir=$(pwd)
         echo "Running Kani list command..."
-        "$kani_path" list -Z list $unstable_args ./library --std --format json
+        "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json
         pushd scripts/kani-std-analysis
         echo "Running Kani's std-analysis command..."
         ./std-analysis.sh $build_dir