[klee-dev] -DSPEC_CPU -DNDEBUG -DSPEC_CPU_LP64
asantosa1999 at gmail.com
asantosa1999 at gmail.com
Fri Jul 14 18:05:06 BST 2017
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 <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