[cfe-dev] SymbolRef and SVal confusion

[Richard]

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
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20121220/3af190f2/attachment.html>