klee: build with klee-uclibc
This ends up enabling more of the KLEE test suite, so apply patches to fix those too.
This commit is contained in:
Morgan Jones
parent
96255dd472
commit
98a951c509
2 changed files with 162 additions and 17 deletions
|
|
@ -1,5 +1,5 @@
|
|||
{ stdenv
|
||||
, lib
|
||||
{ lib
|
||||
, callPackage
|
||||
, fetchFromGitHub
|
||||
, fetchpatch
|
||||
, cmake
|
||||
|
|
@ -14,13 +14,37 @@
|
|||
, 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 clang_9 llvmPackages_9 extraKleeuClibcConfig debugRuntime runtimeAsserts;
|
||||
};
|
||||
in
|
||||
stdenv.mkDerivation rec {
|
||||
clang_9.stdenv.mkDerivation rec {
|
||||
pname = "klee";
|
||||
version = "2.2";
|
||||
src = fetchFromGitHub {
|
||||
|
|
@ -30,11 +54,12 @@ stdenv.mkDerivation rec {
|
|||
sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M=";
|
||||
};
|
||||
buildInputs = [
|
||||
llvmPackages_9.llvm clang_9 z3 stp cryptominisat
|
||||
llvmPackages_9.llvm
|
||||
z3 stp cryptominisat
|
||||
gperftools sqlite
|
||||
];
|
||||
nativeBuildInputs = [
|
||||
cmake
|
||||
cmake clang_9
|
||||
];
|
||||
checkInputs = [
|
||||
gtest
|
||||
|
|
@ -46,14 +71,17 @@ stdenv.mkDerivation rec {
|
|||
];
|
||||
|
||||
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"
|
||||
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"}"
|
||||
"-DKLEE_ENABLE_TIMESTAMP=${onOff false}"
|
||||
"-DENABLE_KLEE_UCLIBC=${onOff true}"
|
||||
"-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"
|
||||
|
|
@ -66,21 +94,40 @@ stdenv.mkDerivation rec {
|
|||
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 [
|
||||
/* 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.
|
||||
*/
|
||||
{
|
||||
name = "fix-gtest";
|
||||
sha256 = "F+/6videwJZz4sDF9lnV4B8lMx6W11KFJ0Q8t1qUDf4=";
|
||||
url = "https://github.com/klee/klee/pull/1458.patch";
|
||||
}
|
||||
|
||||
# This patch fixes test compile issues with glibc 2.33+.
|
||||
{
|
||||
name = "fix-glibc-2.33";
|
||||
sha256 = "PzxqtFyLy9KF1eA9AAKg1tu+ggRdvu7leuvXifayIcc=";
|
||||
url = "https://github.com/klee/klee/pull/1385.patch";
|
||||
}
|
||||
|
||||
# /etc/mtab doesn't exist in the Nix build sandbox.
|
||||
{
|
||||
name = "fix-etc-mtab-in-tests";
|
||||
sha256 = "2Yb/rJA791esNNqq8uAXV+MML4YXIjPKkHBOufvyRoQ=";
|
||||
url = "https://github.com/klee/klee/pull/1471.patch";
|
||||
}
|
||||
];
|
||||
|
||||
doCheck = true;
|
||||
checkTarget = "check";
|
||||
|
||||
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 = ''
|
||||
|
|
|
|||
98
pkgs/applications/science/logic/klee/klee-uclibc.nix
Normal file
98
pkgs/applications/science/logic/klee/klee-uclibc.nix
Normal file
|
|
@ -0,0 +1,98 @@
|
|||
{ lib
|
||||
, fetchurl
|
||||
, fetchFromGitHub
|
||||
, which
|
||||
, linuxHeaders
|
||||
, clang_9
|
||||
, llvmPackages_9
|
||||
, python3
|
||||
, debugRuntime ? true
|
||||
, runtimeAsserts ? false
|
||||
, extraKleeuClibcConfig ? {}
|
||||
}:
|
||||
|
||||
let
|
||||
localeSrcBase = "uClibc-locale-030818.tgz";
|
||||
localeSrc = fetchurl {
|
||||
url = "http://www.uclibc.org/downloads/${localeSrcBase}";
|
||||
sha256 = "xDYr4xijjxjZjcz0YtItlbq5LwVUi7k/ZSmP6a+uvVc=";
|
||||
};
|
||||
resolvedExtraKleeuClibcConfig = lib.mapAttrsToList (name: value: "${name}=${value}") (extraKleeuClibcConfig // {
|
||||
"UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA" = "n";
|
||||
"RUNTIME_PREFIX" = "/";
|
||||
"DEVEL_PREFIX" = "/";
|
||||
});
|
||||
in
|
||||
clang_9.stdenv.mkDerivation rec {
|
||||
pname = "klee-uclibc";
|
||||
version = "1.2";
|
||||
src = fetchFromGitHub {
|
||||
owner = "klee";
|
||||
repo = "klee-uclibc";
|
||||
rev = "klee_uclibc_v${version}";
|
||||
sha256 = "qdrGMw+2XwpDsfxdv6swnoaoACcF5a/RWgUxUYbtPrI=";
|
||||
};
|
||||
nativeBuildInputs = [
|
||||
clang_9
|
||||
llvmPackages_9.llvm
|
||||
python3
|
||||
which
|
||||
];
|
||||
|
||||
# Some uClibc sources depend on Linux headers.
|
||||
UCLIBC_KERNEL_HEADERS = "${linuxHeaders}/include";
|
||||
|
||||
# HACK: needed for cross-compile.
|
||||
# See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03141.html
|
||||
KLEE_CFLAGS = "-idirafter ${clang_9}/resource-root/include";
|
||||
|
||||
prePatch = ''
|
||||
patchShebangs ./configure
|
||||
patchShebangs ./extra
|
||||
'';
|
||||
|
||||
# klee-uclibc configure does not support --prefix, so we override configurePhase entirely
|
||||
configurePhase = ''
|
||||
./configure ${lib.escapeShellArgs (
|
||||
["--make-llvm-lib"]
|
||||
++ lib.optional (!debugRuntime) "--enable-release"
|
||||
++ lib.optional runtimeAsserts "--enable-assertions"
|
||||
)}
|
||||
|
||||
# Set all the configs we care about.
|
||||
configs=(
|
||||
PREFIX=$out
|
||||
)
|
||||
for value in ${lib.escapeShellArgs resolvedExtraKleeuClibcConfig}; do
|
||||
configs+=("$value")
|
||||
done
|
||||
|
||||
for configFile in .config .config.cmd; do
|
||||
for config in "''${configs[@]}"; do
|
||||
prefix="''${config%%=*}="
|
||||
if grep -q "$prefix" "$configFile"; then
|
||||
sed -i "s"'\001'"''${prefix}"'\001'"#''${prefix}"'\001'"g" "$configFile"
|
||||
fi
|
||||
echo "$config" >> "$configFile"
|
||||
done
|
||||
done
|
||||
'';
|
||||
|
||||
# Link the locale source into the correct place
|
||||
preBuild = ''
|
||||
ln -sf ${localeSrc} extra/locale/${localeSrcBase}
|
||||
'';
|
||||
|
||||
makeFlags = ["HAVE_DOT_CONFIG=y"];
|
||||
|
||||
meta = with lib; {
|
||||
description = "A modified version of uClibc for KLEE.";
|
||||
longDescription = ''
|
||||
klee-uclibc is a bitcode build of uClibc meant for compatibility with the
|
||||
KLEE symbolic virtual machine.
|
||||
'';
|
||||
homepage = "https://klee.github.io/";
|
||||
license = licenses.lgpl3;
|
||||
maintainers = with maintainers; [ numinit ];
|
||||
};
|
||||
}
|
||||
Loading…
Reference in a new issue