From: soeren@soeren-tempel.net
To: 68296@debbugs.gnu.org
Subject: [bug#68296] [PATCH v3 2/2] gnu: Add klee.
Date: Wed, 28 Feb 2024 18:04:48 +0100 [thread overview]
Message-ID: <262a52af77537ec120f0ac58a5d8c76d73a7aa92.1709139885.git.soeren@soeren-tempel.net> (raw)
In-Reply-To: <99fdb88daa1db94c659f2c79b42b39c704fd8bde.1709139885.git.soeren@soeren-tempel.net>
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee): New variable.
Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
Changes since v2: Switch to a non-debug build-type to workaround an
internal error being triggered in clang while building KLEE with it.
gnu/packages/check.scm | 55 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 55 insertions(+)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 50fd105b2c..534852f029 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -74,6 +74,7 @@ (define-module (gnu packages check)
#: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)
@@ -83,6 +84,7 @@ (define-module (gnu packages check)
#: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)
@@ -92,6 +94,7 @@ (define-module (gnu packages check)
#: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)
@@ -3697,3 +3700,55 @@ (define-public klee-uclibc
with the @code{klee} package.")
(home-page "https://klee.github.io/")
(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.github.io/")
+ (license (list license:expat license:bsd-4))))
next prev parent reply other threads:[~2024-02-28 17:41 UTC|newest]
Thread overview: 10+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-01-06 20:40 [bug#68296] [PATCH] gnu: Add KLEE soeren
2024-02-13 8:49 ` Julien Lepiller
2024-02-13 14:09 ` Sören Tempel
2024-02-13 14:08 ` [bug#68296] [PATCH v2 1/2] gnu: Add klee-uclibc soeren
2024-02-13 14:08 ` [bug#68296] [PATCH v2 2/2] gnu: Add klee soeren
2024-02-28 17:04 ` [bug#68296] [PATCH v3 1/2] gnu: Add klee-uclibc soeren
2024-02-28 17:04 ` soeren [this message]
2024-03-11 9:54 ` [bug#68296] gnu: Add KLEE Sören Tempel
2024-03-28 19:20 ` [bug#68296] [PATCH v4 1/2] gnu: Add klee-uclibc soeren
2024-03-28 19:20 ` [bug#68296] [PATCH v4 2/2] gnu: Add klee soeren
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=262a52af77537ec120f0ac58a5d8c76d73a7aa92.1709139885.git.soeren@soeren-tempel.net \
--to=soeren@soeren-tempel.net \
--cc=68296@debbugs.gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.