Hi Delphine, > On 25. Apr 2023, at 16:07, LONGUET Delphine > <delphine.long...@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.now...@imperial.ac.uk> >> Envoyé : mardi 25 avril 2023 15:59 >> À : LONGUET Delphine <delphine.long...@thalesgroup.com> >> Cc : klee-dev <klee-dev@imperial.ac.uk> >> Objet : Re: [klee-dev] Symbolic calls to mqueue.h functions ? >> >> Hi, >> >>> On 24. Apr 2023, at 10:53, LONGUET Delphine >> <delphine.long...@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 _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
