Parse log file of multi-threaded Kani run (terse output) into JSON (#324)

Given a run of Kani on the standard library with `--jobs=<N>
--output-format=terse` (and, typically, `autoharness`) enabled this
produces a machine-processable JSON result via
```
python3 log_parser.py \
  --kani-list-file kani-list.json \
  --analysis-results-dir std_lib_analysis/results/ \
  verification.log -o results.json
```
where each entry in the resulting JSON array is of the form
```
{
  "thread_id": int,
  "result": {
    "harness": string,
    "is_autoharness": bool,
    "autoharness_result": string,
    "with_contract": bool,
    "crate": string,
    "function": string,
    "function_safeness": string,
    "file_name": string,
    "n_failed_properties": int,
    "n_total_properties": int,
    "result": string,
    "time": string,
    "output": array
  }
}
```
With the help of `jq` one can then conveniently compute various metrics,
e.g.,
```
jq 'map(select(.result.result == "SUCCESSFUL" and
               .result.is_autoharness == true and
               .result.crate == "core" and
               .result.function_safeness == "unsafe" and
               .result.with_contract == true)) | length' results.json
```
to find the number of successfully-verified contracts of unsafe
functions in crate `core` that were verified using automatically
generated harnesses.


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-metrics.yml

@@ -26,7 +26,9 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
+      run: |
+        ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
+        rm kani-list.json
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7

.github/workflows/kani.yml

@@ -53,7 +53,7 @@ jobs:
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
-  kani-autoharness:
+  kani_autoharness:
     name: Verify std library using autoharness
     runs-on: ${{ matrix.os }}
     strategy:
@@ -124,7 +124,121 @@ jobs:
             --exclude-pattern ::precondition_check \
             --harness-timeout 10m \
             --default-unwind 1000 \
-            --jobs=3 --output-format=terse
+            --jobs=3 --output-format=terse | tee autoharness-verification.log
+          gzip autoharness-verification.log
+
+      - name: Upload Autoharness Verification Log
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-autoharness-verification.log.gz
+          path: autoharness-verification.log.gz
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+  run_kani_metrics:
+    name: Kani Metrics
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: true
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+
+      # Step 2: Run list on the std library
+      - name: Run Kani Metrics
+        run: |
+          scripts/run-kani.sh --run metrics --with-autoharness
+          pushd /tmp/std_lib_analysis
+          tar czf results.tar.gz results
+          popd
+
+      - name: Upload kani-list.json
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-kani-list.json
+          path: kani-list.json
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+      - name: Upload scanner results
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.tar.gz
+          path: /tmp/std_lib_analysis/results.tar.gz
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+  run-log-analysis:
+    name: Build JSON from logs
+    needs: [run_kani_metrics, kani_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:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: false
+
+      - name: Download log
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-autoharness-verification.log.gz
+
+      - name: Download kani-list.json
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-kani-list.json
+
+      - name: Download scanner results
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.tar.gz
+
+      - name: Run log parser
+        run: |
+          gunzip autoharness-verification.log.gz
+          tar xzf results.tar.gz
+          python3 scripts/kani-std-analysis/log_parser.py \
+            --kani-list-file kani-list.json \
+            --analysis-results-dir results/ \
+            autoharness-verification.log \
+            -o results.json
+
+      - name: Upload JSON
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.json
+          path: results.json
+          if-no-files-found: error
 
   run-kani-list:
     name: Kani List