batch of questions

[Unknown]

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 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.

- 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?

- Are the statistics used by the StatsTracker used in any of the the
searchers? How will the search perform without these statistics?

- Did you see in practice any implications from the the warning "this
target does not support llvm.stacksave intrinsic"?

- 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.

- 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

Hope I didn't batch too many questions ;)

Thank you very much,

Cristi

[Unknown]

Hi Cristian,

I'll try to answer some of your questions, and defer the rest to others who
are more knowledgeable with Klee ...

Post by Unknown
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

Post by Unknown
- 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

Post by Unknown
- 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);
}

Post by Unknown
- 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.

Post by Unknown
- 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 :)

Post by Unknown
- 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.

Post by Unknown
- 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.

Post by Unknown
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

[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?

[Unknown]

Post by Unknown
- 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.

Yes, you can use concrete files. Each syscall model checks if the
file is concrete or symbolic, and if it's concrete, it simply forwards
the request to the native OS. For example, the check in ioctl() is:

if (f->dfile) {
/* symbolic case */
...
}
else {
/* concrete case, simply forward to native OS */
int r = syscall(__NR_ioctl, f->fd, request, buf );
if (r == -1)
errno = klee_get_errno();
return r;
}

You'll see this check for pretty much all system call models.

Post by Unknown
- 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.

KLEE needs to be aware of where all objects are allocated in memory,
so the only way in which you could do this w/o executing the code
under KLEE would be to use annotations to inform KLEE of where such
external objects were allocated. That's very easy to add (and in
fact, we might already provide support for such annotations).

--Cristian

[Unknown]

Hi Cristian and Philip,

Thank you for your answers.

Indeed, concrete files are handled, I assumed wrong based on the ioctl
code that returns the "bad file descriptor" error for sockets, which
is actually the correct thing to do, but I will gradually start to
replace it while implementing a simple network model.

How do the annotations about external allocations look like? I could
try to experiment with them to improve the support for code that links
against external libraries. However, besides making the allocation
visible, I would also need a way to specify the content of the data
written to the allocated buffer and this seems hard to achieve with
the current design.

Thanks,
Cristi

Post by Unknown

Post by Unknown
- 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.

Yes, you can use concrete files. Each syscall model checks if the
file is concrete or symbolic, and if it's concrete, it simply
forwards the request to the native OS. For example, the check in
if (f->dfile) {
/* symbolic case */
...
}
else {
/* concrete case, simply forward to native OS */
int r = syscall(__NR_ioctl, f->fd, request, buf );
if (r == -1)
errno = klee_get_errno();
return r;
}
You'll see this check for pretty much all system call models.

Post by Unknown
- 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.

KLEE needs to be aware of where all objects are allocated in
memory, so the only way in which you could do this w/o executing
the code under KLEE would be to use annotations to inform KLEE of
where such external objects were allocated. That's very easy to
add (and in fact, we might already provide support for such
annotations).
--Cristian

[Unknown]

Hi Cristi,

We actually already have an effective network model, and we can share it
after publishing a paper that discusses it.

With respect to external allocations, I don't think we have the
necessary annotations in place for what you need, but you should be able
to adapt the code in AddressSpace::copyInConcretes() to copy the
contents of an external buffer specified by your annotations. Let me
know if have more questions about this.

Best,
Cristian

Post by Unknown
Hi Cristian and Philip,
Thank you for your answers.
Indeed, concrete files are handled, I assumed wrong based on the ioctl
code that returns the "bad file descriptor" error for sockets, which
is actually the correct thing to do, but I will gradually start to
replace it while implementing a simple network model.
How do the annotations about external allocations look like? I could
try to experiment with them to improve the support for code that links
against external libraries. However, besides making the allocation
visible, I would also need a way to specify the content of the data
written to the allocated buffer and this seems hard to achieve with
the current design.
Thanks,
Cristi

Post by Unknown

Post by Unknown
- 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.

Yes, you can use concrete files. Each syscall model checks if the
file is concrete or symbolic, and if it's concrete, it simply
forwards the request to the native OS. For example, the check in
if (f->dfile) {
/* symbolic case */
...
}
else {
/* concrete case, simply forward to native OS */
int r = syscall(__NR_ioctl, f->fd, request, buf );
if (r == -1)
errno = klee_get_errno();
return r;
}
You'll see this check for pretty much all system call models.

Post by Unknown
- 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.

KLEE needs to be aware of where all objects are allocated in
memory, so the only way in which you could do this w/o executing
the code under KLEE would be to use annotations to inform KLEE of
where such external objects were allocated. That's very easy to
add (and in fact, we might already provide support for such
annotations).
--Cristian