From 4cd73c2026053942ffdd1606119000c2567c8a5e Mon Sep 17 00:00:00 2001 From: Sören Tempel Date: Thu, 28 Mar 2024 20:20:19 +0100 Subject: gnu: Add klee. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/check.scm (klee): New variable. Signed-off-by: Sören Tempel --- gnu/packages/check.scm | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index cc74c8e317..6bb773c281 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -76,6 +76,7 @@ #:use-module (gnu packages bash) #:use-module (gnu packages cmake) #:use-module (gnu packages compression) + #:use-module (gnu packages cpp) #:use-module (gnu packages linux) #:use-module (gnu packages llvm) #:use-module (gnu packages glib) @@ -86,6 +87,7 @@ #:use-module (gnu packages gtk) #:use-module (gnu packages guile) #:use-module (gnu packages guile-xyz) + #:use-module (gnu packages maths) #:use-module (gnu packages ncurses) #:use-module (gnu packages perl) #:use-module (gnu packages pkg-config) @@ -95,6 +97,7 @@ #:use-module (gnu packages python-web) #:use-module (gnu packages python-xyz) #:use-module (gnu packages python-science) + #:use-module (gnu packages sqlite) #:use-module (gnu packages texinfo) #:use-module (gnu packages time) #:use-module (gnu packages xml) @@ -3871,3 +3874,55 @@ Unix userland software. This library can only be used in conjunction with the @code{klee} package.") (home-page "https://klee-se.org/") (license license:lgpl2.1)))) + +(define-public klee + (package + (name "klee") + (version "3.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/klee/klee") + (commit (string-append "v" version)))) + (sha256 + (base32 "0dj20nazkcq84ryr87dihvjznapsbl1n21sa8dhhnb0wsad5d6fb")) + (file-name (git-file-name name version)))) + (build-system cmake-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (supported-systems '("x86_64-linux")) + (arguments + `(#:test-target "systemtests" + ;; Default build type (RelWithDebInfo) causes an internal error + ;; in clang while compiling KLEE, hence use a different build type. + #:build-type "Release" + #:strip-directories '("bin") + #:configure-flags ,#~(list "-DENABLE_KLEE_ASSERTS=OFF" + "-DENABLE_TCMALLOC=ON" + "-DENABLE_POSIX_RUNTIME=ON" + (string-append "-DKLEE_UCLIBC_PATH=" + #$klee-uclibc)) + #:phases (modify-phases %standard-phases + (add-after 'unpack 'patch-lit-config + (lambda _ + ;; Make sure that we retain the value of the GUIX_PYTHONPATH + ;; environment variable in the test environmented created by + ;; python-lit. Otherwise, the test scripts won't be able to + ;; find the python-tabulate dependency, causing test failures. + (substitute* "test/lit.cfg" + (("addEnv\\('PWD'\\)" env) + (string-append env "\n" "addEnv('GUIX_PYTHONPATH')")))))))) + ;; KLEE operates on LLVM IR generated by a specific toolchain version. + ;; Propergate the toolchain to allow users to transform code to this version. + (propagated-inputs (list clang-toolchain-13 llvm-13 python python-tabulate)) + (inputs (list z3 gperftools sqlite)) + (native-inputs (list python-lit)) + (synopsis + "Symbolic execution engine built on top of the LLVM compiler infastructure") + (description + "Dynamic symbolic execution engine built on top of +LLVM. Symbolic execution is an automated software testing technique, +KLEE leverage this technique to automatically generate test cases for +software compiled to LLVM IR.") + (home-page "https://klee-se.org/") + (license (list license:expat license:bsd-4)))) -- cgit v1.2.3