ci: enable running kani on ARM

Kani supports verification on ARM since version 0.37.0 [1], so enable it in our CI. [1]: https://github.com/model-checking/kani/blob/main/CHANGELOG.md#0370 Signed-off-by: Patrick Roy <[email protected]> Signed-off-by: Pablo Barbáchano <[email protected]>
loopholelabs · Oct 8, 2024 · 886c66d · 886c66d
1 parent e70195f
commit 886c66d
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 3 deletions.
diff --git a/.buildkite/pipeline_pr.py b/.buildkite/pipeline_pr.py
@@ -56,7 +56,7 @@
         "./tools/devtool -y test --no-build -- ../tests/integration_tests/test_kani.py -n auto",
         # Kani step default
         # Kani runs fastest on m6a.metal
-        instances=["m6a.metal"],
+        instances=["m6a.metal", "m7g.metal"],
         platforms=[("al2", "linux_5.10")],
         timeout_in_minutes=300,
         **DEFAULTS_PERF,

diff --git a/tests/integration_tests/test_kani.py b/tests/integration_tests/test_kani.py
@@ -17,7 +17,6 @@
 # The `check_output` timeout will always fire before this one, but we need to
 # set a timeout here to override the default pytest timeout of 180s.
 @pytest.mark.timeout(2420)
-@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",

diff --git a/tools/devctr/Dockerfile b/tools/devctr/Dockerfile
@@ -108,7 +108,7 @@ RUN curl https://sh.rustup.rs -sSf | sh -s -- -y --profile minimal --default-too
     && rustup target add aarch64-unknown-linux-musl \
     && rustup component add llvm-tools-preview clippy rustfmt \
     && cargo install --locked cargo-audit cargo-deny grcov cargo-sort cargo-afl \
-    && (if [ "$ARCH" = "x86_64" ]; then cargo install --locked kani-verifier && cargo kani setup; else true; fi) \
+    && cargo install --locked kani-verifier && cargo kani setup \
     \
     && apt-get update \
     && apt-get -y install --no-install-recommends \