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
On Apr 15, 2009, at 11:38 PM, Cristian Cadar wrote:
>
> 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
>
