Skip to content

Commit 1efe387

Browse files
wdvxdr1123gopherbot
wdvxdr1123
authored and
gopherbot
committed
cmd/compile: teach prove about and operation
For this code: z &= 63 _ = x<<z | x>>(64-z) Now can prove 'x<<z' in bound. In ppc64 lowering pass, it will not produce an extra '(ANDconst <typ.Int64> [63] z)' causing codegen/rotate.go failed. Just remove the type check in rewrite rules as the workaround. Removes 32 bounds checks during make.bat. Fixes #52563. Change-Id: I14ed2c093ff5638dfea7de9bc7649c0f756dd71a Reviewed-on: https://go-review.googlesource.com/c/go/+/404315 Reviewed-by: Keith Randall <[email protected]> Reviewed-by: Keith Randall <[email protected]> Reviewed-by: David Chase <[email protected]> Auto-Submit: Keith Randall <[email protected]> Run-TryBot: Wayne Zuo <[email protected]> TryBot-Result: Gopher Robot <[email protected]>
1 parent 3391517 commit 1efe387

File tree

4 files changed

+49
-38
lines changed

4 files changed

+49
-38
lines changed

‎src/cmd/compile/internal/ssa/gen/PPC64.rules

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -127,20 +127,20 @@
127127

128128
// Rotate generation with non-const shift
129129
// these match patterns from math/bits/RotateLeft[32|64], but there could be others
130-
(ADD (SLD x (ANDconst <typ.Int64> [63] y)) (SRD x (SUB <typ.UInt> (MOVDconst [64]) (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
131-
(ADD (SLD x (ANDconst <typ.Int64> [63] y)) (SRD x (SUBFCconst <typ.UInt> [64] (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
132-
( OR (SLD x (ANDconst <typ.Int64> [63] y)) (SRD x (SUB <typ.UInt> (MOVDconst [64]) (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
133-
( OR (SLD x (ANDconst <typ.Int64> [63] y)) (SRD x (SUBFCconst <typ.UInt> [64] (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
134-
(XOR (SLD x (ANDconst <typ.Int64> [63] y)) (SRD x (SUB <typ.UInt> (MOVDconst [64]) (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
135-
(XOR (SLD x (ANDconst <typ.Int64> [63] y)) (SRD x (SUBFCconst <typ.UInt> [64] (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
136-
137-
138-
(ADD (SLW x (ANDconst <typ.Int32> [31] y)) (SRW x (SUBFCconst <typ.UInt> [32] (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
139-
(ADD (SLW x (ANDconst <typ.Int32> [31] y)) (SRW x (SUB <typ.UInt> (MOVDconst [32]) (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
140-
( OR (SLW x (ANDconst <typ.Int32> [31] y)) (SRW x (SUBFCconst <typ.UInt> [32] (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
141-
( OR (SLW x (ANDconst <typ.Int32> [31] y)) (SRW x (SUB <typ.UInt> (MOVDconst [32]) (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
142-
(XOR (SLW x (ANDconst <typ.Int32> [31] y)) (SRW x (SUBFCconst <typ.UInt> [32] (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
143-
(XOR (SLW x (ANDconst <typ.Int32> [31] y)) (SRW x (SUB <typ.UInt> (MOVDconst [32]) (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
130+
(ADD (SLD x (ANDconst [63] y)) (SRD x (SUB <typ.UInt> (MOVDconst [64]) (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
131+
(ADD (SLD x (ANDconst [63] y)) (SRD x (SUBFCconst <typ.UInt> [64] (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
132+
( OR (SLD x (ANDconst [63] y)) (SRD x (SUB <typ.UInt> (MOVDconst [64]) (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
133+
( OR (SLD x (ANDconst [63] y)) (SRD x (SUBFCconst <typ.UInt> [64] (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
134+
(XOR (SLD x (ANDconst [63] y)) (SRD x (SUB <typ.UInt> (MOVDconst [64]) (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
135+
(XOR (SLD x (ANDconst [63] y)) (SRD x (SUBFCconst <typ.UInt> [64] (ANDconst <typ.UInt> [63] y)))) => (ROTL x y)
136+
137+
138+
(ADD (SLW x (ANDconst [31] y)) (SRW x (SUBFCconst <typ.UInt> [32] (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
139+
(ADD (SLW x (ANDconst [31] y)) (SRW x (SUB <typ.UInt> (MOVDconst [32]) (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
140+
( OR (SLW x (ANDconst [31] y)) (SRW x (SUBFCconst <typ.UInt> [32] (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
141+
( OR (SLW x (ANDconst [31] y)) (SRW x (SUB <typ.UInt> (MOVDconst [32]) (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
142+
(XOR (SLW x (ANDconst [31] y)) (SRW x (SUBFCconst <typ.UInt> [32] (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
143+
(XOR (SLW x (ANDconst [31] y)) (SRW x (SUB <typ.UInt> (MOVDconst [32]) (ANDconst <typ.UInt> [31] y)))) => (ROTLW x y)
144144

145145

146146
// Lowering rotates

‎src/cmd/compile/internal/ssa/prove.go

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -831,6 +831,9 @@ func prove(f *Func) {
831831
case OpCtz64, OpCtz32, OpCtz16, OpCtz8, OpBitLen64, OpBitLen32, OpBitLen16, OpBitLen8:
832832
ft.update(b, v, ft.zero, signed, gt|eq)
833833
// TODO: we could also do <= 64/32/16/8, if that helped.
834+
case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
835+
ft.update(b, v, v.Args[1], unsigned, lt|eq)
836+
ft.update(b, v, v.Args[0], unsigned, lt|eq)
834837
}
835838
}
836839
}

‎src/cmd/compile/internal/ssa/rewritePPC64.go

Lines changed: 24 additions & 24 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎test/prove.go

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1036,6 +1036,14 @@ func divShiftClean32(n int32) int32 {
10361036
return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
10371037
}
10381038

1039+
func and(p []byte) ([]byte, []byte) { // issue #52563
1040+
const blocksize = 16
1041+
fullBlocks := len(p) &^ (blocksize - 1)
1042+
blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
1043+
rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
1044+
return blk, rem
1045+
}
1046+
10391047
//go:noinline
10401048
func useInt(a int) {
10411049
}

0 commit comments

Comments
 (0)