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 · 4 comments

Comments

@agnivade
Copy link
Member

commented Jun 10, 2019

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)

@mvdan

This comment has been minimized.

Copy link
Member

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

This comment has been minimized.

Copy link
Member Author

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.

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

This comment has been minimized.

Copy link
Member

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

This comment has been minimized.

Copy link
Member Author

commented Jun 10, 2019

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.