[klee-dev] Symbolic calls to mqueue.h functions ?

[Nowack, Martin]

Hi Delphine,

> On 25. Apr 2023, at 16:07, LONGUET Delphine <delphine.longuet at thalesgroup.com> wrote:
> 
> Hi Martin,
> 
> Thanks a lot for your answer. That works, in the sense that now mq_open is found, but unfortunately, the implementation contains assembly code not supported by Klee :
> 
> KLEE: WARNING: function "__syscall_mq_open" has inline asm
> [...]
> KLEE: ERROR: librt/mq_open.c:15: inline assembly is unsupported
> 
> In file librt/mq_open.c (lines 14-15):
> 
> #define __NR___syscall_mq_open __NR_mq_open
> static inline _syscall4(int, __syscall_mq_open, const char*, name, int, oflag, __kernel_mode_t, mode, void *, attr);
> 
> Is there anything I can do about it?

Yes, there are mainly two options:
* support for handling inline assembly was added recently and is available as part of upstream but not as part of a released version of KLEE.
  If you can, use the development branch to check if that helps you.
  (If you want to back port specific changes to your code base, have a look here: https://github.com/klee/klee/pull/1515)
* In KLEE uclibc’s libc, we use a different technique. Essentially, a generic `syscall` function call is used for all system calls (https://www.gnu.org/software/libc/manual/html_node/System-Calls.html).
  The same approach is used for libc as well by disabling system-specific  asm includes, which triggers a fallback to the function call approach (https://github.com/klee/klee-uclibc/commit/e7b3e0f0e8c7cfff58f3770b1bb1434ede0fb6c3)
  I haven’t had a closer look, why this isn’t used for `librt` either, but you could rewrite the librt code to use the syscall function as well, e.g as a proof of concept.

Let me know if any of those options work for you.

Best,
Martin


> 
> Thank you.
> Best regards,
> Delphine
> 
>> -----Message d'origine-----
>> De : Nowack, Martin <m.nowack at imperial.ac.uk>
>> Envoyé : mardi 25 avril 2023 15:59
>> À : LONGUET Delphine <delphine.longuet at thalesgroup.com>
>> Cc : klee-dev <klee-dev at imperial.ac.uk>
>> Objet : Re: [klee-dev] Symbolic calls to mqueue.h functions ?
>> 
>> Hi,
>> 
>>> On 24. Apr 2023, at 10:53, LONGUET Delphine
>> <delphine.longuet at thalesgroup.com> wrote:
>>> 
>>> 
>>> I am trying to execute Klee on a code using mqueue.h and despite the -
>> posix-runtime and -libc=uclibc options, functions mq_open, mq_close, etc,
>> remain "undefined references". I can see that there actually are
>> implementations of these functions in /klee-uclibc/librt/, but they don't seem
>> to exist in klee-uclibc.bca which is used during the execution of Klee.
>> 
>> With `-libc=uclibc`, only  `klee-uclibc/lib/libc.a` is linked/loaded (it’s an
>> archive containing respective bitcode files). Functions like `mq_*` are part of
>> `lib/librt.a`. This library is not loaded which is unfortunately not that obvious.
>> Can you try to link/load the library using `--link-llvm-lib=/path/to/klee-
>> uclibc/lib/librt.a` as an additional argument for KLEE? The library should
>> contain the necessary additional bitcode files.
>> 
>>> In a more general way, how can I know what exactly is in klee-uclibc?
>> With `ar t klee-uclibc/lib/libc.a` the files that are part of the library are listed.
>> Their names mirror the source code files.
>> 
>> Let me know if that works.
>> 
>> Best,
>> Martin