Fix incompleteness with nil checking change

[jcp19]

PR #531 makes Gobra report a possible panic whenever a program dereferences a pointer that may be nil. The checks it added were too strict, and rejected correct programs (see the comments in that PR for examples). This PR changes what is checked and where.

Correct programs were rejected

requires  8 <= len(raw)
preserves forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> acc(&raw[i])
func DecodeFromBytes(raw []byte) {
	assert forall i int :: 0 <= i && i < len(raw[2:4]) ==>
		&raw[2:4][i] == &raw[2 + i]     // The receiver raw[2:4][i] might be nil
}

We own every element of raw, and nothing here is even a pointer that could be nil. The old check asked whether the address of the element is non-nil. Gobra computes that address by combining the offset of the sub-slice with the index, and the verifier could not relate the result to the permissions we hold, which are written in terms of raw[i].

The new check asks a simpler question: which pointer is dereferenced here, and can it be nil? In the example, none is — raw is a variable, and a slice already carries its own array — so no proof obligation is generated at all. When a pointer is dereferenced, as in p.f, the obligation is just p != nil, which is normally immediate from the surrounding specification.

Checks were reported in specifications

pred (s *Raw) Mem(buf []byte) {
	s.Base.Mem() &&                     // The receiver s.Base might be nil
	acc(&s.Raw) && ...
}

A predicate definition is not executed, so it cannot panic — and a predicate about a nil receiver can never be folded in the first place. The check nevertheless fired here, before the definition had mentioned any permission. Putting checks into specifications also changed the shape of the formulas the prover sees, which made unrelated proofs fail elsewhere. Checks are now generated only in code that actually runs; bodies of pure functions keep theirs, since a pure function that is not ghost is real code. In the future, we could disable the checks in the bodies of pure ghost functions, but we don't do it atm.

[ArquintL]

predicate about a nil receiver can never be folded in the first place

Why is that? Is this something that Gobra simply enforces (even though we technically won't have to)?

[ArquintL]

First batch of comments

[ArquintL]

what's the "root"?

[jcp19]

This was a stale comment; It's the outermost dereference, i.e. the last one evaluated (for l.next.val, the dereference of l.next) — what outermostDeref returns. Reworded.

[ArquintL]

What does it mean to use this function as the footprint of zeros-zed types and not as a runtime-panic check?

[jcp19]

A location of a zero-sized type (struct{}, [0]int, …) occupies no memory, so no permission can constitute its footprint — acc(x) would degenerate to true and an allocated *struct{} would be indistinguishable from a nil one. Gobra therefore defines the footprint of such a location to be the non-nilness of its address. So this is not an obligation imposed on a usage of the L-value (that is the other checkNotNil, which asserts before a use); it is inhaled and exhaled where the permissions of a non-zero-sized type would be: inhaled by initialization/allocate and the New encoding, exhaled and re-inhaled by assignment, and exhaled wherever acc(loc) is exhaled via ctx.footprint. The two functions used to be one, because the panic check was previously stated over &loc; now that it checks the dereferenced pointer instead, they share nothing but the name, so this one is renamed to addressNotNil and documented as above.

[jcp19]

predicate about a nil receiver can never be folded in the first place

Why is that? Is this something that Gobra simply enforces (even though we technically won't have to)?

It is a convention; we could definitely consider alternative designs.
As it stands, it is something we must enforce (and I believe we do). If you have a nil of an interface value i, you can never fold i.Mem() for the same reason you can never call a method i.M() on it: you do not have a concrete implementation of Mem to resolve to.