False positive in checking nilabilty of slice using `len(s)` assigned to a variable

[sonalmahajan15]

The following code reports a false positive.

func test(mp map[string][]*int) {
	sl := mp["foo"]
	slLen := len(sl)
	if slLen == 0 {
		return
	}
	_ = sl[0] // FP: error: deep read from parameter `mp` lacking guarding; sliced
}

However, using len directly in the condition works as expected, reporting no error.

func test(mp map[string][]*int) {
	sl := mp["foo"]
	if len(sl) == 0 {
		return
	}
	_ = sl[0]
}

[abhinav]

Similar issue in Zap. nilaway found this:

[..]/zap/buffer/buffer.go:136:11: error: Potential nil panic detected. Observed nil flow from source to dereference point:
        -> strconv/itoa.go:200:2: unassigned variable `d` returned from `formatBits()` via named return `d`
        -> strconv/itoa.go:45:9: result 0 of `formatBits()` returned from `AppendInt()` in position 0
        -> buffer/buffer.go:57:9: result 0 of `AppendInt()` assigned into field `bs`
        -> buffer/buffer.go:136:11: field `bs` sliced into

Code: https://github.com/uber-go/zap/blob/f69ffe389b030fad13633c0ef1166528aec7994c/buffer/buffer.go#L133-L134

However, if len(slice) - 1 >= 0, then len(slice) > 0 so it should infer that the slice is non-nil.

Changing that snippet to the following resolves the issue:

	if len(b.bs) > 0 {
		i := len(b.bs) - 1
		// ...

[sonalmahajan15]

@abhinav, thanks for reporting this. :) We'll try and add support for this soon.

[lazaroclapp]

However, if len(slice) - 1 >= 0, then len(slice) > 0 so it should infer that the slice is non-nil.

Just to set expectations a bit here, while we are happy to build heuristics for common cases, in the limit NilAway shouldn't be expected to reason about arbitrarily complex integer arithmetic. This is a type system for nilability and that sort of thing is the domain of SMT solvers.

I do think x-1 >= 0 => x > 0 can be special cased, though! 😅

I just wouldn't expect say, this, to ever work:

j := len(b.bs)
i := (j - 1) % 2
if i >= 0 {
  b.bs[i] = ...
}

Even though, of course, it's equally safe (len(nil) = 0 => i = (0-1) % 2 = -1).

In theory a tool can be built that reasons about whether values can contain nil and the possible value ranges of every integer variable in the program, but the later is a harder problem than the former.

[abhinav]

Thanks, @lazaroclapp, that's completely reasonable.

I'm aware that not requiring code annotations was one of the goals of nilaway, but just thinking out loud: Would there be room in the system to annotate code with comments for these corner cases?

For example, for the Zap function above:

func (b *Buffer) TrimNewline() {
	if i := len(b.bs) - 1; i >= 0 {
		if b.bs[i] == '\n' {
			b.bs = b.bs[:i]
		}
	}
}

If authors could do something like this, informing nilaway that that condition implies something about the result:

if i := len(b.bs) - 1; i >= 0 {
	// @implies:not-nil(b.bs) // i > 0 guarantees b.bs is non-nil
	if b.bs[i] == '\n' {
		// ...
	}
}

Then nilaway wouldn't have to worry about special-casing arbitrary arithmetic and other special cases that nilaway shouldn't have to handle.