Add autoharness to run-kani script and use in CI

Author: tautschnig

.github/workflows/kani.yml

@@ -53,6 +53,33 @@ 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 on the std library for selected functions
+      - name: Run Kani Verification
+        run: |
+          scripts/run-kani.sh --kani-args \
+            --include-pattern alloc::__default_lib_allocator:: \
+            --jobs=3 --output-format=terse
+
   run-kani-list:
     name: Kani List
     runs-on: ubuntu-latest

scripts/run-kani.sh

@@ -297,6 +297,15 @@ main() {
                 --enable-unstable \
                 --cbmc-args --object-bits 12
         fi
+      elif [[ "$run_command" == "autoharness" ]]; then
+          # Run verification for all 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