diff options
| -rw-r--r-- | pkgs/applications/science/logic/klee/default.nix | 110 | ||||
| -rw-r--r-- | pkgs/top-level/all-packages.nix | 2 |
2 files changed, 112 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/klee/default.nix b/pkgs/applications/science/logic/klee/default.nix new file mode 100644 index 00000000000..e0ace7e81c8 --- /dev/null +++ b/pkgs/applications/science/logic/klee/default.nix @@ -0,0 +1,110 @@ +{ stdenv +, lib +, fetchFromGitHub +, fetchpatch +, cmake +, llvmPackages_9 +, clang_9 +, python3 +, zlib +, z3 +, stp +, cryptominisat +, gperftools +, sqlite +, gtest +, lit +, debug ? false +}: + +let + kleePython = python3.withPackages (ps: with ps; [ tabulate ]); +in +stdenv.mkDerivation rec { + pname = "klee"; + version = "2.2"; + src = fetchFromGitHub { + owner = "klee"; + repo = "klee"; + rev = "v${version}"; + sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M="; + }; + buildInputs = [ + llvmPackages_9.llvm clang_9 z3 stp cryptominisat + gperftools sqlite + ]; + nativeBuildInputs = [ + cmake + ]; + checkInputs = [ + gtest + + # Should appear BEFORE lit, since lit passes through python rather + # than the python environment we make. + kleePython + (lit.override { python3 = kleePython; }) + ]; + + 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" + "-DGTEST_SRC_DIR=${gtest.src}" + "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include" + "-Wno-dev" + ]; + + # Silence various warnings during the compilation of fortified bitcode. + NIX_CFLAGS_COMPILE = ["-Wno-macro-redefined"]; + + prePatch = '' + 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 [ + { + name = "fix-gtest"; + sha256 = "F+/6videwJZz4sDF9lnV4B8lMx6W11KFJ0Q8t1qUDf4="; + url = "https://github.com/klee/klee/pull/1458.patch"; + } + ]; + + doCheck = true; + checkTarget = "check"; + + meta = with lib; { + description = "A symbolic virtual machine built on top of LLVM"; + longDescription = '' + KLEE is a symbolic virtual machine built on top of the LLVM compiler + infrastructure. Currently, there are two primary components: + + 1. The core symbolic virtual machine engine; this is responsible for + executing LLVM bitcode modules with support for symbolic values. This + is comprised of the code in lib/. + + 2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with + additional support for making parts of the operating system environment + symbolic. + + Additionally, there is a simple library for replaying computed inputs on + native code (for closed programs). There is also a more complicated + infrastructure for replaying the inputs generated for the POSIX/Linux + emulation layer, which handles running native programs in an environment + that matches a computed test input, including setting up files, pipes, + environment variables, and passing command line arguments. + ''; + homepage = "https://klee.github.io/"; + license = licenses.ncsa; + platforms = [ "x86_64-linux" ]; + maintainers = with maintainers; [ numinit ]; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index e43ad8707db..6d0addc1d59 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -26574,6 +26574,8 @@ with pkgs; klayout = libsForQt5.callPackage ../applications/misc/klayout { }; + klee = callPackage ../applications/science/logic/klee { }; + kmetronome = libsForQt5.callPackage ../applications/audio/kmetronome { }; kmplayer = libsForQt5.callPackage ../applications/video/kmplayer { }; |