[klee-dev] -DSPEC_CPU -DNDEBUG -DSPEC_CPU_LP64
dnoorah at gmail.com
dnoorah at gmail.com
Sat Jul 15 11:53:50 BST 2017
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, "asantosa1999 at gmail.com" <asantosa1999 at gmail.com> 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 <dnoorah at 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, asantosa1999 at gmail.com <asantosa1999 at 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 <dnoorah at 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, asantosa1999 at gmail.com <asantosa1999 at 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 <dnoorah at 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 at imperial.ac.uk
> >> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev
> >
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list