[prev in list] [next in list] [prev in thread] [next in thread]
List: cfe-dev
Subject: Re: [cfe-dev] [analyzer] _Nonnull types and checking null constraints in checkBind
From: Artem Dergachev via cfe-dev <cfe-dev () lists ! llvm ! org>
Date: 2018-04-27 23:31:36
Message-ID: 9fd51a31-8927-8d58-2633-069b28a72434 () gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
On 4/26/18 10:12 AM, Timothy J. Wood via cfe-dev wrote:
> 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:
>
>
>
>
> 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}}
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]".
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.
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.
&... is a "memory region value" (loc::MemRegionVal) - a pointer to the
beginning of a memory region.
It's a bit weird - these classes represent different aspects of the same
thing, or different points of view to the same thing.
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).
0 is a byte offset.
'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.
>
> Thanks,
>
> -tim
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev@lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
[Attachment #5 (text/html)]
<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>
[Attachment #6 (text/plain)]
_______________________________________________
cfe-dev mailing list
cfe-dev@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic