[klee-dev] Missing floor, modf and pow

[Dan Liew]

Hi,

On 3 March 2018 at 07:29, Alberto Barbaro <barbaro.alberto at gmail.com> wrote:
> Hi all,
> few months ago I was trying to understand how to test pngpixel via KLEE and
> after few suggestion I was able to do it.
>
> I have just one more question. When I run KLEE I have this output:
>
> klee at 0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ klee
> --libc=uclibc --posix-runtime pngpixel.bc 1 1 file.png
> KLEE: NOTE: Using klee-uclibc :
> /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
> KLEE: NOTE: Using model:
> /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory is
> "/home/klee/targets/libpng-1.6.34/contrib/examples/klee-out-3"
> KLEE: Using STP solver backend
> KLEE: WARNING: undefined reference to function: floor
> KLEE: WARNING: undefined reference to function: modf
> KLEE: WARNING: undefined reference to function: pow
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 92453184) at
> /home/klee/klee_src/runtime/POSIX/fd.c:1044
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled.
> Using alignment of 8.
> KLEE: WARNING ONCE: _setjmp: ignoring
>
> KLEE: done: total instructions = 106954
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
> klee at 0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$
>
> Can I "ignore" the fact that floor, modf and pow are missing because I'm
> using uclibc?

You can ignore the warning as long as the code you run doesn't call
these with symbolic arguments. You'll see a warning if this happens
because KLEE has to concretize the arguments and call the function via
LLVM's JIT.
In your case it doesn't look like you're passing any symbolic data to
the application so you're running concretely so you should be fine. If
any function gets called that's external (i.e. is not in the LLVM
bitcode, like floor is in your example)
KLEE will emit a message telling you its calling an external.

The reason these functions aren't available is because KLEE doesn't
link in Uclibc's C library. My fork of KLEE that supports symbolic
floating-point arithmetic [1] does link this library.

[1] https://github.com/srg-imperial/klee-float