test: Skip kani if not enough RAM

.buildkite/pipeline_pr.py

@@ -109,7 +109,9 @@
 if any(x.parent.name == "tools" and "release" in x.name for x in changed_files):
     steps.append(release_grp)
 
-if not changed_files or any(x.suffix == ".rs" for x in changed_files):
+if not changed_files or any(
+    x.suffix in [".rs", ".toml", ".lock"] for x in changed_files
+):
     steps.append(kani_grp)
 
 if run_all_tests(changed_files):

docs/formal-verification.md

@@ -45,17 +45,18 @@ properties, **all Kani harnesses are run on every pull request in our CI.** To
 check whether the harnesses all work for your pull request, check out the
 “Kani” [Buildkite](https://buildkite.com/) step.
 
-You can also execute our harnesses locally through `./tools/devtool test --
-integration_tests/build/test_kani.py`. To only run individual harnesses, you
-will need to first [install
+To run our harnesses locally, you can either enter our CI docker container
+via `./tools/devtool shell -p`, or by [installing
 Kani](https://model-checking.github.io/kani/install-guide.html#installing-the-latest-version)
-locally.
-From there on, individual test can be run via `cargo kani` similarly to how
-`cargo test` can run individual unit tests, the only difference being that the
-harness needs to be specified via `--harness`. Note that the first invocation
+locally.  Note that the first invocation
 of Kani post-installation might take a while, due to it setting up some
 dependencies.
 
+Individual harnesses can then be executed using `cargo kani` similarly to how
+`cargo test` can run individual unit tests, the only difference being that the
+harness needs to be specified via `--harness`. Note, however, that many harnesses
+require significant memory, and might result in OOM conditions.
+
 ## An example harness
 
 The following is adapted from our Rate Limiter harness suite. It aims to verify

tests/integration_tests/test_kani.py

@@ -4,6 +4,7 @@
 Proofs ensuring memory safety properites, user-defined assertions,
 absence of panics and some types of unexpected behavior (e.g., arithmetic overflows).
 """
+import os
 import platform
 
 import pytest
@@ -15,6 +16,10 @@
 
 @pytest.mark.timeout(1800)
 @pytest.mark.skipif(PLATFORM != "x86_64", reason="Kani proofs run only on x86_64.")
+@pytest.mark.skipif(
+    os.environ.get("BUILDKITE") != "true",
+    reason="Kani's memory requirements likely cannot be satisfied locally",
+)
 def test_kani(results_dir):
     """
     Test all Kani proof harnesses.
@@ -24,10 +29,8 @@ def test_kani(results_dir):
     # -j enables kani harnesses to be verified in parallel (required to keep CI time low)
     # --output-format terse is required by -j
     # --enable-unstable is needed for each of the above
-    rc, stdout, stderr = utils.run_cmd(
+    _, stdout, _ = utils.run_cmd(
         "cargo kani --enable-unstable --enable-stubbing --restrict-vtable -j --output-format terse"
     )
 
-    assert rc == 0, stderr
-
     (results_dir / "kani_log").write_text(stdout, encoding="utf-8")

tools/devtool

@@ -574,7 +574,7 @@ cmd_test() {
     # in order to set-up the Firecracker jail (manipulating cgroups, net
     # namespaces, etc).
     # We need to run a privileged container to get that kind of access.
-    env |grep -P "^(AWS_EMF_|BUILDKITE_|CODECOV_)" > env.list
+    env |grep -P "^(AWS_EMF_|BUILDKITE|CODECOV_)" > env.list
 
     if [[ "$BUILDKITE" = "true" ]]; then
       # Disable turbo boost. Some of our tests are performance tests, and we want minimum variability wrt processor frequency