Hello,
For the last error, the invalid argument to evalConstatnt is a
llvm::blockaddress which is used to initialize globals , but klee does
not seem to handle this.
From
http://blog.llvm.org/2010/01/address-of-label-and-indirect-branches.html, it
is mentioned that this construct along with llvm::indirectbr are added
to llvm 2.7+.
So one may use llvm2.6 to generate python linked bc and use klee
(compiled with llvm 2.6) to interpret it.
Please let me know if there is better way to handle this.
Regards,
Sandeep
On 08/17/2015 08:04 AM, Dipanjan Das wrote:
Hi,
On 17 August 2015 at 20:58, Sven <[email protected]
<mailto:[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 list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://urldefense.proofpoint.com/v2/url?u=https-3A__mailman.ic.ac.uk_mailman_listinfo_klee-2Ddev&d=AwMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=at_zHdaJ5pMt_A20sKa_JLbvjeXndNos3PveVfgUF0o&m=__k_0_NUqhoJNS020I7-WYkoCuzZ200ZJu6WhrzOreE&s=yv8d73I_tMdl8fQbguYhqcDHRKqIga_rZRTFfbYBu2s&e=>
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://urldefense.proofpoint.com/v2/url?u=https-3A__mailman.ic.ac.uk_mailman_listinfo_klee-2Ddev&d=AwMFaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=at_zHdaJ5pMt_A20sKa_JLbvjeXndNos3PveVfgUF0o&m=__k_0_NUqhoJNS020I7-WYkoCuzZ200ZJu6WhrzOreE&s=yv8d73I_tMdl8fQbguYhqcDHRKqIga_rZRTFfbYBu2s&e=>
_______________________________________________
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
