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
On Fri, 2009-05-08 at 18:38 +0200, Cristian Zamfir wrote:
> 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
> >
>
