[klee-dev] Asking for Help about Klee3.4 on docker
Jiarui Wang
jrwwang at ucdavis.edu
Thu Mar 17 23:05:40 GMT 2016
*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
More information about the klee-dev
mailing list