test: Skip kani if not enough RAM available

Trying to run the kani integration test outside of the CI will almost
certainly result in out of memory conditions in the best case, and in
system hangs in the worst case. Therefore, do not attempt to run kani if
running tests locally with too little RAM.

Signed-off-by: Patrick Roy <[email protected]>

tests/integration_tests/test_kani.py

@@ -4,8 +4,10 @@
 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 psutil
 import pytest
 
 from framework import utils
@@ -19,15 +21,23 @@ def test_kani(results_dir):
     """
     Test all Kani proof harnesses.
     """
+    # https://psutil.readthedocs.io/en/latest/#psutil.virtual_memory confusingly enough returns
+    # information about the physical memory. Limiting to 64GB should exclude most consumer hardware,
+    # preventing the test from locking up peoples computers, while still allowing them to force their
+    # way through it with enough swap.
+    if (
+        psutil.swap_memory().total + psutil.virtual_memory().total
+        <= 64 * 1000 * 1000 * 1000
+    ):
+        pytest.skip("kani requires at least 64GB RAM")
+
     # --enable-stubbing is required to enable the stubbing feature
     # --restrict-vtable is required for some virtio queue proofs, which go out of memory otherwise
     # -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")