[bug#71925,2/2] gnu: klee: Build with klee-uclibc support.

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(-)
  

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
  

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
  

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
  

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
  

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
  

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
  

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
  

Liliana Marie Prikler <liliana.prikler@gmail.com> wrote:
> v2's klee-uclibc appears to still install libc.a in /lib rather than
> /klee/lib –

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

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

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

[1]: https://issues.guix.gnu.org/71925#10
[2]: https://github.com/klee/klee/blob/v3.1/CMakeLists.txt#L487