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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
{ lib
, stdenv
, callPackage
, fetchFromGitHub
, cmake
, clang
, llvm
, python3
, zlib
, z3
, stp
, cryptominisat
, gperftools
, 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 stdenv clang llvm extraKleeuClibcConfig debugRuntime runtimeAsserts;
};
in stdenv.mkDerivation rec {
pname = "klee";
version = "3.0";
src = fetchFromGitHub {
owner = "klee";
repo = "klee";
rev = "v${version}";
hash = "sha256-y5lWmtIcLAthQ0oHYQNd+ir75YaxHZR9Jgiz+ZUFQjY=";
};
nativeBuildInputs = [ cmake ];
buildInputs = [
cryptominisat
gperftools
llvm
sqlite
stp
z3
];
nativeCheckInputs = [
gtest
# Should appear BEFORE lit, since lit passes through python rather
# than the python environment we make.
kleePython
(lit.override { python = kleePython; })
];
cmakeFlags = let
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"}"
"-DLLVMCC=${clang}/bin/clang"
"-DLLVMCXX=${clang}/bin/clang++"
"-DKLEE_ENABLE_TIMESTAMP=${onOff false}"
"-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"
];
# Silence various warnings during the compilation of fortified bitcode.
env.NIX_CFLAGS_COMPILE = toString ["-Wno-macro-redefined"];
prePatch = ''
patchShebangs .
'';
doCheck = true;
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 = ''
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 ];
};
}
|