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

Thu Mar 17 23:12:27 GMT 2016

*Hi Andrea,*

*I also want to ask if I can test a specified command using Klee,*
*Like *
tac -r t3.txt t3.txt
mkfifo -Z a b

*Thank you very much*
*Jiarui Wang*

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

> *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