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

[Shweta Shinde]

Thanks for the reply!

I will use the checkAssume callback and check if I can manage to get what I
want.

It will be great if STP is made available as an alternative in cases where
precise results is the priority.
For now, I would like to check if the slowdown due to Ryan's patch is
significant or trivial for my purposes.
Can I get the patch for checking the slowdown on my tests?

Regards,
Shweta


On Fri, Mar 8, 2013 at 2:59 AM, Jordan Rose <jordan_rose at apple.com> wrote:

> There is a checker callback for when constraints are added: checkAssume.
> However, the form in which you receive the assumption. will be the form
> it's constructed in the source, which may not be the most conducive to
> actually tracking constraints being added. (Example: "x + 7 > 42".)
> Deconstructing this properly would require duplicating a lot of the work
> inside the existing constraint solver.
>
> One possible alternative would be to implement your own constraint solver,
> which would wrap or share an implementation with RangeConstraintManager.
> I'm not sure whether this will be useful for your purposes, however.
>
> It's interesting that you bring up STP in particular, because Ryan
> Govostes was working on a patch to add STP as an optional alternate
> constraint solver. Though it has some rough edges, it was basically
> working, though not quite integrated into the build system. It hasn't gone
> in yet because Ryan's been busy, and because we've been too busy to help in
> review. One consequence of this is that STP is *much* slower than our
> range-based constraint manager, so the cost of the analyzer's
> upper-bound-exponential algorithm is much worse. Still, we'd like to get
> that in eventually for people who are willing to throw a lot of time at a
> problem in order to get better results.
>
> Jordan
>
>
> On Mar 5, 2013, at 3:29 , Shweta Shinde <shwetasshinde24 at gmail.com> wrote:
>
> 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
>>
>>
>>
> _______________________________________________
> 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/20130308/8bf053f3/attachment.html>