[klee-dev] KLEE failes to execute Python
Sandeep Dasgupta
sdasgup3 at illinois.edu
Sun Aug 23 09:01:52 BST 2015
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 <programmer at nurfuerspam.de
> <mailto: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 list
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>> 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
> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list