Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
BarrensZeppelin opened this issue Nov 23, 2022 · 5 comments
Closed

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

BarrensZeppelin opened this issue Nov 23, 2022 · 5 comments
Labels
help wanted NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Tools This label describes issues relating to any tools in the x/tools repository.
Milestone
Unreleased

Comments

@BarrensZeppelin
Copy link

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
}
@gopherbot gopherbot added the Tools This label describes issues relating to any tools in the x/tools repository. label Nov 23, 2022
@gopherbot gopherbot added this to the Unreleased milestone Nov 23, 2022
@cherrymui cherrymui added the NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. label Nov 23, 2022
@cherrymui
Copy link
Member

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

@timothy-king
Copy link
Contributor

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
Copy link
Author

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
Copy link

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

@adonovan
Copy link
Member

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
help wanted NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Tools This label describes issues relating to any tools in the x/tools repository.
Projects
None yet
Milestone
Unreleased
Development

No branches or pull requests
6 participants
@timothy-king @BarrensZeppelin @adonovan @gopherbot @cherrymui @danvolchek