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 doesn't know that integer extensions preserve bounds #26292

Closed
mvdan opened this issue Jul 9, 2018 · 4 comments
Closed

cmd/compile: prove doesn't know that integer extensions preserve bounds #26292

mvdan opened this issue Jul 9, 2018 · 4 comments
Assignees
Milestone

Comments

@mvdan
Copy link
Member

@mvdan mvdan commented Jul 9, 2018

As discovered by @aclements on https://go-review.googlesource.com/c/go/+/122459:

It's proving the second of two bounds-checks on that line, possibly because it's redundant with the first. I think it's not getting the first BCE because there's a ZeroExt8to64, and prove doesn't know that preserves the bounds of the original value:

v33 is b; v39 is const 128:

b8: ← b6
v38 (+889) = ZeroExt8to64 v33
v40 (889) = IsInBounds v38 v39
If v40 → b13 b14 (likely) (line 889)

Prove knows that v33 < 128, but that fact doesn't flow through to v38.

So, another way to fix this is to change "b < utf8.RuneSelf" to "int(b) < utf8.RuneSelf". At least for (*encodeState).string and (*encodeState).stringBytes, the only effect of this appears to be eliminating that one bounds check (and some register renaming).

(particular comment: https://go-review.googlesource.com/c/go/+/122459/1//COMMIT_MSG#21)

@gopherbot
Copy link

@gopherbot gopherbot commented Jul 9, 2018

Change https://golang.org/cl/122695 mentions this issue: cmd/compile: handle sign/zero extension in prove

@gopherbot
Copy link

@gopherbot gopherbot 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
Copy link

@gopherbot gopherbot 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
Copy link
Contributor

@agnivade agnivade 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
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
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
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
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
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
6 participants
You can’t perform that action at this time.