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

[Devin Coughlin via cfe-dev]

> On Apr 26, 2018, at 10:26 AM, Gábor Horváth via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hi!
> 
> This is a philosophical question to some extent. I think what _Nonnull means at the return value is that in case all the preconditions of a function is met the result will never be null.
> So in case a function has a _Nonnull parameter and a _Nonnull return value and the caller passes null, the function is free to return null.
> 
> Of course, passing null to this function was an error in the first place.
> 
> There is a tradeoff, constraining these values to not being null will reduce the coverage and lots of the errors found by the analyzer are actually in the error handling code.
> But having this information might increase the precision of the analysis.
> 
> I think the reason why it was developed that way there were lots of legacy APIs where the clients relied on the behavior that a _Nonnull function (which was not annotated
> in the past of course,) returns null when its precondition is not met.
> 
> Maybe people started to fix such code and now it makes sense to change this behavior?

For anything that represents input to a framework we don’t want to change this behavior. This is because the implementation of frameworks must remain robust against, for example, clients passing in nil to a parameter marked as nonnull. If we were to model such parameters as constrained to be non-zero then the analyzer would never cover the defensive code paths that make the framework robust (since it would think that they are not feasible). However, defensive code paths are less likely to be covered and tested — so these are exactly the paths that benefit the most from static analysis!

More broadly speaking, as Gabor notes, the meaning of ‘_Nonnull’ in parameter and return types is not ‘this value can never be nil’ but rather a more complex contract between caller and callee in which the callee promises to respect _Nonnull in its outputs as long as the caller respected it for the passed-in inputs. This kind of nuance is the inevitable result of adding more expressive types to a language where there is a large body of code developed without those types enforced.

Devin


> 
> Regards,
> Gábor
> 
> On 26 April 2018 at 19:12, Timothy J. Wood via cfe-dev <cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>> 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}}
> 
> Thanks,
> 
> -tim
> 
> 
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev <http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev>
> 
> 
> _______________________________________________
> 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/2c453ae0/attachment.html>