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

[LONGUET Delphine]

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?

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