[klee-dev] Asking for Help about Klee3.4 on docker
Andrea Mattavelli
a.mattavelli at imperial.ac.uk
Thu Mar 17 07:58:27 GMT 2016
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 <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 <mailto:a.mattavelli at imperial.ac.uk>>:
> > On 16 Mar 2016, at 23:33, Jiarui Wang <jrwwang at ucdavis.edu <mailto: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 <mailto: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 <https://github.com/travitch/whole-program-llvm>
> >
> > Best,
> > Andrea
> >
> >> On 16 Mar 2016, at 10:09, Jiarui Wang <jrwwang at ucdavis.edu <mailto: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/ <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 <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 <mailto:klee-dev at imperial.ac.uk>
> >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev <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