[klee-dev] KLEE failes to execute Python

[Sven]

hey,

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.

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 have never seen the last ERROR, but maybe someone else can shed some
light on that one.

Cheers,
Sven

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 list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed