Add CI script to check for bookrunner failures

.github/workflows/kani.yml

@@ -45,6 +45,9 @@ jobs:
       - name: Print book runner text results
         run: cat build/output/latest/html/bookrunner.txt
 
+      - name: Detect unpexpected book runner failures
+        run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
+
       # On one OS only, build the documentation, too.
       - name: Build Documentation
         run: ./docs/build-docs.sh

docs/src/bookrunner.md

@@ -46,17 +46,17 @@ This section describes how the book runner operates at a high level.
 To kick off the book runner process use
 
 ```
-./x.py run -i --stage 1 bookrunner
+cargo run -p bookrunner
 ```
 
 The main function of the bookrunner is `generate_run()` in
-[`src/tools/bookrunner/src/books.rs`](https://github.com/model-checking/kani/blob/main/src/tools/bookrunner/src/books.rs),
+[`src/tools/bookrunner/src/books.rs`](https://github.com/model-checking/kani/blob/main/tools/bookrunner/src/books.rs),
 which follows these steps:
- * First, it calls the different `parse_..._hierarchy()` functions which parse
-   the summary files for each book.
+ * First, it sets up all the books.
+ * For each book, it calls the `parse_..._hierarchy()` function to parse its summary files.
  * The `extract_examples(...)` function uses `rustdoc` to extract all examples
-   from the books.
- * Then for each example it will check if there is a corresponding `.props` file
+   from each book.
+ * For each example it will check if there is a corresponding `.props` file
    in `src/tools/bookrunner/configs/`. The contents of these files (e.g.,
    command-line options) are prepended to the example.
  * All examples are written in the `src/test/bookrunner/books/` folder.

scripts/ci/detect_bookrunner_failures.sh

@@ -0,0 +1,36 @@
+#!/bin/bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+# This script checks that the number of failures in a bookrunner run are below
+# the threshold computed below.
+#
+# The threshold is roughly computed as: `1.05 * <number of expected failures>`
+# The extra 5% allows us to account for occasional timeouts. It is reviewed and
+# updated whenever the Rust toolchain version is updated.
+EXPECTED=621
+THRESHOLD=$(expr ${EXPECTED} \* 105 / 100) # Add 5% threshold
+
+if [[ $# -ne 1 ]]; then
+  echo "$0: Error: Specify the bookrunner text report"
+  exit 1
+fi
+
+# Get the summary line, which looks like:
+#   `# of tests: <total> ✔️ <passes>   ❌ <failures>`
+SUMMARY_LINE=`head -n 1 $1`
+
+# Parse the summary line and extract the number of failures
+read -a strarr <<< $SUMMARY_LINE
+NUM_FAILURES=${strarr[-1]}
+
+# Print a message and return a nonzero code if the threshold is exceeded
+if [[ $NUM_FAILURES -ge $THRESHOLD ]]; then
+    echo "Error: The number of failures from bookrunner is higher than expected!"
+    echo "This means that your changes are causing at least 5% more failures than in previous bookrunner runs."
+    echo "To check these failures locally, run \`cargo run -p bookrunner\` and inspect the report in \`build/output/latest/html/index.html\`."
+    echo "For more details on bookrunner, go to https://model-checking.github.io/kani/bookrunner.html"
+    exit 1
+fi