X-Loop: help-debbugs@HIDDEN
Subject: [bug#68296] [PATCH] gnu: Add KLEE.
Resent-From: soeren@HIDDEN
Original-Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
Resent-CC: guix-patches@HIDDEN
Resent-Date: Sat, 06 Jan 2024 20:50:01 +0000
Resent-Message-ID: <handler.68296.B.170457415519410 <at> debbugs.gnu.org>
Resent-Sender: help-debbugs@HIDDEN
X-GNU-PR-Message: report 68296
X-GNU-PR-Package: guix-patches
X-GNU-PR-Keywords: patch
To: 68296 <at> debbugs.gnu.org
X-Debbugs-Original-To: guix-patches@HIDDEN
Received: via spool by submit <at> debbugs.gnu.org id=B.170457415519410
(code B ref -1); Sat, 06 Jan 2024 20:50:01 +0000
Received: (at submit) by debbugs.gnu.org; 6 Jan 2024 20:49:15 +0000
Received: from localhost ([127.0.0.1]:60329 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1rMDbW-00052z-R4
for submit <at> debbugs.gnu.org; Sat, 06 Jan 2024 15:49:15 -0500
Received: from lists.gnu.org ([2001:470:142::17]:51408)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <soeren@HIDDEN>) id 1rMDbV-00052n-AH
for submit <at> debbugs.gnu.org; Sat, 06 Jan 2024 15:49:14 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10])
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <soeren@HIDDEN>)
id 1rMDbK-0003rL-IQ
for guix-patches@HIDDEN; Sat, 06 Jan 2024 15:49:02 -0500
Received: from magnesium.8pit.net ([45.76.88.171])
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <soeren@HIDDEN>)
id 1rMDbI-0006AJ-79; Sat, 06 Jan 2024 15:49:02 -0500
DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=Rp8vwAS+Ii
gH1BWSEwmr55Dc/5d04LLRYmPUyC+DEu4=; h=date:subject:to:from;
d=soeren-tempel.net; b=nPwsls4aCgPKk2SDYAWFnohzoimDmxQFBHZpn8jM7C190k2
OmczvEsvjQqmO0ZipdKFim2Ps1Pyhf13shwF5do4EP5jAAK7lfNoUUrvrZ33DG0I+JNoEJ
A6mezbFJDLv/cp2RaZR8gz3AVZGspIoY1FoDj2d2gViVXMZcprkeV8=
Received: from localhost
(dynamic-2a02-3102-49da-001b-e576-f39c-a415-1e23.310.pool.telefonica.de
[2a02:3102:49da:1b:e576:f39c:a415:1e23])
by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 0b1cbe9f
(TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES);
Sat, 6 Jan 2024 21:48:55 +0100 (CET)
From: soeren@HIDDEN
Date: Sat, 6 Jan 2024 21:40:41 +0100
Message-ID: <890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@HIDDEN>
X-Mailer: git-send-email 2.43.0
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Received-SPF: pass client-ip=45.76.88.171;
envelope-from=soeren@HIDDEN; helo=magnesium.8pit.net
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: 0.9 (/)
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -0.1 (/)
From: Sören Tempel <soeren@HIDDEN>
* gnu/packages/check.scm (klee-uclibc): New variable.
* gnu/packages/check.scm (klee): New variable.
Signed-off-by: Sören Tempel <soeren@HIDDEN>
---
This is a new package for KLEE, a popular piece of academic software
in the software engineering domain. KLEE implements a technique called
symbolic execution <https://en.wikipedia.org/wiki/Symbolic_execution>
which allows for automated testing of software through SMT solving.
KLEE forms the basis for a lot of research in the symbolic execution
domain <https://klee.github.io/publications/>. Packaging KLEE and
other related tools, eases using Guix for conducting reproducible
research in this domain. I have Guix packages for other symbolic
execution tools which I also would like to upstream in the future,
I figured I would start with KLEE as it has little to no dependencies.
I tested this package by conforming that the basic upstream tutorials
work as intended, e.g. <https://klee.github.io/tutorials/testing-function/>.
This is my first Guix package, hence CC'ing the mentors.
gnu/packages/check.scm | 107 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 107 insertions(+)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 5181d3a164..7e97e59955 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -71,6 +71,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)
@@ -79,6 +80,8 @@ (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)
#:use-module (gnu packages python)
@@ -87,6 +90,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)
@@ -3648,3 +3652,106 @@ (define-public subunit
command line filters to process a subunit stream and language bindings for
Python, C, C++ and shell. Bindings are easy to write for other languages.")
(license (list license:asl2.0 license:bsd-3)))) ;user can pick
+
+(define-public klee-uclibc
+ (let ((commit "955d502cc1f0688e82348304b053ad787056c754"))
+ (package
+ (name "klee-uclibc")
+ (version (git-version "20230612" "0" commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/klee/klee-uclibc")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"))))
+ (build-system gnu-build-system)
+ (supported-systems '("x86_64-linux"))
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:phases (modify-phases %standard-phases
+ ;; Disable locales as these would have to be downloaded and
+ ;; shouldn't really be needed for symbolic execution either.
+ (add-after 'unpack 'patch-config
+ (lambda _
+ (substitute* "klee-premade-configs/x86_64/config"
+ (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_HAS_LOCALE=y")
+ "UCLIBC_HAS_LOCALE=n")
+ (("UCLIBC_HAS_XLOCALE=y")
+ "UCLIBC_HAS_XLOCALE=n"))))
+
+ ;; Upstream uses a custom non-GNU configure script written
+ ;; in Python, replace the default configure phase accordingly.
+ (replace 'configure
+ (lambda _
+ (invoke "./configure"
+ "--make-llvm-lib"
+ "--enable-release")))
+
+ ;; Custom install phase to only install the libc.a file manually.
+ ;; This is the only file which is used/needed by KLEE itself.
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (install-file "lib/libc.a"
+ (string-append (assoc-ref outputs "out")
+ "/lib")))))))
+ (inputs (list clang-toolchain-13 python ncurses))
+ (synopsis "Variant of uClibc tailored to symbolic execution")
+ (description
+ "Modified version of uClibc for symbolic execution of
+Unix userland software. This library can only be used in conjunction
+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)
+ (supported-systems '("x86_64-linux"))
+ (arguments
+ `(#:test-target "systemtests"
+ #: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')"))))))))
+ (propagated-inputs (list klee-uclibc clang-toolchain-13 llvm-13 python
+ python-tabulate))
+ (inputs (list python-lit z3 gperftools sqlite))
+ (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))))
base-commit: 29c94dd522833b2603a651c14a5b06120bcf1829
Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) Content-Type: text/plain; charset=utf-8 X-Loop: help-debbugs@HIDDEN From: help-debbugs@HIDDEN (GNU bug Tracking System) To: soeren@HIDDEN Subject: bug#68296: Acknowledgement ([PATCH] gnu: Add KLEE.) Message-ID: <handler.68296.B.170457415519410.ack <at> debbugs.gnu.org> References: <890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@HIDDEN> X-Gnu-PR-Message: ack 68296 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 68296 <at> debbugs.gnu.org Date: Sat, 06 Jan 2024 20:50:01 +0000 Thank you for filing a new bug report with debbugs.gnu.org. This is an automatically generated reply to let you know your message has been received. Your message is being forwarded to the package maintainers and other interested parties for their attention; they will reply in due course. Your message has been sent to the package maintainer(s): guix-patches@HIDDEN If you wish to submit further information on this problem, please send it to 68296 <at> debbugs.gnu.org. Please do not send mail to help-debbugs@HIDDEN unless you wish to report a problem with the Bug-tracking system. --=20 68296: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D68296 GNU Bug Tracking System Contact help-debbugs@HIDDEN with problems
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.