[klee-dev] batch of questions

[Wang Shuai]

Hi *Philip Guo,

*

Recently I have been trying to apply KLEE to busybox and I got the error "inline assembly is unsupported". I saw your method that
pretend like the inline assembly was an external call and simply return a fresh symbolic value and modified code in lib/Executor.cpp
as you suggested. But when I build the klee, there is no declaration fo the function "Expr::getWidthForLLVMType" in the Expr.h. I used the the function"getWidthForLLVMType"
  in the Executor.h to replace it and build klee with some warning:

make[1]: Entering directory `/home/wang/work/klee/lib'
make[2]: Entering directory `/home/wang/work/klee/lib/Basic'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/lib/Basic'
make[2]: Entering directory `/home/wang/work/klee/lib/Support'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/lib/Support'
make[2]: Entering directory `/home/wang/work/klee/lib/Expr'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/lib/Expr'
make[2]: Entering directory `/home/wang/work/klee/lib/Solver'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/lib/Solver'
make[2]: Entering directory `/home/wang/work/klee/lib/Module'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/lib/Module'
make[2]: Entering directory `/home/wang/work/klee/lib/Core'
llvm[2]: Compiling Executor.cpp for Release+Asserts build
llvm[2]: Compiling ExecutorTimers.cpp for Release+Asserts build
llvm[2]: Compiling ExecutorUtil.cpp for Release+Asserts build
llvm[2]: Compiling ImpliedValue.cpp for Release+Asserts build
llvm[2]: Compiling Memory.cpp for Release+Asserts build
llvm[2]: Compiling MemoryManager.cpp for Release+Asserts build
llvm[2]: Compiling PTree.cpp for Release+Asserts build
llvm[2]: Compiling Searcher.cpp for Release+Asserts build
llvm[2]: Compiling SeedInfo.cpp for Release+Asserts build
llvm[2]: Compiling SpecialFunctionHandler.cpp for Release+Asserts build
llvm[2]: Compiling StatsTracker.cpp for Release+Asserts build
StatsTracker.cpp: In constructor 'klee::StatsTracker::StatsTracker(klee::Executor&, std::string, bool)':
StatsTracker.cpp:180: warning: 'bool llvm::sys::Path::isAbsolute() const' is deprecated (declared at /home/wang/work/llvm-2.9/include/llvm/Support/PathV1.h:315)
StatsTracker.cpp:183: warning: 'bool llvm::sys::Path::exists() const' is deprecated (declared at /home/wang/work/llvm-2.9/include/llvm/Support/PathV1.h:383)
llvm[2]: Compiling TimingSolver.cpp for Release+Asserts build
llvm[2]: Compiling UserSearcher.cpp for Release+Asserts build
llvm[2]: Building Release+Asserts Archive Library libkleeCore.a
make[2]: Leaving directory `/home/wang/work/klee/lib/Core'
make[1]: Leaving directory `/home/wang/work/klee/lib'
make[1]: Entering directory `/home/wang/work/klee/tools'
make[2]: Entering directory `/home/wang/work/klee/tools/klee'
llvm[2]: Compiling Debug.cpp for Release+Asserts build
llvm[2]: Compiling main.cpp for Release+Asserts build
main.cpp: In constructor 'KleeHandler::KleeHandler(int, char**)':
main.cpp:306: warning: 'bool llvm::sys::Path::isAbsolute() const' is deprecated (declared at /home/wang/work/llvm-2.9/include/llvm/Support/PathV1.h:315)
main.cpp: In function 'void parseArguments(int, char**)':
main.cpp:603: warning: cast from type 'const char**' to type 'char**' casts away constness
llvm[2]: Linking Release+Asserts executable klee (without symbols)
/home/wang/work/llvm-2.9/Release+Asserts/lib/libLLVMipa.a(CallGraphSCCPass.o): In function `(anonymous namespace)::CGPassManager::runOnModule(llvm::Module&)':
CallGraphSCCPass.cpp:(.text+0x1e61): warning: memset used with constant zero length parameter; this could be due to transposed parameters
llvm[2]: ======= Finished Linking Release+Asserts Executable klee (without symbols)
make[2]: Leaving directory `/home/wang/work/klee/tools/klee'
make[2]: Entering directory `/home/wang/work/klee/tools/kleaver'
llvm[2]: Compiling main.cpp for Release+Asserts build
llvm[2]: Linking Release+Asserts executable kleaver (without symbols)
llvm[2]: ======= Finished Linking Release+Asserts Executable kleaver (without symbols)
make[2]: Leaving directory `/home/wang/work/klee/tools/kleaver'
make[2]: Entering directory `/home/wang/work/klee/tools/ktest-tool'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/tools/ktest-tool'
make[2]: Entering directory `/home/wang/work/klee/tools/gen-random-bout'
llvm[2]: Linking Release+Asserts executable gen-random-bout (without symbols)
llvm[2]: ======= Finished Linking Release+Asserts Executable gen-random-bout (without symbols)
make[2]: Leaving directory `/home/wang/work/klee/tools/gen-random-bout'
make[2]: Entering directory `/home/wang/work/klee/tools/klee-stats'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/tools/klee-stats'
make[2]: Entering directory `/home/wang/work/klee/tools/klee-replay'
llvm[2]: Linking Release+Asserts executable klee-replay (without symbols)
llvm[2]: ======= Finished Linking Release+Asserts Executable klee-replay (without symbols)
make[2]: Leaving directory `/home/wang/work/klee/tools/klee-replay'
make[1]: Leaving directory `/home/wang/work/klee/tools'
make[1]: Entering directory `/home/wang/work/klee/runtime'
make[2]: Entering directory `/home/wang/work/klee/runtime/Intrinsic'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/runtime/Intrinsic'
make[2]: Entering directory `/home/wang/work/klee/runtime/klee-libc'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/runtime/klee-libc'
make[2]: Entering directory `/home/wang/work/klee/runtime/Runtest'
llvm[2]: Linking Release+Asserts Shared Library libkleeRuntest.so
make[2]: Leaving directory `/home/wang/work/klee/runtime/Runtest'
make[2]: Entering directory `/home/wang/work/klee/runtime/POSIX'
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/wang/work/klee/runtime/POSIX'
make[1]: Leaving directory `/home/wang/work/klee/runtime'

Am I right? If not, could you tell me the difference of these two functions?

-------------- next part --------------
HTML attachment scrubbed and removed