Unverified Commit 6c46327d authored by Morgan Jones's avatar Morgan Jones Committed by GitHub
Browse files

klee: 3.1 -> 3.1-unstable-2025-07-11, bump to LLVM 18 (#435927)

parents ba638523 821e8edd

pkgs/applications/science/logic/klee/default.nix

+122 −11
Original line number Diff line number Diff line
@@ -21,7 +21,7 @@ 
  includeDebugInfo ? true,



  # Enable KLEE asserts. Defaults to true, since LLVM is built with them.

  asserts ? true,

  asserts ? false,



  # Build the KLEE runtime in debug mode. Defaults to true, as this improves

  # stack traces of the software under test.
@@ -37,13 +37,6 @@ 
  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 =
@@ -60,13 +53,13 @@ let 
in

llvmPackages.stdenv.mkDerivation rec {

  pname = "klee";

  version = "3.1";

  version = "3.1-unstable-2025-07-11";



  src = fetchFromGitHub {

    owner = "klee";

    repo = "klee";

    rev = "v${version}";

    hash = "sha256-5js1N8qVF0lCkahSU3ojT7+p/a9IaUpPWhIyFHEzqto=";

    rev = "1c9fbc1013a6000b39615cc9a5aba83e43a4bf75";

    hash = "sha256-D93T0mBBrIhQTS42ScUHPrMoqCI55Y6Yp7snLmlriQM=";

  };



  nativeBuildInputs = [ cmake ];
@@ -111,6 +104,7 @@ llvmPackages.stdenv.mkDerivation rec { 
      "-DENABLE_POSIX_RUNTIME=${onOff true}"

      "-DENABLE_UNIT_TESTS=${onOff true}"

      "-DENABLE_SYSTEM_TESTS=${onOff true}"

      "-DLIT_ARGS=--verbose"

      "-DGTEST_SRC_DIR=${gtest.src}"

      "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include"

      "-Wno-dev"
@@ -119,6 +113,107 @@ llvmPackages.stdenv.mkDerivation rec { 
  # Silence various warnings during the compilation of fortified bitcode.

  env.NIX_CFLAGS_COMPILE = toString [ "-Wno-macro-redefined" ];



  env.FILECHECK_OPTS = "--dump-input-filter=all";



  env.LIT_XFAIL = lib.concatStringsSep ";" [

    "KLEE :: ArrayOpt/test_expr_arbitrary.c"

    "KLEE :: CXX/SimpleVirtual.cpp"

    "KLEE :: CXX/StaticConstructor.cpp"

    "KLEE :: CXX/StaticDestructor.cpp"

    "KLEE :: Concrete/ConstantExpr.ll"

    "KLEE :: Concrete/OverlappingPhiNodes.ll"

    "KLEE :: Concrete/UnorderedPhiNodes.ll"

    "KLEE :: DeterministicAllocation/nullpage-read.c"

    "KLEE :: DeterministicAllocation/nullpage-write.c"

    "KLEE :: DeterministicAllocation/use-after-free-loh.c"

    "KLEE :: DeterministicAllocation/use-after-free.c"

    "KLEE :: Dogfood/ImmutableSet.cpp"

    "KLEE :: Feature/Atomic.c"

    "KLEE :: Feature/DivCheck.c"

    "KLEE :: Feature/ExtCall.c"

    "KLEE :: Feature/ExtCallWarnings.c"

    "KLEE :: Feature/FunctionAlias.c"

    "KLEE :: Feature/FunctionAliasExit.c"

    "KLEE :: Feature/LargeArrayBecomesSym.c"

    "KLEE :: Feature/LowerSwitch.c"

    "KLEE :: Feature/MakeSymbolicName.c"

    "KLEE :: Feature/NoExternalCallsAllowed.c"

    "KLEE :: Feature/Optimize.c"

    "KLEE :: Feature/OvershiftCheck.c"

    "KLEE :: Feature/ReadStringAtAddress.c"

    "KLEE :: Feature/SeedConcretizeExternalCall.c"

    "KLEE :: Feature/ShiftCheck.c"

    "KLEE :: Feature/consecutive_divide_by_zero.c"

    "KLEE :: Feature/srem.c"

    "KLEE :: InlineAsm/RaiseAsm.c"

    "KLEE :: InlineAsm/asm_lifting.ll"

    "KLEE :: Intrinsics/IntrinsicTrap.ll"

    "KLEE :: Intrinsics/IsConstant.ll"

    "KLEE :: Intrinsics/Missing.ll"

    "KLEE :: Intrinsics/Overflow.ll"

    "KLEE :: Intrinsics/OverflowMul.ll"

    "KLEE :: Intrinsics/Saturating.ll"

    "KLEE :: Intrinsics/noalias-scope-decl.ll"

    "KLEE :: Intrinsics/objectsize.ll"

    "KLEE :: Replay/klee-replay/KleeZesti.c"

    "KLEE :: Replay/libkleeruntest/replay_posix_runtime.c"

    "KLEE :: Runtime/FreeStanding/memcpy_chk_err.c"

    "KLEE :: Runtime/POSIX/CanonicalizeFileName.c"

    "KLEE :: Runtime/POSIX/DirConsistency.c"

    "KLEE :: Runtime/POSIX/DirSeek.c"

    "KLEE :: Runtime/POSIX/Envp.c"

    "KLEE :: Runtime/POSIX/FDNumbers.c"

    "KLEE :: Runtime/POSIX/FD_Fail.c"

    "KLEE :: Runtime/POSIX/FD_Fail2.c"

    "KLEE :: Runtime/POSIX/Fcntl.c"

    "KLEE :: Runtime/POSIX/FilePerm.c"

    "KLEE :: Runtime/POSIX/FreeArgv.c"

    "KLEE :: Runtime/POSIX/Futimesat.c"

    "KLEE :: Runtime/POSIX/Getenv.c"

    "KLEE :: Runtime/POSIX/Ioctl.c"

    "KLEE :: Runtime/POSIX/Isatty.c"

    "KLEE :: Runtime/POSIX/MixedConcreteSymbolic.c"

    "KLEE :: Runtime/POSIX/Openat.c"

    "KLEE :: Runtime/POSIX/PrgName.c"

    "KLEE :: Runtime/POSIX/Read1.c"

    "KLEE :: Runtime/POSIX/Replay.c"

    "KLEE :: Runtime/POSIX/SeedAndFail.c"

    "KLEE :: Runtime/POSIX/Stdin.c"

    "KLEE :: Runtime/POSIX/SymFileConsistency.c"

    "KLEE :: Runtime/POSIX/TestMain.c"

    "KLEE :: Runtime/POSIX/Usage.c"

    "KLEE :: Runtime/POSIX/Write1.c"

    "KLEE :: Runtime/POSIX/Write2.c"

    "KLEE :: Runtime/POSIX/_exit.c"

    "KLEE :: Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c"

    "KLEE :: Runtime/klee-libc/mempcpy.c"

    "KLEE :: Solver/Z3ConstantArray.c"

    "KLEE :: UBSan/ubsan_alignment-type-mismatch.c"

    "KLEE :: UBSan/ubsan_array_bounds.c"

    "KLEE :: UBSan/ubsan_pointer_overflow-pointer_arithmetic.c"

    "KLEE :: UBSan/ubsan_signed_integer_overflow.c"

    "KLEE :: UBSan/ubsan_unsigned_integer_overflow.c"

    "KLEE :: UBSan/ubsan_unsigned_shift_base.c"

    "KLEE :: UBSan/ubsan_vla_bound.c"

    "KLEE :: VarArgs/FunctionAliasVarArg.c"

    "KLEE :: VarArgs/VarArg.c"

    "KLEE :: VarArgs/VarArgAlignment.c"

    "KLEE :: VarArgs/VarArgByVal.c"

    "KLEE :: VarArgs/VarArgByValReported.c"

    "KLEE :: VarArgs/VarArgLongDouble.c"

    "KLEE :: VectorInstructions/floating_point_ops_constant.c"

    "KLEE :: VectorInstructions/integer_ops_constant.c"

    "KLEE :: VectorInstructions/integer_ops_signed_symbolic.c"

    "KLEE :: VectorInstructions/integer_ops_unsigned_symbolic.c"

    "KLEE :: VectorInstructions/memset.c"

    "KLEE :: VectorInstructions/oob-write.c"

    "KLEE :: VectorInstructions/shuffle_element.c"

    "KLEE :: klee-stats/KleeStatsTermClasses.c"

    "KLEE :: regression/2008-03-11-free-of-malloc-zero.c"

    "KLEE :: regression/2014-07-04-unflushed-error-report.c"

    "KLEE :: regression/2016-11-24-bitcast-weak-alias.c"

  ];



  prePatch = ''

    patchShebangs --build .

  '';
@@ -140,6 +235,8 @@ llvmPackages.stdenv.mkDerivation rec { 
    uclibc = chosenKleeuClibc;

  };



  __structuredAttrs = true;



  meta = with lib; {

    mainProgram = "klee";

    description = "Symbolic virtual machine built on top of LLVM";
@@ -166,5 +263,19 @@ llvmPackages.stdenv.mkDerivation rec { 
    license = licenses.ncsa;

    platforms = [ "x86_64-linux" ];

    maintainers = with maintainers; [ numinit ];

    # Upstream is still working on support for LLVM ≥ 16; see:

    #

    # * <https://github.com/klee/klee/pull/1664>

    # * <https://github.com/klee/klee/pull/1745>

    # * <https://github.com/klee/klee/pull/1751>

    # * <https://github.com/klee/klee/issues/1754>

    #

    # The package builds with LLVM 18 but 23% of the tests unexpectedly

    # fail due to missing functionality for newer LLVM versions. We

    # mark them as expected failures above to allow the package to

    # build for those who want to experiment with KLEE, but mark it

    # broken to avoid giving the impression that this is the expected

    # user experience and level of support.

    broken = true;

  };

}

pkgs/top-level/all-packages.nix

+1 −1
Original line number Diff line number Diff line
@@ -12166,7 +12166,7 @@ with pkgs; 
  klayout = libsForQt5.callPackage ../applications/misc/klayout { };



  klee = callPackage ../applications/science/logic/klee {

    llvmPackages = llvmPackages_13;

    llvmPackages = llvmPackages_18;

  };



  kmplayer = libsForQt5.callPackage ../applications/video/kmplayer { };