*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 <[email protected]>: > *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 <[email protected]>: > >> *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@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@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 <[email protected]> >> : >> >>> 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@00934a05ada8:obj-llvm$ LLVM_COMPILER=clang >>> CC=/home/klee/whole-program-llvm/wllvm ../configure --disable-nls >>> CFLAGS="-g” >>> klee@00934a05ada8:obj-llvm$ LLVM_COMPILER=clang >>> CC=/home/klee/whole-program-llvm/wllvm make >>> klee@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@00934a05ada8:obj-llvm$ cd src/ >>> klee@00934a05ada8:src$ ~/whole-program-llvm/extract-bc cat >>> klee@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@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 <[email protected]> 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/[email protected]/msg01924.html >>> here is my commands >>> >>> >>> export PATH=/home/klee/klee_build/klee/Release+Asserts/bin:$PATH >>> >>> klee@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@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 < >>> [email protected]>: >>> >>>> > On 16 Mar 2016, at 23:33, Jiarui Wang <[email protected]> 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@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@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 < >>>> [email protected]>: >>>> > 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 <[email protected]> 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@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@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/[email protected]/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@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 >>>> >> [email protected] >>>> >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>>> > >>>> > >>>> >>>> >>> <config.log> >>> >>> >>> >> >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
