search

klee / klee-snap

Official snap for KLEE
http://klee.github.io/
MIT License
2 stars 0 forks source link

Missing libkleeRuntimePOSIX64_Debug+Asserts.bca #1

Open mristin opened 7 months ago

mristin commented 7 months ago

Hi! I've just installed klee snap on Ubuntu 22.04 and I receive the following message:

KLEE: NOTE: Using POSIX model: /snap/klee/9/usr/local/lib/klee/runtime/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: ERROR: Loading file /snap/klee/9/usr/local/lib/klee/runtime/libkleeRuntimePOSIX64_Debug+Asserts.bca failed: No such file or directory

... when trying to invoke KLEE on a bitcode with klee --posix-runtime myprogram.bc.

The version used:

$ klee --version
KLEE 3.0 (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: ON)
  Build revision: unknown

Ubuntu LLVM version 13.0.1

  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake

I suspect that klee in the snap has not been built with -DENABLE_POSIX_RUNTIME=ON, see: https://github.com/klee/klee/issues/1475.

marco6 commented 7 months ago

Hi @mristin! Thanks for this report. In this moment the stable channel does not support POSIX runtime and or ulibc/libcxx.

However, I just added support for ulibc and POSIX in the beta channel. libcxx will need to wait a little bit more as I don't have enough time right now.

If you could test that (by switching to the beta channel with snap refresh klee --channel beta and confirm that everything is in place, I could promote that version to the stable channel.

ccadar commented 7 months ago

@marco6 many thanks for your work on this. BTW, I guess you know that we have recently released KLEE 3.1 (on 29 Feb) as well as klee-uclibc 1.4 (on 29 Oct).

marco6 commented 7 months ago

@ccadar I didn't :-) I will try to get the new release up as soon as I have time.

mristin commented 7 months ago

@marco6 thanks! Unfortunately, I couldn't make our code work with KLEE as we rely heavily on smart pointers (std::shared_ptr, std::optional, std::expected). I don't have a working example, and so I can't test.

I suppose it is probably not possible to make these structures symbolically?

marco6 commented 7 months ago

@ccadar I think atomics are implemented, so I guess it's just the lack of libcxx in the snap preventing @mristin to build a working example?

If that's the case I can try to bundle libcxx as soon as I can.

ccadar commented 7 months ago

@mristin is the situation that you can use KLEE for your code when you install it from other sources, but not as a snap? Otherwise, and if you need help with your scenario, you should send a message to the KLEE mailing list with a small example illustrating your problem: https://klee.github.io/support/

mristin commented 7 months ago

@mristin is the situation that you can use KLEE for your code when you install it from other sources, but not as a snap? Otherwise, and if you need help with your scenario, you should send a message to the KLEE mailing list with a small example illustrating your problem: https://klee.github.io/support/

That's correct, thanks! I'll write to the mailing list.