[klee-dev] KLEE failes to execute Python

[Dipanjan Das]

Hi,

On 17 August 2015 at 20:58, Sven <programmer at nurfuerspam.de> wrote:

> KLEE: WARNING ONCE: function "PyOS_string_to_double" has inline asm
>
> Means that there is asm code used inside the C. This is not supported by
> asm, so you will not be able to execute this symbolically.
>

What is the workaround to execute code containing inline ASM?

KLEE: WARNING: undefined reference to function: cos
>
> Means that the function "cos" is used, but the definition is not in the
> bitcode. If you compile the bitcode to machine code, the function will be
> linked directly. If you run the bitcode in C, it is missing and, again, can
> not be executed symbolically.
> You should give each of those functions a look. Maybe you can find the
> code somewhere and compile it to bitcode yourself. Or you can replace the
> call with a function with similar semantics, which does exist in bitcode.
>
> Did you compile against klee's version of ulibc? Some of the undefined
> functions look like they may be in there. The POSIX environment model may
> be helpful as well. The floating-point functions (atan, cos) are simply not
> there, as klee does not support floats. The dlopen, dlsym and dlerror are
> used to open external libraries. Those are not there as bitcode, so klee
> will not be able to execute them symbolically.
>

I executed klee like this: klee --libc=uclibc --posix-runtime python.bc -h

Is there any hack to make supply klee the bitcode for 'cos' function or the
similar ones?



> On 08/17/2015 05:00 AM, Dipanjan Das wrote:
>
> Hi Everybody,
>
> I compiled Python with llvm-gcc to generate LLVM bitcode to be run on top
> of KLEE. Though python.bc gets generated successfully, KLEE throws a bunch
> of warnings during execution. Moreover, there's an LLVM error at the end
> that causes KLEE to abort: "LVM ERROR: invalid argument to evalConstant()".
> Does anybody have any clue on this?
>
> KLEE: WARNING ONCE: function "PyOS_string_to_double" has inline asm
> KLEE: WARNING ONCE: function "PyOS_double_to_string" has inline asm
> KLEE: WARNING: undefined reference to function: __ctype_b_loc
> KLEE: WARNING: undefined reference to function: __finite
> KLEE: WARNING: undefined reference to function: __isinf
> KLEE: WARNING: undefined reference to function: __xstat64
> KLEE: WARNING: undefined reference to function: alarm
> KLEE: WARNING: undefined reference to function: atan2
> KLEE: WARNING: undefined reference to function: bind_textdomain_codeset
> KLEE: WARNING: undefined reference to function: bindtextdomain
> KLEE: WARNING: undefined reference to function: copysign
> KLEE: WARNING: undefined reference to function: cos
> KLEE: WARNING: undefined reference to function: dcgettext
> KLEE: WARNING: undefined reference to function: dgettext
> KLEE: WARNING: undefined reference to function: dlerror
> KLEE: WARNING: undefined reference to function: dlopen
> KLEE: WARNING: undefined reference to function: dlsym
> KLEE: WARNING: undefined reference to function: exp
> KLEE: WARNING: undefined reference to function: fabs
> KLEE: WARNING: undefined reference to function: faccessat
> KLEE: WARNING: undefined reference to function: fchmodat
> KLEE: WARNING: undefined reference to function: fchownat
> KLEE: WARNING: undefined reference to function: fdopendir
> KLEE: WARNING: undefined reference to function: fexecve
> KLEE: WARNING: undefined reference to function: floor
> KLEE: WARNING: undefined reference to function: fmod
> KLEE: WARNING: undefined reference to function: forkpty
> KLEE: WARNING: undefined reference to function: fstat64
> KLEE: WARNING: undefined reference to function: fstatat64
> KLEE: WARNING: undefined reference to function: futimens
> KLEE: WARNING: undefined reference to function: getitimer
> KLEE: WARNING: undefined reference to function: getpgid
> KLEE: WARNING: undefined reference to function: getresgid
> KLEE: WARNING: undefined reference to function: getresuid
> KLEE: WARNING: undefined reference to function: getsid
> KLEE: WARNING: undefined reference to function: gettext
> KLEE: WARNING: undefined reference to function: hypot
> KLEE: WARNING: undefined reference to function: linkat
> KLEE: WARNING: undefined reference to function: log
> KLEE: WARNING: undefined reference to function: lseek64
> KLEE: WARNING: undefined reference to function: lstat64
> KLEE: WARNING: undefined reference to function: lutimes
> KLEE: WARNING: undefined reference to function: mkdirat
> KLEE: WARNING: undefined reference to function: mkfifoat
> KLEE: WARNING: undefined reference to function: mknodat
> KLEE: WARNING: undefined reference to function: modf
> KLEE: WARNING: undefined reference to function: nice
> KLEE: WARNING: undefined reference to function: openat64
> KLEE: WARNING: undefined reference to function: openpty
> KLEE: WARNING: undefined reference to function: posix_fadvise64
> KLEE: WARNING: undefined reference to function: posix_fallocate64
> KLEE: WARNING: undefined reference to function: pow
> KLEE: WARNING: undefined reference to function: pread64
> KLEE: WARNING: undefined reference to function: pwrite64
> KLEE: WARNING: undefined reference to function: readlinkat
> KLEE: WARNING: undefined reference to function: readv
> KLEE: WARNING: undefined reference to function: renameat
> KLEE: WARNING: undefined reference to function: round
> KLEE: WARNING: undefined reference to function: sendfile64
> KLEE: WARNING: undefined reference to function: setegid
> KLEE: WARNING: undefined reference to function: seteuid
> KLEE: WARNING: undefined reference to function: setitimer
> KLEE: WARNING: undefined reference to function: setregid
> KLEE: WARNING: undefined reference to function: setreuid
> KLEE: WARNING: undefined reference to function: sigaltstack
> KLEE: WARNING: undefined reference to function: sin
> KLEE: WARNING: undefined reference to function: stat64
> KLEE: WARNING: undefined reference to function: symlinkat
> KLEE: WARNING: undefined reference to function: textdomain
> KLEE: WARNING: undefined reference to function: truncate64
> KLEE: WARNING: undefined reference to function: utimensat
> KLEE: WARNING: undefined reference to function: writev
> LVM ERROR: invalid argument to evalConstant()
>
>
>
>
> _______________________________________________
> klee-dev mailing listklee-dev at imperial.ac.ukhttps://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed