x/tools/go/pointer: sound models of sync/atomic Pointer[T] and Value

[BarrensZeppelin]

It would be nice to have sound pointer analysis models of the atomic primitives that contain pointers.
Currently the pointer analysis unsoundly ignores their use.

A failing test pointer analysis test go/pointer/testdata/atomic_value.go could be:

//go:build ignore
// +build ignore

package main

import "sync/atomic"

var g1 int

func main() {
	var v atomic.Value
	print(v.Load()) // @types
	v.Store(&g1)
	x := v.Load().(*int)
        // Fails because the points-to set of x is empty.
	print(x) // @pointsto command-line-arguments.g1
}

[cherrymui]

cc @timothy-king @zpavlinovic @golang/tools-team

[timothy-king]

sync.atomic.{Pointer[T],Value} are implemented using unsafe.Pointer internally (Pointer and Value.Store code). This is a documented soundness limitation of the pointer package (doc). This is consistent with the points to set of x being empty.

This can be resolved by modeling the both as intrinsics in go/pointer/intrinsics.go. Work on this is currently unplanned by the Go team. This is a good opportunity for a community contribution.

[BarrensZeppelin]

Yeah, I think the correct thing to do is to model the behaviour with intrinsics.

The semantics are conceptually simple to model, for example in (av *atomic.Value).Store(x any) the value of the argument flows to the struct field av.v. However, implementing this seems to require strong knowledge of the internals of the pointer analysis, which I currently lack. Otherwise I would've been glad to contribute the models myself. 🙂

[danvolchek]

I'd like to work on this - I'll give it a shot!

[adonovan]

x/tools/go/pointer was deleted; see #59676.