Error reported by incorrect association between two method invocations

[sonalmahajan15]

NilAway reports a false positive in the below example. It is incorrectly making an association between the two invocations of foo in bar and testFoo.

L91.	func foo(p *int) *int {
L92.		if p == nil {
L93.			return p
L94.		}
L95.		return new(int)
L96.	}
L97.
L98.	func bar() {
L99.		i := 1
L100.		result := foo(&i)
L101.		print(*result) // error reported on this line
L102.	}
L103.
L104.	func testFoo() {
L105.		v := foo(nil)
L106.		_ = v
L107.	}

Reported error:

Annotation on Param 0: 'p' of Function foo overconstrained:
        	Must be NILABLE because it describes the value passed as arg `p` to func `foo` at "inference/inference.go:105:11", and that value is literal nil at "inference/inference.go:105:11", where it is NILABLE
        		AND
        	Must be NONNIL because it describes the value read from the function parameter `p` of function `foo`, and that value is returned from the function `foo` in position 0 at "inference/inference.go:93:10", where it must be NONNIL because it describes the value returned as result 0 from the function `foo`, and that value is dereferenced at "inference/inference.go:101:9", where it must be NONNIL

Problem illustration with implication graph:

nil (const nil in testFoo) ----> foo param 0 ----> foo return 0 ----> nonnil (dereference in bar)

[zzqatuber]

Contract(nonnil->nonnil) will fix this because the two invocations of the same function foo will be treated separatedly.

[sonalmahajan15]

@zzqatuber, that's right, our current designing of contracts does seem a viable solution for this particular example. But for the nuanced cases where we can't infer contracts, perhaps improving the error message might be better to help the users understand the issue, like we discussed internally.

Currently, here is the message with the new format that is reported by NilAway:

Nonnil `result` expected at "inference/inference.go:101:9", but produced as nilable at "inference/inference.go:105:11". Observed nil flow from source to dereference: 
        	-> inference/inference.go:105:11: literal nil (found NILABLE)
        	-> inference/inference.go:105:11: `nil` passed as argument 0 to func `foo`
        	-> inference/inference.go:91:10: read by function parameter `p`
        	-> inference/inference.go:93:10: `p` returned from the function `foo` in position 0
        	-> inference/inference.go:100:2: result 0 of call to function `foo` assigned into `result`
        	-> inference/inference.go:101:9: `result` dereferenced (must be NONNIL)

(CC: @lazaroclapp, @yuxincs)

(EDIT: error message was copied incorrectly, fixed it)

[lazaroclapp]

(As a note: might want to revise the last few PRs and the error messages, because the chain above has some inaccurate strings, e.g. the duplicated "read from result 0 of function foo")

Ok, how do you think developers would react to something like the following:

Nonnil `result` expected at "inference/inference.go:115:9", but might have been produced as nilable at "inference/inference.go:119:11". 
Potential nil flow from source to dereference: 
        func testFoo():
        	-> inference/inference.go:119:11 literal nil (found NILABLE)
        	-> inference/inference.go:119:11: `nil` passed as argument 0 to func `foo`
        	        	v := foo(nil)
        func foo(p *int) *int:
        	-> inference/inference.go:x1:y1: therefore argument `p` (position 0) of function `foo` MUST accept nil
        	        	func foo(p *int: nilable) *int
        	-> inference/inference.go:x2:y2: read from argument `p` (position 0) of function `foo`
        	-> inference/inference.go:x2:y2: returned as result 0 of function `foo`
        	        	return p
        	-> inference/inference.go:x1:y3: therefore result 0 of function `foo` MAY return nil
        	        	func foo(p *int: nilable) *int: nilable
        func bar():
        	-> inference/inference.go:114:2: read from result 0 of function `foo`
        	        	result := foo(&i)
        	-> inference/inference.go:115:9: `result` dereferenced (must be NONNIL)
        	        	print(*result)

Note that in the above, we print the corresponding line whenever we are done with a set of messages referencing the same file and line number. For the extra messages about the formals of function foo, we print the annotated function signature instead. We could also, in rich text mode: 1) give some context lines around that line in gray, 2) highlight the nilable types in the function signature in red/blue/whatever.

In the case of an inferred contract, the above example would not report an error. But the following would:

func foo(p *int) *int {
	if p == nil {
		return p
	}
	return new(int)
}

func bar() {
	result := foo(nil)
	print(*result) // error reported on this line
}

With the explanation being something like:

Nonnil `result` expected at "inference/inference.go:114:9", but might have been produced as nilable at "inference/inference.go:_:_". 
Potential nil flow from source to dereference: 
        func bar():
        	-> inference/inference.go:113:_ literal nil (found NILABLE)
        	-> inference/inference.go:113:_: `nil` passed as argument 0 to func `foo`
        	        	result := foo(nil)
        func foo(p *int) *int:
        	-> inference/inference.go:x1:y1: therefore argument `p` (position 0) of function `foo` MUST accept nil
        	    [Note: function foo has an inferred contract]
        	        	// contract(nonnil -> nonnil)
        	        	func foo(p *int: nilable) *int
        	-> inference/inference.go:x2:y2: read from argument `p` (position 0) of function `foo`
        	-> inference/inference.go:x2:y2: returned as result 0 of function `foo`
        	        	return p
        	-> inference/inference.go:x1:y3: therefore result 0 of function `foo` MAY return nil
        	    [Note: function foo has an inferred contract]
        	        	// contract(nonnil -> nonnil)
        	        	func foo(p *int: nilable) *int: nilable
        func bar():
        	-> inference/inference.go:113:_: read from result 0 of call to function `foo` with nilable param 0
        	        	result := foo(nil)
        	-> inference/inference.go:114:9: `result` dereferenced (must be NONNIL)
        	        	print(*result)

As a side note, in this example we could potentially prune the spurious flow by noting the calls to foo(...) in the path given do not match, but I am not sure if that will break things in the general case. I suspect it will, since I don't think NilAway is set up to compute all possible nilable->nonnil flows at all, but just to look for a typing contradiction, so if we start pruning at reporting time we will create a ton of false negatives (that's my intuition, haven't spent enough time thinking about it either way)

[sonalmahajan15]

(Ah sorry, realized that I had posted the incorrect error message (the new format one). I have updated the comment with the correct message. Also, I have added corresponding line numbers to the code snippet for easy referencing.)

I think your proposal for revising the error message conveys the point we want to make, but my worry is that it is a little too verbose. Thinking if we can somehow keep the core of the message, but make it more concise....

You are right, pruning to apply to the general case could be tricky. I had tried some pruning when I was implementing the new message format, and it did not work well for all cases. But we can do some more thinking on this part too.

[zzqatuber]

Useful for debugging but for users maybe a TLDR version is better.

how do you think developers would react to something like the following

Correct. We can infer some but far from all.

I don't think NilAway is set up to compute all possible nilable->nonnil flows at all

It could be difficult to have these messages since the current implementation of contracts removes the formal parameter sites from the inference graph. Instead it directly use argument pass site.

   	-> inference/inference.go:x1:y1: therefore argument `p` (position 0) of function `foo` MUST accept nil
   	    [Note: function foo has an inferred contract]
   	        	// contract(nonnil -> nonnil)
   	        	func foo(p *int: nilable) *int
   	-> inference/inference.go:x2:y2: read from argument `p` (position 0) of function `foo`