From b2a767648de9446dbbaa68ef2bfb3a1d59b3b209 Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Wed, 5 Jun 2024 10:24:48 +0000 Subject: [PATCH] nix: Add Kani Signed-off-by: Nick Spinale --- hacking/nix/scope/default.nix | 2 + hacking/nix/scope/kani/cbmc-viewer.nix | 33 ++++++ hacking/nix/scope/kani/default.nix | 130 +++++++++++++++++++++++ hacking/nix/scope/shell-for-hacking.nix | 12 ++- hacking/nix/scope/shell-for-makefile.nix | 2 + hacking/nix/scope/verus/default.nix | 2 +- hacking/nix/top-level/default.nix | 3 + 7 files changed, 180 insertions(+), 4 deletions(-) create mode 100644 hacking/nix/scope/kani/cbmc-viewer.nix create mode 100644 hacking/nix/scope/kani/default.nix diff --git a/hacking/nix/scope/default.nix b/hacking/nix/scope/default.nix index 8b9af45f5..08b3418b8 100644 --- a/hacking/nix/scope/default.nix +++ b/hacking/nix/scope/default.nix @@ -176,6 +176,8 @@ superCallPackage ../rust-utils {} self // capdl-tool = callBuildBuildPackage ./capdl-tool {}; + kani = callBuildBuildPackage ./kani {}; + verus = callBuildBuildPackage ./verus {}; dafny = callBuildBuildPackage ./dafny {}; diff --git a/hacking/nix/scope/kani/cbmc-viewer.nix b/hacking/nix/scope/kani/cbmc-viewer.nix new file mode 100644 index 000000000..320e9f610 --- /dev/null +++ b/hacking/nix/scope/kani/cbmc-viewer.nix @@ -0,0 +1,33 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ lib +, buildPythonPackage +, fetchFromGitHub +, setuptools +, jinja2 +, voluptuous +}: + +buildPythonPackage rec { + pname = "cbmc-viewer"; + version = "3.8"; + + format = "pyproject"; + + src = fetchFromGitHub { + owner = "model-checking"; + repo = "cbmc-viewer"; + rev = "viewer-3.8"; + hash = "sha256-GIpinwjl/v6Dz5HyOsoPfM9fxG0poZ0HPsKLe9js9vM="; + }; + + propagatedBuildInputs = [ + setuptools + jinja2 + voluptuous + ]; +} diff --git a/hacking/nix/scope/kani/default.nix b/hacking/nix/scope/kani/default.nix new file mode 100644 index 000000000..de1b3dfb7 --- /dev/null +++ b/hacking/nix/scope/kani/default.nix @@ -0,0 +1,130 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ lib, stdenv +, callPackage +, fetchFromGitHub +, makeWrapper +, python3 +, python3Packages +, cbmc +, kissat + +, crateUtils +, vendorLockfile +, sources +, fenix +, elaborateRustEnvironment +, mkDefaultElaborateRustEnvironmentArgs +, mkMkCustomTargetPathForEnvironment +}: + +let + cbmc-viewer = python3Packages.callPackage ./cbmc-viewer.nix {}; + + rustToolchainAttrs = builtins.fromTOML (builtins.readFile (src + "/rust-toolchain.toml")); + + rustToolchain = fenix.fromToolchainFile { + file = crateUtils.toTOMLFile "rust-toolchain.toml" (crateUtils.clobber [ + rustToolchainAttrs + { + toolchain.components = rustToolchainAttrs.toolchain.components ++ [ "rust-src" ]; + } + ]); + sha256 = "sha256-akRjdj8CP0mRL4czKC7GssksdunxdckSNiNU36zduV0="; + }; + + rustEnvironment = lib.fix (self: elaborateRustEnvironment (mkDefaultElaborateRustEnvironmentArgs { + inherit rustToolchain; + } // { + inherit (rustToolchainAttrs.toolchain) channel; + mkCustomTargetPath = mkMkCustomTargetPathForEnvironment { + rustEnvironment = self; + }; + })); + + src = fetchFromGitHub { + owner = "model-checking"; + repo = "kani"; + rev = "kani-0.52.0"; + sha256 = "sha256-LyMZt6E1U03n4w5L9JMxgklAyvhltSJTvRl7zxYpw6A="; + }; + + localLockfile = vendorLockfile { + inherit rustToolchain; + lockfile = src + "/Cargo.lock"; + }; + + sysrootLockfile = rustEnvironment.vendoredSysrootLockfile; + + augmentedLockfileValue = { + version = + assert localLockfile.lockfileValue.version == sysrootLockfile.lockfileValue.version; + localLockfile.lockfileValue.version; + package = localLockfile.lockfileValue.package ++ sysrootLockfile.lockfileValue.package; + }; + + augmentedLockfile = vendorLockfile { + inherit rustToolchain; + lockfileValue = augmentedLockfileValue; + }; + + configFragment = crateUtils.toTOMLFile "config" augmentedLockfile.configFragment; + + pythonEnv = python3.buildEnv.override { + extraLibs = [ cbmc-viewer ]; + }; + +in +stdenv.mkDerivation { + name = "kani"; + + inherit src; + + nativeBuildInputs = [ + rustToolchain + makeWrapper + cbmc + kissat + ]; + + postPatch = '' + # HACK + substituteInPlace src/setup.rs \ + --replace \ + 'Command::new("python3")' \ + 'Command::new("true")' + ''; + + configurePhase = '' + cat ${configFragment} >> .cargo/config.toml + ''; + + buildPhase = '' + RUSTUP_HOME=/var/empty/rustup \ + RUSTUP_TOOLCHAIN=none \ + cargo bundle + ''; + + installPhase = '' + install -D -t $out/bin target/kani/bin/{kani,cargo-kani} + + for p in $out/bin/*; do + wrapProgram $p \ + --set KANI_HOME $out/lib/kani \ + --prefix PATH : ${lib.makeBinPath [ rustToolchain pythonEnv ]} + done + + $out/bin/kani setup \ + --use-local-bundle kani-*.tar.gz \ + --use-local-toolchain ${rustToolchain} + ''; + + passthru = { + inherit rustEnvironment; + inherit cbmc-viewer; + }; +} diff --git a/hacking/nix/scope/shell-for-hacking.nix b/hacking/nix/scope/shell-for-hacking.nix index a56026f73..063f75af4 100644 --- a/hacking/nix/scope/shell-for-hacking.nix +++ b/hacking/nix/scope/shell-for-hacking.nix @@ -15,14 +15,15 @@ , python3Packages , cmake +, kani +, verus + , strace , cntr , cachix , openssl -, verus - , shellForMakefile }: @@ -40,10 +41,11 @@ mkShell (shellForMakefile.apply { perl cmake rustPlatform.bindgenHook + kani + verus strace cntr cachix - verus ]; buildInputs = [ @@ -51,6 +53,10 @@ mkShell (shellForMakefile.apply { ]; shellHook = '' + kargo() { + cargo +${kani.rustEnvironment.channel} "$@" + } + vargo() { cargo +${verus.rustEnvironment.channel} "$@" } diff --git a/hacking/nix/scope/shell-for-makefile.nix b/hacking/nix/scope/shell-for-makefile.nix index fa66129d8..2ba156d5b 100644 --- a/hacking/nix/scope/shell-for-makefile.nix +++ b/hacking/nix/scope/shell-for-makefile.nix @@ -8,6 +8,7 @@ , python3 , reuse , cargo-audit +, kani }: let @@ -21,6 +22,7 @@ let python3 reuse cargo-audit + kani ]; }; diff --git a/hacking/nix/scope/verus/default.nix b/hacking/nix/scope/verus/default.nix index 4dc937144..fdd02951b 100644 --- a/hacking/nix/scope/verus/default.nix +++ b/hacking/nix/scope/verus/default.nix @@ -92,6 +92,6 @@ stdenv.mkDerivation { passthru = { inherit rustEnvironment; - rustToolchainChannel = rustToolchainAttrs.toolchain.channel; + inherit z3; }; } diff --git a/hacking/nix/top-level/default.nix b/hacking/nix/top-level/default.nix index f09e2e99f..389722a0f 100644 --- a/hacking/nix/top-level/default.nix +++ b/hacking/nix/top-level/default.nix @@ -62,6 +62,9 @@ in { sel4testInstancesList + pkgs.build.this.kani + pkgs.build.this.verus + pkgs.host.aarch32.none.this.worlds.default.seL4 pkgs.host.ia32.none.this.worlds.default.seL4