[cfe-dev] SymbolRef and SVal confusion
Richard
tarka.t.otter at googlemail.com
Thu Dec 20 07:29:09 PST 2012
Hey Jordan
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.
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:
if (UIAccessibilityIsGuidedAccessEnabled != NULL) {
doIOS6Stuff();
} else {
// this will not trigger a warning
doIOS6Stuff();
}
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:
ProgramStateRef StFalse = assume(State, Cond, false);
// StFalse will always be NULL here for FunctionDecl Conds
if (!StFalse) {
// We are careful to return the original state, /not/ StTrue,
// because we want to avoid having callers generate a new node
// in the ExplodedGraph.
return ProgramStatePair(State, (ProgramStateRef)NULL);
}
So when the function has not already been folded, no global state can be set, eg:
if (UIAccessibilityIsGuidedAccessEnabled) {
// this will erroneously trigger a warning as no global state was set
doIOS6Stuff();
}
Could you advise as to the best solution to this problem?
thanks,
richard
On 20 Dec 2012, at 00:42, Jordan Rose <jordan_rose at apple.com> wrote:
> 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.
>
> 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:
>
> BOOL a = ...;
> BOOL b = ...;
> if (a == b) { ... }
>
> 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.
>
> Jordan
>
>
> On Dec 19, 2012, at 15:30 , Richard <tarka.t.otter at googlemail.com> wrote:
>
>> Thank you Ted, this was very helpful. You are right about the SVal folding, they are already concrete values in the example I sent.
>>
>> ta//
>>
>> On 19 Dec 2012, at 19:03, Ted Kremenek <kremenek at apple.com> wrote:
>>
>>> Hi Richard,
>>>
>>> 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.
>>>
>>> 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.
>>>
>>> If an SVal has no SymbolRef, it means one of two things:
>>>
>>> (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:
>>>
>>>>
>>>> namespace nonloc {
>>>>
>>>> enum Kind { ConcreteIntKind, SymbolValKind,
>>>> LocAsIntegerKind, CompoundValKind, LazyCompoundValKind };
>>>
>>>
>>> and
>>>
>>>> namespace loc {
>>>>
>>>> enum Kind { GotoLabelKind, MemRegionKind, ConcreteIntKind };
>>>
>>>
>>> This is from SVals.h.
>>>
>>> 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.
>>>
>>> (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.
>>>
>>> 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:
>>>
>>> BOOL b = x > 10;
>>>
>>> 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.
>>>
>>> I hope this helps clear things up a bit. If it is still unclear, please do not hesitate to ask for more clarification.
>>>
>>> Cheers,
>>> Ted
>>>
>>> On Dec 19, 2012, at 8:45 AM, Richard <tarka.t.otter at googlemail.com> wrote:
>>>
>>>> hey
>>>>
>>>> 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.
>>>>
>>>> I find that the following code has a SymbolRef for the SVal in the branch condition:
>>>>
>>>> int main(int argc, char *argv[])
>>>> {
>>>> UILabel *l = [[UILabel alloc] init];
>>>>
>>>> BOOL available = [l respondsToSelector:@selector(adjustsLetterSpacingToFitWidth)];
>>>> if (available)
>>>> l.adjustsLetterSpacingToFitWidth = YES;
>>>>
>>>> [l release];
>>>>
>>>> return 0;
>>>> }
>>>>
>>>> But the following code does not:
>>>>
>>>> int main(int argc, char *argv[])
>>>> {
>>>> UILabel *l = [[UILabel alloc] init];
>>>>
>>>> BOOL available = [l respondsToSelector:@selector(adjustsLetterSpacingToFitWidth)];
>>>> BOOL unavailable = !available;
>>>>
>>>> if (available)
>>>> l.adjustsLetterSpacingToFitWidth = YES;
>>>>
>>>> [l release];
>>>>
>>>> return 0;
>>>> }
>>>>
>>>> Any condition that is a binary or unary operator seems to have an SVal with no SymbolRef. I would love to know why.
>>>>
>>>> thanks.
>>>> _______________________________________________
>>>> 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/20121220/357a4e02/attachment.html>
More information about the cfe-dev
mailing list