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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
{ lib
, llvmPackages
, callPackage
, fetchFromGitHub
, cmake
, python3
, z3
, stp
, cryptominisat
, gperftools
, sqlite
, gtest
, lit
, nix-update-script
# 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
# Klee uclibc. Defaults to the bundled version.
, kleeuClibc ? null
# Extra klee-uclibc config for the default klee-uclibc.
, extraKleeuClibcConfig ? {}
}:
# Klee supports these LLVM versions.
let
llvmVersion = llvmPackages.llvm.version;
inherit (lib.strings) versionAtLeast versionOlder;
in
assert versionAtLeast llvmVersion "11" && versionOlder llvmVersion "17";
let
# The chosen version of klee-uclibc.
chosenKleeuClibc =
if kleeuClibc == null then
callPackage ./klee-uclibc.nix {
llvmPackages = llvmPackages;
inherit extraKleeuClibcConfig debugRuntime runtimeAsserts;
}
else
kleeuClibc;
# Python used for KLEE tests.
kleePython = python3.withPackages (ps: with ps; [ tabulate ]);
in
llvmPackages.stdenv.mkDerivation rec {
pname = "klee";
version = "3.1";
src = fetchFromGitHub {
owner = "klee";
repo = "klee";
rev = "v${version}";
hash = "sha256-5js1N8qVF0lCkahSU3ojT7+p/a9IaUpPWhIyFHEzqto=";
};
nativeBuildInputs = [ cmake ];
buildInputs = [
llvmPackages.llvm
cryptominisat
gperftools
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; })
];
cmakeBuildType = if debug then "Debug" else if !debug && includeDebugInfo then "RelWithDebInfo" else "MinSizeRel";
cmakeFlags = let
onOff = val: if val then "ON" else "OFF";
in [
"-DKLEE_RUNTIME_BUILD_TYPE=${if debugRuntime then "Debug" else "Release"}"
"-DLLVMCC=${llvmPackages.clang}/bin/clang"
"-DLLVMCXX=${llvmPackages.clang}/bin/clang++"
"-DKLEE_ENABLE_TIMESTAMP=${onOff false}"
"-DKLEE_UCLIBC_PATH=${chosenKleeuClibc}"
"-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 --build .
'';
# https://github.com/klee/klee/issues/1690
hardeningDisable = [ "fortify" ];
enableParallelBuilding = true;
doCheck = true;
passthru = {
updateScript = nix-update-script {
extraArgs = [ "--version-regex" "v(\d\.\d)" ];
};
# Let the user access the chosen uClibc outside the derivation.
uclibc = chosenKleeuClibc;
};
meta = with lib; {
mainProgram = "klee";
description = "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 ];
};
}
|
