GNU bug report logs - #68296
[PATCH] gnu: Add KLEE.

Previous Next

Full log

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

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 68296 <at> debbugs.gnu.org, guix-patches <at> gnu.org
Subject: Re: [bug#68296] [PATCH] gnu: Add KLEE.
Date: Tue, 13 Feb 2024 15:09:12 +0100

Hi Julien,

Thanks a lot for your feedback! I send an updated revision of the
patchset based on your feedback. More information on changes below.

Julien Lepiller <julien <at> lepiller.eu> wrote:
> First, could you separate this in two patches, one per package?

Sorry, oversight on my part. Fixed!

> Is there a reason why this is limited to the x86_64 architecture?

Yes, despite operating on LLVM IR abstraction, KLEE is tightly
integrated with the host architecture. Therefore, upstream currently
only support x86_64. Packages for other package manager (e.g. Nix)
also only support KLEE on x86_64 [1].

I added a comment explaining this.

> You have mixed native and normal inputs. In uclibc, since python is
> only used for the build, it should be native.

Fixed, ncurses should also be native as it is only used for menuconfig.

> Does it make sense to propagate uclibc in klee, when it only contains
> a static library? Some for clang and llvm. Isn't z3 used at runtime?
> Shouldn't it be propagated?

Sorry, I should have done a better job at explaining this: KLEE is a
symbolic analyzer for LLVM IR. Users of KLEE will need to translate
their C/C++ source to LLVM IR in order to analyze it with KLEE [2].
Furthermore, as KLEE is tightly integrated with a specific LLVM version,
it makes (at least from my point of view) sense to propagate a specific
clang toolchain so users can just run `guix shell klee` and get started
with it. However, if preferred I can also remove the propagation.

z3 isn't used at runtime, KLEE just uses the Z3 library interface and
links against z3. AFAIK, it doesn't use any binaries from z3. Does z3
still need to be propagated in this case?

uclibc does not need to be a propagated input since the KLEE build
systems generates LLVM IR from the .a archive [3]. I fixed this.

> Using #$klee-uclibc directly in the phase could be problematic I
> think, you should use this-package-inputs or similar (can't remember
> the exact name or syntax right now, you can leave it to me if you
> don't find it).

Sorry, I am new to Guix so I am not sure what you mean. Let me know if
you have more information on this but also feel free to just adjust this
as you wish :)

Greetings
Sören

[1]: https://github.com/NixOS/nixpkgs/blob/40a7b182e0a00245d69f6b8c1dfd3ea4bfc6257c/pkgs/applications/science/logic/klee/default.nix
[2]: https://klee.github.io/tutorials/testing-function/#compiling-to-llvm-bitcode
[3]: https://github.com/klee/klee/blob/v3.0/CMakeLists.txt#L473-L487

Previous Next

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