diff options
author | Tristan Ross <tristan.ross@midstall.com> | 2024-06-23 20:04:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2024-06-23 20:04:10 -0700 |
commit | 6d16d94dd4cea5c5a4089f94302628640758100a (patch) | |
tree | b03d4b535398e910c75c97eddb534438fed023da /pkgs/applications/science | |
parent | 09970d497ebbdaef1c662cad561725f2ea2c736b (diff) | |
parent | bc9fffbb3b62a9894c3bcd49356f09cb02adafd6 (diff) |
Merge pull request #304204 from numinit/klee-llvm-override
klee: make llvmPackages and uclibc overridable
Diffstat (limited to 'pkgs/applications/science')
-rw-r--r-- | pkgs/applications/science/logic/klee/default.nix | 58 | ||||
-rw-r--r-- | pkgs/applications/science/logic/klee/klee-uclibc.nix | 32 |
2 files changed, 59 insertions, 31 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 ]; diff --git a/pkgs/applications/science/logic/klee/klee-uclibc.nix b/pkgs/applications/science/logic/klee/klee-uclibc.nix index 5bbd8e69a46fa..c87a881e75336 100644 --- a/pkgs/applications/science/logic/klee/klee-uclibc.nix +++ b/pkgs/applications/science/logic/klee/klee-uclibc.nix @@ -1,13 +1,12 @@ { lib -, stdenv +, llvmPackages , fetchurl , fetchFromGitHub -, which , linuxHeaders -, clang -, llvm , python3 , curl +, which +, nix-update-script , debugRuntime ? true , runtimeAsserts ? false , extraKleeuClibcConfig ? {} @@ -24,21 +23,22 @@ let "RUNTIME_PREFIX" = "/"; "DEVEL_PREFIX" = "/"; }); -in stdenv.mkDerivation rec { +in +llvmPackages.stdenv.mkDerivation rec { pname = "klee-uclibc"; version = "1.4"; src = fetchFromGitHub { owner = "klee"; repo = "klee-uclibc"; rev = "klee_uclibc_v${version}"; - sha256 = "sha256-sogQK5Ed0k5tf4rrYwCKT4YRKyEovgT25p0BhGvJ1ok="; + hash = "sha256-sogQK5Ed0k5tf4rrYwCKT4YRKyEovgT25p0BhGvJ1ok="; }; nativeBuildInputs = [ - clang - curl - llvm + llvmPackages.clang + llvmPackages.llvm python3 + curl which ]; @@ -47,11 +47,11 @@ in stdenv.mkDerivation rec { # HACK: needed for cross-compile. # See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03141.html - KLEE_CFLAGS = "-idirafter ${clang}/resource-root/include"; + KLEE_CFLAGS = "-idirafter ${llvmPackages.clang}/resource-root/include"; prePatch = '' - patchShebangs ./configure - patchShebangs ./extra + patchShebangs --build ./configure + patchShebangs --build ./extra ''; # klee-uclibc configure does not support --prefix, so we override configurePhase entirely @@ -88,13 +88,19 @@ in stdenv.mkDerivation rec { makeFlags = ["HAVE_DOT_CONFIG=y"]; + enableParallelBuilding = true; + + passthru.updateScript = nix-update-script { + extraArgs = [ "--version-regex" "v(\d\.\d)" ]; + }; + meta = with lib; { description = "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/"; + homepage = "https://github.com/klee/klee-uclibc"; license = licenses.lgpl3; maintainers = with maintainers; [ numinit ]; }; |