Hi, I removed the optimisation flags (-o2) from the makefile and it works fine. Best, Nora
Sent from my iPhone > On 14 Jul 2017, at 18:05, "[email protected]" <[email protected]> > wrote: > > 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 ./shrc > 4. cd config > 5. cp Example-linux64-amd64-gcc43+.cfg linux.cfg > 6. 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=clang > 8. runspec --config=linux.cfg --action=build --tune=base hmmer > 9. cd ../benchspec/CPU2006/456.hmmer/exe > 10. <whole-program-llvm_dir>/exract-bc hmmer_base.gcc43-64bit > 11. 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.bc > llvm-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 <[email protected]> > 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, [email protected] <[email protected]> > 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 > > <[email protected]> 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, [email protected] <[email protected]> > > 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 <[email protected]> > >> 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 > >> [email protected] > >> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
