Update to go1.25.0
This commit is contained in:
393
test/prove.go
393
test/prove.go
@@ -1391,8 +1391,8 @@ func bitLen8(x uint8, ensureBothBranchesCouldHappen bool) int {
|
||||
}
|
||||
|
||||
func xor64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
|
||||
a &= 0xff
|
||||
b &= 0xfff
|
||||
a = min(a, 0xff)
|
||||
b = min(b, 0xfff)
|
||||
|
||||
z := a ^ b
|
||||
|
||||
@@ -1409,8 +1409,8 @@ func xor64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
|
||||
}
|
||||
|
||||
func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
|
||||
a &= 0xff
|
||||
b &= 0xfff
|
||||
a = min(a, 0xff)
|
||||
b = min(b, 0xfff)
|
||||
|
||||
z := a | b
|
||||
|
||||
@@ -1427,8 +1427,8 @@ func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
|
||||
}
|
||||
|
||||
func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
|
||||
a &= 0xff
|
||||
b &= 0xfff
|
||||
a = min(a, 0xff)
|
||||
b = min(b, 0xfff)
|
||||
|
||||
z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
|
||||
|
||||
@@ -1444,8 +1444,8 @@ func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen boo
|
||||
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)
|
||||
a = min(a, 0xfff)
|
||||
b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
|
||||
|
||||
z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
|
||||
|
||||
@@ -1461,8 +1461,8 @@ func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool
|
||||
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)
|
||||
a = min(a, 0x10)
|
||||
b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
|
||||
|
||||
z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
|
||||
|
||||
@@ -1481,8 +1481,8 @@ func mod64sPositiveWithSmallerDividendMax(a, b int64, ensureBothBranchesCouldHap
|
||||
if a < 0 || b < 0 {
|
||||
return 42
|
||||
}
|
||||
a &= 0xff
|
||||
b &= 0xfff
|
||||
a = min(a, 0xff)
|
||||
b = min(b, 0xfff)
|
||||
|
||||
z := a % b // ERROR "Proved Mod64 does not need fix-up$"
|
||||
|
||||
@@ -1501,8 +1501,8 @@ func mod64sPositiveWithSmallerDivisorMax(a, b int64, ensureBothBranchesCouldHapp
|
||||
if a < 0 || b < 0 {
|
||||
return 42
|
||||
}
|
||||
a &= 0xfff
|
||||
b &= 0xff
|
||||
a = min(a, 0xfff)
|
||||
b = min(b, 0xff)
|
||||
|
||||
z := a % b // ERROR "Proved Mod64 does not need fix-up$"
|
||||
|
||||
@@ -1521,8 +1521,8 @@ func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bo
|
||||
if a < 0 || b < 0 {
|
||||
return 42
|
||||
}
|
||||
a &= 0xfff
|
||||
b &= 0xfff
|
||||
a = min(a, 0xfff)
|
||||
b = min(b, 0xfff)
|
||||
|
||||
z := a % b // ERROR "Proved Mod64 does not need fix-up$"
|
||||
|
||||
@@ -1539,10 +1539,10 @@ func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bo
|
||||
}
|
||||
|
||||
func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
|
||||
a &= 0xffff
|
||||
a |= 0xfff
|
||||
b &= 0xff
|
||||
b |= 0xf
|
||||
a = min(a, 0xffff)
|
||||
a = max(a, 0xfff)
|
||||
b = min(b, 0xff)
|
||||
b = max(b, 0xf)
|
||||
|
||||
z := a / b // ERROR "Proved Neq64$"
|
||||
|
||||
@@ -1564,10 +1564,10 @@ func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
|
||||
if a < 0 || b < 0 {
|
||||
return 42
|
||||
}
|
||||
a &= 0xffff
|
||||
a |= 0xfff
|
||||
b &= 0xff
|
||||
b |= 0xf
|
||||
a = min(a, 0xffff)
|
||||
a = max(a, 0xfff)
|
||||
b = min(b, 0xff)
|
||||
b = max(b, 0xf)
|
||||
|
||||
z := a / b // ERROR "(Proved Div64 does not need fix-up|Proved Neq64)$"
|
||||
|
||||
@@ -1587,8 +1587,8 @@ func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
|
||||
}
|
||||
|
||||
func trunc64to16(a uint64, ensureAllBranchesCouldHappen func() bool) uint16 {
|
||||
a &= 0xfff
|
||||
a |= 0xff
|
||||
a = min(a, 0xfff)
|
||||
a = max(a, 0xff)
|
||||
|
||||
z := uint16(a)
|
||||
if ensureAllBranchesCouldHappen() && z > 0xfff { // ERROR "Disproved Less16U$"
|
||||
@@ -1607,8 +1607,8 @@ func trunc64to16(a uint64, ensureAllBranchesCouldHappen func() bool) uint16 {
|
||||
}
|
||||
|
||||
func com64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
|
||||
a &= 0xffff
|
||||
a |= 0xff
|
||||
a = min(a, 0xffff)
|
||||
a = max(a, 0xff)
|
||||
|
||||
z := ^a
|
||||
|
||||
@@ -1629,8 +1629,8 @@ func com64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
|
||||
|
||||
func neg64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
|
||||
var lo, hi uint64 = 0xff, 0xfff
|
||||
a &= hi
|
||||
a |= lo
|
||||
a = min(a, hi)
|
||||
a = max(a, lo)
|
||||
|
||||
z := -a
|
||||
|
||||
@@ -1650,8 +1650,8 @@ func neg64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
|
||||
}
|
||||
func neg64mightOverflowDuringNeg(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
|
||||
var lo, hi uint64 = 0, 0xfff
|
||||
a &= hi
|
||||
a |= lo
|
||||
a = min(a, hi)
|
||||
a = max(a, lo)
|
||||
|
||||
z := -a
|
||||
|
||||
@@ -1691,6 +1691,317 @@ func phiMin(a, b []byte) {
|
||||
_ = b[:y] // ERROR "Proved IsSliceInBounds"
|
||||
}
|
||||
|
||||
func minPhiLeq[T uint | int](x, y T) (z T) {
|
||||
if x <= y {
|
||||
z = x
|
||||
} else {
|
||||
z = y
|
||||
}
|
||||
return z
|
||||
}
|
||||
func maxPhiLeq[T uint | int](x, y T) (z T) {
|
||||
if y <= x {
|
||||
z = x
|
||||
} else {
|
||||
z = y
|
||||
}
|
||||
return z
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinUFirstLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = minPhiLeq(x, maxc)
|
||||
x = maxPhiLeq(x, minc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinUSecondLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = maxPhiLeq(x, minc)
|
||||
x = minPhiLeq(x, maxc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinFirstLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = minPhiLeq(x, maxc)
|
||||
x = maxPhiLeq(x, minc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinSecondLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = maxPhiLeq(x, minc)
|
||||
x = minPhiLeq(x, maxc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
|
||||
func minPhiLess[T uint | int](x, y T) (z T) {
|
||||
if x < y {
|
||||
z = x
|
||||
} else {
|
||||
z = y
|
||||
}
|
||||
return z
|
||||
}
|
||||
func maxPhiLess[T uint | int](x, y T) (z T) {
|
||||
if y < x {
|
||||
z = x
|
||||
} else {
|
||||
z = y
|
||||
}
|
||||
return z
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinUFirstLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = minPhiLess(x, maxc)
|
||||
x = maxPhiLess(x, minc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinUSecondLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = maxPhiLess(x, minc)
|
||||
x = minPhiLess(x, maxc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinFirstLess(x int, ensureAllBranchesCouldHappen func() bool) int {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = minPhiLess(x, maxc)
|
||||
x = maxPhiLess(x, minc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiLosangeMinSecondLess(x int, ensureAllBranchesCouldHappen func() bool) int {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = maxPhiLess(x, minc)
|
||||
x = minPhiLess(x, maxc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
|
||||
func mathBasedOnPhiBuiltinMinUFirst(x uint, ensureAllBranchesCouldHappen func() bool) uint {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = min(x, maxc)
|
||||
x = max(x, minc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiBuiltinMinUSecond(x uint, ensureAllBranchesCouldHappen func() bool) uint {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = max(x, minc)
|
||||
x = min(x, maxc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiBuiltinMinFirst(x int, ensureAllBranchesCouldHappen func() bool) int {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = min(x, maxc)
|
||||
x = max(x, minc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
func mathBasedOnPhiBuiltinMinSecond(x int, ensureAllBranchesCouldHappen func() bool) int {
|
||||
const maxc = 0xf2a
|
||||
const minc = 0xf0a
|
||||
x = max(x, minc)
|
||||
x = min(x, maxc)
|
||||
|
||||
const k = 1
|
||||
x += k
|
||||
|
||||
if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
|
||||
return 42
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
|
||||
return 4242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
|
||||
return 424242
|
||||
}
|
||||
if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
|
||||
return 42424242
|
||||
}
|
||||
return x
|
||||
}
|
||||
|
||||
func issue16833(a, b []byte) {
|
||||
n := copy(a, b)
|
||||
_ = a[n:] // ERROR "Proved IsSliceInBounds"
|
||||
@@ -1712,6 +2023,24 @@ func clampedIdx2(x []int, i int) int {
|
||||
return x[max(min(i, len(x)-1), 0)] // TODO: can't get rid of this bounds check yet
|
||||
}
|
||||
|
||||
func cvtBoolToUint8Disprove(b bool) byte {
|
||||
var c byte
|
||||
if b {
|
||||
c = 1
|
||||
}
|
||||
if c == 2 { // ERROR "Disproved Eq8"
|
||||
c = 3
|
||||
}
|
||||
return c
|
||||
}
|
||||
func cvtBoolToUint8BCE(b bool, a [2]int64) int64 {
|
||||
c := byte(0)
|
||||
if b {
|
||||
c = 1
|
||||
}
|
||||
return a[c] // ERROR "Proved IsInBounds$"
|
||||
}
|
||||
|
||||
//go:noinline
|
||||
func useInt(a int) {
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user