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

cmd/compile: in prove.go:addLocalFacts ft.update propagates limits depends on value ordering and can't propagate ft.updateft.flowLimit dependencies #68857

Open
Jorropo opened this issue Aug 13, 2024 · 3 comments
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Performance
Milestone

Comments

@Jorropo
Copy link
Member

Jorropo commented Aug 13, 2024

Go version

go1.24-793b14b455

Output of go env in your module/workspace:

GO111MODULE=''
GOARCH='amd64'
GOBIN=''
GOCACHE='/tmp/go-build'
GOENV='/home/hugo/.config/go/env'
GOEXE=''
GOEXPERIMENT='rangefunc'
GOFLAGS=''
GOHOSTARCH='amd64'
GOHOSTOS='linux'
GOINSECURE=''
GOMODCACHE='/home/hugo/go/pkg/mod'
GONOPROXY=''
GONOSUMDB=''
GOOS='linux'
GOPATH='/home/hugo/go'
GOPRIVATE=''
GOPROXY='https://proxy.golang.org,direct'
GOROOT='/home/hugo/k/go'
GOSUMDB='sum.golang.org'
GOTMPDIR=''
GOTOOLCHAIN='local'
GOTOOLDIR='/home/hugo/k/go/pkg/tool/linux_amd64'
GOVCS=''
GOVERSION='devel go1.24-793b14b455 Tue Aug 13 17:23:56 2024 +0200 X:rangefunc'
GODEBUG=''
GOTELEMETRY='local'
GOTELEMETRYDIR='/home/hugo/.config/go/telemetry'
GCCGO='/usr/bin/gccgo'
GOAMD64='v3'
AR='ar'
CC='gcc'
CXX='g++'
CGO_ENABLED='1'
GOMOD='/home/hugo/k/go/src/go.mod'
GOWORK=''
CGO_CFLAGS='-O2 -g'
CGO_CPPFLAGS=''
CGO_CXXFLAGS='-O2 -g'
CGO_FFLAGS='-O2 -g'
CGO_LDFLAGS='-O2 -g'
PKG_CONFIG='pkg-config'
GOGCCFLAGS='-fPIC -m64 -pthread -Wl,--no-gc-sections -fmessage-length=0 -ffile-prefix-map=/tmp/go-build127661744=/tmp/go-build -gno-record-gcc-switches'

What did you do?

Add theses in test/prove.go and run:

func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
	a &= 0xff
	b &= 0xfff

	z := bits.Len64(a % b)

	if ensureBothBranchesCouldHappen {
		if z > bits.Len64(0xff) { // ERROR "Disproved Less64$"
			return 42
		}
	} else {
		if z <= bits.Len64(0xff) { // ERROR "Proved Leq64$"
			return 1337
		}
	}
	return z
}
func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
	a &= 0xfff
	b &= 0x10 // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)

	z := bits.Len64(a % b)

	if ensureBothBranchesCouldHappen {
		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
			return 42
		}
	} else {
		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
			return 1337
		}
	}
	return z
}
func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
	a &= 0x10
	b &= 0x10 // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)

	z := bits.Len64(a % b)

	if ensureBothBranchesCouldHappen {
		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
			return 42
		}
	} else {
		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
			return 1337
		}
	}
	return z
}

What did you see happen?

--- FAIL: Test (0.02s)
    --- FAIL: Test/prove.go (0.31s)
        testdir_test.go:145: 
            prove.go:1436: missing error "Disproved Less64$"
            prove.go:1440: missing error "Proved Leq64$"
            prove.go:1453: missing error "Disproved Less64$"
            prove.go:1457: missing error "Proved Leq64$"
            prove.go:1470: missing error "Disproved Less64$"
            prove.go:1474: missing error "Proved Leq64$"
            
FAIL
FAIL	cmd/internal/testdir	0.336s
FAIL

What did you expect to see?

ok  	cmd/internal/testdir	0.350s
@gopherbot gopherbot added the compiler/runtime Issues related to the Go compiler and/or runtime. label Aug 13, 2024
@Jorropo
Copy link
Member Author

Jorropo commented Aug 13, 2024

cc @randall77

@gopherbot
Copy link
Contributor

Change https://go.dev/cl/605156 mentions this issue: cmd/compile: compute Modu's maximum limits from argument's limits

@cagedmantis cagedmantis added the NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. label Aug 14, 2024
@cagedmantis cagedmantis added this to the Backlog milestone Aug 14, 2024
gopherbot pushed a commit that referenced this issue Sep 3, 2024
addLocalFacts loop already ft.update which sets up limits correctly, but doing this in flowLimit help us since other values might depend on this limit.

Updates #68857

We could improve this further:
- remove mod alltogheter when we can prove a < b.
- we could do more adhoc computation in flowLimit to set umax and umin tighter

Change-Id: I5184913577b6a51a07cb53a6e6b73552a982de0b
Reviewed-on: https://go-review.googlesource.com/c/go/+/605156
Reviewed-by: Keith Randall <[email protected]>
Reviewed-by: David Chase <[email protected]>
Reviewed-by: Keith Randall <[email protected]>
LUCI-TryBot-Result: Go LUCI <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Performance
Projects
Development

No branches or pull requests

5 participants