GNU bug report logs - #72106
[PATCH 0/3] gnu: klee: Enable test suite

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 72106 in the body.
You can then email your comments to 72106 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: guix-patches <at> gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH 0/3] gnu: klee: Enable test suite
Date: Sun, 14 Jul 2024 12:36:16 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

The KLEE version packaged added in #71634 did not enable the KLEE
test suite.  This patchset re-adds the changes from #68296 to get
the test suite to pass.  Additionally, while working on this, I
noticed that the current KLEE package does not propagate the Python
dependencies needed by klee-stats, which I fixed as well.  Lastly,
I also passed a custom #:strip-directories argument to avoid stripping
of LLVM bitcode which (prior to this patchset) caused strip(1) to
emit several warnings in the build log.

P.S.: I also think it might be worthwhile to only enable the KLEE
package on x86_64 Linux <https://issues.guix.gnu.org/71925#18>.  Let me
know if I should add that as well :-)


Sören Tempel (3):
  gnu: klee: Propagate Python dependencies needed by klee-stats.
  gnu: klee: Enable the test suite.
  gnu: klee: Only strip bin directory.

 gnu/packages/check.scm | 32 +++++++++++++++++++++++++++++---
 1 file changed, 29 insertions(+), 3 deletions(-)


base-commit: c1d367f57e89c3f2efd964e6d638bd89b0b1df97

Message #8 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH 1/3] gnu: klee: Propagate Python dependencies needed by
 klee-stats.
Date: Sun, 14 Jul 2024 12:42:13 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

Without these dependencies, the klee-stats Python script,
which is shipped by the klee package, does not work correctly.

* gnu/packages/check.scm (klee): Add propagated Python inputs.
---
 gnu/packages/check.scm | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 3bfcf5a37e..f31e1bdb36 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1087,6 +1087,8 @@ (define-public klee
              (string-append "-DKLEE_UCLIBC_PATH="
                             (search-input-file %build-inputs "/lib/klee/libc.a"))
              "-DENABLE_POSIX_RUNTIME=ON")))
+   ;; klee-stats tool (shipped in /bin) requires Python.
+   (propagated-inputs (list python python-tabulate))
    (native-inputs (list clang-13 llvm-13 python-lit))
    (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
    (build-system cmake-build-system)

Message #11 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH 2/3] gnu: klee: Enable the test suite.
Date: Sun, 14 Jul 2024 12:42:14 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Enable all tests.
[arguments]: Add phase to patch lit configuration, set #:test-target.
<#:configure-flags?>: Enable system and unit tests, configure gtest.
[inputs]: Add googletest and python-lit.
---
 gnu/packages/check.scm | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index f31e1bdb36..14d7124908 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,13 +1063,23 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases
-                      (add-after 'unpack 'patch
+                      (add-after 'unpack 'patch-cmake
                         (lambda _
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
                              "${KLEE_UCLIBC_PATH}"))))
+                      (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')")))))
                       (add-after 'install 'wrap-hooks
                         (lambda* (#:key inputs outputs #:allow-other-keys)
                           (let* ((out (assoc-ref outputs "out"))
@@ -1080,7 +1090,13 @@ (define-public klee
                               `("KLEE_RUNTIME_LIBRARY_PATH" =
                                 (,(string-append lib "/klee/runtime/"))))))))
      #:configure-flags
-     #~(list (string-append "-DLLVMCC="
+     #~(list "-DENABLE_UNIT_TESTS=ON"
+             "-DENABLE_SYSTEM_TESTS=ON"
+             (string-append "-DGTEST_SRC_DIR="
+                            (assoc-ref %build-inputs "googletest"))
+             (string-append "-DGTEST_INCLUDE_DIR="
+                            (assoc-ref %build-inputs "googletest") "/googletest/include")
+             (string-append "-DLLVMCC="
                             (search-input-file %build-inputs "/bin/clang"))
              (string-append "-DLLVMCXX="
                             (search-input-file %build-inputs "/bin/clang++"))
@@ -1090,7 +1106,14 @@ (define-public klee
    ;; klee-stats tool (shipped in /bin) requires Python.
    (propagated-inputs (list python python-tabulate))
    (native-inputs (list clang-13 llvm-13 python-lit))
-   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
+   (inputs
+     `(("bash-minimal" ,bash-minimal)
+       ("klee-uclibc" ,klee-uclibc)
+       ("gperftools" ,gperftools)
+       ("sqlite" ,sqlite)
+       ("z3" ,z3)
+       ("python-lit" ,python-lit)
+       ("googletest" ,(package-source googletest))))
    (build-system cmake-build-system)
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")

Message #14 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH 3/3] gnu: klee: Only strip bin directory.
Date: Sun, 14 Jul 2024 12:42:15 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

This avoid several warnings to be emitted by strip(1) when attempting
to strip .bca (i.e. LLVM bitcode) files shipped in /lib/klee/runtime/.

* gnu/packages/check.scm (klee): Set #:strip-directories.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 14d7124908..47e99a6be5 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,6 +1063,7 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:strip-directories #~(list "bin") ;don't strip LLVM bitcode in /lib
      #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases

Message #17 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH 1/3] gnu: klee: Propagate Python dependencies needed by
 klee-stats.
Date: Sun, 14 Jul 2024 13:43:13 +0200

Am Sonntag, dem 14.07.2024 um 12:42 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> Without these dependencies, the klee-stats Python script,
> which is shipped by the klee package, does not work correctly.
> 
> * gnu/packages/check.scm (klee): Add propagated Python inputs.
Can we use a wrapper instead?

Message #20 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH 0/3] gnu: klee: Enable test suite
Date: Sun, 14 Jul 2024 18:17:00 +0200

Am Sonntag, dem 14.07.2024 um 12:36 +0200 schrieb
soeren <at> soeren-tempel.net:

> Lastly, I also passed a custom #:strip-directories argument to avoid
> stripping of LLVM bitcode which (prior to this patchset) caused
> strip(1) to emit several warnings in the build log.
There is only .bca files in there, right?

> P.S.: I also think it might be worthwhile to only enable the KLEE
> package on x86_64 Linux <https://issues.guix.gnu.org/71925#18>.  Let
> me know if I should add that as well :-)
Ah, yes, good catch.

Message #23 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v2 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
Date: Sun, 14 Jul 2024 20:25:24 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Wrap klee-stats.
---
 gnu/packages/check.scm | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 3bfcf5a37e..6b0ea0aaa8 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1070,7 +1070,15 @@ (define-public klee
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
                              "${KLEE_UCLIBC_PATH}"))))
-                      (add-after 'install 'wrap-hooks
+                      (add-after 'install 'wrap-klee-stats
+                        (lambda* (#:key outputs #:allow-other-keys)
+                          (let* ((out (assoc-ref outputs "out"))
+                                 (bin (string-append out "/bin")))
+                            (wrap-program (string-append bin "/klee-stats")
+                              `("GUIX_PYTHONPATH" ":" prefix
+                                ,(search-path-as-string->list
+                                   (getenv "GUIX_PYTHONPATH")))))))
+                      (add-after 'install 'wrap-klee
                         (lambda* (#:key inputs outputs #:allow-other-keys)
                           (let* ((out (assoc-ref outputs "out"))
                                  (bin (string-append out "/bin"))
@@ -1088,7 +1096,7 @@ (define-public klee
                             (search-input-file %build-inputs "/lib/klee/libc.a"))
              "-DENABLE_POSIX_RUNTIME=ON")))
    (native-inputs (list clang-13 llvm-13 python-lit))
-   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
+   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
    (build-system cmake-build-system)
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")

base-commit: c1d367f57e89c3f2efd964e6d638bd89b0b1df97

Message #26 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v2 2/5] gnu: klee: Enable the test suite.
Date: Sun, 14 Jul 2024 20:25:25 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Enable all tests.
[arguments]: Add phase to patch lit configuration, set #:test-target.
<#:configure-flags?>: Enable system and unit tests, configure gtest.
[inputs]: Add googletest and python-lit.
---
 gnu/packages/check.scm | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 6b0ea0aaa8..552cb39de5 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,13 +1063,23 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases
-                      (add-after 'unpack 'patch
+                      (add-after 'unpack 'patch-cmake
                         (lambda _
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
                              "${KLEE_UCLIBC_PATH}"))))
+                      (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')")))))
                       (add-after 'install 'wrap-klee-stats
                         (lambda* (#:key outputs #:allow-other-keys)
                           (let* ((out (assoc-ref outputs "out"))
@@ -1088,7 +1098,13 @@ (define-public klee
                               `("KLEE_RUNTIME_LIBRARY_PATH" =
                                 (,(string-append lib "/klee/runtime/"))))))))
      #:configure-flags
-     #~(list (string-append "-DLLVMCC="
+     #~(list "-DENABLE_UNIT_TESTS=ON"
+             "-DENABLE_SYSTEM_TESTS=ON"
+             (string-append "-DGTEST_SRC_DIR="
+                            (assoc-ref %build-inputs "googletest"))
+             (string-append "-DGTEST_INCLUDE_DIR="
+                            (assoc-ref %build-inputs "googletest") "/googletest/include")
+             (string-append "-DLLVMCC="
                             (search-input-file %build-inputs "/bin/clang"))
              (string-append "-DLLVMCXX="
                             (search-input-file %build-inputs "/bin/clang++"))
@@ -1096,7 +1112,15 @@ (define-public klee
                             (search-input-file %build-inputs "/lib/klee/libc.a"))
              "-DENABLE_POSIX_RUNTIME=ON")))
    (native-inputs (list clang-13 llvm-13 python-lit))
-   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
+   (inputs
+     `(("bash-minimal" ,bash-minimal)
+       ("klee-uclibc" ,klee-uclibc)
+       ("gperftools" ,gperftools)
+       ("sqlite" ,sqlite)
+       ("z3" ,z3)
+       ("python", python)
+       ("python-tabulate" ,python-tabulate)
+       ("googletest" ,(package-source googletest))))
    (build-system cmake-build-system)
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")

Message #29 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v2 3/5] gnu: klee: Only strip bin directory.
Date: Sun, 14 Jul 2024 20:25:26 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

This avoid several warnings to be emitted by strip(1) when attempting
to strip .bca (i.e. LLVM bitcode) files shipped in /lib/klee/runtime/.

* gnu/packages/check.scm (klee): Set #:strip-directories.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 552cb39de5..3f3cc64e8e 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,6 +1063,7 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:strip-directories #~(list "bin") ;don't strip LLVM bitcode in /lib
      #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases

Message #32 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v2 4/5] gnu: klee: Only build on x86_64 Linux.
Date: Sun, 14 Jul 2024 20:25:27 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Add supported-systems.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 3f3cc64e8e..3fc88b078f 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1123,6 +1123,7 @@ (define-public klee
        ("python-tabulate" ,python-tabulate)
        ("googletest" ,(package-source googletest))))
    (build-system cmake-build-system)
+   (supported-systems '("x86_64-linux"))
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")
    (description "KLEE is a symbolic virtual machine built on top of the LLVM

Message #35 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v2 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
Date: Sun, 14 Jul 2024 20:25:28 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Add supported-systems.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 3fc88b078f..e48d392251 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1006,6 +1006,7 @@ (define-public klee-uclibc
          (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
          #:strip-directories '() ;only ships a static library, so don't strip anything.

Message #38 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH 0/3] gnu: klee: Enable test suite
Date: Sun, 14 Jul 2024 20:29:48 +0200

Hi Liliana,

Thanks for your feedback, I added a v2 to incorporate your feedback.

Liliana Marie Prikler <liliana.prikler <at> gmail.com> wrote:
> Can we use a wrapper instead?

Sure, good idea! I modified the patch to wrap klee-stats instead.
Haven't done that so far so please check if I did it correctly :)

> > Lastly, I also passed a custom #:strip-directories argument to avoid
> > stripping of LLVM bitcode which (prior to this patchset) caused
> > strip(1) to emit several warnings in the build log.
>
> There is only .bca files in there, right?

Only .bca files and one shared library (libkleeRuntest.so) are in /lib.
Does stripping of shared libraries do anything? If so: Should we just
live with the warnings or should we strip that file individually?

> > P.S.: I also think it might be worthwhile to only enable the KLEE
> > package on x86_64 Linux <https://issues.guix.gnu.org/71925#18>.  Let
> > me know if I should add that as well :-)
>
> Ah, yes, good catch.

I added two additional commits to set supported-systems for KLEE.

Best,
Sören

Message #41 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH v2 2/5] gnu: klee: Enable the test suite.
Date: Sun, 14 Jul 2024 20:53:49 +0200

Am Sonntag, dem 14.07.2024 um 20:25 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> * gnu/packages/check.scm (klee): Enable all tests.
> [arguments]: Add phase to patch lit configuration, set #:test-target.
> <#:configure-flags?>: Enable system and unit tests, configure gtest.
> [inputs]: Add googletest and python-lit.
> ---
>  gnu/packages/check.scm | 30 +++++++++++++++++++++++++++---
>  1 file changed, 27 insertions(+), 3 deletions(-)
> 
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 6b0ea0aaa8..552cb39de5 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -1063,13 +1063,23 @@ (define-public klee
>        (base32
> "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
>     (arguments
>      (list
> +     #:test-target "check"
>       #:phases
>       #~(modify-phases %standard-phases
> -                      (add-after 'unpack 'patch
> +                      (add-after 'unpack 'patch-cmake
>                          (lambda _
>                            (substitute* "CMakeLists.txt"
>                             
> (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
>                               "${KLEE_UCLIBC_PATH}"))))
> +                      (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')")))))
If this is a test, then we should use native-inputs below.
>                        (add-after 'install 'wrap-klee-stats
>                          (lambda* (#:key outputs #:allow-other-keys)
>                            (let* ((out (assoc-ref outputs "out"))
> @@ -1088,7 +1098,13 @@ (define-public klee
>                                `("KLEE_RUNTIME_LIBRARY_PATH" =
>                                  (,(string-append lib
> "/klee/runtime/"))))))))
>       #:configure-flags
> -     #~(list (string-append "-DLLVMCC="
> +     #~(list "-DENABLE_UNIT_TESTS=ON"
> +             "-DENABLE_SYSTEM_TESTS=ON"
> +             (string-append "-DGTEST_SRC_DIR="
> +                            (assoc-ref %build-inputs "googletest"))
> +             (string-append "-DGTEST_INCLUDE_DIR="
> +                            (assoc-ref %build-inputs "googletest")
> "/googletest/include")
> +             (string-append "-DLLVMCC="
>                              (search-input-file %build-inputs
> "/bin/clang"))
>               (string-append "-DLLVMCXX="
>                              (search-input-file %build-inputs
> "/bin/clang++"))
> @@ -1096,7 +1112,15 @@ (define-public klee
>                              (search-input-file %build-inputs
> "/lib/klee/libc.a"))
>               "-DENABLE_POSIX_RUNTIME=ON")))
>     (native-inputs (list clang-13 llvm-13 python-lit))
> -   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3
> python python-tabulate))
> +   (inputs
> +     `(("bash-minimal" ,bash-minimal)
> +       ("klee-uclibc" ,klee-uclibc)
> +       ("gperftools" ,gperftools)
> +       ("sqlite" ,sqlite)
> +       ("z3" ,z3)
> +       ("python", python)
> +       ("python-tabulate" ,python-tabulate)
> +       ("googletest" ,(package-source googletest))))
Why the package source and not the compiled package?  Can we make it so
that we can use a prebuilt compiled one?

Cheers

Message #44 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH v2 4/5] gnu: klee: Only build on x86_64 Linux.
Date: Sun, 14 Jul 2024 20:54:04 +0200

Am Sonntag, dem 14.07.2024 um 20:25 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> * gnu/packages/check.scm (klee): Add supported-systems.
> ---
>  gnu/packages/check.scm | 1 +
>  1 file changed, 1 insertion(+)
> 
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 3f3cc64e8e..3fc88b078f 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -1123,6 +1123,7 @@ (define-public klee
>         ("python-tabulate" ,python-tabulate)
>         ("googletest" ,(package-source googletest))))
>     (build-system cmake-build-system)
> +   (supported-systems '("x86_64-linux"))
>     (home-page "https://klee-se.org/")
>     (synopsis "Symbolic execution engine")
>     (description "KLEE is a symbolic virtual machine built on top of
> the LLVM
LGTM

Message #47 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH v2 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
Date: Sun, 14 Jul 2024 20:54:53 +0200

Am Sonntag, dem 14.07.2024 um 20:25 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> * gnu/packages/check.scm (klee): Add supported-systems.
Should be klee-uclibc.
> ---
>  gnu/packages/check.scm | 1 +
>  1 file changed, 1 insertion(+)
> 
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 3fc88b078f..e48d392251 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -1006,6 +1006,7 @@ (define-public klee-uclibc
>           (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
>           #:strip-directories '() ;only ships a static library, so
> don't strip anything.
Cheers

Message #50 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH v2 2/5] gnu: klee: Enable the test suite.
Date: Sun, 14 Jul 2024 22:04:09 +0200

Hello Liliana,

Liliana Marie Prikler <liliana.prikler <at> gmail.com> wrote:
> Why the package source and not the compiled package?  Can we make it so
> that we can use a prebuilt compiled one?

Unfortunately, this does not seem to be possible. You can only point the
KLEE build system to a googletest source [1]. This seems to be related
to some peculiarity of googletest as other Guix package do the same
thing [2] [3] [4] (there are more grep for "package-source googletest").

> If this is a test, then we should use native-inputs below.

What exact dependency are you referring to? python-lit is already
declared as a dependency through native-inputs.

> Should be klee-uclibc.

Good catch! I can send a revision fixing the commit message.

Is there anything else I should adjust in a v3 revision?

Cheers,
Sören

[1]: https://github.com/klee/klee/blob/master/README-CMake.md?plain=1#L60-L62
[2]: https://git.savannah.gnu.org/cgit/guix.git/tree/gnu/packages/crypto.scm?id=eb508e32d2d359c94d2cabebfe90dc32ca5dcf4f#n336
[3]: https://git.savannah.gnu.org/cgit/guix.git/tree/gnu/packages/benchmark.scm?id=eb508e32d2d359c94d2cabebfe90dc32ca5dcf4f#n241
[4]: https://git.savannah.gnu.org/cgit/guix.git/tree/gnu/packages/chemistry.scm?id=eb508e32d2d359c94d2cabebfe90dc32ca5dcf4f#n407

Message #53 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: soeren <at> soeren-tempel.net
Cc: 72106 <at> debbugs.gnu.org, liliana.prikler <at> gmail.com
Subject: Re: [bug#72106] [PATCH v2 2/5] gnu: klee: Enable the test suite.
Date: Sat, 20 Jul 2024 11:56:57 +0200

Hello Sören,

soeren <at> soeren-tempel.net skribis:

>                                  (,(string-append lib "/klee/runtime/"))))))))
>       #:configure-flags
> -     #~(list (string-append "-DLLVMCC="
> +     #~(list "-DENABLE_UNIT_TESTS=ON"
> +             "-DENABLE_SYSTEM_TESTS=ON"
> +             (string-append "-DGTEST_SRC_DIR="
> +                            (assoc-ref %build-inputs "googletest"))
> +             (string-append "-DGTEST_INCLUDE_DIR="
> +                            (assoc-ref %build-inputs "googletest") "/googletest/include")

I would replace (assoc-ref …) by:

  #+(package-source googletest)

> -   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
> +   (inputs
> +     `(("bash-minimal" ,bash-minimal)
> +       ("klee-uclibc" ,klee-uclibc)
> +       ("gperftools" ,gperftools)
> +       ("sqlite" ,sqlite)
> +       ("z3" ,z3)
> +       ("python", python)
> +       ("python-tabulate" ,python-tabulate)
> +       ("googletest" ,(package-source googletest))))

… and leave ‘googletest’ out of ‘inputs’ entirely, keeping the concise
input list without labels.  (I think we shouldn’t reintroduce input
labels; the goal has always been to remove them.)

WDYT?

Besides, to answer Liliana, Googletest is often used as a “source
library” like you’re doing here; there are quite a few other packages
that do that in Guix already, as you explained.  That’s OK.

Thanks,
Ludo’.

Message #56 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, liliana.prikler <at> gmail.com
Subject: [PATCH v3 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
Date: Thu, 25 Jul 2024 22:39:59 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Wrap klee-stats.
---
 gnu/packages/check.scm | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 412b94569c..3c5ed7a3c3 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1070,7 +1070,15 @@ (define-public klee
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
                              "${KLEE_UCLIBC_PATH}"))))
-                      (add-after 'install 'wrap-hooks
+                      (add-after 'install 'wrap-klee-stats
+                        (lambda* (#:key outputs #:allow-other-keys)
+                          (let* ((out (assoc-ref outputs "out"))
+                                 (bin (string-append out "/bin")))
+                            (wrap-program (string-append bin "/klee-stats")
+                              `("GUIX_PYTHONPATH" ":" prefix
+                                ,(search-path-as-string->list
+                                   (getenv "GUIX_PYTHONPATH")))))))
+                      (add-after 'install 'wrap-klee
                         (lambda* (#:key inputs outputs #:allow-other-keys)
                           (let* ((out (assoc-ref outputs "out"))
                                  (bin (string-append out "/bin"))
@@ -1088,7 +1096,7 @@ (define-public klee
                             (search-input-file %build-inputs "/lib/klee/libc.a"))
              "-DENABLE_POSIX_RUNTIME=ON")))
    (native-inputs (list clang-13 llvm-13 python-lit))
-   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
+   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
    (build-system cmake-build-system)
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")

base-commit: 03062c7a9fd74d625639e1a325e9cb58d1cd74e3

Message #59 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, liliana.prikler <at> gmail.com
Subject: [PATCH v3 2/5] gnu: klee: Enable the test suite.
Date: Thu, 25 Jul 2024 22:40:00 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Enable all tests.
[arguments]: Add phase to patch lit configuration, set #:test-target.
<#:configure-flags?>: Enable system and unit tests, configure gtest.
[inputs]: Add googletest and python-lit.
---
 gnu/packages/check.scm | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 3c5ed7a3c3..48e8ae3aef 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,13 +1063,23 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases
-                      (add-after 'unpack 'patch
+                      (add-after 'unpack 'patch-cmake
                         (lambda _
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
                              "${KLEE_UCLIBC_PATH}"))))
+                      (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')")))))
                       (add-after 'install 'wrap-klee-stats
                         (lambda* (#:key outputs #:allow-other-keys)
                           (let* ((out (assoc-ref outputs "out"))
@@ -1088,7 +1098,13 @@ (define-public klee
                               `("KLEE_RUNTIME_LIBRARY_PATH" =
                                 (,(string-append lib "/klee/runtime/"))))))))
      #:configure-flags
-     #~(list (string-append "-DLLVMCC="
+     #~(list "-DENABLE_UNIT_TESTS=ON"
+             "-DENABLE_SYSTEM_TESTS=ON"
+             (string-append "-DGTEST_SRC_DIR="
+                            #+(package-source googletest))
+             (string-append "-DGTEST_INCLUDE_DIR="
+                            #+(package-source googletest) "/googletest/include")
+             (string-append "-DLLVMCC="
                             (search-input-file %build-inputs "/bin/clang"))
              (string-append "-DLLVMCXX="
                             (search-input-file %build-inputs "/bin/clang++"))

Message #62 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, liliana.prikler <at> gmail.com
Subject: [PATCH v3 3/5] gnu: klee: Only strip bin directory.
Date: Thu, 25 Jul 2024 22:40:01 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

This avoid several warnings to be emitted by strip(1) when attempting
to strip .bca (i.e. LLVM bitcode) files shipped in /lib/klee/runtime/.

* gnu/packages/check.scm (klee): Set #:strip-directories.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 48e8ae3aef..1b7381cd36 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,6 +1063,7 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:strip-directories #~(list "bin") ;don't strip LLVM bitcode in /lib
      #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases

Message #65 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, liliana.prikler <at> gmail.com
Subject: [PATCH v3 4/5] gnu: klee: Only build on x86_64 Linux.
Date: Thu, 25 Jul 2024 22:40:02 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Add supported-systems.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 1b7381cd36..75393ca179 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1115,6 +1115,7 @@ (define-public klee
    (native-inputs (list clang-13 llvm-13 python-lit))
    (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
    (build-system cmake-build-system)
+   (supported-systems '("x86_64-linux"))
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")
    (description "KLEE is a symbolic virtual machine built on top of the LLVM

Message #68 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org, liliana.prikler <at> gmail.com
Subject: [PATCH v3 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
Date: Thu, 25 Jul 2024 22:40:03 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee-uclibc): Add supported-systems.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 75393ca179..493829082b 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1006,6 +1006,7 @@ (define-public klee-uclibc
          (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
          #:strip-directories '() ;only ships a static library, so don't strip anything.

Message #71 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 72106 <at> debbugs.gnu.org, liliana.prikler <at> gmail.com
Subject: Re: [bug#72106] [PATCH v2 2/5] gnu: klee: Enable the test suite.
Date: Thu, 25 Jul 2024 22:43:11 +0200

Ludovic Courtès <ludo <at> gnu.org> wrote:
> Hello Sören,

Hi Ludo,

> … and leave ‘googletest’ out of ‘inputs’ entirely, keeping the concise
> input list without labels.  (I think we shouldn’t reintroduce input
> labels; the goal has always been to remove them.)
> 
> WDYT?

Thanks for this suggestion, this sounds very good to me!

I just send a v3 which implements this and also fixes the commit message
typo that Liliana pointed out. Let me know if there is anything else
that needs to be done :)

Best,
Sören

Message #74 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org
Subject: Re: [PATCH v3 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
Date: Fri, 26 Jul 2024 20:37:33 +0200

Am Donnerstag, dem 25.07.2024 um 22:39 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> * gnu/packages/check.scm (klee): Wrap klee-stats.
> ---
>  gnu/packages/check.scm | 12 ++++++++++--
>  1 file changed, 10 insertions(+), 2 deletions(-)
> 
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 412b94569c..3c5ed7a3c3 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -1070,7 +1070,15 @@ (define-public klee
>                            (substitute* "CMakeLists.txt"
>                             
> (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
>                               "${KLEE_UCLIBC_PATH}"))))
> -                      (add-after 'install 'wrap-hooks
> +                      (add-after 'install 'wrap-klee-stats
> +                        (lambda* (#:key outputs #:allow-other-keys)
> +                          (let* ((out (assoc-ref outputs "out"))
> +                                 (bin (string-append out "/bin")))
> +                            (wrap-program (string-append bin "/klee-
> stats")
> +                              `("GUIX_PYTHONPATH" ":" prefix
> +                                ,(search-path-as-string->list
> +                                   (getenv "GUIX_PYTHONPATH")))))))
> +                      (add-after 'install 'wrap-klee
>                          (lambda* (#:key inputs outputs #:allow-
> other-keys)
>                            (let* ((out (assoc-ref outputs "out"))
>                                   (bin (string-append out "/bin"))
Why not consolidate these into a single 'wrap phase?

Cheers

Message #77 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org
Subject: Re: [PATCH v3 3/5] gnu: klee: Only strip bin directory.
Date: Fri, 26 Jul 2024 20:38:31 +0200

Am Donnerstag, dem 25.07.2024 um 22:40 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> This avoid several warnings to be emitted by strip(1) when attempting
> to strip .bca (i.e. LLVM bitcode) files shipped in
> /lib/klee/runtime/.
> 
> * gnu/packages/check.scm (klee): Set #:strip-directories.
> ---
LGTM

Message #80 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106 <at> debbugs.gnu.org
Cc: ludo <at> gnu.org
Subject: Re: [PATCH v3 4/5] gnu: klee: Only build on x86_64 Linux.
Date: Fri, 26 Jul 2024 20:41:38 +0200

Am Donnerstag, dem 25.07.2024 um 22:40 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> * gnu/packages/check.scm (klee): Add supported-systems.
> ---
To recall, i386 does not work?

Message #83 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v4 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
Date: Sat, 27 Jul 2024 11:10:54 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Wrap klee-stats.
---
 gnu/packages/check.scm | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 412b94569c..347bd2e1aa 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1070,12 +1070,17 @@ (define-public klee
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
                              "${KLEE_UCLIBC_PATH}"))))
-                      (add-after 'install 'wrap-hooks
+                      (add-after 'install 'wrap-programs
                         (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).
+                            ;; Ensure that klee-stats finds its Python dependencies.
+                            (wrap-program (string-append bin "/klee-stats")
+                              `("GUIX_PYTHONPATH" ":" prefix
+                                ,(search-path-as-string->list
+                                   (getenv "GUIX_PYTHONPATH"))))
+                            ;; Ensure that klee finds runtime libraries (e.g. uclibc).
                             (wrap-program (string-append bin "/klee")
                               `("KLEE_RUNTIME_LIBRARY_PATH" =
                                 (,(string-append lib "/klee/runtime/"))))))))
@@ -1088,7 +1093,7 @@ (define-public klee
                             (search-input-file %build-inputs "/lib/klee/libc.a"))
              "-DENABLE_POSIX_RUNTIME=ON")))
    (native-inputs (list clang-13 llvm-13 python-lit))
-   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
+   (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
    (build-system cmake-build-system)
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")

base-commit: c6ff1d6ff761af0bd9bac5403fd834f04a14a192

Message #86 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v4 2/5] gnu: klee: Enable the test suite.
Date: Sat, 27 Jul 2024 11:10:55 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Enable all tests.
[arguments]: Patch lit configuration and set #:test-target.
<#:configure-flags?>: Enable system and unit tests, configure gtest.
---
 gnu/packages/check.scm | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 347bd2e1aa..aeaa2e807f 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,13 +1063,22 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases
                       (add-after 'unpack 'patch
                         (lambda _
+                          ;; Allow specification of an absolute full path to uclibc.
                           (substitute* "CMakeLists.txt"
                             (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
-                             "${KLEE_UCLIBC_PATH}"))))
+                             "${KLEE_UCLIBC_PATH}"))
+                          ;; 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')")))))
                       (add-after 'install 'wrap-programs
                         (lambda* (#:key inputs outputs #:allow-other-keys)
                           (let* ((out (assoc-ref outputs "out"))
@@ -1085,7 +1094,13 @@ (define-public klee
                               `("KLEE_RUNTIME_LIBRARY_PATH" =
                                 (,(string-append lib "/klee/runtime/"))))))))
      #:configure-flags
-     #~(list (string-append "-DLLVMCC="
+     #~(list "-DENABLE_UNIT_TESTS=ON"
+             "-DENABLE_SYSTEM_TESTS=ON"
+             (string-append "-DGTEST_SRC_DIR="
+                            #+(package-source googletest))
+             (string-append "-DGTEST_INCLUDE_DIR="
+                            #+(package-source googletest) "/googletest/include")
+             (string-append "-DLLVMCC="
                             (search-input-file %build-inputs "/bin/clang"))
              (string-append "-DLLVMCXX="
                             (search-input-file %build-inputs "/bin/clang++"))

Message #89 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v4 3/5] gnu: klee: Only strip bin directory.
Date: Sat, 27 Jul 2024 11:10:56 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

This avoid several warnings to be emitted by strip(1) when attempting
to strip .bca (i.e. LLVM bitcode) files shipped in /lib/klee/runtime/.

* gnu/packages/check.scm (klee): Set #:strip-directories.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index aeaa2e807f..250206886f 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1063,6 +1063,7 @@ (define-public klee
       (base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
    (arguments
     (list
+     #:strip-directories #~(list "bin") ;don't strip LLVM bitcode in /lib
      #:test-target "check"
      #:phases
      #~(modify-phases %standard-phases

Message #92 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v4 4/5] gnu: klee: Only build on x86_64 Linux.
Date: Sat, 27 Jul 2024 11:10:57 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee): Add supported-systems.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 250206886f..ae3ec90944 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1111,6 +1111,7 @@ (define-public klee
    (native-inputs (list clang-13 llvm-13 python-lit))
    (inputs (list bash-minimal klee-uclibc gperftools sqlite z3 python python-tabulate))
    (build-system cmake-build-system)
+   (supported-systems '("x86_64-linux"))
    (home-page "https://klee-se.org/")
    (synopsis "Symbolic execution engine")
    (description "KLEE is a symbolic virtual machine built on top of the LLVM

Message #95 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: soeren <at> soeren-tempel.net
To: 72106 <at> debbugs.gnu.org
Cc: liliana.prikler <at> gmail.com
Subject: [PATCH v4 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
Date: Sat, 27 Jul 2024 11:10:58 +0200

From: Sören Tempel <soeren <at> soeren-tempel.net>

* gnu/packages/check.scm (klee-uclibc): Add supported-systems.
---
 gnu/packages/check.scm | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index ae3ec90944..b8fbe3f6a8 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1006,6 +1006,7 @@ (define-public klee-uclibc
          (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
          #:strip-directories '() ;only ships a static library, so don't strip anything.

Message #98 received at 72106 <at> debbugs.gnu.org (full text, mbox):

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 72106 <at> debbugs.gnu.org
Subject: Re: [PATCH v3 4/5] gnu: klee: Only build on x86_64 Linux.
Date: Sat, 27 Jul 2024 11:13:57 +0200

Liliana Marie Prikler <liliana.prikler <at> gmail.com> wrote:
> To recall, i386 does not work?

Yes, i386 does not work as KLEE assumes a 64-bit pointer representation.

Liliana Marie Prikler <liliana.prikler <at> gmail.com> wrote:
> Why not consolidate these into a single 'wrap phase?

Good idea, I consolidated everything into a single 'wrap phase.
Additionally, I also consolidated the patching into a single
'patch phase.

Best,
Sören

Message #103 received at 72106-done <at> debbugs.gnu.org (full text, mbox):

From: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
To: soeren <at> soeren-tempel.net, 72106-done <at> debbugs.gnu.org
Subject: Re: [PATCH v4 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
Date: Sat, 27 Jul 2024 19:28:27 +0200

Am Samstag, dem 27.07.2024 um 11:10 +0200 schrieb
soeren <at> soeren-tempel.net:
> From: Sören Tempel <soeren <at> soeren-tempel.net>
> 
> * gnu/packages/check.scm (klee-uclibc): Add supported-systems.
> ---
Pushed as 46a64c7fdd057283063aae6df058579bb07c4b6a.

Cheers

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.