@@ -0,0 +1,110 @@
1+{ stdenv
2+, lib
3+, fetchFromGitHub
4+, fetchpatch
5+, cmake
6+, llvmPackages_9
7+, clang_9
8+, python3
9+, zlib
10+, z3
11+, stp
12+, cryptominisat
13+, gperftools
14+, sqlite
15+, gtest
16+, lit
17+, debug ? false
18+}:
19+
20+let
21+ kleePython = python3.withPackages (ps: with ps; [ tabulate ]);
22+in
23+stdenv.mkDerivation rec {
24+ pname = "klee";
25+ version = "2.2";
26+ src = fetchFromGitHub {
27+ owner = "klee";
28+ repo = "klee";
29+ rev = "v${version}";
30+ sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M=";
31+ };
32+ buildInputs = [
33+ llvmPackages_9.llvm clang_9 z3 stp cryptominisat
34+ gperftools sqlite
35+ ];
36+ nativeBuildInputs = [
37+ cmake
38+ ];
39+ checkInputs = [
40+ gtest
41+
42+ # Should appear BEFORE lit, since lit passes through python rather
43+ # than the python environment we make.
44+ kleePython
45+ (lit.override { python3 = kleePython; })
46+ ];
47+
48+ cmakeFlags = let
49+ buildType = if debug then "Debug" else "Release";
50+ in
51+ [
52+ "-DCMAKE_BUILD_TYPE=${buildType}"
53+ "-DKLEE_RUNTIME_BUILD_TYPE=${buildType}"
54+ "-DENABLE_POSIX_RUNTIME=ON"
55+ "-DENABLE_UNIT_TESTS=ON"
56+ "-DENABLE_SYSTEM_TESTS=ON"
57+ "-DGTEST_SRC_DIR=${gtest.src}"
58+ "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include"
59+ "-Wno-dev"
60+ ];
61+
62+ # Silence various warnings during the compilation of fortified bitcode.
63+ NIX_CFLAGS_COMPILE = ["-Wno-macro-redefined"];
64+
65+ prePatch = ''
66+ patchShebangs .
67+ '';
68+
69+ /* This patch is currently necessary for the unit test suite to run correctly.
70+ * See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03136.html
71+ * and https://github.com/klee/klee/pull/1458 for more information.
72+ */
73+ patches = map fetchpatch [
74+ {
75+ name = "fix-gtest";
76+ sha256 = "F+/6videwJZz4sDF9lnV4B8lMx6W11KFJ0Q8t1qUDf4=";
77+ url = "https://github.com/klee/klee/pull/1458.patch";
78+ }
79+ ];
80+
81+ doCheck = true;
82+ checkTarget = "check";
83+
84+ meta = with lib; {
85+ description = "A symbolic virtual machine built on top of LLVM";
86+ longDescription = ''
87+ KLEE is a symbolic virtual machine built on top of the LLVM compiler
88+ infrastructure. Currently, there are two primary components:
89+
90+ 1. The core symbolic virtual machine engine; this is responsible for
91+ executing LLVM bitcode modules with support for symbolic values. This
92+ is comprised of the code in lib/.
93+
94+ 2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with
95+ additional support for making parts of the operating system environment
96+ symbolic.
97+
98+ Additionally, there is a simple library for replaying computed inputs on
99+ native code (for closed programs). There is also a more complicated
100+ infrastructure for replaying the inputs generated for the POSIX/Linux
101+ emulation layer, which handles running native programs in an environment
102+ that matches a computed test input, including setting up files, pipes,
103+ environment variables, and passing command line arguments.
104+ '';
105+ homepage = "https://klee.github.io/";
106+ license = licenses.ncsa;
107+ platforms = [ "x86_64-linux" ];
108+ maintainers = with maintainers; [ numinit ];
109+ };
110+}