Package: guix-patches;
Reported by: soeren <at> soeren-tempel.net
Date: Sat, 6 Jan 2024 20:50:01 UTC
Severity: normal
Tags: patch
Done: Sören Tempel <soeren <at> soeren-tempel.net>
Bug is archived. No further changes may be made.
View this message in rfc822 format
From: help-debbugs <at> gnu.org (GNU bug Tracking System) To: Sören Tempel <soeren <at> soeren-tempel.net> Cc: tracker <at> debbugs.gnu.org Subject: bug#68296: closed ([PATCH] gnu: Add KLEE.) Date: Mon, 13 Jan 2025 17:53:02 +0000
[Message part 1 (text/plain, inline)]
Your message dated Mon, 13 Jan 2025 18:52:06 +0100 with message-id <2C8JOOUL2GHJR.32GXTU4IR3YKE <at> 8pit.net> and subject line Re: [PATCH] gnu: Add KLEE. has caused the debbugs.gnu.org bug report #68296, regarding [PATCH] gnu: Add KLEE. to be marked as done. (If you believe you have received this mail in error, please contact help-debbugs <at> gnu.org.) -- 68296: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=68296 GNU Bug Tracking System Contact help-debbugs <at> gnu.org with problems
[Message part 2 (message/rfc822, inline)]
From: soeren <at> soeren-tempel.net To: guix-patches <at> gnu.org Subject: [PATCH] gnu: Add KLEE. Date: Sat, 6 Jan 2024 21:40:41 +0100From: Sören Tempel <soeren <at> soeren-tempel.net> * gnu/packages/check.scm (klee-uclibc): New variable. * gnu/packages/check.scm (klee): New variable. Signed-off-by: Sören Tempel <soeren <at> soeren-tempel.net> --- 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
[Message part 3 (message/rfc822, inline)]
From: Sören Tempel <soeren <at> soeren-tempel.net> To: 68296-done <at> debbugs.gnu.org Subject: Re: [PATCH] gnu: Add KLEE. Date: Mon, 13 Jan 2025 18:52:06 +0100Hi, klee has been added in fe7c898750e3fdad586ab3929c67b4b4643ffece, klee-uclibc has been added as well in a follow-up commit, namely 3bdaa223b363b6986baa4bfa11f629f6ba974bba. Hence, this can be closed.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.