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

[Shweta Shinde]

Hello Jordan,

Thanks for your reply and sharing the talk details. It helped to get a
better understanding of the static analyzer design.

In the talk it is mentioned that static analyzer collects the constraints
on symbolic values along each path while building a graph of reachable
program states.
I am trying to collect all the program points where a new constraint is
added. In the end, I want to track where and what new constraints are being
added for all variables in program. By this, I can construct a symbolic
expression for symbolic variable.

To do this, I am considering the possibility of implementing a checker --
just to access the program point and program state data stored in the node.
This checker will not update the node state or generate a sink. Is it
feasible? If a sink node is not added, will the analysis terminate?

Although the constraint solver doesn't handle bitwise operations and
multiple symbols, is there a way to just generate these constraints and
then use a better solver, perhaps STP?

Thanks,
Shweta


On Tue, Mar 5, 2013 at 10:46 AM, Jordan Rose <jordan_rose at apple.com> wrote:

> 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 <http://llvm.org/devmtg/2012-11/>. 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/20130305/bffa3e8b/attachment.html>