<div dir="ltr"><div>Hi!</div><div><br></div><div>I think being able to write such summaries is valuable for the analyzer!<br><br>Please see some comments/questions inline.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Feb 3, 2020 at 8:23 AM Gábor Márton via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi,<br><br>This year we plan to experiment with function summaries in CSA. We have a budge roughly for 2 people to work on this.<br><br>Short-term plans:<br>^^^^^^^^^^^^^^^^^<br>We'd like to be able to read and use hand-written function summaries. A good example of such hand-written summaries are in <a href="https://github.com/danmar/cppcheck/blob/master/cfg/std.cfg" target="_blank">Cppcheck</a>.<br></div></blockquote><div><br></div><div>How does the content of the summaries you proposed compare to CppCheck's summaries? Is it the same or did you add/remove something?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><br>What could be in a summary?<br><br></div></blockquote><div><br></div><div>Some of these items like nullability have dedicated annotations. I think the design should include the following point:<br>* Should we have this duplicate information or only rely on annotations? Should we use/upstream APINotes?<br>* What would happen if the annotation and the summary contradict each other?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><br>Perhaps we should come up with a summary description file format (e.g. json or<br>whatever) that could be parsed by the future variant of the existing<br>StdLibraryFunctionsChecker.<br></div></blockquote><div><br></div><div>Being able to write summaries in a file that is not hardcoded into the compiler is nice. Would APINotes work for this purpose? What would be the distribution model for those summaries? Would clang ship them? Would the library authors ship them along with their libraries? If the latter how would clang pick it up? What if multiple files have summaries for the same function? (In C it is not that hard to have a situation like this due to the lack of namespaces.) How widespread is CppCheck's format? Should we support that?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><br>Mid-term plans:<br>^^^^^^^^^^^^^^^<br>Automatically create summaries based on the methods described in SMART and Microsoft PEX [Godefroid2007, Godefroid2008].<br>...<br>A summary is in the form [pre]f(x)[post], where `pre` is the preconditions over function inputs and `post` is postconditions over function outputs.<br></div></blockquote><div><br></div><div>While I'd really like to have summaries I think we should lower our expectations a bit here. The current constraint solver of the analyzer might not be powerful enough to handle non-trivial summaries of this form. I do believe it can provide some value but often those papers describing these summaries are using a much more powerful SMT solver as a backend. The other concern is how to model checker specific pre- and post-conditions. Our checker API is not written in an SMT solver friendly way, so it would be fairly hard to synthesize those summaries for our checkers. </div><div><br></div><div>Also, I do believe the analyzer could profit a lot from some classical dataflow analysis like mod/ref analysis. If we would annotate the arguments with the results of such an analysis it could help the analyzer to invalidate the right amount of state when evaluating a function call without a body.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><br><br>Long-term plans:<br>^^^^^^^^^^^^^^^^<br>Create summaries based on the ideas in Facebook Infer's publications [FBInfer2005, FBInfer2020].<br>The basic idea here is to create summaries the are free from the calling-context.<br>This can be done only with a special data-flow computation and with a proofing system.<br>This solution would render the analysis to a two-phase analysis.<br></div></blockquote><div><br></div><div>I think the previous plans with automatically generated summaries would already render the analyzer into a two-phase analysis. In case we are interested in infer style summaries I think we should first make our memory modeling based on separation logic. I have no idea how far we are from that at this point and how much work would it be. Also, I believe reasoning about such summaries requires specialized solvers that are much more powerful than the current range based one. </div><div><br></div><div>Cheers,</div><div>Gabor</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><div><br><br></div></div></div>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div></div>