[cfe-dev] [analyzer] Summary IPA thoughts

[Ted Kremenek via cfe-dev]

> On Oct 21, 2015, at 4:50 AM, hao/NoQ via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Now, the design we implemented as a quick proof-of-concept is roughly
> as follows:
>  (a) Analyze the function without any context, as top-level;
>  (b) Save its ExplodedGraph, which *is* *the* summary of the function;
>  (c) When modeling the call, take the final states in leaf nodes of
> its graph, and
>    (c.i) Rename the symbolic values inside them according to the context;
>    (c.ii) Merge the renamed range constraints into the current state;
> (c.iii) Merge the GDM into the current state, with inevitable help
> from checkers;
>    (c.iv) Throw bug reports if a bug was revealed while applying the summary;
>    (c.v) Merge the renamed store bindings into the current state,
> including invalidation markers.

I’ve had a similar idea to summaries like this for a long time, and I’m glad to see it get pushed forward.

You can possibly trim the summary down substantially by doing a BFS from the exit/error nodes of the graph to the entrance nodes.  We use this trick when displaying trimmed graphs in GraphViz to show a path to an error node.  That could result in a massive savings.

What kind of participation is needed from a checker author to participate in this design?  Since it is based on the ExplodedGraph, it would seem their participation would be automatic.  Is the participation needed for serializing out state if we want to make these summaries persistent?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20151021/60ec3233/attachment.html>