Hi, On 17 August 2015 at 20:58, Sven <[email protected]> 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 > [email protected]https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
