[PATCH 0/3] gnu: klee: Enable test suite

  • Done
  • quality assurance status badge
Details
3 participants
  • Liliana Marie Prikler
  • Ludovic Courtès
  • soeren
Owner
unassigned
Submitted by
soeren
Severity
normal
S
S
soeren wrote on 14 Jul 12:36 +0200
(address . guix-patches@gnu.org)(address . liliana.prikler@gmail.com)
cover.1720953093.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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
S
S
soeren wrote on 14 Jul 12:42 +0200
[PATCH 1/3] gnu: klee: Propagate Python dependencies needed by klee-stats.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
2f96e525abd91df6bf774c18e601f497bffa618f.1720953093.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(+)

Toggle diff (13 lines)
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)
S
S
soeren wrote on 14 Jul 12:42 +0200
[PATCH 2/3] gnu: klee: Enable the test suite.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
3628ef5ffdfff900c749131956e3109dbd813493.1720953093.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(-)

Toggle diff (60 lines)
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")
S
S
soeren wrote on 14 Jul 12:42 +0200
[PATCH 3/3] gnu: klee: Only strip bin directory.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
c692edb365bb126a03b27a9bbb63df29726ff8e5.1720953093.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(+)

Toggle diff (12 lines)
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
L
L
Liliana Marie Prikler wrote on 14 Jul 13:43 +0200
Re: [PATCH 1/3] gnu: klee: Propagate Python dependencies needed by klee-stats.
1de2040ef0eb380b20bd893a67428826ec547698.camel@gmail.com
Am Sonntag, dem 14.07.2024 um 12:42 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (6 lines)
> From: Sören Tempel <soeren@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?
L
L
Liliana Marie Prikler wrote on 14 Jul 18:17 +0200
Re: [PATCH 0/3] gnu: klee: Enable test suite
5bc6bc1832077b3153fcb28ed0ef9233411ea69d.camel@gmail.com
Am Sonntag, dem 14.07.2024 um 12:36 +0200 schrieb
soeren@soeren-tempel.net:

Toggle quote (3 lines)
> 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?

Toggle quote (3 lines)
> 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.
S
S
soeren wrote on 14 Jul 20:25 +0200
[PATCH v2 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
3ba31459921293a61ca8933ce7395f4a6d58b559.1720981528.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (32 lines)
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
S
S
soeren wrote on 14 Jul 20:25 +0200
[PATCH v2 2/5] gnu: klee: Enable the test suite.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
b65bd1448a381db7821c51380d549643a0942601.1720981528.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(-)

Toggle diff (61 lines)
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")
S
S
soeren wrote on 14 Jul 20:25 +0200
[PATCH v2 3/5] gnu: klee: Only strip bin directory.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
e3fe86a32c89fa2a8c50a249d32cbcc4a3c6b75e.1720981528.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(+)

Toggle diff (12 lines)
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
S
S
soeren wrote on 14 Jul 20:25 +0200
[PATCH v2 4/5] gnu: klee: Only build on x86_64 Linux.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
a6bff0cfd82df47c3664fecca42a8b0e0d259b68.1720981528.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (12 lines)
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
S
S
soeren wrote on 14 Jul 20:25 +0200
[PATCH v2 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
96e57f4f5fc4ea592923427484333c7dfea55a3c.1720981528.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (12 lines)
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.
S
S
Sören Tempel wrote on 14 Jul 20:29 +0200
Re: [PATCH 0/3] gnu: klee: Enable test suite
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)(address . 72106@debbugs.gnu.org)
2RJBKARQLC2CS.2DWJ8IEINRRAC@8pit.net
Hi Liliana,

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

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (2 lines)
> 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 :)

Toggle quote (6 lines)
> > 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?

Toggle quote (6 lines)
> > 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
L
L
Liliana Marie Prikler wrote on 14 Jul 20:53 +0200
Re: [PATCH v2 2/5] gnu: klee: Enable the test suite.
68c1ee2dec2780cc8d6d5bc0db0f36492236b85c.camel@gmail.com
Am Sonntag, dem 14.07.2024 um 20:25 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (43 lines)
> From: Sören Tempel <soeren@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.
Toggle quote (38 lines)
>                        (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
L
L
Liliana Marie Prikler wrote on 14 Jul 20:54 +0200
Re: [PATCH v2 4/5] gnu: klee: Only build on x86_64 Linux.
270253dd66bbaf388b3e279174f9bacaac434a07.camel@gmail.com
Am Sonntag, dem 14.07.2024 um 20:25 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (20 lines)
> From: Sören Tempel <soeren@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
L
L
Liliana Marie Prikler wrote on 14 Jul 20:54 +0200
Re: [PATCH v2 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
89de2118659f749a31b0f777d9ac4d1f700a4819.camel@gmail.com
Am Sonntag, dem 14.07.2024 um 20:25 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (3 lines)
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee): Add supported-systems.
Should be klee-uclibc.
Toggle quote (18 lines)
> ---
>  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
S
S
Sören Tempel wrote on 14 Jul 22:04 +0200
Re: [PATCH v2 2/5] gnu: klee: Enable the test suite.
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)(address . 72106@debbugs.gnu.org)
39BYRNCZVFJV2.39MMBNJU3FT1T@8pit.net
Hello Liliana,

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (3 lines)
> 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").

Toggle quote (2 lines)
> 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.

Toggle quote (2 lines)
> Should be klee-uclibc.

L
L
Ludovic Courtès wrote on 20 Jul 11:56 +0200
Re: [bug#72106] [PATCH v2 2/5] gnu: klee: Enable the test suite.
(address . soeren@soeren-tempel.net)
87cyn8qtcm.fsf@gnu.org
Hello Sören,

soeren@soeren-tempel.net skribis:

Toggle quote (10 lines)
> (,(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)

Toggle quote (11 lines)
> - (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’.
S
S
soeren wrote on 25 Jul 22:39 +0200
[PATCH v3 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
(address . 72106@debbugs.gnu.org)
da306a33548cc76d5a647bdba7e2cb423f37b1ff.1721940003.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (32 lines)
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
S
S
soeren wrote on 25 Jul 22:40 +0200
[PATCH v3 2/5] gnu: klee: Enable the test suite.
(address . 72106@debbugs.gnu.org)
879a9aeca685352ce048738e127b8ab3cbb58460.1721940003.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(-)

Toggle diff (44 lines)
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++"))
S
S
soeren wrote on 25 Jul 22:40 +0200
[PATCH v3 3/5] gnu: klee: Only strip bin directory.
(address . 72106@debbugs.gnu.org)
4f359d704cbadd3884b16b41a7d4799ed14a2990.1721940003.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(+)

Toggle diff (12 lines)
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
S
S
soeren wrote on 25 Jul 22:40 +0200
[PATCH v3 4/5] gnu: klee: Only build on x86_64 Linux.
(address . 72106@debbugs.gnu.org)
6d51c298a83bcbc8581f229dd7bdb07ccadaf525.1721940003.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (12 lines)
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
S
S
soeren wrote on 25 Jul 22:40 +0200
[PATCH v3 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
(address . 72106@debbugs.gnu.org)
e2ef2adbfb638bcb13700e2a1a6f530cffbe9e16.1721940003.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (12 lines)
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.
S
S
Sören Tempel wrote on 25 Jul 22:43 +0200
Re: [bug#72106] [PATCH v2 2/5] gnu: klee: Enable the test suite.
(name . Ludovic Courtès)(address . ludo@gnu.org)
2U760OLV542OU.37ELTO3E6V5BR@8pit.net
Ludovic Courtès <ludo@gnu.org> wrote:
Toggle quote (2 lines)
> Hello Sören,

Hi Ludo,

Toggle quote (6 lines)
> … 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
L
L
Liliana Marie Prikler wrote on 26 Jul 20:37 +0200
Re: [PATCH v3 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
(address . ludo@gnu.org)
56b8badbe6e918f25aa542b22b26582683c0271f.camel@gmail.com
Am Donnerstag, dem 25.07.2024 um 22:39 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (31 lines)
> From: Sören Tempel <soeren@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
L
L
Liliana Marie Prikler wrote on 26 Jul 20:38 +0200
Re: [PATCH v3 3/5] gnu: klee: Only strip bin directory.
(address . ludo@gnu.org)
79cfa1459d9da25e594f5ff49ebc01232fcc4554.camel@gmail.com
Am Donnerstag, dem 25.07.2024 um 22:40 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (8 lines)
> From: Sören Tempel <soeren@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
L
L
Liliana Marie Prikler wrote on 26 Jul 20:41 +0200
Re: [PATCH v3 4/5] gnu: klee: Only build on x86_64 Linux.
(address . ludo@gnu.org)
9a2d14183cf4e700652b162126b018b246e94ce0.camel@gmail.com
Am Donnerstag, dem 25.07.2024 um 22:40 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (4 lines)
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee): Add supported-systems.
> ---
To recall, i386 does not work?
S
S
soeren wrote on 27 Jul 11:10 +0200
[PATCH v4 1/5] gnu: klee: Wrap klee-stats for Python dependencies.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
bb9ba2aac923eaee9a447bd424d76e2a4013c7a3.1722071458.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (35 lines)
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
S
S
soeren wrote on 27 Jul 11:10 +0200
[PATCH v4 2/5] gnu: klee: Enable the test suite.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
fa4abb7890783400a49a76f9b7f88b7da9861687.1722071458.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(-)

Toggle diff (43 lines)
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++"))
S
S
soeren wrote on 27 Jul 11:10 +0200
[PATCH v4 3/5] gnu: klee: Only strip bin directory.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
8fe1c17fdbaf83b685d95b5717e84d2f23036660.1722071458.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@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(+)

Toggle diff (12 lines)
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
S
S
soeren wrote on 27 Jul 11:10 +0200
[PATCH v4 4/5] gnu: klee: Only build on x86_64 Linux.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
4a6fe96af9b83df4604fbc485eb080da722c7609.1722071458.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (12 lines)
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
S
S
soeren wrote on 27 Jul 11:10 +0200
[PATCH v4 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
(address . 72106@debbugs.gnu.org)(address . liliana.prikler@gmail.com)
219dfd8a2b8f710ccf632c838524a23b77575eca.1722071458.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

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

Toggle diff (12 lines)
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.
S
S
Sören Tempel wrote on 27 Jul 11:13 +0200
Re: [PATCH v3 4/5] gnu: klee: Only build on x86_64 Linux.
(name . Liliana Marie Prikler)(address . liliana.prikler@gmail.com)(address . 72106@debbugs.gnu.org)
2KZX7K5B5F7SC.24V48OE5C6IF8@8pit.net
Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (2 lines)
> To recall, i386 does not work?

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

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
Toggle quote (2 lines)
> 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
L
L
Liliana Marie Prikler wrote on 27 Jul 19:28 +0200
Re: [PATCH v4 5/5] gnu: klee-uclibc: Only build on x86_64 Linux.
65f1753857a6181cfcaf1c44924cd4bfba400fd5.camel@gmail.com
Am Samstag, dem 27.07.2024 um 11:10 +0200 schrieb
soeren@soeren-tempel.net:
Toggle quote (4 lines)
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee-uclibc): Add supported-systems.
> ---
Pushed as 46a64c7fdd057283063aae6df058579bb07c4b6a.

Cheers
Closed
?
Your comment

This issue is archived.

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

To respond to this issue using the mumi CLI, first switch to it
mumi current 72106
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