[klee-dev] Asking for Help about Klee3.4 on docker

Thu Mar 17 23:09:17 GMT 2016

*After I terminated ptx.bc, I got*

^CKLEE: ctrl-c detected, requesting interpreter to halt.

KLEE: halting execution, dumping remaining states

KLEE: done: total instructions = 115911

KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

*I am sure the number of total instructions is growing , how long should I
wait for a test ?*

2016-03-17 16:05 GMT-07:00 Jiarui Wang <jrwwang at ucdavis.edu>:

> *Hi Andrea,*
>
> *Thank you for your help, I have fixed the problem.*
> *But I have a question, about testing the coreuitls.*
>
> *Usually when I run the test for some .bc files, klee will return the
> result.*
> *Like seq.bc :*
>
> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$ klee --libc=uclibc
> --posix-runtime ./seq.bc
>
> KLEE: NOTE: Using klee-uclibc :
> /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
>
> KLEE: NOTE: Using model:
> /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
>
> KLEE: output directory is
> "/home/klee/test/coreutils-6.11/obj-llvm/src/./klee-out-29"
>
> Using STP solver backend
>
> KLEE: WARNING ONCE: function "vasnprintf" has inline asm
>
> KLEE: WARNING: undefined reference to function: __ctype_b_loc
>
> KLEE: WARNING: undefined reference to function: __finitel
>
> KLEE: WARNING: undefined reference to function: fabs
>
> KLEE: WARNING: undefined reference to function: freelocale
>
> KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
>
> KLEE: WARNING: undefined reference to function: newlocale
>
> KLEE: WARNING: undefined reference to function: strtold_l
>
> KLEE: WARNING: executable has module level assembly (ignoring)
>
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 59783008)
>
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
>
> missing operand
>
> KLEE: WARNING ONCE: calling external: vprintf(45858240, 42170816)
>
> Try `./seq.bc --help' for more information.
>
> KLEE: WARNING ONCE: calling close_stdout with extra arguments.
>
>
> KLEE: done: total instructions = 12028
>
> KLEE: done: completed paths = 1
>
> KLEE: done: generated tests = 1
>
> *but when I run some .bc files, the process seems won't finish. I have to
> press Ctrl-C to terminate them.*
> *Like ptx.bc :*
>
> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$ klee --libc=uclibc
> --posix-runtime ./ptx.bc
>
> KLEE: NOTE: Using klee-uclibc :
> /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
>
> KLEE: NOTE: Using model:
> /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
>
> KLEE: output directory is
> "/home/klee/test/coreutils-6.11/obj-llvm/src/./klee-out-30"
>
> Using STP solver backend
>
> KLEE: WARNING ONCE: function "vasnprintf" has inline asm
>
> KLEE: WARNING: undefined reference to function: __ctype_b_loc
>
> KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
>
> KLEE: WARNING: executable has module level assembly (ignoring)
>
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 85840016)
>
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
>
> KLEE: WARNING ONCE: calling external: __ctype_b_loc()
>
> *Does this mean these command have bugs? If not, what klee will return if
> there is a bug and klee finds out?*
>
> *Thank you very much*
> *Jiarui Wang*
>
> 2016-03-17 0:58 GMT-07:00 Andrea Mattavelli <a.mattavelli at imperial.ac.uk>:
>
>> Hi,
>> please remember to always include the mailing list address when replying.
>> I would try to run configure and run by explicitly saying what compiler
>> you want to use:
>>
>> klee at 00934a05ada8:obj-llvm$ LLVM_COMPILER=clang
>> CC=/home/klee/whole-program-llvm/wllvm ../configure --disable-nls
>> CFLAGS="-g”
>> klee at 00934a05ada8:obj-llvm$ LLVM_COMPILER=clang
>> CC=/home/klee/whole-program-llvm/wllvm make
>> klee at 00934a05ada8:obj-llvm$ LLVM_COMPILER=clang
>> CC=/home/klee/whole-program-llvm/wllvm make -C src arch hostname
>>
>> Then, go to the obj-llvm/src and extract the bitcode:
>>
>> klee at 00934a05ada8:obj-llvm$ cd src/
>> klee at 00934a05ada8:src$ ~/whole-program-llvm/extract-bc cat
>> klee at 00934a05ada8:src$ ll cat.bc
>> -rw-r--r-- 1 klee klee 148408 Mar 17 07:55 cat.bc
>>
>> You can now run Klee on the extracted bitcode:
>>
>> klee at 00934a05ada8:src$ klee --libc=uclibc --posix-runtime cat.bc
>> --version
>> KLEE: NOTE: Using klee-uclibc :
>> /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
>> KLEE: NOTE: Using model:
>> /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
>> KLEE: output directory is
>> "/home/klee/coreutils-6.11/obj-llvm/src/klee-out-1"
>> Using STP solver backend
>> KLEE: WARNING ONCE: function "vasnprintf" has inline asm
>> KLEE: WARNING: undefined reference to function: __ctype_b_loc
>> KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
>> KLEE: WARNING: executable has module level assembly (ignoring)
>> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 32425008)
>> KLEE: WARNING ONCE: calling __user_main with extra arguments.
>> KLEE: WARNING ONCE: calling external: getpagesize()
>> KLEE: WARNING ONCE: calling external: vprintf(39865600, 27218384)
>> cat (GNU coreutils) 6.11
>>
>> License GPLv3+: GNU GPL version 3 or later <
>> http://gnu.org/licenses/gpl.html>
>> This is free software: you are free to change and redistribute it.
>> There is NO WARRANTY, to the extent permitted by law.
>>
>> Written by Torbjorn Granlund and Richard M. Stallman.
>> KLEE: WARNING ONCE: calling close_stdout with extra arguments.
>>
>> KLEE: done: total instructions = 27363
>> KLEE: done: completed paths = 1
>> KLEE: done: generated tests = 1
>>
>>
>> Andrea
>>
>> On 17 Mar 2016, at 00:43, Jiarui Wang <jrwwang at ucdavis.edu> wrote:
>>
>> Hi Andrea,
>>
>> I deleted obj-llvm to restart the process, but I encounter OLD problem.
>> I follow the instruction on this email
>> https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01924.html
>> here is my commands
>>
>>
>> export PATH=/home/klee/klee_build/klee/Release+Asserts/bin:$PATH
>>
>> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm$ echo $PATH
>>
>>
>> /home/klee/klee_build/klee/Release+Asserts/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/home/klee/klee_build/klee/Release+Asserts/bin:/home/klee/test/whole-program-llvm-master
>>
>> export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
>>
>> export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
>>
>>
>> export LD_LIBRARY_PATH=/usr/lib/gcc/x86_64-linux-gnu/4.8.4
>>
>> export LIBRARY_PATH=/usr/lib/gcc/x86_64-linux-gnu/
>>
>> export LLVM_COMPILER=clang
>>
>>
>> export LLVM_COMPILER_PATH=/usr/lib/llvm-3.4/build/Release/bin
>>
>> *mkdir obj-llvm*
>> *cd obj-llvm*
>> * ../configure --disable-nls CFLAGS="-g"*
>>
>> the last command went wrong.
>>
>> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm$ ../configure --disable-nls CFLAGS="-g"
>>
>> checking build system type... x86_64-unknown-linux-gnu
>>
>> checking host system type... x86_64-unknown-linux-gnu
>>
>> configure: autobuild project... GNU coreutils
>>
>> configure: autobuild revision... 6.11
>>
>> configure: autobuild hostname... 3cc1aa045534
>>
>> configure: autobuild timestamp... 20160317-002339
>>
>> checking for a BSD-compatible install... /usr/bin/install -c
>>
>> checking whether build environment is sane... yes
>>
>> checking for a thread-safe mkdir -p... /bin/mkdir -p
>>
>> checking for gawk... no
>>
>> checking for mawk... mawk
>>
>> checking whether make sets $(MAKE)... yes
>>
>> checking for style of include used by make... GNU
>>
>> checking for gcc... CC=wllvm
>>
>> checking for C compiler default output file name...
>>
>> configure: error: C compiler cannot create executables
>>
>> See `config.log' for more details.
>>
>>
>> HERE is the config.log.
>>
>>
>> I don't know what to do. Please help me
>>
>>
>> Thank you very much
>>
>> Jiarui Wang
>>
>>
>> 2016-03-16 16:57 GMT-07:00 Andrea Mattavelli <a.mattavelli at imperial.ac.uk
>> >:
>>
>>> > On 16 Mar 2016, at 23:33, Jiarui Wang <jrwwang at ucdavis.edu> wrote:
>>> >
>>> > Hi Andrea,
>>> >
>>> > I have fixed error with your help. And get the most of .bc files.
>>> > But when I run *extract-bc hostname* I still got the error. It is the
>>> only one has problem.
>>> > Infomation as followed:
>>> > klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$
>>> /home/klee/test/whole-program-llvm-master/extract-bc hostname
>>> > Exception: Could not find ".llvm_bc" ELF section in "hostname"
>>> >
>>> > Why this only one does not work?
>>>
>>> Did you run ‘make -C src arch hostname’ after the first make invocation?
>>>
>>> > Then when I run  *klee --libc=uclibc --posix-runtime ./cat.bc
>>> --version* I get a klee error :failed external call:version_etc
>>> >
>>> > Whole information as followed:
>>> > klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$ klee
>>> --libc=uclibc --posix-runtime ./cat.bc --version
>>> > KLEE: NOTE: Using klee-uclibc :
>>> /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
>>> > KLEE: NOTE: Using model:
>>> /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
>>> > KLEE: output directory is
>>> "/home/klee/test/coreutils-6.11/obj-llvm/src/./klee-out-1"
>>> > Using STP solver backend
>>> > KLEE: WARNING: undefined reference to function: close_stdout
>>> > KLEE: WARNING: undefined reference to function: full_write
>>> > KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
>>> > KLEE: WARNING: undefined reference to function: quote
>>> > KLEE: WARNING: undefined reference to function: safe_read
>>> > KLEE: WARNING: undefined reference to function: version_etc
>>> > KLEE: WARNING: undefined reference to function: xmalloc
>>> > KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 46792144)
>>> > KLEE: WARNING ONCE: calling __user_main with extra arguments.
>>> > KLEE: WARNING ONCE: calling external: getpagesize()
>>> > KLEE: WARNING ONCE: calling external: version_etc(41196576, 33728688,
>>> 33729248, 33729808, 33730464, 33730928, 0)
>>> > KLEE: ERROR:
>>> /home/klee/test/coreutils-6.11/obj-llvm/src/../../src/cat.c:631: failed
>>> external call: version_etc
>>> > KLEE: NOTE: now ignoring this error at this location
>>> > KLEE: done: total instructions = 8715
>>> > KLEE: done: completed paths = 1
>>> > KLEE: done: generated tests = 1
>>> >
>>> > Other .bc files also have this klee error.
>>> > Is this normal or what's wrong with this?
>>>
>>> Hmm, this seems a problem with linking. Have you tried to remove
>>> obj-llvm and both reconfigure and compile everything from scratch?
>>>
>>> > Thank you very much
>>> > Jiarui Wang
>>> >
>>> > 2016-03-16 3:35 GMT-07:00 Andrea Mattavelli <
>>> a.mattavelli at imperial.ac.uk>:
>>> > Hi Jiarui,
>>> > in the first case you are running extract-bc on the wrong object:
>>> extract-bc must be run on the executable (base64) and not on the object
>>> file.
>>> > In the second case the problem is that you are running configure with
>>> wllvm without specifying LLVM_COMPILER=clang (configure: error: C compiler
>>> cannot create executables). Try to look into config.log to confirm the
>>> problem.
>>> >
>>> > You can find some more explanations on the wllvm page:
>>> https://github.com/travitch/whole-program-llvm
>>> >
>>> > Best,
>>> > Andrea
>>> >
>>> >> On 16 Mar 2016, at 10:09, Jiarui Wang <jrwwang at ucdavis.edu> wrote:
>>> >>
>>> >> Hi,
>>> >>
>>> >> I followed   Tutorial on How to Use KLEE to Test GNU Coreutils
>>> http://klee.github.io/tutorials/testing-coreutils/  .
>>> >>
>>> >> In the step 2, I got all the *.o files by using whole-program-llvm.
>>> But there is no *.bc files.
>>> >>
>>> >> So I used
>>> >>
>>> >> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$
>>> /home/klee/test/whole-program-llvm-master/extract-bc base64.o
>>> >>
>>> >> to get *.bc files. But I got the error
>>> >>
>>> >> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$
>>> /home/klee/test/whole-program-llvm-master/extract-bc base64.o
>>> >> DEBUG::popenwrapper.Popen() at popenwrapper.py:13 ::WLLVM Executing:
>>> >> ['file', '/home/klee/test/coreutils-6.11/obj-llvm/src/base64.o']
>>> >> in: /home/klee/test/coreutils-6.11/obj-llvm/src
>>> >> DEBUG::extract-bc.process_file_unix() at extract-bc:341 ::Detected
>>> file type is ELF_OBJECT
>>> >> INFO::extract-bc.process_file_unix() at extract-bc:348 ::Generating
>>> LLVM Bitcode module
>>> >> DEBUG::popenwrapper.Popen() at popenwrapper.py:13 ::WLLVM Executing:
>>> >> ['objdump', '-h', '-w', 'base64.o']
>>> >> in: /home/klee/test/coreutils-6.11/obj-llvm/src
>>> >> Traceback (most recent call last):
>>> >>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line
>>> 380, in <module>
>>> >>     sys.exit(main(sys.argv))
>>> >>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line
>>> 327, in main
>>> >>     process_file_unix(inputFile, outputFile, llvmLinker, llvmArchiver)
>>> >>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line
>>> 349, in process_file_unix
>>> >>     return handleExecutable(inputFile, outputFile, extractor,
>>> llvmLinker)
>>> >>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line
>>> 139, in handleExecutable
>>> >>     fileNames = extractor(inputFile)
>>> >>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line
>>> 129, in extract_section_linux
>>> >>     (sectionSize, sectionOffset) =
>>> getSectionSizeAndOffset(elfSectionName, inputFile)
>>> >>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line
>>> 79, in getSectionSizeAndOffset
>>> >>     filename)
>>> >> Exception: Could not find ".llvm_bc" ELF section in "base64.o"
>>> >>
>>> >> Just like this email
>>> https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01926.html  and
>>> it does not work for both base64 and base64.o
>>> >>
>>> >> Then I tried
>>> >> ```
>>> >> export WLLVM_OUTPUT=DEBUG
>>> >> export CC=wllvm
>>> >> export CXX=wllvm++
>>> >>  ../configure --disable-nls CFLAGS="-g"
>>> >> make
>>> >> ```
>>> >>
>>> >> when I run ../configure --disable-nls CFLAGS="-g”  there was an error
>>> >> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm$ ../configure
>>> --disable-nls CFLAGS="-g"
>>> >> checking build system type... x86_64-unknown-linux-gnu
>>> >> checking host system type... x86_64-unknown-linux-gnu
>>> >> configure: autobuild project... GNU coreutils
>>> >> configure: autobuild revision... 6.11
>>> >> configure: autobuild hostname... 3cc1aa045534
>>> >> configure: autobuild timestamp... 20160316-095126
>>> >> checking for a BSD-compatible install... /usr/bin/install -c
>>> >> checking whether build environment is sane... yes
>>> >> checking for a thread-safe mkdir -p... /bin/mkdir -p
>>> >> checking for gawk... no
>>> >> checking for mawk... mawk
>>> >> checking whether make sets $(MAKE)... yes
>>> >> checking for style of include used by make... GNU
>>> >> checking for gcc... wllvm
>>> >> checking for C compiler default output file name...
>>> >> configure: error: C compiler cannot create executables
>>> >> See `config.log' for more details.
>>> >> Hope you can help me asap.
>>> >> Thank you very much
>>> >> Jiarui Wang
>>> >>
>>> >> _______________________________________________
>>> >> klee-dev mailing list
>>> >> klee-dev at imperial.ac.uk
>>> >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>> >
>>> >
>>>
>>>
>> <config.log>
>>
>>
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed