Hi,
I have some problems running BusyBox with Klee, and I imagine you may
have encountered the same problem and maybe fixed it.
In fact, it seems to be a problem with LLVM and the fact that BusyBox
is a multi-call binary.
This is the error:
klee: LoadValueNumbering.cpp:512: virtual
void<unnamed>::LoadVN::getEqualNumberNodes(llvm::Value*,
std::vector<llvm::Value*, std::allocator<llvm::Value*> >&) const:
Assertion `BBI != StoreBB->begin() && "There is a store in this block
of the pointer, but the store" " doesn't mod the address being stored
to?? Must be a bug in" " the alias analysis implementation!"' failed.
../../../../Debug/bin/klee[0x8bc65f2]
../../../../Debug/bin/klee[0x8bc6724]
[0xb7f51420]
/lib/tls/i686/cmov/libc.so.6(abort+0x101)[0xb7cd4a01]
/lib/tls/i686/cmov/libc.so.6(__assert_fail+0xee)[0xb7ccc10e]
../../../../Debug/bin/klee[0x8a8e359]
../../../../Debug/bin/klee[0x893f0e8]
../../../../Debug/bin/klee
(_ZN4llvm13FPPassManager13runOnFunctionERNS_8FunctionE+0x11a)[0x8b593dc]
../../../../Debug/bin/klee
(_ZN4llvm13FPPassManager11runOnModuleERNS_6ModuleE+0x62)[0x8b5957e]
../../../../Debug/bin/klee
(_ZN4llvm13MPPassManager11runOnModuleERNS_6ModuleE+0x100)[0x8b590b2]
../../../../Debug/bin/klee(_ZN4llvm15PassManagerImpl3runERNS_6ModuleE
+0x6e)[0x8b5926a]
../../../../Debug/bin/klee(_ZN4llvm11PassManager3runERNS_6ModuleE+0x1b)
[0x8b592bd]
../../../../Debug/bin/klee(_ZN4llvm8OptimizeEPNS_6ModuleE+0x2f4)
[0x8760e1e]
../../../../Debug/bin/klee
(_ZN4klee7KModule7prepareEbPNS_18InterpreterHandlerE+0x5ad)[0x86fcc81]
../../../../Debug/bin/klee
(_ZN4klee8Executor9setModuleEPN4llvm6ModuleEbRKSt6vectorISsSaISsEE
+0xd5)[0x86c2bf3]
../../../../Debug/bin/klee(main+0x2ca6)[0x854fc26]
/lib/tls/i686/cmov/libc.so.6(__libc_start_main+0xe0)[0xb7cbe450]
../../../../Debug/bin/klee[0x8548a31]
Aborted
Since LLVM changed quite a bit, here is the code where the assert fires:
// getEqualNumberNodes - Return nodes with the same value number as the
// specified Value. This fills in the argument vector with any equal
values.
//
void LoadVN::getEqualNumberNodes(Value *V,
std::vector<Value*> &RetVals) const {
// If the alias analysis has any must alias information to share
with us, we
// can definitely use it.
...
...
BasicBlock::iterator BBI = StoreBB->end();
while (1) {
assert(BBI != StoreBB->begin() &&
"There is a store in this block of the pointer, but
the store"
" doesn't mod the address being stored to?? Must be
a bug in"
" the alias analysis implementation!");
...
llvm-dis works on busybox.bc and I looked at the generated assembly
and it seems ok, but I am not sure the linking worked well.
I checked the instructions for which the assert fires and it seems to
have something to do with fdisk_main.
I see one alternative, which is modify all BusyBox tools to run as
standalone, but that seems too messy, so I am wondering if you
encountered this problem and have already found a solution.
Thanks,
Cristi
