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 > <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 <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 > <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> > > >
Makefile
Description: Binary data
INCLUDES= -I '/home/klee/klee_src/include' TUNE=base EXT=amd64-m64-gcc41-nn NUMBER=456 NAME=hmmer SOURCES= alphabet.c core_algorithms.c debug.c display.c emit.c emulation.c \ fast_algorithms.c histogram.c hmmio.c hmmcalibrate.c hmmsearch.c \ mathsupport.c masks.c misc.c modelmakers.c plan7.c plan9.c postprob.c \ prior.c tophits.c trace.c ucbqsort.c a2m.c aligneval.c alignio.c \ clustal.c cluster.c dayhoff.c eps.c file.c getopt.c gki.c gsi.c \ hsregex.c iupac.c msa.c msf.c phylip.c revcomp.c rk.c selex.c \ seqencode.c shuffle.c sqerror.c sqio.c squidcore.c sre_ctype.c \ sre_math.c sre_random.c sre_string.c ssi.c stack.c stockholm.c \ translate.c types.c vectorops.c weight.c EXEBASE=hmmer NEED_MATH=yes BENCHLANG=C ONESTEP= CONESTEP= CC = wllvm COPTIMIZE = -O2 CXX = wllvm++ CXXOPTIMIZE = -O2 FC = /usr/local/gcc41/bin/gfortran FOPTIMIZE = -O2 FPBASE = yes OS = unix PORTABILITY = -DSPEC_CPU_LP64 abstol = 1e-05 action = build allow_extension_override = 0 backup_config = 1 baseexe = hmmer basepeak = 0 benchdir = benchspec benchmark = 456.hmmer binary = bindir = exe calctol = 0 changedmd5 = 0 check_integrity = 1 check_md5 = 1 check_version = 1 command_add_redirect = 0 commanderrfile = speccmds.err commandexe = hmmer_base.amd64-m64-gcc41-nn commandfile = speccmds.cmd commandoutfile = speccmds.out commandstdoutfile = speccmds.stdout compareerrfile = compare.err comparefile = compare.cmd compareoutfile = compare.out comparestdoutfile = compare.stdout compile_error = 0 compwhite = configdir = config configpath = /home/naloboud/SpecCPU2006/cpu2006/config/./mytest.cfg copies = 1 datadir = data delay = 0 deletebinaries = 0 deletework = 0 difflines = 10 dirprot = 511 endian = 12345678 env_vars = 0 exitvals = spec_exit expand_notes = 0 expid = ext = amd64-m64-gcc41-nn fake = 0 feedback = 1 flag_url_base = http://www.spec.org/auto/cpu2006/flags/ floatcompare = help = 0 http_proxy = http_timeout = 30 hw_avail = Dec-9999 hw_cpu_char = hw_cpu_mhz = 3000 hw_cpu_name = AMD Opteron 256 hw_disk = SATA hw_fpu = Integrated hw_memory = 2 GB (2 x 1GB DDR333 CL2.5) hw_model = Tyan Thunder KKQS Pro (S4882) hw_nchips = 1 hw_ncores = 1 hw_ncoresperchip = 1 hw_ncpuorder = 1 chip hw_nthreadspercore = 1 hw_ocache = None hw_pcache = 64 KB I + 64 KB D on chip per chip hw_scache = 1 MB I+D on chip per chip hw_tcache = None hw_vendor = Tyan ignore_errors = yes ignore_sigint = 0 ignorecase = info_wrap_columns = 50 inputdir = input iteration = -1 iterations = 3 license_num = 9999 line_width = 0 locking = 1 log = CPU2006 log_line_width = 0 logname = /home/naloboud/SpecCPU2006/cpu2006/result/CPU2006.063.log lognum = 063 mach = default mail_reports = all mailcompress = 0 mailmethod = smtp mailport = 25 mailserver = 127.0.0.1 mailto = make = specmake make_no_clobber = 0 makeflags = max_active_compares = 0 mean_anyway = 0 min_report_runs = 3 minimize_builddirs = 0 minimize_rundirs = 0 name = hmmer nc = 0 need_math = yes no_input_handler = close no_monitor = notes0100 = C base flags: -O2 notes0110 = C++ base flags: -O2 notes0120 = Fortran base flags: -O2 notes25 = PORTABILITY=-DSPEC_CPU_LP64 is applied to all benchmarks in base. notes_wrap_columns = 0 notes_wrap_indent = num = 456 obiwan = os_exe_ext = output = asc output_format = asc output_root = outputdir = output path = /home/naloboud/SpecCPU2006/cpu2006/benchspec/CPU2006/456.hmmer plain_train = 1 prefix = prepared_by = rate = 0 rawfile = rawformat = 0 realuser = your name here rebuild = 0 reftime = reftime reltol = 0.002 reportable = 1 resultdir = result review = 0 run = all runspec = /home/naloboud/SpecCPU2006/cpu2006/bin/runspec --config=./mytest.cfg --action=build --tune=base --tune=base 456.hmmer safe_eval = 1 section_specifier_fatal = 1 sendmail = /usr/sbin/sendmail setpgrp_enabled = 1 setprocgroup = 1 shrate = 0 sigint = 2 size = ref skipabstol = skipobiwan = skipreltol = skiptol = 10 smarttune = base specdiff = specdiff specmake = Makefile.YYYtArGeTYYYspec specrun = specinvoke speed = 0 srcalt = srcdir = src stagger = 10 strict_rundir_verify = 1 subworkdir = work sw_auto_parallel = No sw_avail = Dec-9999 sw_base_ptrsize = 64-bit sw_compiler = gcc , g++ & gfortran 4.1.0 (for AMD64) sw_file = ext3 sw_os = SUSE SLES9 (for AMD64) sw_other = None sw_peak_ptrsize = Not Applicable sw_state = runlevel 3 sysinfo_program = table = 1 teeout = yes teerunout = yes test_date = Dec-9999 test_sponsor = Turbo Computers tester = top = /home/naloboud/SpecCPU2006/cpu2006 tune = base uid = 1000 unbuffer = 1 update-flags = 0 use_submit_for_speed = 0 username = naloboud vendor = anon vendor_makefiles = 0 verbose = 5 version = 0 version_url = http://www.spec.org/auto/cpu2006/current_version workdir = run worklist = list
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
