[cfe-dev] Static Analyzer - symbolic expressions in a program

[Jordan Rose]

Hello, Shweta. Currently, the static analyzer infrastructure isn't set up to run without any bug reporting—the "core" checkers which check for things like "division by zero" and "null pointer dereference" are used both for generating warnings and for halting analysis along a certain path.

I'm not sure what you mean by "getting symbolic expressions statically". The analyzer works in terms of symbolic and concrete values (SVals); the symbolic values have a typed representation with a basic hierarchical structure (SymExpr and SymbolData). In most parts of the analyzer, you don't ask for the current value of a variable but rather construct an expression involving the variable and ask the current state (ProgramState) to evaluate it.

Our current constraint solver is fairly simple, keeping sets of possible (scalar) values for symbols and applying a set-union each time a new constraint is added. The implementation uses sets of ranges as a fairly compact way to represent an accumulation of constraints on integers. However, constraints on symbols are not the only way a path can be deemed infeasible; any checker can mark the path as such. This is useful for, say, exceptions, which involve a control flow transfer that we can't follow without whole-program analysis.


Anna Zaks and I gave a talk at last year's LLVM Developer Meeting, which you can watch here. It's more aimed at checker writers, but the first part does contain a discussion of the high-level design of the analyzer and some of the important classes, including the ones I mentioned above.

Please feel free to e-mail us if you have specific questions about the static analyzer.

Best,
Jordan


On Mar 4, 2013, at 3:06 , Shweta Shinde <shwetasshinde24 at gmail.com> wrote:

> Hi all,
> 
> I am working on static symbolic analysis and came across Clang Static Analyzer.
> However, I am interested only in getting the symbolic expressions statically and not the bug finding logic of static analyzer. 
> 
> So far, I am able to view the graph (which show the value ranges for symbolic variables) using the following option:
> clang -cc1 -analyze -analyzer-checker=core -analyzer-viz-egraph-graphviz test.c
> 
> Now, I want to get the actual symbolic expressions for these variables. How can I get it? 
> As I won't be doing any bug analysis should I still write a checker just to access the analysis data, or is there any other way I can get the path symbolic expressions for all paths?
> 
> Also, what kind of solver does clang static analyzer use for path satisfiability?
> 
> Regards,
> Shweta
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130304/ab7dd2bb/attachment.html>