[cfe-dev] [StaticAnalyzer] How to give hint on path execution

Gábor Horváth via cfe-dev cfe-dev at lists.llvm.org
Wed May 10 13:50:23 PDT 2017


Hi!

I think this is a great use case for the body farm!

There is one possible mistake that is easy to make when one uses this
feature. (Which does not affect your example, so do not worry about that. I
just wanted to share this for future reference.)

Let's imagine you have an API call like:

func(int *,  void (*callback)(void))

If you provide a fake body like:
void func(int *, void (*callback)(void)) {
  callback();
}

This can introduce false positives. The reason is the following:
* When you do not have a fake body, the memory region that is pointed by
the first argument is invalidated (pointer escape happens).
* When you have the fake body, pointer escape won't happen, the analyzer
will derive from the fake body that the first argument is unchanged

The proper way to model something like this:
void func(int *p, void (*callback)(void)) {
  void unknownFunction(int*);
  unknownFunction(p);
  callback();
}

So the call to unknownFunction (which has no body) will trigger the pointer
escape.

Regards,
Gábor

On 10 May 2017 at 07:44, Anna Zaks <ganna at apple.com> wrote:

> + Gabor, who worked on extending body farms last
>
> > On May 8, 2017, at 1:06 PM, Artem Dergachev via cfe-dev <
> cfe-dev at lists.llvm.org> wrote:
> >
> > Yay: It turns out that it might be a lot easier to accomplish with body
> farms(!)
> >
> > Generally, the idea is to provide a fake body instead of the unavailable
> body of your close() function which would probably look like:
> >
> >  void close(FILE *fp, void (*callback)(void)) {
> >    fclose(fp);
> >    callback();
> >  }
> >
> > See how, for example, dispatch_sync() is modeled in
> lib/Analysis/BodyFarm.cpp.
> >
> > Once you have a fake body, the path-sensitive engine would be able to
> execute it with the desired effect. It's much easier than what i originally
> proposed.
> >
> > Adding Gábor because it's his realm :)
> >
> > On 5/8/17 8:08 PM, Artem Dergachev wrote:
> >> Unfortunately, allowing checkers to trigger an immediate inlining of a
> function is quite tricky to implement, and we don't have a ready-made
> mechanism for that (though some of the existing checkers could make use of
> such functionality).
> >>
> >> It might theoretically be possible, within a checker callback, to
> manually construct an exploded graph node that represents entering a stack
> frame of the callback function, and then addTransition() to such node
> (similarly to how ExprEngine does that) and see what happens. That'd be an
> interesting problem to tackle, and such mechanism would be good to have.
> >>
> >> Also, are you sure it is necessary to model the callback exactly in
> your use case? Maybe a simple invalidation/escape pass would suffice to
> avoid false positives?
> >>
> >>
> >> On 5/7/17 11:03 PM, Paul Bert via cfe-dev wrote:
> >>> Hi,
> >>>
> >>> I wrote a checker similar to the  SimpleStreamChecker except that the
> close function that moves the state of the stream to released,  takes a
> second parameter, a callback, for instance
> >>>
> >>> close(FILE *, mycallback).
> >>>
> >>> When the stream moves to release state, the callback is executed.
> >>>
> >>> The "close" function is defined externally so that the checker cannot
> reason on it except using the rules I give it in checkPostCall callback.
> How can I make the analyzer  aware that the callback has to be executed
> when the state move to release?
> >>>
> >>> Thanks for any help,
> >>>
> >>> Paul
> >>>
> >>>
> >>> _______________________________________________
> >>> cfe-dev mailing list
> >>> cfe-dev at lists.llvm.org
> >>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
> >>
> >
> > _______________________________________________
> > cfe-dev mailing list
> > cfe-dev at lists.llvm.org
> > http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170510/7d91f5af/attachment.html>


More information about the cfe-dev mailing list