From 98a951c50952598b6eedcf291c8f8d88fadd0943 Mon Sep 17 00:00:00 2001 From: Morgan Jones <me@numin.it> Date: Sun, 23 Jan 2022 18:58:56 -0700 Subject: [PATCH] klee: build with klee-uclibc This ends up enabling more of the KLEE test suite, so apply patches to fix those too. --- .../science/logic/klee/default.nix | 81 +++++++++++---- .../science/logic/klee/klee-uclibc.nix | 98 +++++++++++++++++++ 2 files changed, 162 insertions(+), 17 deletions(-) create mode 100644 pkgs/applications/science/logic/klee/klee-uclibc.nix diff --git a/pkgs/applications/science/logic/klee/default.nix b/pkgs/applications/science/logic/klee/default.nix index e0ace7e81c82..612d9fd57c7c 100644 --- a/pkgs/applications/science/logic/klee/default.nix +++ b/pkgs/applications/science/logic/klee/default.nix @@ -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 = '' diff --git a/pkgs/applications/science/logic/klee/klee-uclibc.nix b/pkgs/applications/science/logic/klee/klee-uclibc.nix new file mode 100644 index 000000000000..2e3826c50c42 --- /dev/null +++ b/pkgs/applications/science/logic/klee/klee-uclibc.nix @@ -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 ]; + }; +}