Hi Nora, The LLVM bitcode for 456.hmmer of SPEC CPU2006 contains vectorized code. This might have caused the problem. In any case, as far as I know, the support for vectorized code in KLEE is still being worked on (see KLEE PR 657 here: https://github.com/klee/klee/pull/657 ), and therefore it seems this particular benchmark currently cannot be analyzed using KLEE.
I repeated the crash in the following way (on Ubuntu 16.04):1. Install SPEC CPU2006 in <cpu2006_install> a. cd <cpu2006_cd> b. ./install.sh -d <cpu2006_install> 2. cd <cpu2006_install>3. source ./shrc4. cd config5. cp Example-linux64-amd64-gcc43+.cfg linux.cfg6. Change the following two lines in config/linux.cfg: CC=/usr/bin/gcc CXX=/usr/bin/g++ into: CC=<whole-progam-llvm_dir>/wllvm CXX=<whole-program-llvm_dir>/wllvm++7. export LLVM_COMPILER=clang8. runspec --config=linux.cfg --action=build --tune=base hmmer9. cd ../benchspec/CPU2006/456.hmmer/exe10. <whole-program-llvm_dir>/exract-bc hmmer_base.gcc43-64bit11. klee --emit-all-errors --allow-external-sym-calls --optimize --libc=uclibc --posix-runtime --max-memory=1000 ./hmmer_base.gcc43-64bit.bc <cpu2006_install>/benchspec/CPU2006/456.hmmer/data/test/input/bombesin.hmm KLEE: NOTE: Using klee-uclibc : /home/dcsandr/software/klee/Release+Asserts/lib/klee-uclibc.bca KLEE: NOTE: Using model: /home/dcsandr/software/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/dcsandr/software/spec_cpu_2006_install/benchspec/CPU2006/456.hmmer/exe/./klee-out-8" KLEE: Using STP solver backend Terminator found in the middle of a basic block! label %37 Broken module found, compilation aborted! 0 libLLVM-3.4.so.1 0x00002b56908e5042 llvm::sys::PrintStackTrace(_IO_FILE*) + 34 1 libLLVM-3.4.so.1 0x00002b56908e4e34 2 libpthread.so.0 0x00002b56913ac390 3 libc.so.6 0x00002b5693634428 gsignal + 56 4 libc.so.6 0x00002b569363602a abort + 362 5 libLLVM-3.4.so.1 0x00002b56902d44f1 6 libLLVM-3.4.so.1 0x00002b56902dd5b3 7 libLLVM-3.4.so.1 0x00002b56902b4a27 llvm::FPPassManager::runOnFunction(llvm::Function&) + 471 8 libLLVM-3.4.so.1 0x00002b56902b4aab llvm::FPPassManager::runOnModule(llvm::Module&) + 43 9 libLLVM-3.4.so.1 0x00002b56902b6f65 llvm::legacy::PassManagerImpl::run(llvm::Module&) + 693 10 klee 0x00000000004aa238 llvm::Optimize(llvm::Module*, std::string const&) + 216 11 klee 0x00000000004a5b55 klee::KModule::prepare(klee::Interpreter::ModuleOptions const&, klee::InterpreterHandler*) + 3541 12 klee 0x0000000000457aee klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 254 13 klee 0x0000000000446ff1 main + 4545 14 libc.so.6 0x00002b569361f830 __libc_start_main + 240 15 klee 0x0000000000450509 _start + 41 Aborted (core dumped) Regarding the problem with llvm-link, that seems to be because hmmsearch.bc, which contains a main function is somehow included twice or more in the linking. In my case, the file name is .hmmsearch.o.bc, and I could repeat the same error as follows: llvm-link -o y.bc .hmmsearch.o.bc .hmmsearch.o.bcllvm-link: link error in '.hmmsearch.o.bc': Linking globals named 'main': symbol multiply defined! I hope the above helps. Best, Andrew On Sun Jul 09 2017 04:10:37 GMT+0800 (SGT), Nourah mmm <dnoo...@gmail.com> wrote: Hi, Sorry to bother you again. After using make and wllvm, KLEE stopped working and it generated this error: ---------------------------------------------------------------------------------------------------------------- myklee --emit-all-errors --allow-external-sym-calls --optimize --libc=uclibc --posix-runtime --max-memory=1000 ./hmmer.bc '/home/naloboud/SpecCPU2006/cpu2006/benchspec/CPU2006/456.hmmer/data/test/input/bombesin.hmm' KLEE: NOTE: Using klee-uclibc : /home/naloboud/klee/Release+Asserts/lib/klee-uclibc.bca KLEE: NOTE: Using model: /home/naloboud/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/naloboud/klee/examples/hammer2_make/./klee-out-1" Using STP solver backend Terminator found in the middle of a basic block! label %34 Broken module found, compilation aborted! 0 klee 0x0000000000cdc1d5 llvm::sys::PrintStackTrace(_IO_FILE*) + 37 1 klee 0x0000000000cdc61f 2 libpthread.so.0 0x00007f2edccc4390 3 libc.so.6 0x00007f2eda88a428 gsignal + 56 4 libc.so.6 0x00007f2eda88c02a abort + 362 5 klee 0x0000000000c9750d 6 klee 0x0000000000c97331 7 klee 0x0000000000c7b863 llvm::FPPassManager::runOnFunction(llvm::Function&) + 547 8 klee 0x0000000000c7ba2b llvm::FPPassManager::runOnModule(llvm::Module&) + 43 9 klee 0x0000000000c7be3e llvm::legacy::PassManagerImpl::run(llvm::Module&) + 782 10 klee 0x00000000005a469c llvm::Optimize(llvm::Module*, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&) + 236 11 klee 0x00000000005a030b klee::KModule::prepare(klee::Interpreter::ModuleOptions const&, klee::InterpreterHandler*) + 3691 12 klee 0x000000000054e416 klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 278 13 klee 0x0000000000531e99 main + 3561 14 libc.so.6 0x00007f2eda875830 __libc_start_main + 240 15 klee 0x00000000005471d9 _start + 41 Aborted (core dumped) ------------------------------------------------------------------------------------------------------ However, when I use llvm-link it works but it generates this error: /llvm2/Release/bin/llvm-link: link error in 'hmmsearch.bc': Linking globals named 'main': symbol multiply defined! attached is the make file. Please advise Thank you in advance On 5 July 2017 at 02:43, asantosa1...@gmail.com <asantosa1...@gmail.com> wrote: > Sorry it was my mistake. Please replace "sudo apt install wllvm" with the > following two commands: > > sudo apt install python-pip > sudo pip install wllvm > > Best, > Andrew > > > > On Wednesday, July 5, 2017, 7:35:00 AM GMT+8, Nourah mmm <dnoo...@gmail.com> > wrote: > > > Thank you very much for your replay. > > I tried to do that, however, its print extract-bc: command not found. > > I'm trying to extract the bc from SPEC cpu2006 Integer benchmarks. So I did > the following. > 1. sudo apt install wllvm > 2. LLVM_COMPILER=clang CC=wllvm make --> here I use clang version 3.4 and > I just write wllvm without a path. > 3. Then, it generate the .o files and an executable program(mcf) > 4. extract-bc mcf > Thank you > Nora > > On 4 July 2017 at 03:04, asantosa1...@gmail.com <asantosa1...@gmail.com> > wrote: >> I suppose what you want is to produce a bitcode for running with KLEE. You >> can probably >> do a normal build procedure for the program, but with replacing your C >> compiler with wllvm. >> wllvm is available here: https://github.com/travitch/ whole-program-llvm See >> also an installation >> instruction as the Step 2 here: Testing Coreutils · KLEE >> >> | | | | Testing Coreutils · KLEE | | | >> | | | | | | >> >> >> Alternatively, on Ubuntu 16.04, you can do >> >> sudo apt install wllvm >> >> to install wllvm. >> >> I assume you would normally build the program using "make". In that case, >> and assuming >> that both clang and wllvm are in your PATH, the following might work to >> produce the binary: >> >> LLVM_COMPILER=clang CC=wllvm make >> >> And then you can do: >> >> extract-bc program >> >> To get the program.bc for running with KLEE. >> >> Best, >> Andrew >> On Tuesday, July 4, 2017, 9:05:49 AM GMT+8, Nourah mmm <dnoo...@gmail.com> >> wrote: >> >> >> Hi, >> >> I'm testing a program that compress and decompress files. >> For C compilation I'm using these flags: >> >> -DSPEC_CPU -DNDEBUG -DSPEC_CPU_LP64 >> >> How could I use these in KLEE? >> >> Thank you >> Nora >> ______________________________ _________________ >> klee-dev mailing list >> klee-dev@imperial.ac.uk >> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
