<div dir="ltr"><div><div><div>Hi!<br><br></div>I think this is a great use case for the body farm!<br><br></div>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.)<br><br></div>Let's imagine you have an API call like:<br><br>func(int *,  void (*callback)(void))<div><br></div><div>If you provide a fake body like:<br></div><div>void func(int *,  void (*callback)(void)) {<br>  callback();<br>}<br><br></div><div>This can introduce false positives. The reason is the following:<br></div><div>* When you do not have a fake body, the memory region that is pointed by the first argument is invalidated (pointer escape happens).<br></div><div>* 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<br><br></div><div>The proper way to model something like this:<br>void func(int *p,  void (*callback)(void)) {<br></div><div>  void unknownFunction(int*);<br></div><div>  unknownFunction(p);<br></div><div>  callback();<br>}<br><br></div><div>So the call to unknownFunction (which has no body) will trigger the pointer escape.<br><br></div><div>Regards,<br></div><div>Gábor<br></div><div><div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 10 May 2017 at 07:44, Anna Zaks <span dir="ltr"><<a href="mailto:ganna@apple.com" target="_blank">ganna@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">+ Gabor, who worked on extending body farms last<br>
<div class="gmail-HOEnZb"><div class="gmail-h5"><br>
> On May 8, 2017, at 1:06 PM, Artem Dergachev via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<br>
><br>
> Yay: It turns out that it might be a lot easier to accomplish with body farms(!)<br>
><br>
> Generally, the idea is to provide a fake body instead of the unavailable body of your close() function which would probably look like:<br>
><br>
>  void close(FILE *fp, void (*callback)(void)) {<br>
>    fclose(fp);<br>
>    callback();<br>
>  }<br>
><br>
> See how, for example, dispatch_sync() is modeled in lib/Analysis/BodyFarm.cpp.<br>
><br>
> 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.<br>
><br>
> Adding Gábor because it's his realm :)<br>
><br>
> On 5/8/17 8:08 PM, Artem Dergachev wrote:<br>
>> 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).<br>
>><br>
>> 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.<br>
>><br>
>> 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?<br>
>><br>
>><br>
>> On 5/7/17 11:03 PM, Paul Bert via cfe-dev wrote:<br>
>>> Hi,<br>
>>><br>
>>> 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<br>
>>><br>
>>> close(FILE *, mycallback).<br>
>>><br>
>>> When the stream moves to release state, the callback is executed.<br>
>>><br>
>>> 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?<br>
>>><br>
>>> Thanks for any help,<br>
>>><br>
>>> Paul<br>
>>><br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> cfe-dev mailing list<br>
>>> <a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a><br>
>>> <a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br>
>><br>
><br>
> ______________________________<wbr>_________________<br>
> cfe-dev mailing list<br>
> <a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a><br>
> <a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br>
<br>
</div></div></blockquote></div><br></div></div></div></div></div></div>