[klee-dev] -DSPEC_CPU -DNDEBUG -DSPEC_CPU_LP64

Sat Jul 8 21:10:35 BST 2017

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
> <https://github.com/travitch/whole-program-llvm> See also an installation
> instruction as the Step 2 here: Testing Coreutils · KLEE
> <https://klee.github.io/tutorials/testing-coreutils/>
>
> Testing Coreutils · KLEE
>
> <https://klee.github.io/tutorials/testing-coreutils/>
>
>
> 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
> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Makefile
Type: application/octet-stream
Size: 24531 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20170708/98337d10/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Makefile.spec
Type: text/x-rpm-spec
Size: 6048 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20170708/98337d10/attachment.bin>