[cfe-dev] [Analyzer][RFC] Function Summaries

[Gábor Horváth via cfe-dev]

Hi!

I think being able to write such summaries is valuable for the analyzer!

Please see some comments/questions inline.

On Mon, Feb 3, 2020 at 8:23 AM Gábor Márton via cfe-dev <
cfe-dev at lists.llvm.org> wrote:

> Hi,
>
> This year we plan to experiment with function summaries in CSA. We have a
> budge roughly for 2 people to work on this.
>
> Short-term plans:
> ^^^^^^^^^^^^^^^^^
> We'd like to be able to read and use hand-written function summaries. A
> good example of such hand-written summaries are in Cppcheck
> <https://github.com/danmar/cppcheck/blob/master/cfg/std.cfg>.
>

How does the content of the summaries you proposed compare to
CppCheck's summaries? Is it the same or did you add/remove something?


>
> What could be in a summary?
>
>
Some of these items like nullability have dedicated annotations. I think
the design should include the following point:
* Should we have this duplicate information or only rely on annotations?
Should we use/upstream APINotes?
* What would happen if the annotation and the summary contradict each other?


>
> Perhaps we should come up with a summary description file format (e.g.
> json or
> whatever) that could be parsed by the future variant of the existing
> StdLibraryFunctionsChecker.
>

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?


>
> Mid-term plans:
> ^^^^^^^^^^^^^^^
> Automatically create summaries based on the methods described in SMART and
> Microsoft PEX [Godefroid2007, Godefroid2008].
> ...
> 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.
>

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.

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.


>
>
> Long-term plans:
> ^^^^^^^^^^^^^^^^
> Create summaries based on the ideas in Facebook Infer's publications
> [FBInfer2005, FBInfer2020].
> The basic idea here is to create summaries the are free from the
> calling-context.
> This can be done only with a special data-flow computation and with a
> proofing system.
> This solution would render the analysis to a two-phase analysis.
>

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.

Cheers,
Gabor


>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://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/20200203/9d354841/attachment.html>