
<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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 <i>much</i> 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.</div><div><br></div><div>Jordan</div><div><br></div><br><div><div>On Mar 5, 2013, at 3:29 , Shweta Shinde <<a href="mailto:shwetasshinde24@gmail.com">shwetasshinde24@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;"><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="">Thanks,</span><br style=""><span style="">Shweta</span><br></div><br><br><div class="gmail_quote">On Tue, Mar 5, 2013 at 10:46 AM, Jordan Rose<span class="Apple-converted-space"> </span><span dir="ltr"><<a href="mailto:jordan_rose@apple.com" target="_blank">jordan_rose@apple.com</a>></span><span class="Apple-converted-space"> </span>wrote:<br><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: 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><span>Regards,</span><br><span>Shweta</span><br></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>_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br><a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a></div></blockquote></div><br></body></html>