Merge pull request #304204 from numinit/klee-llvm-override

klee: make llvmPackages and uclibc overridable

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 ]);
-
+in
-  # The klee-uclibc derivation.
+llvmPackages.stdenv.mkDerivation rec {
-  kleeuClibc = callPackage ./klee-uclibc.nix {
-    inherit stdenv clang llvm extraKleeuClibcConfig debugRuntime runtimeAsserts;
-  };
-in 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"
+    "-DLLVMCC=${llvmPackages.clang}/bin/clang"
-    "-DLLVMCXX=${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
+    updateScript = nix-update-script {
-    uclibc = kleeuClibc;
+      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 ];

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
+    llvmPackages.clang
-    curl
+    llvmPackages.llvm
-    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 --build ./configure
-    patchShebangs ./extra
+    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 ];
   };

pkgs/top-level/all-packages.nix

@@ -31972,11 +31972,9 @@ with pkgs;
 
   klayout = libsForQt5.callPackage ../applications/misc/klayout { };
 
-  klee = callPackage ../applications/science/logic/klee (with llvmPackages_13; {
+  klee = callPackage ../applications/science/logic/klee {
-    clang = clang;
+    llvmPackages = llvmPackages_13;
-    llvm = llvm;
+  };
-    stdenv = stdenv;
-  });
 
   kmetronome = qt6Packages.callPackage ../applications/audio/kmetronome { };