<div>Hello Jordan,</div><div><br></div><div>Thanks for your reply and sharing the talk details. It helped to get a better understanding of the static analyzer design.</div><div><br></div><div>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.</div>
<div>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.</div>
<div><br></div><div>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?</div>
<div><br></div><div>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?</div><div><br></div>
<div><span style="color:rgb(0,0,0)">Thanks,</span><br style="color:rgb(0,0,0)"><span style="color:rgb(0,0,0)">Shweta</span><br></div>
<br><br><div class="gmail_quote">On Tue, Mar 5, 2013 at 10:46 AM, Jordan Rose <span dir="ltr"><<a href="mailto:jordan_rose@apple.com" target="_blank">jordan_rose@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word"><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div><br></div><div>Anna Zaks and I gave a talk at last year's LLVM Developer Meeting, which you can watch <a href="http://llvm.org/devmtg/2012-11/" target="_blank">here</a>. 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.</div>
<div><br></div><div>Please feel free to e-mail us if you have specific questions about the static analyzer.</div><div><br></div><div>Best,</div><div>Jordan</div><div><br></div><br><div><div><div class="h5"><div>On Mar 4, 2013, at 3:06 , Shweta Shinde <<a href="mailto:shwetasshinde24@gmail.com" target="_blank">shwetasshinde24@gmail.com</a>> wrote:</div>
<br></div></div><blockquote type="cite"><div><div class="h5"><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif">Hi all,</span></div><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif"><br>
</span></div><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif">I am working on static symbolic analysis and came across Clang Static Analyzer.</span></div>
<div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif">However, I am interested only in getting the symbolic expressions statically and not the bug finding logic of static analyzer. </span></div>
<span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif"><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif"><br>
</span></div><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif">So far, I am able to view the graph (which </span><span style="font-size:small;background-color:transparent">show the value ranges for symbolic variables)</span> using the following option:</div>
</span><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif">clang -cc1 -analyze -analyzer-checker=core -analyzer-viz-egraph-graphviz test.c</span><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif"><br>
</span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif">Now, I want to get the actual symbolic expressions for these variables. How can I get it? </span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif">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?</span></div>
<div><span style="color:rgb(34,34,34);font-family:arial,sans-serif"><br></span></div><div><font color="#222222" face="arial, sans-serif">Also, what kind of solver does clang static analyzer use for path satisfiability?</font></div>
<div><br></div><div><div><span>Regards,</span><br><span>Shweta</span><br></div>
</div></div></div>
_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu" target="_blank">cfe-dev@cs.uiuc.edu</a><br><a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a><br>
</blockquote></div><br></div></blockquote></div><br>