-
Notifications
You must be signed in to change notification settings - Fork 17.9k
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: BCE does not take transitivity into account #19714
Comments
cc @brtzsnr |
I just submitted a CL that fixes the initial example. The more complex example (hextable) has two additional problems: first, prove does not know how to handle loops; I have a solution coming for this though (which is merging loopbce into prove). Second, prove doesn't know how to handle math operations on indices or induction variables. This is harder. Feel free to re-submit a new issue for the more complex case. |
Change https://golang.org/cl/100277 mentions this issue: |
@rasky thanks for taking a look at this problem. |
Please answer these questions before submitting your issue. Thanks!
What did you do?
Hello up there. Please consider the following function:
(https://play.golang.org/p/pACbUNtHoB)
here
i
is in valid range forb
andj
is iterating in [0,i) so it is also in valid range for b. However Aaa compiles to:with
b[j]
access being bounds checked at runtime.Just for the reference, if loop for
j
is in[0,len(b))
:no bounds checking is generated.
So looks like what is needed is to teach BCE that if i1 is in valid bounds, i2 in [0, i1] => i2 is also in valid bounds.
This actually came up as simplified case of
where bounds checks are unneccessarily generated for
dst[i]
.The above case in turn tries to model e.g.
encoding/hex.Encode
in simplified way:where even if initial check for
len(dst) < len(src) * 2 => error
is activated, still 2 bounds checks are generated (fordst[i*2]
anddst[i*2+1
]) makinghex.Encode
(together with #15808) much slower than it should be:What did you expect to see?
No runtime bound checks.
What did you see instead?
Runtime bound check present for
b[j]
access.Does this issue reproduce with the latest release (go1.8)?
Yes.
System details
Thanks beforehand,
Kirill
/cc @randall77, @dr2chase
The text was updated successfully, but these errors were encountered: