Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cmd/compile: prove pass disabled on int32/int64 #29964

Closed
rsc opened this issue Jan 28, 2019 · 15 comments

Comments

@rsc
Copy link
Contributor

commented Jan 28, 2019

Consider this program:

package p

func f(x []int, j int) int {
	if x[j] != 0 {
		return 1
	}
	if j > 0 && x[j-1] != 0 {
		return 1
	}
	return 0
}

The bounds check for x[j-1] can be eliminated: at that point, x[j] did not panic, so j < len(x), and the if statement has also tested j > 0, so 0 <= j-1 < len(x).

The compiler does eliminate this check:

$ go tool compile -S x.go |grep panicindex
	0x006e 00110 (x.go:4)	CALL	runtime.panicindex(SB)
	rel 111+4 t=8 runtime.panicindex+0
$ 

But if I change j to be int32 then the check is not eliminated:

package p

func f(x []int, j int32) int {
	if x[j] != 0 {
		return 1
	}
	if j > 0 && x[j-1] != 0 {
		return 1
	}
	return 0
}
$ go tool compile -S x.go |grep panicindex
	0x0078 00120 (x.go:7)	CALL	runtime.panicindex(SB)
	0x007f 00127 (x.go:4)	CALL	runtime.panicindex(SB)
	rel 121+4 t=8 runtime.panicindex+0
	rel 128+4 t=8 runtime.panicindex+0
$

Is this necessary? /cc @aclements

@rsc rsc added this to the Go1.13 milestone Jan 28, 2019

@mvdan mvdan added the Performance label Jan 28, 2019

@randall77

This comment has been minimized.

Copy link
Contributor

commented Jan 28, 2019

I think this is probably because we extend indexes to int width before we do the bounds check.

The code in ssa.go for OINDEX does:

			i = s.extendIndex(i, panicindex)
			if !n.Bounded() {
				len := s.newValue1(ssa.OpStringLen, types.Types[TINT], a)
				s.boundsCheck(i, len)
			}

extendindex will insert an int32->int cast. So the bounds check is not on the int32, but the int.

The extra cast probably makes the prove pass give up, because it can't go from j>0 to int(j-1)>=0.

We could do the bounds check before the extension. That would fix this problem, probably. I'm not sure what else it would do. Probably it would be fine, it was just easier when first implementing ssa to only deal with one index type during bounds check generation.

We do need extendindex regardless, as we need a full register of index for indexed loads.

@mvdan

This comment has been minimized.

Copy link
Member

commented Jan 28, 2019

If the only problem here is the prove pass's handling of integer extensions, that's #26292, which has had a CL semi-ready for a while.

@rsc

This comment has been minimized.

Copy link
Contributor Author

commented Jan 31, 2019

Thanks @mvdan. The pending CL 122695 does not eliminate this bounds check, for what that's worth.

@rsc

This comment has been minimized.

Copy link
Contributor Author

commented Jan 31, 2019

@randall77, I am not sure I follow completely, but

The extra cast probably makes the prove pass give up, because it can't go from j>0 to int(j-1)>=0.

It should be able to go in two steps, from j>0 to j-1 >= 0 to int(j-1) >= 0, right?
Because int32->int is a value-preserving conversion.
(If this were int64 j on a 32-bit system,
then obviously you can't conclude from j-1 >= 0 that int(j-1) >= 0.)

Is the problem that the prove pass does not explore a "two-step" option
or that it doesn't know about the second step at all, or both?

@randall77

This comment has been minimized.

Copy link
Contributor

commented Jan 31, 2019

I believe it's because it doesn't know about the second step at all. That is, it doesn't know anything about sign extensions.

@zdjones

This comment has been minimized.

Copy link
Contributor

commented Feb 13, 2019

When testing the negative branch of the offending bounds check, prove asserts that j-1 >= len(x). This assertion is passed to the fact table's update method. Within the update method, there is logic to identify and process fence-post patterns, such as x>y -> x-1 >= y. When it finds this pattern, update asserts the additional, inferred inequality, which in this case is j > len(x). Prove finds that second, inferred inequality, j > len(x), unsatisfiable and therefore removes the branch/bounds check.

In the int32 case, the inequality being asserted on the negative branch of the bounds check is instead int(j-1) >= len(x). Note the int(j-1) step in the second SSA below (v31). Because prove cannot see through the extension op, it might as well be asserting f[18y43f934hg >= len(x). This means the fence-post logic is never exposed to the underlying j - 1 >= len(x), update never infers and asserts the unsatisfiable condition, j > len(x), and the bounds check remains.

Relevant SSA blocks for int and int32, respectively

b8: ← b3

    v27 (+57) = Add64 <int> v37 v8          // -1 (v37) +  j (v8)
    ...
    v29 (57) = IsInBounds <bool> v27 v10     // v10 is len(x)

If v29 → b9 b10 (likely) (57)
b8: ← b3

    v30 (+67) = Add32 <int32> v41 v8       // -1 (v41) +  j (v8)
    v31 (67) = SignExt32to64 <int> v30
    ...
    v33 (67) = IsInBounds <bool> v31 v11    // v11 is len(x)

If v33 → b9 b10 (likely) (67)

I've found what seems to me like an unobtrusive change that fixes this issue, though it is pretty specific to this case. I'm not sure how complicated a more general solution would be, I have to think about it more.

When the bounds check assertion is first produced by addBranchRestrictions(), the value.Op can be checked for an extension, and the underlying value passed-through. After a quick test, this change seems to also rely on the pending CL 122695 referenced above. I have to play with it a bit more to find out exactly why that is.

@zdjones

This comment has been minimized.

Copy link
Contributor

commented Feb 14, 2019

Oops, I'd failed previously to account for the sign extension at the first bounds check, where prove needs to learn that int(j) < len(x) also means j < len(x). CL 122695 is sufficient to learn this, but doesn't help with getting from int(j - 1) >= len(x) to j > len(x). This issue can be fixed without CL 122695, but is more complete with it.

CL is forthcoming.

@zdjones

This comment has been minimized.

Copy link
Contributor

commented Feb 16, 2019

@randall77, please let me know if moving the extendindex to after the bounds check is preferable to a fix in the prove pass.

@randall77

This comment has been minimized.

Copy link
Contributor

commented Feb 16, 2019

@randall77, please let me know if moving the extendindex to after the bounds check is preferable to a fix in the prove pass.

@zdjones That's a possibility. I don't think it is easy, though. If we did that we'd need to compare, say, a 16-bit index with a 64-bit length. Those instructions don't exist on most (any?) processors.

For 32-bit archs, extendIndex is also used to truncate a 64-bit index to a 32-bit value (and panic if the upper half is not zero). That part should be moveable to after the standard bounds check.

@randall77

This comment has been minimized.

Copy link
Contributor

commented Feb 16, 2019

I guess we could introduce those mixed-length comparisons in the machine-independent code, then lower them to an extend+compare pair.

@josharian

This comment has been minimized.

Copy link
Contributor

commented Feb 16, 2019

It sounds like that might significantly increase the number of ops and generic rules.

@zdjones

This comment has been minimized.

Copy link
Contributor

commented Feb 16, 2019

The patch I've got working sounds far simpler. I'll try to mail it today or tomorrow.

@gopherbot

This comment has been minimized.

Copy link

commented Apr 30, 2019

Change https://golang.org/cl/174309 mentions this issue: cmd/compile: handle sign/zero extension in prove, at bounds checks

@gopherbot

This comment has been minimized.

Copy link

commented May 2, 2019

Change https://golang.org/cl/174704 mentions this issue: cmd/compile: handle sign/zero extensions in prove, via update method

@agnivade agnivade modified the milestones: Go1.13, Go1.14 May 30, 2019

@agnivade

This comment has been minimized.

Copy link
Member

commented May 30, 2019

CL is ready to go in for 1.14.

zdjones added a commit to zdjones/go that referenced this issue Jul 19, 2019
cmd/compile: handle sign/zero extensions in prove, via update method
Array accesses with index types smaller than the machine word size may
involve a sign or zero extension of the index value before bounds
checking. Currently, this defeats prove because the facts about the
original index value don't flow through the sign/zero extension.

This CL fixes this by looking back through value-preserving sign/zero
extensions when adding facts via Update and, where appropriate, applying
the same facts using the pre-extension value. This fix is enhanced by
also looking back through value-preserving extensions within
ft.isNonNegative to infer whether the extended value is known to be
non-negative. Without this additional isNonNegative enhancement, this
logic is rendered significantly less effective by the limitation
discussed in the next paragraph.

In Update, the application of facts to pre-extension values is limited
to cases where the domain of the new fact is consistent with the type of
the pre-extension value. There may be cases where this cross-domain
passing of facts is valid, but distinguishing them from the invalid
cases is difficult for me to reason about and to implement.
Assessing which cases to allow requires details about the context and
inferences behind the fact being applied which are not available
within Update. Additional difficulty arises from the fact that the SSA
does not curently differentiate extensions added by the compiler for
indexing operations, extensions added by the compiler for implicit
conversions, or explicit extensions from the source.

Examples of some cases that would need to be filtered correctly for
cross-domain facts:

(1) A uint8 is zero-extended to int for indexing (a value-preserving
zeroExt). When, if ever, can signed domain facts learned about the int be
applied to the uint8?

(2) An int8 is sign-extended to int16 (value-preserving) for an equality
comparison. Equality comparison facts are currently always learned in both
the signed and unsigned domains. When, if ever, can the unsigned facts
learned about the int16, from the int16 != int16 comparison, be applied
to the original int8?

This is an alternative to CL 122695 and CL 174309. Compared to CL 122695,
this CL differs in that the facts added about the pre-extension value will
pass through the Update method, where additional inferences are processed
(e.g. fence-post implications, see golang#29964). CL 174309 is limited to bounds
checks, so is narrower in application, and makes the code harder to read.

Fixes golang#26292. Fixes golang#29964.

Removes 238 bounds checks from std/cmd.

Change-Id: I1f87c32ee672bfb8be397b27eab7a4c2f304893f
zdjones added a commit to zdjones/go that referenced this issue Jul 19, 2019
cmd/compile: handle sign/zero extensions in prove, via update method
DO NOT SUBMIT

Potential alternative/complement to CL 122695 and CL 174309

Fixes golang#26292. Fixes golang#29964.

Removes 221 bounds checks from std/cmd, 64 of which are not common to CL 122695.

Change-Id: I1f87c32ee672bfb8be397b27eab7a4c2f304893f

@gopherbot gopherbot closed this in 69ff0ba Aug 27, 2019

tomocy added a commit to tomocy/go that referenced this issue Sep 1, 2019
cmd/compile: handle sign/zero extensions in prove, via update method
Array accesses with index types smaller than the machine word size may
involve a sign or zero extension of the index value before bounds
checking. Currently, this defeats prove because the facts about the
original index value don't flow through the sign/zero extension.

This CL fixes this by looking back through value-preserving sign/zero
extensions when adding facts via Update and, where appropriate, applying
the same facts using the pre-extension value. This fix is enhanced by
also looking back through value-preserving extensions within
ft.isNonNegative to infer whether the extended value is known to be
non-negative. Without this additional isNonNegative enhancement, this
logic is rendered significantly less effective by the limitation
discussed in the next paragraph.

In Update, the application of facts to pre-extension values is limited
to cases where the domain of the new fact is consistent with the type of
the pre-extension value. There may be cases where this cross-domain
passing of facts is valid, but distinguishing them from the invalid
cases is difficult for me to reason about and to implement.
Assessing which cases to allow requires details about the context and
inferences behind the fact being applied which are not available
within Update. Additional difficulty arises from the fact that the SSA
does not curently differentiate extensions added by the compiler for
indexing operations, extensions added by the compiler for implicit
conversions, or explicit extensions from the source.

Examples of some cases that would need to be filtered correctly for
cross-domain facts:

(1) A uint8 is zero-extended to int for indexing (a value-preserving
zeroExt). When, if ever, can signed domain facts learned about the int be
applied to the uint8?

(2) An int8 is sign-extended to int16 (value-preserving) for an equality
comparison. Equality comparison facts are currently always learned in both
the signed and unsigned domains. When, if ever, can the unsigned facts
learned about the int16, from the int16 != int16 comparison, be applied
to the original int8?

This is an alternative to CL 122695 and CL 174309. Compared to CL 122695,
this CL differs in that the facts added about the pre-extension value will
pass through the Update method, where additional inferences are processed
(e.g. fence-post implications, see golang#29964). CL 174309 is limited to bounds
checks, so is narrower in application, and makes the code harder to read.

Fixes golang#26292.
Fixes golang#29964.
Fixes golang#15074

Removes 238 bounds checks from std/cmd.

Change-Id: I1f87c32ee672bfb8be397b27eab7a4c2f304893f
Reviewed-on: https://go-review.googlesource.com/c/go/+/174704
Run-TryBot: Zach Jones <zachj1@gmail.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>
t4n6a1ka added a commit to t4n6a1ka/go that referenced this issue Sep 5, 2019
cmd/compile: handle sign/zero extensions in prove, via update method
Array accesses with index types smaller than the machine word size may
involve a sign or zero extension of the index value before bounds
checking. Currently, this defeats prove because the facts about the
original index value don't flow through the sign/zero extension.

This CL fixes this by looking back through value-preserving sign/zero
extensions when adding facts via Update and, where appropriate, applying
the same facts using the pre-extension value. This fix is enhanced by
also looking back through value-preserving extensions within
ft.isNonNegative to infer whether the extended value is known to be
non-negative. Without this additional isNonNegative enhancement, this
logic is rendered significantly less effective by the limitation
discussed in the next paragraph.

In Update, the application of facts to pre-extension values is limited
to cases where the domain of the new fact is consistent with the type of
the pre-extension value. There may be cases where this cross-domain
passing of facts is valid, but distinguishing them from the invalid
cases is difficult for me to reason about and to implement.
Assessing which cases to allow requires details about the context and
inferences behind the fact being applied which are not available
within Update. Additional difficulty arises from the fact that the SSA
does not curently differentiate extensions added by the compiler for
indexing operations, extensions added by the compiler for implicit
conversions, or explicit extensions from the source.

Examples of some cases that would need to be filtered correctly for
cross-domain facts:

(1) A uint8 is zero-extended to int for indexing (a value-preserving
zeroExt). When, if ever, can signed domain facts learned about the int be
applied to the uint8?

(2) An int8 is sign-extended to int16 (value-preserving) for an equality
comparison. Equality comparison facts are currently always learned in both
the signed and unsigned domains. When, if ever, can the unsigned facts
learned about the int16, from the int16 != int16 comparison, be applied
to the original int8?

This is an alternative to CL 122695 and CL 174309. Compared to CL 122695,
this CL differs in that the facts added about the pre-extension value will
pass through the Update method, where additional inferences are processed
(e.g. fence-post implications, see golang#29964). CL 174309 is limited to bounds
checks, so is narrower in application, and makes the code harder to read.

Fixes golang#26292.
Fixes golang#29964.
Fixes golang#15074

Removes 238 bounds checks from std/cmd.

Change-Id: I1f87c32ee672bfb8be397b27eab7a4c2f304893f
Reviewed-on: https://go-review.googlesource.com/c/go/+/174704
Run-TryBot: Zach Jones <zachj1@gmail.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
7 participants
You can’t perform that action at this time.