diff options
| author | Jorropo <jorropo.pgm@gmail.com> | 2025-10-25 09:25:27 +0200 |
|---|---|---|
| committer | Gopher Robot <gobot@golang.org> | 2025-10-27 19:08:00 -0700 |
| commit | 77dc1380308f5129952c16b6940dea7ddd4e17b9 (patch) | |
| tree | 4cc336a8786000b4200d9c0b6123e281c1a6794f /src/cmd/compile | |
| parent | a0f33b28878817546fa6233f9701672482e39834 (diff) | |
| download | go-77dc1380308f5129952c16b6940dea7ddd4e17b9.tar.xz | |
cmd/compile: teach prove about unsigned rounding-up divide
Change-Id: Ia7b5242c723f83ba85d12e4ca64a19fbbd126016
Reviewed-on: https://go-review.googlesource.com/c/go/+/714622
Auto-Submit: Jorropo <jorropo.pgm@gmail.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>
Diffstat (limited to 'src/cmd/compile')
| -rw-r--r-- | src/cmd/compile/internal/ssa/prove.go | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 5a9e0a65c7..168bb29984 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -2473,6 +2473,41 @@ func addLocalFacts(ft *factsTable, b *Block) { OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8, OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8, OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8: + switch add := v.Args[0]; add.Op { + // round-up division pattern; given: + // v = (x + y) / z + // if y < z then v <= x + case OpAdd64, OpAdd32, OpAdd16, OpAdd8: + z := v.Args[1] + zl := ft.limits[z.ID] + var uminDivisor uint64 + switch v.Op { + case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u: + uminDivisor = zl.umin + case OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8, + OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8, + OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8, + OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8: + uminDivisor = 1 << zl.umin + default: + panic("unreachable") + } + + x := add.Args[0] + xl := ft.limits[x.ID] + y := add.Args[1] + yl := ft.limits[y.ID] + if unsignedAddOverflows(xl.umax, yl.umax, add.Type) { + continue + } + + if xl.umax < uminDivisor { + ft.update(b, v, y, unsigned, lt|eq) + } + if yl.umax < uminDivisor { + ft.update(b, v, x, unsigned, lt|eq) + } + } ft.update(b, v, v.Args[0], unsigned, lt|eq) case OpMod64, OpMod32, OpMod16, OpMod8: a := ft.limits[v.Args[0].ID] |