From: Jorropo <jorropo.pgm@gmail.com>
Date: Wed, 7 Aug 2024 18:20:21 +0000 (+0200)
Subject: cmd/compile: compute bits.Len*'s limits from argument's limits
X-Git-Tag: go1.24rc1~1064
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=0c7523ff599b56e455eee9a89cd1da9b2b2515f1;p=gostls13.git

cmd/compile: compute bits.Len*'s limits from argument's limits

Change-Id: Ie3c7e5eaba6a9a29389018625c4b784d07c6f173
Reviewed-on: https://go-review.googlesource.com/c/go/+/603537
Reviewed-by: David Chase <drchase@google.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>
---

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 87d83ba762..d2880636aa 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -1666,6 +1666,27 @@ func (ft *factsTable) flowLimit(v *Value) bool {
 			return ft.unsignedMax(v, 7)
 		}
 
+	case OpBitLen64:
+		a := ft.limits[v.Args[0].ID]
+		return ft.unsignedMinMax(v,
+			uint64(bits.Len64(a.umin)),
+			uint64(bits.Len64(a.umax)))
+	case OpBitLen32:
+		a := ft.limits[v.Args[0].ID]
+		return ft.unsignedMinMax(v,
+			uint64(bits.Len32(uint32(a.umin))),
+			uint64(bits.Len32(uint32(a.umax))))
+	case OpBitLen16:
+		a := ft.limits[v.Args[0].ID]
+		return ft.unsignedMinMax(v,
+			uint64(bits.Len16(uint16(a.umin))),
+			uint64(bits.Len16(uint16(a.umax))))
+	case OpBitLen8:
+		a := ft.limits[v.Args[0].ID]
+		return ft.unsignedMinMax(v,
+			uint64(bits.Len8(uint8(a.umin))),
+			uint64(bits.Len8(uint8(a.umax))))
+
 	// Masks.
 	case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
 		// AND can only make the value smaller.
diff --git a/test/prove.go b/test/prove.go
index 32096eafff..3c8395c7f5 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -8,7 +8,10 @@
 
 package main
 
-import "math"
+import (
+	"math"
+	"math/bits"
+)
 
 func f0(a []int) int {
 	a[0] = 1
@@ -1193,6 +1196,103 @@ func f22(b bool, x, y int) int {
 	return 0
 }
 
+func bitLen64(x uint64, ensureBothBranchesCouldHappen bool) int {
+	const max = math.MaxUint64
+	sz := bits.Len64(max)
+
+	if x >= max>>3 {
+		return 42
+	}
+	if x <= max>>6 {
+		return 42
+	}
+
+	y := bits.Len64(x)
+
+	if ensureBothBranchesCouldHappen {
+		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
+			return -42
+		}
+	} else {
+		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
+			return 1337
+		}
+	}
+	return y
+}
+func bitLen32(x uint32, ensureBothBranchesCouldHappen bool) int {
+	const max = math.MaxUint32
+	sz := bits.Len32(max)
+
+	if x >= max>>3 {
+		return 42
+	}
+	if x <= max>>6 {
+		return 42
+	}
+
+	y := bits.Len32(x)
+
+	if ensureBothBranchesCouldHappen {
+		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
+			return -42
+		}
+	} else {
+		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
+			return 1337
+		}
+	}
+	return y
+}
+func bitLen16(x uint16, ensureBothBranchesCouldHappen bool) int {
+	const max = math.MaxUint16
+	sz := bits.Len16(max)
+
+	if x >= max>>3 {
+		return 42
+	}
+	if x <= max>>6 {
+		return 42
+	}
+
+	y := bits.Len16(x)
+
+	if ensureBothBranchesCouldHappen {
+		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
+			return -42
+		}
+	} else {
+		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
+			return 1337
+		}
+	}
+	return y
+}
+func bitLen8(x uint8, ensureBothBranchesCouldHappen bool) int {
+	const max = math.MaxUint8
+	sz := bits.Len8(max)
+
+	if x >= max>>3 {
+		return 42
+	}
+	if x <= max>>6 {
+		return 42
+	}
+
+	y := bits.Len8(x)
+
+	if ensureBothBranchesCouldHappen {
+		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
+			return -42
+		}
+	} else {
+		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
+			return 1337
+		}
+	}
+	return y
+}
+
 //go:noinline
 func useInt(a int) {
 }