Use log parser in workflow

Author: tautschnig

.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,110 @@ jobs:
             --exclude-pattern ::precondition_check \
             --harness-timeout 5m \
             --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
+
+      # 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: TestLocalToolchain
+    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: 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 ${{ matrix.os }}-autoharness-verification.log.gz
+          tar xzf ${{ matrix.os }}-results.tar.gz
+          python3 scripts/kani-std-analysis/log_parser.py \
+            --kani-list-file kani-list.json \
+            --analysis-results-dir results/ \
+            ${{ matrix.os }}-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

scripts/run-kani.sh

@@ -340,7 +340,6 @@ main() {
           --kani-list-file $current_dir/kani-list.json \
           --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 \