[PATCH] gnu: Add KLEE.

  • Open
  • quality assurance status badge
Details
2 participants
  • Julien Lepiller
  • soeren
Owner
unassigned
Submitted by
soeren
Severity
normal
S
S
soeren wrote on 6 Jan 21:40 +0100
(address . guix-patches@gnu.org)
890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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@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
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

This is my first Guix package, hence CC'ing the mentors.

gnu/packages/check.scm | 107 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 107 insertions(+)

Toggle diff (138 lines)
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
J
J
Julien Lepiller wrote on 13 Feb 09:49 +0100
CE0F11CA-6E29-4456-B537-6D36EEE1498C@lepiller.eu
Le 6 janvier 2024 21:40:41 GMT+01:00, soeren@soeren-tempel.net a écrit :
Toggle quote (168 lines)
>From: Sören Tempel <soeren@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@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
>
>
>

Hi Sören,

I'm sorry nobody looked at this before. Here are a few remarks.

First, could you separate this in two patches, one per package?

Is there a reason why this is limited to the x86_64 architecture?

You have mixed native and normal inputs. In uclibc, since python is only used for the build, it should be native.

Does it make sense to propagate uclibc in klee, when it only contains a static library? Some for clang and llvm. Isn't z3 used at runtime? Shouldn't it be propagated?

Using #$klee-uclibc directly in the phase could be problematic I think, you should use this-package-inputs or similar (can't remember the exact name or syntax right now, you can leave it to me if you don't find it).

Otherwise, looks good for a first patch :)
S
S
soeren wrote on 13 Feb 15:08 +0100
[PATCH v2 1/2] gnu: Add klee-uclibc.
(address . 68296@debbugs.gnu.org)
168e4aa2bfe10a6b15190c93bd3453d665cebd33.1707833332.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee-uclibc): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/check.scm | 62 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 62 insertions(+)

Toggle diff (86 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 4f593cde8d..ecf48ab121 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -48,6 +48,7 @@
;;; Copyright © 2023 Reza Housseini <reza@housseini.me>
;;; Copyright © 2023 Hilton Chain <hako@ultrarare.space>
;;; Copyright © 2023 Troy Figiel <troy@troyfigiel.com>
+;;; Copyright © 2024 Sören Tempel <soeren@soeren-tempel.net>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -80,6 +81,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 ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -3610,3 +3612,63 @@ (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)
+ ;; Only x86_64 is presently supported by KLEE upstream.
+ (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))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list 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))))

base-commit: 85e67f7feac14a1290022b9500c333c51c7f3ca3
S
S
soeren wrote on 13 Feb 15:08 +0100
[PATCH v2 2/2] gnu: Add klee.
(address . 68296@debbugs.gnu.org)
dc1ce12d1f6f53d1ad14fd133f8c013f26725560.1707833332.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>
---
gnu/packages/check.scm | 52 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 52 insertions(+)

Toggle diff (81 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index ecf48ab121..82c40b63b1 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -73,6 +73,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)
@@ -81,6 +82,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)
@@ -90,6 +92,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)
@@ -3672,3 +3675,52 @@ (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"
+ #: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))))
S
S
Sören Tempel wrote on 13 Feb 15:09 +0100
Re: [bug#68296] [PATCH] gnu: Add KLEE.
(name . Julien Lepiller)(address . julien@lepiller.eu)
3TGIYFPTVHXE1.3QGMCQNGUI376@8pit.net
Hi Julien,

Thanks a lot for your feedback! I send an updated revision of the
patchset based on your feedback. More information on changes below.

Julien Lepiller <julien@lepiller.eu> wrote:
Toggle quote (2 lines)
> First, could you separate this in two patches, one per package?

Sorry, oversight on my part. Fixed!

Toggle quote (2 lines)
> Is there a reason why this is limited to the x86_64 architecture?

Yes, despite operating on LLVM IR abstraction, KLEE is tightly
integrated with the host architecture. Therefore, upstream currently
only support x86_64. Packages for other package manager (e.g. Nix)
also only support KLEE on x86_64 [1].

I added a comment explaining this.

Toggle quote (3 lines)
> You have mixed native and normal inputs. In uclibc, since python is
> only used for the build, it should be native.

Fixed, ncurses should also be native as it is only used for menuconfig.

Toggle quote (4 lines)
> Does it make sense to propagate uclibc in klee, when it only contains
> a static library? Some for clang and llvm. Isn't z3 used at runtime?
> Shouldn't it be propagated?

Sorry, I should have done a better job at explaining this: KLEE is a
symbolic analyzer for LLVM IR. Users of KLEE will need to translate
their C/C++ source to LLVM IR in order to analyze it with KLEE [2].
Furthermore, as KLEE is tightly integrated with a specific LLVM version,
it makes (at least from my point of view) sense to propagate a specific
clang toolchain so users can just run `guix shell klee` and get started
with it. However, if preferred I can also remove the propagation.

z3 isn't used at runtime, KLEE just uses the Z3 library interface and
links against z3. AFAIK, it doesn't use any binaries from z3. Does z3
still need to be propagated in this case?

uclibc does not need to be a propagated input since the KLEE build
systems generates LLVM IR from the .a archive [3]. I fixed this.

Toggle quote (5 lines)
> Using #$klee-uclibc directly in the phase could be problematic I
> think, you should use this-package-inputs or similar (can't remember
> the exact name or syntax right now, you can leave it to me if you
> don't find it).

Sorry, I am new to Guix so I am not sure what you mean. Let me know if
you have more information on this but also feel free to just adjust this
as you wish :)

Greetings
Sören

S
S
soeren wrote on 28 Feb 18:04 +0100
[PATCH v3 1/2] gnu: Add klee-uclibc.
(address . 68296@debbugs.gnu.org)
99fdb88daa1db94c659f2c79b42b39c704fd8bde.1709139885.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee-uclibc): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
Changes since v2: Rebase against the current master branch, this resolves
a merge conflict in the copyright comment section. No functional changes.

gnu/packages/check.scm | 62 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 62 insertions(+)

Toggle diff (86 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 5428098c15..50fd105b2c 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -49,6 +49,7 @@
;;; Copyright © 2023 Hilton Chain <hako@ultrarare.space>
;;; Copyright © 2023 Troy Figiel <troy@troyfigiel.com>
;;; Copyright © 2024 Giacomo Leidi <goodoldpaul@autistici.org>
+;;; Copyright © 2024 Sören Tempel <soeren@soeren-tempel.net>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -82,6 +83,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 ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -3635,3 +3637,63 @@ (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)
+ ;; Only x86_64 is presently supported by KLEE upstream.
+ (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))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list 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))))

base-commit: bc6840316c665e5959469e5c857819142cc4a47b
S
S
soeren wrote on 28 Feb 18:04 +0100
[PATCH v3 2/2] gnu: Add klee.
(address . 68296@debbugs.gnu.org)
262a52af77537ec120f0ac58a5d8c76d73a7aa92.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(+)

Toggle diff (84 lines)
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))))
S
S
Sören Tempel wrote on 11 Mar 10:54 +0100
Re: gnu: Add KLEE.
(address . 68296@debbugs.gnu.org)
3209APKM19WGZ.39BXJ12FGTBCL@8pit.net
Hi,

What does "QA: Investigate" mean? The build should be fixed now with the
v3 revision. I don't see any build failures on the QA. Is there anything
I need to do on my end in order to have the build restarted?

Greetings
Sören
S
S
soeren wrote on 28 Mar 20:20 +0100
[PATCH v4 1/2] gnu: Add klee-uclibc.
(address . 68296@debbugs.gnu.org)(address . julien@lepiller.eu)
d5c66ff568b4e9c84b2ecd4d8b44b88cf2dad619.1711653619.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee-uclibc): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
Change since v3: Resolve merge conflict, update KLEE website.

gnu/packages/check.scm | 62 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 62 insertions(+)

Toggle diff (86 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 7fd28c3ac7..9beba88788 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -51,6 +51,7 @@
;;; Copyright © 2024 Giacomo Leidi <goodoldpaul@autistici.org>
;;; Copyright © 2024 Zheng Junjie <873216071@qq.com>
;;; Copyright © 2024 Navid Afkhami <navid.afkhami@mdc-berlin.de>
+;;; Copyright © 2024 Sören Tempel <soeren@soeren-tempel.net>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -84,6 +85,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 ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -3705,3 +3707,63 @@ (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)
+ ;; Only x86_64 is presently supported by KLEE upstream.
+ (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))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list 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-se.org/")
+ (license license:lgpl2.1))))

base-commit: daab3da5042a5803ffa13ee759b3f8895dd92de4
S
S
soeren wrote on 28 Mar 20:20 +0100
[PATCH v4 2/2] gnu: Add klee.
(address . 68296@debbugs.gnu.org)(address . julien@lepiller.eu)
375eabc4693b9416e53c58fead36e0b8d4dde25d.1711653619.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>
---
Change since v3: Update KLEE website.

gnu/packages/check.scm | 55 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 55 insertions(+)

Toggle diff (84 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 9beba88788..f936bb12c1 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -76,6 +76,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)
@@ -85,6 +86,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)
@@ -94,6 +96,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)
@@ -3767,3 +3770,55 @@ (define-public klee-uclibc
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))))
?