Not clear whether pointers to empty structs/slices have same semantics as go

[lredlin]

I had trouble proving that a points-to for a value that happens to be an empty type is not null. It seems that we are modelling this in a way that could allow verifying nonnull in that case but whether Go uses an arbitrary nonnull pointer is something worth investigating. This is no longer applicable to my proof but could come up again in the future so filing an issue

[tchajed]

I did the investigation into this.

• Go constructs non-nil pointers to empty structs: https://go.dev/play/p/yi6y9fmmmhR
• mem.alloc v is just ref v which is just AllocN 1 v. The semantics of this operation is to create a new block in the heap (in the same sense as the CompCert memory model) whose contents are flatten_struct v, even if that ends up being empty. Thus the semantics do create a non-null pointer.
• new goose's wp_ref calls wp_alloc1_seq. This gives pointsto_vals, which is just [* list] over the flatten_struct elements and thus forgets that the base pointer is non-null.

To summarize, the semantics are correct, but the proof principles are too weak from the first lifting lemma.

[upamanyus]

I think the Perennial semantics is technically wrong. The current semantics always gives allocations a fresh address, which does always happen with compiled Go code. E.g. https://go.dev/play/p/rVZAlPFuaBD shows that two different zero-sized objects can have different addresses. However, simply enabling the print statement as in https://go.dev/play/p/u0nwPu42bZd results in the two objects having the same address.

I have not found anything in the Go specification to clarify this.

[tchajed]

The spec actually does say this:

Pointer types are comparable. Two pointer values are equal if they point to the same variable or if both have value nil. Pointers to distinct zero-size variables may or may not be equal.

So we should make comparisons on pointers to zero-sized structs non-deterministic (that is, arbitrary booleans), unless one of them is nil.