mirror of
https://github.com/golang/go
synced 2025-04-02 23:16:37 +00:00
99411d7847
Change-Id: Ia90d48ea0fab363c8592221fad88958b522edefe Reviewed-on: https://go-review.googlesource.com/c/go/+/656159 Reviewed-by: David Chase <drchase@google.com> Auto-Submit: Jorropo <jorropo.pgm@gmail.com> Reviewed-by: Keith Randall <khr@google.com> Reviewed-by: Keith Randall <khr@golang.org> LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
61 lines
1.7 KiB
Go
61 lines
1.7 KiB
Go
// errorcheck -0 -d=ssa/prove/debug=1
|
|
|
|
//go:build amd64.v3 || arm64
|
|
|
|
// Copyright 2025 The Go Authors. All rights reserved.
|
|
// Use of this source code is governed by a BSD-style
|
|
// license that can be found in the LICENSE file.
|
|
|
|
// FIXME(@Jorropo): this file exists because I havn't yet bothered to
|
|
// make prove work on the pure go function call fallback.
|
|
// My idea was to wait until CL 637936 is merged, then we can always emit
|
|
// the PopCount SSA operation and translate them to pure function calls
|
|
// in late-opt.
|
|
|
|
package main
|
|
|
|
import "math/bits"
|
|
|
|
func onesCountsBounds(x uint64, ensureAllBranchesCouldHappen func() bool) int {
|
|
z := bits.OnesCount64(x)
|
|
if ensureAllBranchesCouldHappen() && z > 64 { // ERROR "Disproved Less64$"
|
|
return 42
|
|
}
|
|
if ensureAllBranchesCouldHappen() && z <= 64 { // ERROR "Proved Leq64$"
|
|
return 4242
|
|
}
|
|
if ensureAllBranchesCouldHappen() && z < 0 { // ERROR "Disproved Less64$"
|
|
return 424242
|
|
}
|
|
if ensureAllBranchesCouldHappen() && z >= 0 { // ERROR "Proved Leq64$"
|
|
return 42424242
|
|
}
|
|
return z
|
|
}
|
|
|
|
func onesCountsTight(x uint64, ensureAllBranchesCouldHappen func() bool) int {
|
|
const maxv = 0xff0f
|
|
const minv = 0xff00
|
|
x = max(x, minv)
|
|
x = min(x, maxv)
|
|
|
|
z := bits.OnesCount64(x)
|
|
|
|
if ensureAllBranchesCouldHappen() && z > bits.OnesCount64(maxv) { // ERROR "Disproved Less64$"
|
|
return 42
|
|
}
|
|
if ensureAllBranchesCouldHappen() && z <= bits.OnesCount64(maxv) { // ERROR "Proved Leq64$"
|
|
return 4242
|
|
}
|
|
if ensureAllBranchesCouldHappen() && z < bits.OnesCount64(minv) { // ERROR "Disproved Less64$"
|
|
return 424242
|
|
}
|
|
if ensureAllBranchesCouldHappen() && z >= bits.OnesCount64(minv) { // ERROR "Proved Leq64$"
|
|
return 42424242
|
|
}
|
|
return z
|
|
}
|
|
|
|
func main() {
|
|
}
|