* [bug#71925] [PATCH 1/2] gnu: Add klee-uclibc.
2024-07-03 19:03 [bug#71925] [PATCH 0/2] Add klee-uclibc soeren
@ 2024-07-03 19:09 ` soeren
2024-07-06 18:50 ` Liliana Marie Prikler
2024-07-03 19:09 ` [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support soeren
` (4 subsequent siblings)
5 siblings, 1 reply; 19+ messages in thread
From: soeren @ 2024-07-03 19:09 UTC (permalink / raw)
To: 71925; +Cc: julien, liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee-uclibc): New variable.
---
gnu/packages/check.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..35e26ba6da 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#:use-module (gnu packages guile)
#:use-module (gnu packages guile-xyz)
#:use-module (gnu packages maths)
+ #:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(define-public klee-uclibc
+ (let ((commit "955d502cc1f0688e82348304b053ad787056c754"))
+ (package
+ (name "klee-uclibc")
+ (version (git-version "20230612" "0" commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/klee/klee-uclibc")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #:phases (modify-phases %standard-phases
+ ;; Disable locales as these would have to be downloaded and
+ ;; shouldn't really be needed for symbolic execution either.
+ (add-after 'unpack 'patch-config
+ (lambda _
+ (substitute* "klee-premade-configs/x86_64/config"
+ (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_HAS_LOCALE=y")
+ "UCLIBC_HAS_LOCALE=n")
+ (("UCLIBC_HAS_XLOCALE=y")
+ "UCLIBC_HAS_XLOCALE=n"))))
+
+ ;; Upstream uses a custom non-GNU configure script written
+ ;; in Python, replace the default configure phase accordingly.
+ (replace 'configure
+ (lambda _
+ (invoke "./configure" "--make-llvm-lib"
+ "--enable-release")))
+
+ ;; Custom install phase to only install the libc.a file manually.
+ ;; This is the only file which is used/needed by KLEE itself.
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (install-file "lib/libc.a"
+ (string-append (assoc-ref outputs "out")
+ "/lib")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-13 python ncurses))
+ (synopsis "Variant of uClibc tailored to symbolic execution")
+ (description
+ "Modified version of uClibc for symbolic execution of
+Unix userland software. This library can only be used in conjunction
+with the @code{klee} package.")
+ (home-page "https://klee-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 1/2] gnu: Add klee-uclibc.
2024-07-03 19:09 ` [bug#71925] [PATCH 1/2] gnu: " soeren
@ 2024-07-06 18:50 ` Liliana Marie Prikler
0 siblings, 0 replies; 19+ messages in thread
From: Liliana Marie Prikler @ 2024-07-06 18:50 UTC (permalink / raw)
To: soeren, 71925; +Cc: julien
Am Mittwoch, dem 03.07.2024 um 21:09 +0200 schrieb
soeren@soeren-tempel.net:
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee-uclibc): New variable.
> ---
> gnu/packages/check.scm | 58
> ++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 58 insertions(+)
>
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 550a5d0f1d..35e26ba6da 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -87,6 +87,7 @@ (define-module (gnu packages check)
> #:use-module (gnu packages guile)
> #:use-module (gnu packages guile-xyz)
> #:use-module (gnu packages maths)
> + #:use-module (gnu packages ncurses)
> #:use-module (gnu packages perl)
> #:use-module (gnu packages pkg-config)
> #:use-module (gnu packages python)
> @@ -989,6 +990,63 @@ (define-public greatest
> runner. It is quite unopinionated with most of its features being
> optional.")
> (license license:isc)))
>
> +(define-public klee-uclibc
> + (let ((commit "955d502cc1f0688e82348304b053ad787056c754"))
> + (package
> + (name "klee-uclibc")
> + (version (git-version "20230612" "0" commit))
> + (source
> + (origin
> + (method git-fetch)
> + (uri (git-reference
> + (url "https://github.com/klee/klee-uclibc")
> + (commit commit)))
> + (file-name (git-file-name name version))
> + (sha256
> + (base32
> "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"))))
> + (build-system gnu-build-system)
> + (arguments
> + `(#:tests? #f ;upstream uClibc tests do not work in the fork
> + #:strip-directories '() ;only ships a static library, so
> don't strip anything.
> + #:phases (modify-phases %standard-phases
> + ;; Disable locales as these would have to be
> downloaded and
> + ;; shouldn't really be needed for symbolic
> execution either.
> + (add-after 'unpack 'patch-config
> + (lambda _
> + (substitute* "klee-premade-
> configs/x86_64/config"
> +
> (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y")
> +
> "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n")
> + (("UCLIBC_PREGENERATED_LOCALE_DATA=y")
> + "UCLIBC_PREGENERATED_LOCALE_DATA=n")
> + (("UCLIBC_HAS_LOCALE=y")
> + "UCLIBC_HAS_LOCALE=n")
> + (("UCLIBC_HAS_XLOCALE=y")
> + "UCLIBC_HAS_XLOCALE=n"))))
> +
> + ;; Upstream uses a custom non-GNU configure
> script written
> + ;; in Python, replace the default configure
> phase accordingly.
> + (replace 'configure
> + (lambda _
> + (invoke "./configure" "--make-llvm-lib"
> + "--enable-release")))
> +
> + ;; Custom install phase to only install the
> libc.a file manually.
> + ;; This is the only file which is used/needed by
> KLEE itself.
> + (replace 'install
> + (lambda* (#:key outputs #:allow-other-keys)
> + (install-file "lib/libc.a"
> + (string-append (assoc-ref
> outputs "out")
> + "/lib")))))))
> + ;; ncurses is only needed for the `make menuconfig` interface.
> + (native-inputs (list clang-13 llvm-13 python ncurses))
> + (synopsis "Variant of uClibc tailored to symbolic execution")
> + (description
> + "Modified version of uClibc for symbolic execution of
> +Unix userland software. This library can only be used in
> conjunction
> +with the @code{klee} package.")
> + (home-page "https://klee-se.org/")
> + (license license:lgpl2.1))))
Is this only distributed as an .a file or could we make a .so out of
it?
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-03 19:03 [bug#71925] [PATCH 0/2] Add klee-uclibc soeren
2024-07-03 19:09 ` [bug#71925] [PATCH 1/2] gnu: " soeren
@ 2024-07-03 19:09 ` soeren
2024-07-06 18:49 ` Liliana Marie Prikler
2024-07-07 17:26 ` [bug#71925] [PATCH v2 1/2] gnu: Add klee-uclibc soeren
` (3 subsequent siblings)
5 siblings, 1 reply; 19+ messages in thread
From: soeren @ 2024-07-03 19:09 UTC (permalink / raw)
To: 71925; +Cc: julien, liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee): Use klee-uclibc.
---
gnu/packages/check.scm | 17 +++++++++++++++--
1 file changed, 15 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 35e26ba6da..ad589f6e15 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1062,13 +1062,26 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" ":" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ "-DENABLE_POSIX_RUNTIME=ON"
+ (string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc))))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-03 19:09 ` [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support soeren
@ 2024-07-06 18:49 ` Liliana Marie Prikler
2024-07-07 11:24 ` Sören Tempel
0 siblings, 1 reply; 19+ messages in thread
From: Liliana Marie Prikler @ 2024-07-06 18:49 UTC (permalink / raw)
To: soeren, 71925; +Cc: julien
Am Mittwoch, dem 03.07.2024 um 21:09 +0200 schrieb
soeren@soeren-tempel.net:
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> * gnu/packages/check.scm (klee): Use klee-uclibc.
> ---
> gnu/packages/check.scm | 17 +++++++++++++++--
> 1 file changed, 15 insertions(+), 2 deletions(-)
>
> diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
> index 35e26ba6da..ad589f6e15 100644
> --- a/gnu/packages/check.scm
> +++ b/gnu/packages/check.scm
> @@ -1062,13 +1062,26 @@ (define-public klee
> (base32
> "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
> (arguments
> (list
> + #:phases
> + #~(modify-phases %standard-phases
> + (add-after 'install 'wrap-hooks
> + (lambda* (#:key inputs outputs #:allow-
> other-keys)
> + (let* ((out (assoc-ref outputs "out"))
> + (bin (string-append out "/bin"))
> + (lib (string-append out "/lib")))
> + ;; Ensure that KLEE finds runtime
> libraries (e.g. uclibc).
> + (wrap-program (string-append bin
> "/klee")
> + `("KLEE_RUNTIME_LIBRARY_PATH" ":" =
> + (,(string-append lib
> "/klee/runtime/"))))))))
The leading colon is pointless here, since you're doing an "=" assign.
More importantly, can we make this a search path?
> #:configure-flags
> #~(list (string-append "-DLLVMCC="
> (search-input-file %build-inputs
> "/bin/clang"))
> (string-append "-DLLVMCXX="
> - (search-input-file %build-inputs
> "/bin/clang++")))))
> + (search-input-file %build-inputs
> "/bin/clang++"))
> + "-DENABLE_POSIX_RUNTIME=ON"
> + (string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc))))
Can we use search-input-file for this and dirname our way up?
> (native-inputs (list clang-13 llvm-13 python-lit))
> - (inputs (list gperftools sqlite z3))
> + (inputs (list bash-minimal gperftools sqlite z3))
> (build-system cmake-build-system)
> (home-page "https://klee-se.org/")
> (synopsis "Symbolic execution engine")
Cheers
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-06 18:49 ` Liliana Marie Prikler
@ 2024-07-07 11:24 ` Sören Tempel
2024-07-07 12:51 ` Liliana Marie Prikler
0 siblings, 1 reply; 19+ messages in thread
From: Sören Tempel @ 2024-07-07 11:24 UTC (permalink / raw)
To: Liliana Marie Prikler; +Cc: julien, 71925
Hi Liliana,
Thanks a lot for the quick feedback, responses below.
Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> The leading colon is pointless here, since you're doing an "=" assign.
Good catch! I can fix this in a patch revision.
> More importantly, can we make this a search path?
I don't think so as it's not a colon separated search path, it can only
point to a single directory; hence, I assumed that wrap-program is more
appropriate here.
> Can we use search-input-file for this and dirname our way up?
The input file that we are looking for here is called libc.a, I am not
sure what the benefit of using search-input-file is, but I personally
think something along the lines of `(dirname (search-input-file
%build-inputs "/lib/libc.a"))` is less readable then `#$klee-uclibc` but
I can definitely change this if you want me to :)
> Is this only distributed as an .a file or could we make a .so out of
> it?
This is only distributed as a .a, not as a shared object. In fact, KLEE
also doesn't not link against this library at all and instead converts
it to an LLVM .bca file (shipped in /lib/klee/runtime/klee-uclibc.bca)
during build. This file is then used directly by KLEE's symbolic LLVM
interpreter to execute code utilizing libc functions. Hence, klee-uclibc
is also not a propagated input for the klee package.
Let me know if I should send a revision, would love to get this merged.
Greetings
Sören
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 11:24 ` Sören Tempel
@ 2024-07-07 12:51 ` Liliana Marie Prikler
2024-07-07 16:50 ` Sören Tempel
0 siblings, 1 reply; 19+ messages in thread
From: Liliana Marie Prikler @ 2024-07-07 12:51 UTC (permalink / raw)
To: Sören Tempel; +Cc: julien, 71925
Am Sonntag, dem 07.07.2024 um 13:24 +0200 schrieb Sören Tempel:
> Hi Liliana,
>
> Thanks a lot for the quick feedback, responses below.
>
> Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> > The leading colon is pointless here, since you're doing an "="
> > assign.
>
> Good catch! I can fix this in a patch revision.
>
> > More importantly, can we make this a search path?
>
> I don't think so as it's not a colon separated search path, it can
> only point to a single directory; hence, I assumed that wrap-program
> is more appropriate here.
Fair enough.
> > Can we use search-input-file for this and dirname our way up?
>
> The input file that we are looking for here is called libc.a, I am
> not
> sure what the benefit of using search-input-file is, but I personally
> think something along the lines of `(dirname (search-input-file
> %build-inputs "/lib/libc.a"))` is less readable then `#$klee-uclibc`
> but I can definitely change this if you want me to :)
>
> > Is this only distributed as an .a file or could we make a .so out
> > of it?
>
> This is only distributed as a .a, not as a shared object. In fact,
> KLEE also doesn't not link against this library at all and instead
> converts it to an LLVM .bca file (shipped in
> /lib/klee/runtime/klee-uclibc.bca)
> during build. This file is then used directly by KLEE's symbolic LLVM
> interpreter to execute code utilizing libc functions. Hence, klee-
> uclibc is also not a propagated input for the klee package.
>
> Let me know if I should send a revision, would love to get this
> merged.
Can we make it so that it uses the file directly instead of inferring
the name? Then we could install klee-uclibc to, say
"/lib/klee/uclibc.a" and reference it in this build by said file name.
Cheers
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 12:51 ` Liliana Marie Prikler
@ 2024-07-07 16:50 ` Sören Tempel
2024-07-07 16:53 ` Liliana Marie Prikler
0 siblings, 1 reply; 19+ messages in thread
From: Sören Tempel @ 2024-07-07 16:50 UTC (permalink / raw)
To: Liliana Marie Prikler; +Cc: julien, 71925
Hello!
Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> Can we make it so that it uses the file directly instead of inferring
> the name? Then we could install klee-uclibc to, say
> "/lib/klee/uclibc.a" and reference it in this build by said file name.
That would require us to patch KLEE's CMakeLists.txt and I am not sure
if that's worth it [1]. I think I would personally prefer using
search-input-file and dirname then. However, I am also still somewhat
new to Guix, could you elaborate what the problem with using
`(string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc)` is (for the sake
of expanding my understanding of Guix in this regard)?
Greetings,
Sören
[1]: https://github.com/klee/klee/blob/v3.1/CMakeLists.txt#L480-L501
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 16:50 ` Sören Tempel
@ 2024-07-07 16:53 ` Liliana Marie Prikler
2024-07-07 17:28 ` Sören Tempel
0 siblings, 1 reply; 19+ messages in thread
From: Liliana Marie Prikler @ 2024-07-07 16:53 UTC (permalink / raw)
To: Sören Tempel; +Cc: julien, 71925
Am Sonntag, dem 07.07.2024 um 18:50 +0200 schrieb Sören Tempel:
> Hello!
>
> Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> > Can we make it so that it uses the file directly instead of
> > inferring the name? Then we could install klee-uclibc to, say
> > "/lib/klee/uclibc.a" and reference it in this build by said file
> > name.
>
> That would require us to patch KLEE's CMakeLists.txt and I am not
> sure if that's worth it [1]. I think I would personally prefer using
> search-input-file and dirname then. However, I am also still somewhat
> new to Guix, could you elaborate what the problem with using
> `(string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc)` is (for the
> sake of expanding my understanding of Guix in this regard)?
Well, the question is mainly what people ought to do to swap out klee-
uclibc from their builds – e.g. if they want to replace it with a newer
one etc. Inputs are our means of making sure that people have a handle
for this kind of thing.
Cheers
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 16:53 ` Liliana Marie Prikler
@ 2024-07-07 17:28 ` Sören Tempel
2024-07-07 18:27 ` Liliana Marie Prikler
0 siblings, 1 reply; 19+ messages in thread
From: Sören Tempel @ 2024-07-07 17:28 UTC (permalink / raw)
To: Liliana Marie Prikler; +Cc: julien, 71925
Hello again!
Thanks for the explanation, I send a v2 revision which (hopefully)
addresses your feedback. I have opted to install the libc.a file
to /klee/lib/libc.a this way, it's compatible with search-inputs
without requiring us to patch KLEE's build system.
Let me know what you think :)
Best,
Sören
Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> Am Sonntag, dem 07.07.2024 um 18:50 +0200 schrieb Sören Tempel:
> > Hello!
> >
> > Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> > > Can we make it so that it uses the file directly instead of
> > > inferring the name? Then we could install klee-uclibc to, say
> > > "/lib/klee/uclibc.a" and reference it in this build by said file
> > > name.
> >
> > That would require us to patch KLEE's CMakeLists.txt and I am not
> > sure if that's worth it [1]. I think I would personally prefer using
> > search-input-file and dirname then. However, I am also still somewhat
> > new to Guix, could you elaborate what the problem with using
> > `(string-append "-DKLEE_UCLIBC_PATH=" #$klee-uclibc)` is (for the
> > sake of expanding my understanding of Guix in this regard)?
> Well, the question is mainly what people ought to do to swap out klee-
> uclibc from their builds – e.g. if they want to replace it with a newer
> one etc. Inputs are our means of making sure that people have a handle
> for this kind of thing.
>
> Cheers
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 17:28 ` Sören Tempel
@ 2024-07-07 18:27 ` Liliana Marie Prikler
2024-07-07 19:18 ` Sören Tempel
0 siblings, 1 reply; 19+ messages in thread
From: Liliana Marie Prikler @ 2024-07-07 18:27 UTC (permalink / raw)
To: Sören Tempel; +Cc: julien, 71925
Am Sonntag, dem 07.07.2024 um 19:28 +0200 schrieb Sören Tempel:
> Hello again!
>
> Thanks for the explanation, I send a v2 revision which (hopefully)
> addresses your feedback. I have opted to install the libc.a file
> to /klee/lib/libc.a this way, it's compatible with search-inputs
> without requiring us to patch KLEE's build system.
v2's klee-uclibc appears to still install libc.a in /lib rather than
/klee/lib – do you want it do be this way around or would /lib/klee/
(honouring FHS) be smarter?
Cheers
^ permalink raw reply [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH v2 1/2] gnu: Add klee-uclibc.
2024-07-03 19:03 [bug#71925] [PATCH 0/2] Add klee-uclibc soeren
2024-07-03 19:09 ` [bug#71925] [PATCH 1/2] gnu: " soeren
2024-07-03 19:09 ` [bug#71925] [PATCH 2/2] gnu: klee: Build with klee-uclibc support soeren
@ 2024-07-07 17:26 ` soeren
2024-07-07 17:26 ` [bug#71925] [PATCH v2 2/2] gnu: klee: Build with klee-uclibc support soeren
2024-07-07 19:19 ` [bug#71925] [PATCH v3 1/2] gnu: Add klee-uclibc soeren
` (2 subsequent siblings)
5 siblings, 1 reply; 19+ messages in thread
From: soeren @ 2024-07-07 17:26 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee-uclibc): New variable.
---
gnu/packages/check.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..35e26ba6da 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#:use-module (gnu packages guile)
#:use-module (gnu packages guile-xyz)
#:use-module (gnu packages maths)
+ #:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(define-public klee-uclibc
+ (let ((commit "955d502cc1f0688e82348304b053ad787056c754"))
+ (package
+ (name "klee-uclibc")
+ (version (git-version "20230612" "0" commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/klee/klee-uclibc")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #:phases (modify-phases %standard-phases
+ ;; Disable locales as these would have to be downloaded and
+ ;; shouldn't really be needed for symbolic execution either.
+ (add-after 'unpack 'patch-config
+ (lambda _
+ (substitute* "klee-premade-configs/x86_64/config"
+ (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_HAS_LOCALE=y")
+ "UCLIBC_HAS_LOCALE=n")
+ (("UCLIBC_HAS_XLOCALE=y")
+ "UCLIBC_HAS_XLOCALE=n"))))
+
+ ;; Upstream uses a custom non-GNU configure script written
+ ;; in Python, replace the default configure phase accordingly.
+ (replace 'configure
+ (lambda _
+ (invoke "./configure" "--make-llvm-lib"
+ "--enable-release")))
+
+ ;; Custom install phase to only install the libc.a file manually.
+ ;; This is the only file which is used/needed by KLEE itself.
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (install-file "lib/libc.a"
+ (string-append (assoc-ref outputs "out")
+ "/lib")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-13 python ncurses))
+ (synopsis "Variant of uClibc tailored to symbolic execution")
+ (description
+ "Modified version of uClibc for symbolic execution of
+Unix userland software. This library can only be used in conjunction
+with the @code{klee} package.")
+ (home-page "https://klee-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")
base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH v2 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 17:26 ` [bug#71925] [PATCH v2 1/2] gnu: Add klee-uclibc soeren
@ 2024-07-07 17:26 ` soeren
0 siblings, 0 replies; 19+ messages in thread
From: soeren @ 2024-07-07 17:26 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee): Use klee-uclibc.
---
gnu/packages/check.scm | 21 ++++++++++++++++++---
1 file changed, 18 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 35e26ba6da..52941681a9 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1036,7 +1036,7 @@ (define-public klee-uclibc
(lambda* (#:key outputs #:allow-other-keys)
(install-file "lib/libc.a"
(string-append (assoc-ref outputs "out")
- "/lib")))))))
+ "/klee/lib")))))))
;; ncurses is only needed for the `make menuconfig` interface.
(native-inputs (list clang-13 llvm-13 python ncurses))
(synopsis "Variant of uClibc tailored to symbolic execution")
@@ -1062,13 +1062,28 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ (string-append "-DKLEE_UCLIBC_PATH="
+ (let ((uclibc (search-input-file %build-inputs "/klee/lib/libc.a")))
+ (dirname (dirname uclibc))))
+ "-DENABLE_POSIX_RUNTIME=ON")))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH v3 1/2] gnu: Add klee-uclibc.
2024-07-03 19:03 [bug#71925] [PATCH 0/2] Add klee-uclibc soeren
` (2 preceding siblings ...)
2024-07-07 17:26 ` [bug#71925] [PATCH v2 1/2] gnu: Add klee-uclibc soeren
@ 2024-07-07 19:19 ` soeren
2024-07-07 19:19 ` [bug#71925] [PATCH v3 2/2] gnu: klee: Build with klee-uclibc support soeren
2024-07-08 7:44 ` [bug#71925] [PATCH v4 1/2] gnu: Add klee-uclibc soeren
2024-07-08 8:47 ` [bug#71925] [PATCH 0/2] Add klee-uclibc Sören Tempel
5 siblings, 1 reply; 19+ messages in thread
From: soeren @ 2024-07-07 19:19 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee-uclibc): New variable.
---
gnu/packages/check.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..c4bae49165 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#:use-module (gnu packages guile)
#:use-module (gnu packages guile-xyz)
#:use-module (gnu packages maths)
+ #:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(define-public klee-uclibc
+ (let ((commit "955d502cc1f0688e82348304b053ad787056c754"))
+ (package
+ (name "klee-uclibc")
+ (version (git-version "20230612" "0" commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/klee/klee-uclibc")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #:phases (modify-phases %standard-phases
+ ;; Disable locales as these would have to be downloaded and
+ ;; shouldn't really be needed for symbolic execution either.
+ (add-after 'unpack 'patch-config
+ (lambda _
+ (substitute* "klee-premade-configs/x86_64/config"
+ (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_HAS_LOCALE=y")
+ "UCLIBC_HAS_LOCALE=n")
+ (("UCLIBC_HAS_XLOCALE=y")
+ "UCLIBC_HAS_XLOCALE=n"))))
+
+ ;; Upstream uses a custom non-GNU configure script written
+ ;; in Python, replace the default configure phase accordingly.
+ (replace 'configure
+ (lambda _
+ (invoke "./configure" "--make-llvm-lib"
+ "--enable-release")))
+
+ ;; Custom install phase to only install the libc.a file manually.
+ ;; This is the only file which is used/needed by KLEE itself.
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (install-file "lib/libc.a"
+ (string-append (assoc-ref outputs "out")
+ "/klee/lib")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-13 python ncurses))
+ (synopsis "Variant of uClibc tailored to symbolic execution")
+ (description
+ "Modified version of uClibc for symbolic execution of
+Unix userland software. This library can only be used in conjunction
+with the @code{klee} package.")
+ (home-page "https://klee-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")
base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH v3 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-07 19:19 ` [bug#71925] [PATCH v3 1/2] gnu: Add klee-uclibc soeren
@ 2024-07-07 19:19 ` soeren
0 siblings, 0 replies; 19+ messages in thread
From: soeren @ 2024-07-07 19:19 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee): Use klee-uclibc.
---
gnu/packages/check.scm | 19 +++++++++++++++++--
1 file changed, 17 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index c4bae49165..52941681a9 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1062,13 +1062,28 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ (string-append "-DKLEE_UCLIBC_PATH="
+ (let ((uclibc (search-input-file %build-inputs "/klee/lib/libc.a")))
+ (dirname (dirname uclibc))))
+ "-DENABLE_POSIX_RUNTIME=ON")))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH v4 1/2] gnu: Add klee-uclibc.
2024-07-03 19:03 [bug#71925] [PATCH 0/2] Add klee-uclibc soeren
` (3 preceding siblings ...)
2024-07-07 19:19 ` [bug#71925] [PATCH v3 1/2] gnu: Add klee-uclibc soeren
@ 2024-07-08 7:44 ` soeren
2024-07-08 7:44 ` [bug#71925] [PATCH v4 2/2] gnu: klee: Build with klee-uclibc support soeren
2024-07-08 8:47 ` [bug#71925] [PATCH 0/2] Add klee-uclibc Sören Tempel
5 siblings, 1 reply; 19+ messages in thread
From: soeren @ 2024-07-08 7:44 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee-uclibc): New variable.
---
Changes since v3: Move klee-uclibc library to `/lib/klee/libc.a`.
gnu/packages/check.scm | 58 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 58 insertions(+)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index 550a5d0f1d..e02dc1b23d 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -87,6 +87,7 @@ (define-module (gnu packages check)
#:use-module (gnu packages guile)
#:use-module (gnu packages guile-xyz)
#:use-module (gnu packages maths)
+ #:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
#:use-module (gnu packages pkg-config)
#:use-module (gnu packages python)
@@ -989,6 +990,63 @@ (define-public greatest
runner. It is quite unopinionated with most of its features being optional.")
(license license:isc)))
+(define-public klee-uclibc
+ (let ((commit "955d502cc1f0688e82348304b053ad787056c754"))
+ (package
+ (name "klee-uclibc")
+ (version (git-version "20230612" "0" commit))
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/klee/klee-uclibc")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f ;upstream uClibc tests do not work in the fork
+ #:strip-directories '() ;only ships a static library, so don't strip anything.
+ #:phases (modify-phases %standard-phases
+ ;; Disable locales as these would have to be downloaded and
+ ;; shouldn't really be needed for symbolic execution either.
+ (add-after 'unpack 'patch-config
+ (lambda _
+ (substitute* "klee-premade-configs/x86_64/config"
+ (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_PREGENERATED_LOCALE_DATA=y")
+ "UCLIBC_PREGENERATED_LOCALE_DATA=n")
+ (("UCLIBC_HAS_LOCALE=y")
+ "UCLIBC_HAS_LOCALE=n")
+ (("UCLIBC_HAS_XLOCALE=y")
+ "UCLIBC_HAS_XLOCALE=n"))))
+
+ ;; Upstream uses a custom non-GNU configure script written
+ ;; in Python, replace the default configure phase accordingly.
+ (replace 'configure
+ (lambda _
+ (invoke "./configure" "--make-llvm-lib"
+ "--enable-release")))
+
+ ;; Custom install phase to only install the libc.a file manually.
+ ;; This is the only file which is used/needed by KLEE itself.
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (install-file "lib/libc.a"
+ (string-append (assoc-ref outputs "out")
+ "/lib/klee")))))))
+ ;; ncurses is only needed for the `make menuconfig` interface.
+ (native-inputs (list clang-13 llvm-13 python ncurses))
+ (synopsis "Variant of uClibc tailored to symbolic execution")
+ (description
+ "Modified version of uClibc for symbolic execution of
+Unix userland software. This library can only be used in conjunction
+with the @code{klee} package.")
+ (home-page "https://klee-se.org/")
+ (license license:lgpl2.1))))
+
(define-public klee
(package
(name "klee")
base-commit: bab73e413b3421f4aa051e9438d147040a52e1be
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH v4 2/2] gnu: klee: Build with klee-uclibc support.
2024-07-08 7:44 ` [bug#71925] [PATCH v4 1/2] gnu: Add klee-uclibc soeren
@ 2024-07-08 7:44 ` soeren
0 siblings, 0 replies; 19+ messages in thread
From: soeren @ 2024-07-08 7:44 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
From: Sören Tempel <soeren@soeren-tempel.net>
* gnu/packages/check.scm (klee): Use klee-uclibc.
---
Changes since v3: Move klee-uclibc library to `/lib/klee/libc.a`.
gnu/packages/check.scm | 23 +++++++++++++++++++++--
1 file changed, 21 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm
index e02dc1b23d..c4eaaef18f 100644
--- a/gnu/packages/check.scm
+++ b/gnu/packages/check.scm
@@ -1062,13 +1062,32 @@ (define-public klee
(base32 "1nma6dqi8chjb97llsa8mzyskgsg4dx56lm8j514j5wmr8vkafz6"))))
(arguments
(list
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'patch
+ (lambda _
+ (substitute* "CMakeLists.txt"
+ (("\\$\\{KLEE_UCLIBC_PATH\\}/lib/libc\\.a")
+ "${KLEE_UCLIBC_PATH}"))))
+ (add-after 'install 'wrap-hooks
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin"))
+ (lib (string-append out "/lib")))
+ ;; Ensure that KLEE finds runtime libraries (e.g. uclibc).
+ (wrap-program (string-append bin "/klee")
+ `("KLEE_RUNTIME_LIBRARY_PATH" =
+ (,(string-append lib "/klee/runtime/"))))))))
#:configure-flags
#~(list (string-append "-DLLVMCC="
(search-input-file %build-inputs "/bin/clang"))
(string-append "-DLLVMCXX="
- (search-input-file %build-inputs "/bin/clang++")))))
+ (search-input-file %build-inputs "/bin/clang++"))
+ (string-append "-DKLEE_UCLIBC_PATH="
+ (search-input-file %build-inputs "/lib/klee/libc.a"))
+ "-DENABLE_POSIX_RUNTIME=ON")))
(native-inputs (list clang-13 llvm-13 python-lit))
- (inputs (list gperftools sqlite z3))
+ (inputs (list bash-minimal klee-uclibc gperftools sqlite z3))
(build-system cmake-build-system)
(home-page "https://klee-se.org/")
(synopsis "Symbolic execution engine")
^ permalink raw reply related [flat|nested] 19+ messages in thread
* [bug#71925] [PATCH 0/2] Add klee-uclibc.
2024-07-03 19:03 [bug#71925] [PATCH 0/2] Add klee-uclibc soeren
` (4 preceding siblings ...)
2024-07-08 7:44 ` [bug#71925] [PATCH v4 1/2] gnu: Add klee-uclibc soeren
@ 2024-07-08 8:47 ` Sören Tempel
5 siblings, 0 replies; 19+ messages in thread
From: Sören Tempel @ 2024-07-08 8:47 UTC (permalink / raw)
To: 71925; +Cc: liliana.prikler
Hello,
I just send a v4 which moves the library file from /klee/lib/libc.a to
/lib/klee/libc.a. I tested this a bit and it sees to work fine. From my
point of view, the only problem that remains is that KLEE only really
supports x86_64; hence, the build fails on aarch64 [1].
In #68296, I therefore added `(supported-systems '("x86_64-linux"))` but
this wasn't included in #71634. Should I re-add that here or do we want
to do that separately?
Best,
Sören
[1]: https://github.com/klee/klee/issues/1670#issuecomment-1959595283
^ permalink raw reply [flat|nested] 19+ messages in thread