[cfe-dev] [analyzer] _Nonnull types and checking null constraints in checkBind

[Artem Dergachev via cfe-dev]

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 at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180427/1ca979ab/attachment.html>