1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
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 ];
};
}
|