[PATCH 0/2] Add klee-uclibc.

  • Open
  • quality assurance status badge
Details
2 participants
  • Liliana Marie Prikler
  • soeren
Owner
unassigned
Submitted by
soeren
Severity
normal
S
S
soeren wrote on 3 Jul 21:03 +0200
(address . guix-patches@gnu.org)
cover.1720033365.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

As requested by Liliana Marie Prikler in #68296, this patchset readds
support for KLEE uclibc based on the new version of the KLEE package
merged via #71634.

Sören Tempel (2):
gnu: Add klee-uclibc.
gnu: klee: Build with klee-uclibc support.

gnu/packages/check.scm | 75 ++++++++++++++++++++++++++++++++++++++++--
1 file changed, 73 insertions(+), 2 deletions(-)


base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
S
S
soeren wrote on 3 Jul 21:09 +0200
[PATCH 1/2] gnu: Add klee-uclibc.
(address . 71925@debbugs.gnu.org)
05cf10c887315b7b2ee2a4ee5d43a6baea969d6c.1720033365.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 | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)

Toggle diff (76 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..35e26ba6da 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#: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)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(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)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #: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")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-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-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")
S
S
soeren wrote on 3 Jul 21:09 +0200
[PATCH 2/2] gnu: klee: Build with klee-uclibc support.
(address . 71925@debbugs.gnu.org)
50e13182dab9f13a90c63a670a286eb447133e44.1720033365.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee): Use klee-uclibc.
---
gnu/packages/check.scm | 17 +++++++++++++++--
1 file changed, 15 insertions(+), 2 deletions(-)

Toggle diff (33 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 35e26ba6da..ad589f6e15 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1062,13 +1062,26 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" ":" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ "-DENABLE_POSIX_RUNTIME=ON"
+ (string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc))))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
L
L
Liliana Marie Prikler wrote on 6 Jul 20:49 +0200
(address . julien@lepiller.eu)
beaba06e67a41d85922028cb56dbffb85f4e87e1.camel@gmail.com
Am Mittwoch, dem 03.07.2024 um 21:09 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (31 lines)
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee): Use klee-uclibc.
> ---
>  gnu/packages/check.scm | 17 +++++++++++++++--
>  1 file changed, 15 insertions(+), 2 deletions(-)
>
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 35e26ba6da..ad589f6e15 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -1062,13 +1062,26 @@ (define-public klee
>        (base32
> "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
>     (arguments
>      (list
> +     #:phases
> +     #~(modify-phases %standard-phases
> +                      (add-after 'install 'wrap-hooks
> +                        (lambda* (#:key inputs outputs #:allow-
> other-keys)
> +                          (let* ((out (assoc-ref outputs "out"))
> +                                 (bin (string-append out "/bin"))
> +                                 (lib (string-append out "/lib")))
> +                            ;; Ensure that KLEE finds runtime
> libraries (e.g. uclibc).
> +                            (wrap-program (string-append bin
> "/klee")
> +                              `("KLEE_RUNTIME_LIBRARY_PATH" ":" =
> +                                (,(string-append lib
> "/klee/runtime/"))))))))
The leading colon is pointless here, since you're doing an "=" assign.
More importantly, can we make this a search path?
Toggle quote (11 lines)
>       #:configure-flags
>       #~(list (string-append "-DLLVMCC="
>                              (search-input-file %build-inputs
> "/bin/clang"))
>               (string-append "-DLLVMCXX="
> -                            (search-input-file %build-inputs
> "/bin/clang++")))))
> +                            (search-input-file %build-inputs
> "/bin/clang++"))
> +             "-DENABLE_POSIX_RUNTIME=ON"
> +             (string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc))))
Can we use search-input-file for this and dirname our way up?
Toggle quote (7 lines)
>     (native-inputs (list clang-13 llvm-13 python-lit))
> -   (inputs (list gperftools sqlite z3))
> +   (inputs (list bash-minimal gperftools sqlite z3))
>     (build-system cmake-build-system)
>     (home-page "https://klee-se.org/")
>     (synopsis "Symbolic execution engine")

Cheers
L
L
Liliana Marie Prikler wrote on 6 Jul 20:50 +0200
Re: [PATCH 1/2] gnu: Add klee-uclibc.
(address . julien@lepiller.eu)
ddaeaed1aaf85915778faf0f63060af899f114f9.camel@gmail.com
Am Mittwoch, dem 03.07.2024 um 21:09 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (94 lines)
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee-uclibc): New variable.
> ---
>  gnu/packages/check.scm | 58
> ++++++++++++++++++++++++++++++++++++++++++
>  1 file changed, 58 insertions(+)
>
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 550a5d0f1d..35e26ba6da 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -87,6 +87,7 @@ (define-module (gnu packages check)
>    #: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)
> @@ -989,6 +990,63 @@ (define-public greatest
>  runner.  It is quite unopinionated with most of its features being
> optional.")
>     (license license:isc)))
>  
> +(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)
> +      (arguments
> +       `(#:tests? #f ;upstream uClibc tests do not work in the fork
> +         #:strip-directories '() ;only ships a static library, so
> don't strip anything.
> +         #: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")))))))
> +      ;; ncurses is only needed for the `make menuconfig` interface.
> +      (native-inputs (list clang-13 llvm-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-se.org/")
> +      (license license:lgpl2.1))))
Is this only distributed as an .a file or could we make a .so out of
it?
S
S
Sören Tempel wrote on 7 Jul 13:24 +0200
Re: [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)
2XB2CJ5QYV5K9.2OYVJ6R77DM9T@8pit.net
Hi Liliana,

Thanks a lot for the quick feedback, responses below.

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (2 lines)
> The leading colon is pointless here, since you're doing an "=" assign.

Good catch! I can fix this in a patch revision.

Toggle quote (2 lines)
> More importantly, can we make this a search path?

I don't think so as it's not a colon separated search path, it can only
point to a single directory; hence, I assumed that wrap-program is more
appropriate here.

Toggle quote (2 lines)
> Can we use search-input-file for this and dirname our way up?

The input file that we are looking for here is called libc.a, I am not
sure what the benefit of using search-input-file is, but I personally
think something along the lines of `(dirname (search-input-file
%build-inputs "/lib/libc.a"))` is less readable then `#$klee-uclibc` but
I can definitely change this if you want me to :)

Toggle quote (3 lines)
> Is this only distributed as an .a file or could we make a .so out of
> it?

This is only distributed as a .a, not as a shared object. In fact, KLEE
also doesn't not link against this library at all and instead converts
it to an LLVM .bca file (shipped in /lib/klee/runtime/klee-uclibc.bca)
during build. This file is then used directly by KLEE's symbolic LLVM
interpreter to execute code utilizing libc functions. Hence, klee-uclibc
is also not a propagated input for the klee package.

Let me know if I should send a revision, would love to get this merged.

Greetings
Sören
L
L
Liliana Marie Prikler wrote on 7 Jul 14:51 +0200
(name . Sören Tempel)(address . soeren@soeren-tempel.net)
03ef8e192f61f68529f3ce252f8564e4d16adf22.camel@gmail.com
Am Sonntag, dem 07.07.2024 um 13:24 +0200 schrieb Sören Tempel:
Toggle quote (15 lines)
> Hi Liliana,
>
> Thanks a lot for the quick feedback, responses below.
>
> Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> > The leading colon is pointless here, since you're doing an "="
> > assign.
>
> Good catch! I can fix this in a patch revision.
>
> > More importantly, can we make this a search path?
>
> I don't think so as it's not a colon separated search path, it can
> only point to a single directory; hence, I assumed that wrap-program
> is more appropriate here.
Fair enough.

Toggle quote (22 lines)
> > Can we use search-input-file for this and dirname our way up?
>
> The input file that we are looking for here is called libc.a, I am
> not
> sure what the benefit of using search-input-file is, but I personally
> think something along the lines of `(dirname (search-input-file
> %build-inputs "/lib/libc.a"))` is less readable then `#$klee-uclibc`
> but I can definitely change this if you want me to :)
>
> > Is this only distributed as an .a file or could we make a .so out
> > of it?
>
> This is only distributed as a .a, not as a shared object. In fact,
> KLEE also doesn't not link against this library at all and instead
> converts it to an LLVM .bca file (shipped in
> /lib/klee/runtime/klee-uclibc.bca)
> during build. This file is then used directly by KLEE's symbolic LLVM
> interpreter to execute code utilizing libc functions. Hence, klee-
> uclibc is also not a propagated input for the klee package.
>
> Let me know if I should send a revision, would love to get this
> merged.
Can we make it so that it uses the file directly instead of inferring
the name? Then we could install klee-uclibc to, say
"/lib/klee/uclibc.a" and reference it in this build by said file name.

Cheers
S
S
Sören Tempel wrote on 7 Jul 18:50 +0200
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)
2I2XVCBZLFNGD.2I6J74TIZU0U6@8pit.net
Hello!

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (4 lines)
> Can we make it so that it uses the file directly instead of inferring
> the name? Then we could install klee-uclibc to, say
> "/lib/klee/uclibc.a" and reference it in this build by said file name.

That would require us to patch KLEE's CMakeLists.txt and I am not sure
if that's worth it [1]. I think I would personally prefer using
search-input-file and dirname then. However, I am also still somewhat
new to Guix, could you elaborate what the problem with using
`(string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc)` is (for the sake
of expanding my understanding of Guix in this regard)?

Greetings,
Sören

L
L
Liliana Marie Prikler wrote on 7 Jul 18:53 +0200
(name . Sören Tempel)(address . soeren@soeren-tempel.net)
9104732dc4c3cd3ee69efbebdf91f695227ba409.camel@gmail.com
Am Sonntag, dem 07.07.2024 um 18:50 +0200 schrieb Sören Tempel:
Toggle quote (14 lines)
> Hello!
>
> Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> > Can we make it so that it uses the file directly instead of
> > inferring the name?  Then we could install klee-uclibc to, say
> > "/lib/klee/uclibc.a" and reference it in this build by said file
> > name.
>
> That would require us to patch KLEE's CMakeLists.txt and I am not
> sure if that's worth it [1]. I think I would personally prefer using
> search-input-file and dirname then. However, I am also still somewhat
> new to Guix, could you elaborate what the problem with using
> `(string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc)` is (for the
> sake of expanding my understanding of Guix in this regard)?
Well, the question is mainly what people ought to do to swap out klee-
uclibc from their builds – e.g. if they want to replace it with a newer
one etc. Inputs are our means of making sure that people have a handle
for this kind of thing.

Cheers
S
S
soeren wrote on 7 Jul 19:26 +0200
[PATCH v2 1/2] gnu: Add klee-uclibc.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
05cf10c887315b7b2ee2a4ee5d43a6baea969d6c.1720373191.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 | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)

Toggle diff (78 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..35e26ba6da 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#: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)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(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)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #: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")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-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-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")

base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
S
S
soeren wrote on 7 Jul 19:26 +0200
[PATCH v2 2/2] gnu: klee: Build with klee-uclibc support.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
635839070779883196fec8119d70c273f46fc841.1720373191.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee): Use klee-uclibc.
---
gnu/packages/check.scm | 21 ++++++++++++++++++---
1 file changed, 18 insertions(+), 3 deletions(-)

Toggle diff (44 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 35e26ba6da..52941681a9 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1036,7 +1036,7 @@ (define-public klee-uclibc
(lambda* (#:key outputs #:allow-other-keys)
(install-file "lib/libc.a"
(string-append (assoc-ref outputs "out")
- "/lib")))))))
+ "/klee/lib")))))))
;; ncurses is only needed for the `make menuconfig` interface.
(native-inputs (list clang-13 llvm-13 python ncurses))
(synopsis "Variant of uClibc tailored to symbolic execution")
@@ -1062,13 +1062,28 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ (string-append "-DKLEE_UCLIBC_PATH="
+ (let ((uclibc (search-input-file %build-inputs "/klee/lib/libc.a")))
+ (dirname (dirname uclibc))))
+ "-DENABLE_POSIX_RUNTIME=ON")))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
S
S
Sören Tempel wrote on 7 Jul 19:28 +0200
Re: [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)
3OHFY87A45M1V.3QUHDHLCMIAUN@8pit.net
Hello again!

Thanks for the explanation, I send a v2 revision which (hopefully)
addresses your feedback. I have opted to install the libc.a file
to /klee/lib/libc.a this way, it's compatible with search-inputs
without requiring us to patch KLEE's build system.

Let me know what you think :)

Best,
Sören

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (21 lines)
> Am Sonntag, dem 07.07.2024 um 18:50 +0200 schrieb Sören Tempel:
> > Hello!
> >
> > Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> > > Can we make it so that it uses the file directly instead of
> > > inferring the name?  Then we could install klee-uclibc to, say
> > > "/lib/klee/uclibc.a" and reference it in this build by said file
> > > name.
> >
> > That would require us to patch KLEE's CMakeLists.txt and I am not
> > sure if that's worth it [1]. I think I would personally prefer using
> > search-input-file and dirname then. However, I am also still somewhat
> > new to Guix, could you elaborate what the problem with using
> > `(string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc)` is (for the
> > sake of expanding my understanding of Guix in this regard)?
> Well, the question is mainly what people ought to do to swap out klee-
> uclibc from their builds – e.g. if they want to replace it with a newer
> one etc. Inputs are our means of making sure that people have a handle
> for this kind of thing.
>
> Cheers
L
L
Liliana Marie Prikler wrote on 7 Jul 20:27 +0200
(name . Sören Tempel)(address . soeren@soeren-tempel.net)
ab01d0562524d094ea3fb368d46be7a684cae7cd.camel@gmail.com
Am Sonntag, dem 07.07.2024 um 19:28 +0200 schrieb Sören Tempel:
Toggle quote (6 lines)
> Hello again!
>
> Thanks for the explanation, I send a v2 revision which (hopefully)
> addresses your feedback. I have opted to install the libc.a file
> to /klee/lib/libc.a this way, it's compatible with search-inputs
> without requiring us to patch KLEE's build system.
v2's klee-uclibc appears to still install libc.a in /lib rather than
/klee/lib – do you want it do be this way around or would /lib/klee/
(honouring FHS) be smarter?

Cheers
S
S
Sören Tempel wrote on 7 Jul 21:18 +0200
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)
3HKO6B5FBRRNO.3SLAKAED4GW6B@8pit.net
Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (3 lines)
> v2's klee-uclibc appears to still install libc.a in /lib rather than
> /klee/lib –

Sorry, I messed up the rebase and added the change to klee-uclibc in
the second patch by accident, see [1]. I will send a v3 which fixes
this in a second.

Toggle quote (3 lines)
> do you want it do be this way around or would /lib/klee/ (honouring
> FHS) be smarter?

If we want to install the file to /lib/klee, then we would have to
patch the KLEE build system [2], which I wanted to avoid. I can also
patch it if you think that this is preferable, might need some source
code changes too.

S
S
soeren wrote on 7 Jul 21:19 +0200
[PATCH v3 1/2] gnu: Add klee-uclibc.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
ca2fbf509971b2989d19a8453104f39b9bf83b31.1720379948.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 | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)

Toggle diff (78 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..c4bae49165 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#: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)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(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)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #: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")
+ "/klee/lib")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-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-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")

base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
S
S
soeren wrote on 7 Jul 21:19 +0200
[PATCH v3 2/2] gnu: klee: Build with klee-uclibc support.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
bc626248787fef81cae9516e769b6c7f66761bdb.1720379948.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee): Use klee-uclibc.
---
gnu/packages/check.scm | 19 +++++++++++++++++--
1 file changed, 17 insertions(+), 2 deletions(-)

Toggle diff (35 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index c4bae49165..52941681a9 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1062,13 +1062,28 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ (string-append "-DKLEE_UCLIBC_PATH="
+ (let ((uclibc (search-input-file %build-inputs "/klee/lib/libc.a")))
+ (dirname (dirname uclibc))))
+ "-DENABLE_POSIX_RUNTIME=ON")))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
S
S
soeren wrote on 8 Jul 09:44 +0200
[PATCH v4 1/2] gnu: Add klee-uclibc.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
d57c4626695febcdecb7c311683ff13aea38cd62.1720424666.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee-uclibc): New variable.
---
Changes since v3: Move klee-uclibc library to `/lib/klee/libc.a`.

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

Toggle diff (78 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..e02dc1b23d 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#: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)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(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)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #: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/klee")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-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-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")

base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
S
S
soeren wrote on 8 Jul 09:44 +0200
[PATCH v4 2/2] gnu: klee: Build with klee-uclibc support.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
f7fcf9dc63120ba16998fd03aac4c5c55ce1cab6.1720424666.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/check.scm (klee): Use klee-uclibc.
---
Changes since v3: Move klee-uclibc library to `/lib/klee/libc.a`.

gnu/packages/check.scm | 23 +++++++++++++++++++++--
1 file changed, 21 insertions(+), 2 deletions(-)

Toggle diff (39 lines)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index e02dc1b23d..c4eaaef18f 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1062,13 +1062,32 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch
+ (lambda _
+ (substitute* "CMakeLists.txt"
+ (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
+ "${KLEE_UCLIBC_PATH}"))))
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ (string-append "-DKLEE_UCLIBC_PATH="
+ (search-input-file %build-inputs "/lib/klee/libc.a"))
+ "-DENABLE_POSIX_RUNTIME=ON")))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
S
S
Sören Tempel wrote on 8 Jul 10:47 +0200
Re: [PATCH 0/2] Add klee-uclibc.
(address . 71925@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
3G0ABCR7EO6BC.2W7E130L8W7IA@8pit.net
Hello,

I just send a v4 which moves the library file from /klee/lib/libc.a to
/lib/klee/libc.a. I tested this a bit and it sees to work fine. From my
point of view, the only problem that remains is that KLEE only really
supports x86_64; hence, the build fails on aarch64 [1].

In #68296, I therefore added `(supported-systems '("x86_64-linux"))` but
this wasn't included in #71634. Should I re-add that here or do we want
to do that separately?

Best,
Sören

?
Your comment

Commenting via the web interface is currently disabled.

To comment on this conversation send an email to 71925@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 71925
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch