Hi Cristi, my answers to some of your questions are inlined below:
> - 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.
> - 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
