<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hey Jordan</div><div><br></div><div>I am currently using a combination of both. First I check for an availability checking call in checkBranchCondition, if it is already a concrete int then the global state is set. If it is not, then the Symbol (or Memregion in the case of a FunctionDecl) is set in the state, which is later checked in evalAssume when the assumption has been made.</div><div><br></div><div>This works well, except for FunctionDecls. I am currently having a problem with state not being set when returning from evalAssume. I have looked through the code, and the problem seems to be the assumeAux function in SimpleConstraintManager. When the Cond is a MemoryRegionKind with no SubRegion, the switch falls through to the GotoLabelKind, which will always return NULL for false assumptions. If that is the case, then when doing something like this, the false case is never tested, as the branch condition is always true:</div><div><br></div><div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "><span style="color: #bb2ca2">if</span> (UIAccessibilityIsGuidedAccessEnabled != NULL) {</div><div style="font-size: 14px; margin: 0px; font-family: Monaco; color: rgb(0, 132, 0); "><span style="color: rgb(0, 0, 0); "> doIOS6Stuff();</span></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">} else {</div></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "><div style="margin: 0px; color: rgb(0, 132, 0); "> // this will not trigger a warning</div><div> doIOS6Stuff();</div></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">}</div><div><br></div><div>Also, this has the knock on effect of not setting any state for the true assumption when not already a concrete int, because of the following code in the ConstraintManager:</div><div><br></div><div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">ProgramStateRef StFalse = assume(State, Cond, <span style="color: #bb2ca2">false</span>);</div><div style="font-size: 14px; margin: 0px; font-family: Monaco; color: rgb(0, 132, 0); ">// StFalse will always be NULL here for FunctionDecl Conds</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "><span style="color: rgb(187, 44, 162); ">if</span> (!StFalse) {</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; color: rgb(0, 132, 0); "><span style="color: #000000"> </span>// We are careful to return the original state, /not/ StTrue,</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; color: rgb(0, 132, 0); "><span style="color: #000000"> </span>// because we want to avoid having callers generate a new node</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; color: rgb(0, 132, 0); "><span style="color: #000000"> </span>// in the ExplodedGraph.</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> <span style="color: #bb2ca2">return</span> ProgramStatePair(State, (ProgramStateRef)<span style="color: #bb2ca2">NULL</span>);</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">}</div></div><div><br></div><div>So when the function has not already been folded, no global state can be set, eg:</div><div><br></div><div><div style="font-size: 14px; margin: 0px; font-family: Monaco; "><span style="color: rgb(187, 44, 162); ">if</span> (UIAccessibilityIsGuidedAccessEnabled) {</div><div style="font-size: 14px; margin: 0px; font-family: Monaco; "><div style="margin: 0px; color: rgb(0, 132, 0); "> // this will erroneously trigger a warning as no global state was set</div></div><div style="font-size: 14px; margin: 0px; font-family: Monaco; color: rgb(0, 132, 0); "><span style="color: rgb(0, 0, 0); "> doIOS6Stuff();</span></div><div style="font-size: 14px; margin: 0px; font-family: Monaco; ">} </div></div><div><br></div><div>Could you advise as to the best solution to this problem?</div><div><br></div><div>thanks,</div><div>richard</div><br><div><div>On 20 Dec 2012, at 00:42, Jordan Rose <<a href="mailto:jordan_rose@apple.com">jordan_rose@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=us-ascii"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>The check you probably want is evalAssume. As you've seen, evalBranchCondition checks when there's a branch in the control flow graph, but not when the analyzer decides to split states.</div><div><br></div><div>However, you have to be careful with evalAssume: the SVal being assumed can affect the condition on your symbol even if it doesn't directly wrap that symbol:</div><div><br></div><div>BOOL a = ...;</div><div>BOOL b = ...;</div><div>if (a == b) { ... }</div><div><br></div><div>So you'll probably end up having to ask the constraint checker if anything changed with regards to your symbols. You could make this cheaper by iterating over the symbols in the SVal first and seeing if they match your set of unresolved calls to -respondsToSelector: and friends.</div><div><br></div><div>Jordan</div><div><br></div><br><div><div>On Dec 19, 2012, at 15:30 , Richard <<a href="mailto:tarka.t.otter@googlemail.com">tarka.t.otter@googlemail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=us-ascii"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Thank you Ted, this was very helpful. You are right about the SVal folding, they are already concrete values in the example I sent.</div><div><br></div><div>ta//</div><br><div><div>On 19 Dec 2012, at 19:03, Ted Kremenek <<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=us-ascii"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hi Richard,</div><div><br></div><div>SVals are value objects. They should just be viewed as a union of different abstract values that an expression can evaluate to. They are "nameless" values. SVals can wrap SymbolRefs, but they also can wrap other values such as constants, addresses of goto labels, etc. When the analyzer evaluates an expression, it computes an SVal. Another way to look at SVals is that they "box" more interesting values that have different meanings.</div><div><br></div><div>SymbolRefs are "named" symbolic values. They represent the name of a value along a path. For example, in your code snippet 'argc' has an initial value that has a symbol. Along a path the analyzer can reason about properties of that value, e.g., constraints such as the value of argc being greater than 0, etc. Constraints cannot be associated with SVals, as they are value types that are just used to box more persistent named values like symbols.</div><div><br></div><div>If an SVal has no SymbolRef, it means one of two things:</div><div><br></div><div>(1) The value isn't symbolic. There are many cases where this can be. Roughly SVals are divided into locations and non-locations, with those breaking up further into other sets of values:</div><div><br></div><div><blockquote type="cite"><div><br></div><div>namespace nonloc {</div><div><br></div><div>enum Kind { ConcreteIntKind, SymbolValKind,</div><div> LocAsIntegerKind, CompoundValKind, LazyCompoundValKind };</div></blockquote></div><div><br></div><div>and</div><div><br></div><div><blockquote type="cite"><div>namespace loc {</div><div><br></div><div>enum Kind { GotoLabelKind, MemRegionKind, ConcreteIntKind };</div></blockquote></div><div><br></div><div>This is from SVals.h.</div><div><br></div><div>If a value isn't symbolic, usually that means there is no symbolic information to track. For example, if the value was an integer, such as 42, it would be a ConcreteInt, and the checker doesn't usually need to track any state with the number 42. That's why the checkers bail out early.</div><div><br></div><div>(2) The other reason an SVal has no Symbol, but it really should be a symbolic value, is when the analyzer cannot reason about something (yet). An example is floating point numbers. In such cases, the SVal will evaluate to UnknownVal. This represents a case that is outside the realm of the analyzer's reasoning capabilities.</div><div><br></div><div>Now to your question about binary and unary operators. It is possible that the analyzer is constant folding the operations when the symbolic value is known to be constrained. In such cases, the analyzer may eagerly "concretize" a symbolic value and split the path. For example, suppose we have:</div><div><br></div><div> BOOL b = x > 10;</div><div><br></div><div>In this case, 'b' will not be symbolic value. What happens when the analyzer evaluates 'x > 10' is that it eagerly asserts both (a) x > 10 and (b) x <= 10 and splits the path with either (a) being true or (b) being true. Along those two paths, the value of 'b' will either be 1 or 0 respectively. If you do a dump of the SVal (using the .dump() method) you will likely see the value 1 or 0 get printed out. This value isn't symbolic, it is concrete.</div><div><br></div><div>I hope this helps clear things up a bit. If it is still unclear, please do not hesitate to ask for more clarification.</div><div><br></div><div>Cheers,</div><div>Ted</div><br><div><div>On Dec 19, 2012, at 8:45 AM, Richard <<a href="mailto:tarka.t.otter@googlemail.com">tarka.t.otter@googlemail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=us-ascii"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">hey<div><br></div><div>I am having a bit of a hard time understanding the connection between SVals and SymbolRefs, could someone enlighten me? As I understand it, SVals are transient, and SymbolRefs are not, which makes them handy for tracking state. However, some SVals don't have SymbolRefs. What is the recommended way of identifying an SVal with no SymbolRef at a later stage in a checker execution? All the examples I have looked at just bail when there is no SymbolRef.</div><div><br></div><div>I find that the following code has a SymbolRef for the SVal in the branch condition:</div><div><br></div><div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "><span style="color: #bb2ca2">int</span> main(<span style="color: #bb2ca2">int</span> argc, <span style="color: #bb2ca2">char</span> *argv[])</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">{</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> UILabel *l = [[UILabel alloc] init];</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> <span style="color: #bb2ca2">BOOL</span> available = [l respondsToSelector:<span style="color: #bb2ca2">@selector</span>(adjustsLetterSpacingToFitWidth)]; </div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> <span style="color: #bb2ca2">if</span> (available)</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> l.adjustsLetterSpacingToFitWidth = <span style="color: #bb2ca2">YES</span>;</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> [l release];</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; color: rgb(187, 44, 162); "><span style=""><span class="Apple-tab-span" style="white-space:pre"> </span></span>return<span style=""> </span><span style="color: #272ad8">0</span><span style="">;</span></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">}</div></div><div><br></div><div>But the following code does not:</div><div><br></div><div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "><span style="color: #bb2ca2">int</span> main(<span style="color: #bb2ca2">int</span> argc, <span style="color: #bb2ca2">char</span> *argv[])</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">{</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> UILabel *l = [[UILabel alloc] init];</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> <span style="color: #bb2ca2">BOOL</span> available = [l respondsToSelector:<span style="color: #bb2ca2">@selector</span>(adjustsLetterSpacingToFitWidth)];</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> <span style="color: #bb2ca2">BOOL</span> unavailable = !available;</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> <span style="color: #bb2ca2">if</span> (available)</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> l.adjustsLetterSpacingToFitWidth = <span style="color: #bb2ca2">YES</span>;</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; "> [l release];</div><div style="margin: 0px; font-size: 14px; font-family: Monaco; min-height: 19px; "> <br class="webkit-block-placeholder"></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; color: rgb(187, 44, 162); "><span style=""><span class="Apple-tab-span" style="white-space:pre"> </span></span>return<span style=""> </span><span style="color: #272ad8">0</span><span style="">;</span></div><div style="margin: 0px; font-size: 14px; font-family: Monaco; ">}</div></div><div><br></div><div>Any condition that is a binary or unary operator seems to have an SVal with no SymbolRef. I would love to know why.</div><div><br></div><div>thanks.</div></div>_______________________________________________<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><br></blockquote></div><br></div></blockquote></div><br></div>_______________________________________________<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><br></blockquote></div><br></div></blockquote></div><br></body></html>