[klee-dev] KLEE failes to execute Python
Sandeep Dasgupta
sdasgup3 at illinois.edu
Sun Aug 23 10:50:47 BST 2015
Hello All,
I am also facing the same issue with
llvmerror: invalid argument to evalConstant().
Can somebody please help me with how klee should handle
llvm::blockaddress and llvm::indirectbr?
Thanks
Sandeep
On 08/23/2015 03:01 AM, Sandeep Dasgupta wrote:
> 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: fstat64invalid argument to evalConstant()
>>> 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 functIt occurs to be that klee is stable built with llvm 2.9+. So my suggestion does not seem right. errorion: 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: modfinvalid argument to evalConstant()
>>> 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
>
>
>
> _______________________________________________
> 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