<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<br>
<br>
<div class="moz-cite-prefix">On 4/26/18 10:12 AM, Timothy J. Wood
via cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:94339239-057E-433F-897C-603C6FFD2C24@omnigroup.com">
<pre class="moz-quote-pre" wrap="">
While working on my outError-writing checker, I thought I’d try to use as much of the built-in checker support for tracking which values/regions are marked a non-null as possible rather than adding tracking of every `NSError *` in my own state.
The tl;dr version of the rest of this is whether the analyzer will mark a _Nonnull result as being constrained to nonnull.
Here is what I’m doing, which makes it seem like the answer is “no”, but maybe I’m doing it wrong...
In my test input I have something like:
@interface NSError : NSObject <NSCopying, NSCoding> {}
+ (instancetype _Nonnull)make; // convenient fiction to make exploded graph smaller while debugging
@end
...
- (BOOL)failWithErrorLocal:(NSError **)outError;
{
NSError *e = [NSError make];
if (outError) {
*outError = e;
}
return NO;
}
Since +make is marked as returning a nonnull result, I was expecting/hoping the checkBind call for that assignment to have a r-value that was constrained to nonnull (and that this would get propagated to *outError if the body of the `if` was executed). But, in my checkBind(), if I do:
dmsg << " Val " << Val << "\n";
ConditionTruthVal IsNull = State->isNull(Val);
dmsg << " IsNull.isConstrained() " << IsNull.isConstrained() << "\n";
dmsg << " IsNull.isConstrainedTrue() " << IsNull.isConstrainedTrue() << "\n”;
I see:
Val &SymRegion{conj_$4{id _Nonnull}}
IsNull.isConstrained() 0
IsNull.isConstrainedTrue() 0
If I set a breakpoint on my checkBind() and then finish out to ExprEngine::VisitDeclStmt, I get a exploded graph dot file like:
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">
I’m still not really sure how to read these, but can see that it has bound the local `e` to the nonnull result of +make:
(e,0,direct) : &SymRegion{conj_$4{NSError * _Nonnull}}</pre>
</blockquote>
<br>
This is deciphered as follows: "A certain number of bytes of
variable 'e' of the current stack frame, starting from the byte at
offset 0, represent a pointer with a symbolic numeric value of type
'NSError * _Nonnull' that denotes the unknown return value of
[NSError make]".<br>
<br>
conj_$4{NSError * _Nonnull} is a "conjured symbol" (SymbolConjured)
- an atomic symbol that represents a value of an expression for
which we didn't have any better representation. It contains a
reference to the AST expression within itself, even though it
doesn't dump() it.<br>
<br>
SymRegion{...} is a "symbolic region" (SymbolicRegion) - a segment
of memory that corresponds to a certain symbolic numeric value. The
address of the start of the segment is equal to that numeric value.
The length of the segment is assumed to be unknown.<br>
<br>
&... is a "memory region value" (loc::MemRegionVal) - a pointer
to the beginning of a memory region.<br>
<br>
It's a bit weird - these classes represent different aspects of the
same thing, or different points of view to the same thing.<br>
<br>
e is a "variable region" (VarRegion) that represents a segment of
memory that corresponds to a variable. The same local variable
within different calls to the same function will be represented by
different VarRegions (which is especially important during
recursion).<br>
<br>
0 is a byte offset.<br>
<br>
'direct' means that there's only one binding of this value; the
binding affects only that immediate offset. It's pretty technical.
The antonym is 'default' which would represent that the region is
wiped clean with many instances of the same binding starting from
this offset. This is a performance optimization in the analyzer that
doesn't require us to make 1000 bindings to indicate that calloc()
or memset() zero-initializes an array of 1000 elements - we just
make one "default" binding. Some other tricks rely on that as well.<br>
<br>
<blockquote type="cite"
cite="mid:94339239-057E-433F-897C-603C6FFD2C24@omnigroup.com">
<pre class="moz-quote-pre" wrap="">
Thanks,
-tim
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>