diff options
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic/klee/default.nix')
| -rw-r--r-- | nixpkgs/pkgs/applications/science/logic/klee/default.nix | 81 |
1 files changed, 64 insertions, 17 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/klee/default.nix b/nixpkgs/pkgs/applications/science/logic/klee/default.nix index e0ace7e81c82..612d9fd57c7c 100644 --- a/nixpkgs/pkgs/applications/science/logic/klee/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/klee/default.nix @@ -1,5 +1,5 @@ -{ stdenv -, lib +{ lib +, callPackage , fetchFromGitHub , fetchpatch , cmake @@ -14,13 +14,37 @@ , sqlite , gtest , lit + +# Build KLEE in debug mode. Defaults to false. , debug ? false + +# Include debug info in the build. Defaults to true. +, includeDebugInfo ? true + +# Enable KLEE asserts. Defaults to true, since LLVM is built with them. +, asserts ? true + +# Build the KLEE runtime in debug mode. Defaults to true, as this improves +# stack traces of the software under test. +, debugRuntime ? true + +# Enable runtime asserts. Default false. +, runtimeAsserts ? false + +# Extra klee-uclibc config. +, extraKleeuClibcConfig ? {} }: let + # Python used for KLEE tests. kleePython = python3.withPackages (ps: with ps; [ tabulate ]); + + # The klee-uclibc derivation. + kleeuClibc = callPackage ./klee-uclibc.nix { + inherit clang_9 llvmPackages_9 extraKleeuClibcConfig debugRuntime runtimeAsserts; + }; in -stdenv.mkDerivation rec { +clang_9.stdenv.mkDerivation rec { pname = "klee"; version = "2.2"; src = fetchFromGitHub { @@ -30,11 +54,12 @@ stdenv.mkDerivation rec { sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M="; }; buildInputs = [ - llvmPackages_9.llvm clang_9 z3 stp cryptominisat + llvmPackages_9.llvm + z3 stp cryptominisat gperftools sqlite ]; nativeBuildInputs = [ - cmake + cmake clang_9 ]; checkInputs = [ gtest @@ -46,14 +71,17 @@ stdenv.mkDerivation rec { ]; cmakeFlags = let - buildType = if debug then "Debug" else "Release"; - in - [ - "-DCMAKE_BUILD_TYPE=${buildType}" - "-DKLEE_RUNTIME_BUILD_TYPE=${buildType}" - "-DENABLE_POSIX_RUNTIME=ON" - "-DENABLE_UNIT_TESTS=ON" - "-DENABLE_SYSTEM_TESTS=ON" + onOff = val: if val then "ON" else "OFF"; + in [ + "-DCMAKE_BUILD_TYPE=${if debug then "Debug" else if !debug && includeDebugInfo then "RelWithDebInfo" else "MinSizeRel"}" + "-DKLEE_RUNTIME_BUILD_TYPE=${if debugRuntime then "Debug" else "Release"}" + "-DKLEE_ENABLE_TIMESTAMP=${onOff false}" + "-DENABLE_KLEE_UCLIBC=${onOff true}" + "-DKLEE_UCLIBC_PATH=${kleeuClibc}" + "-DENABLE_KLEE_ASSERTS=${onOff asserts}" + "-DENABLE_POSIX_RUNTIME=${onOff true}" + "-DENABLE_UNIT_TESTS=${onOff true}" + "-DENABLE_SYSTEM_TESTS=${onOff true}" "-DGTEST_SRC_DIR=${gtest.src}" "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include" "-Wno-dev" @@ -66,21 +94,40 @@ stdenv.mkDerivation rec { patchShebangs . ''; - /* This patch is currently necessary for the unit test suite to run correctly. - * See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03136.html - * and https://github.com/klee/klee/pull/1458 for more information. - */ patches = map fetchpatch [ + /* This patch is currently necessary for the unit test suite to run correctly. + * See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03136.html + * and https://github.com/klee/klee/pull/1458 for more information. + */ { name = "fix-gtest"; sha256 = "F+/6videwJZz4sDF9lnV4B8lMx6W11KFJ0Q8t1qUDf4="; url = "https://github.com/klee/klee/pull/1458.patch"; } + + # This patch fixes test compile issues with glibc 2.33+. + { + name = "fix-glibc-2.33"; + sha256 = "PzxqtFyLy9KF1eA9AAKg1tu+ggRdvu7leuvXifayIcc="; + url = "https://github.com/klee/klee/pull/1385.patch"; + } + + # /etc/mtab doesn't exist in the Nix build sandbox. + { + name = "fix-etc-mtab-in-tests"; + sha256 = "2Yb/rJA791esNNqq8uAXV+MML4YXIjPKkHBOufvyRoQ="; + url = "https://github.com/klee/klee/pull/1471.patch"; + } ]; doCheck = true; checkTarget = "check"; + passthru = { + # Let the user depend on `klee.uclibc` for klee-uclibc + uclibc = kleeuClibc; + }; + meta = with lib; { description = "A symbolic virtual machine built on top of LLVM"; longDescription = '' |