Hi Cristian,
I'll try to answer some of your questions, and defer the rest to others who
are more knowledgeable with Klee ...
On Wed, Apr 15, 2009 at 8:47 AM, Cristian Zamfir <cristian.zamfir at
epfl.ch>wrote:
>
> Hello,
>
> I have a few questions about KLEE and I batched them in this email.
>
> - When using the file model, are the modeled calls allowed to work
> with concrete files? From reading the current snapshot of the code it
> seems this is not true, for instance ioctl is only allowed for
> symbolic files, else it returns an error.
i dunno so i'll defer this, but i'm sure cristian cadar knows the answer to
this one
>
>
> - I got the memory error "unbound pointer" when I mixed the symbolic
> file system and allowed some syscalls to go through the OS. I assume
> this is due to the fact that memory is modified outside of the KLEE
> environment. It also happens when the code calls into a native
> library. To go around it, I usually compile all dependencies with klee-
> gcc but for instance, for libX11, there are a lot of dependencies ;) I
> was wondering if you see an alternative to this, such as making KLEE
> aware of the memory object even if it was allocated by a native library.
same as above
>
>
> - Currently KLEE does not support inline assembly and it is sometimes
> too complicated to rewrite all asm functions. Do you think there
> could be a way to execute inline asm, pretending for instance that it
> is an external call?
yes, grep for the line:
} else if (isa<InlineAsm>(fp)) {
in lib/Executor.cpp ... this is the Klee handler for inline assembly code.
you can hack this branch to, like you suggested, pretend like the inline
assembly was an external call and simply return a fresh symbolic value.
note that this might really screw up the correctness of your execution,
because inline assembly does something concrete, so returning an
unconstrained symbolic value might be bogus, but nonetheless, it keeps your
program executing :)
you can use this code that i wrote in my own branch as a template, but it
might not work 100% correctly for your particular case ...
} else if (isa<InlineAsm>(fp)) {
// for UC, let's skip over inline assembly code, but don't croak ...
//terminateStateOnExecError(state, "inline assembly is
unsupported");
InlineAsm* fpAsm = dyn_cast<InlineAsm>(fp);
const llvm::Type* fpAsmRetType =
fpAsm->getFunctionType()->getReturnType();
// if the inline assembly returns an aggregate type (components
// must be extracted later with 'getresult' instruction), don't
// do anything yet, and handle later when handling getresult
// instruction - this is only for primitive returned types
//
// (also don't do anything if it returns a void type, obviously)
if ((fpAsmRetType->getTypeID() != llvm::Type::VoidTyID) &&
(fpAsmRetType->getTypeID() != llvm::Type::StructTyID)) {
// allocate an MO of the same size as the returned value:
Expr::Width width_in_bits =
Expr::getWidthForLLVMType(fpAsm->getFunctionType()- >getReturnType());
uint64_t width_in_bytes = width_in_bits / 8;
// allocate a new block of memory
MemoryObject *mo = memory->allocate(width_in_bytes, false, false,
0);
// make it symbolic
executeMakeSymbolic(state, mo);
// bind it in your current state's address space
const ObjectState* os = state.addressSpace.findObject(mo);
// do a READ from it
ref<Expr> ucRead = os->read(0, width_in_bits);
// bind that READ as the result
bindLocal(ki, state, ucRead);
}
>
>
> - Are the statistics used by the StatsTracker used in any of the the
> searchers? How will the search perform without these statistics?
yes, it seems like some searchers, like WeightedRandomSearcher, depend
heavily on statistics such as instruction count and minimum distance until
you reach an uncovered instruction. each searcher's code is fairly
well-encapsulated as a subclass of Searcher in lib/Searcher.cpp, so if you
look thru each searcher's code, you can see whether it relies on variables
or functions in StatsTracker. i would assume that WeightedRandomSearcher
wouldn't work so hot without statistics. but something simple like depth
first search (DFSSearcher) would work just fine, since it doesn't rely on
statistics.
>
>
> - Did you see in practice any implications from the the warning "this
> target does not support llvm.stacksave intrinsic"?
i've never seen any ill effects of this, but then again, i don't know what
this is, either, so someone else should answer this one :)
>
>
> - Do you have any experience with the LLVM/CLANG static analyzer?
> Would it be a good framework to perform static analysis on LLVM
> bytecode and use it for instance to maximize code coverage under KLEE?
> We are currently doing this more or less "manually" but it would be
> great to have a better framework. First of all, is the analysis done
> on LLVM bytecode? I am guessing no, since C++ would then be easy to
> support, however it is not fully supported yet by the CLANG static
> analyzer.
daniel dunbar would be the best person to ask about this.
>
>
> - There are two new interns helping out with KLEE in our lab, could
> you please add them as well to the klee-dev list?
> There emails are liviu.ciortea at epfl.ch and vlad.georgescu at epfl.ch
>
sure, i just added both to the mailing list.
>
> Hope I didn't batch too many questions ;)
>
> Thank you very much,
>
> Cristi
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.Stanford.EDU
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090415/b28000c2/attachment.html
