diff options
Diffstat (limited to 'pkgs/applications/science/logic/klee/default.nix')
-rw-r--r-- | pkgs/applications/science/logic/klee/default.nix | 58 |
1 files changed, 40 insertions, 18 deletions
diff --git a/pkgs/applications/science/logic/klee/default.nix b/pkgs/applications/science/logic/klee/default.nix index b610ce558605d..fb02c6d40b9dc 100644 --- a/pkgs/applications/science/logic/klee/default.nix +++ b/pkgs/applications/science/logic/klee/default.nix @@ -1,10 +1,8 @@ { lib -, stdenv +, llvmPackages , callPackage , fetchFromGitHub , cmake -, clang -, llvm , python3 , z3 , stp @@ -13,6 +11,7 @@ , sqlite , gtest , lit +, nix-update-script # Build KLEE in debug mode. Defaults to false. , debug ? false @@ -30,19 +29,35 @@ # Enable runtime asserts. Default false. , runtimeAsserts ? false -# Extra klee-uclibc config. +# 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 ]); - - # The klee-uclibc derivation. - kleeuClibc = callPackage ./klee-uclibc.nix { - inherit stdenv clang llvm extraKleeuClibcConfig debugRuntime runtimeAsserts; - }; -in stdenv.mkDerivation rec { +in +llvmPackages.stdenv.mkDerivation rec { pname = "klee"; version = "3.1"; @@ -54,14 +69,16 @@ in stdenv.mkDerivation rec { }; nativeBuildInputs = [ cmake ]; + buildInputs = [ + llvmPackages.llvm cryptominisat gperftools - llvm sqlite stp z3 ]; + nativeCheckInputs = [ gtest @@ -77,10 +94,10 @@ in stdenv.mkDerivation rec { onOff = val: if val then "ON" else "OFF"; in [ "-DKLEE_RUNTIME_BUILD_TYPE=${if debugRuntime then "Debug" else "Release"}" - "-DLLVMCC=${clang}/bin/clang" - "-DLLVMCXX=${clang}/bin/clang++" + "-DLLVMCC=${llvmPackages.clang}/bin/clang" + "-DLLVMCXX=${llvmPackages.clang}/bin/clang++" "-DKLEE_ENABLE_TIMESTAMP=${onOff false}" - "-DKLEE_UCLIBC_PATH=${kleeuClibc}" + "-DKLEE_UCLIBC_PATH=${chosenKleeuClibc}" "-DENABLE_KLEE_ASSERTS=${onOff asserts}" "-DENABLE_POSIX_RUNTIME=${onOff true}" "-DENABLE_UNIT_TESTS=${onOff true}" @@ -94,20 +111,25 @@ in stdenv.mkDerivation rec { env.NIX_CFLAGS_COMPILE = toString ["-Wno-macro-redefined"]; prePatch = '' - patchShebangs . + patchShebangs --build . ''; # https://github.com/klee/klee/issues/1690 hardeningDisable = [ "fortify" ]; + enableParallelBuilding = true; doCheck = true; passthru = { - # Let the user depend on `klee.uclibc` for klee-uclibc - uclibc = kleeuClibc; + 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 @@ -128,7 +150,7 @@ in stdenv.mkDerivation rec { that matches a computed test input, including setting up files, pipes, environment variables, and passing command line arguments. ''; - homepage = "https://klee.github.io/"; + homepage = "https://klee.github.io"; license = licenses.ncsa; platforms = [ "x86_64-linux" ]; maintainers = with maintainers; [ numinit ]; |