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 unable to eliminate bounds check when a variable is assigned from len #32515

Open
agnivade opened this issue Jun 10, 2019 · 6 comments
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Performance
Milestone

Comments

@agnivade
Copy link
Contributor

What version of Go are you using (go version)?

$ go version
go version devel +98100c56da Mon Jun 3 01:37:58 2019 +0000 linux/amd64

What did you do?

Consider -

func bce2(s string) {
	n := len(s)
	buf := make([]byte, n+1)
	for i := 0; i <= n; i++ {
		_ = buf[i] // bounds check
	}
}

The compiler is unable to prove that buf[i] will be always in range. But it should be, because n is positive, and len(buf) = n+1.

A hint of _ = buf[n] or alternatively, changing the bounds from <= n to < len(buf) fixes it.

This actually came from a real-world code from my levenshtein library. See agnivade/levenshtein@1e1f2ae#diff-12f7126b3ca34e44fe76e482d22fba93R46.

What did you expect to see?

No bounds check

What did you see instead?

Bounds check

Apologies if this is already filed somewhere else. I did not see it in my search.

@zdjones @rasky

Also @mvdan (we had a conversation on this on slack)

@agnivade agnivade added NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Performance labels Jun 10, 2019
@agnivade agnivade added this to the Unplanned milestone Jun 10, 2019
@mvdan
Copy link
Member

mvdan commented Jun 10, 2019

Does the BCE work if you get rid of +1 and use < instead of <=? Perhaps it's the combination of the variable and the extra element that confuses the compiler.

What if you keep the +1 but inline the variable?

@agnivade
Copy link
Contributor Author

Does the BCE work if you get rid of +1 and use < instead of <=? Perhaps it's the combination of the variable and the extra element that confuses the compiler.

It doesn't work.

What if you keep the +1 but inline the variable?

You mean have something like n := 5 ? Yes, of course that works :). The compiler is just unable to deduce that since len(s) is >=0, so n will also be >=0.

@rasky
Copy link
Member

rasky commented Jun 10, 2019

The problem here is that the compiler doesn't know that b := make([]byte, n) implies that len(b) == cap(b) == n. We already have an issue for that somewhere. I investigated this a little bit, but the only solution would be to introduce a new SSA op OpSliceBuild (or something like that), because otherwise the make call is lowered far before prove is able to see it.

EDIT: this is the issue I was thinking of, with also Keith agreeing that a new op is the way to go (#24660 (comment)).

@agnivade
Copy link
Contributor Author

agnivade commented Jun 10, 2019

Thanks @rasky. If that is the only way forward for #24660, should we close this as duplicate ?

@dr2chase
Copy link
Contributor

We might want to revisit this, because calls are now lowered later. It might not be enough (yet).

@rasky
Copy link
Member

rasky commented Nov 12, 2020

Actually, the "call" part of this issue was already solved by a CL last year that made each make call have OpSliceMake wrapper in the SSA form, and prove has already been modified to handle this (87e2b34, CL196784).

What's left here is the +1 part of the argument to make, that confuses prove.

@gopherbot gopherbot added the compiler/runtime Issues related to the Go compiler and/or runtime. label Jul 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. Performance
Projects
None yet
Development

No branches or pull requests

5 participants