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: teach prove about more type conversion operations #26299

Open
mvdan opened this Issue Jul 9, 2018 · 2 comments

Comments

Projects
None yet
3 participants
@mvdan
Member

mvdan commented Jul 9, 2018

#26292 is about teaching the prove pass that, if x byte is <N, int(x) is also <N. In particular, it helps when using byte variables as indices, since that seems to mean an implicit conversion to int. That was causing an unnecessary bounds check in an encoding/json hot path.

Here are some other cases which might be worthwhile to do. I don't know how useful they would be for software out there, like removing bounds checks in the standard library.

  • If x uint32 is <10, uint(x) < 10 (and same for int32/int)
  • If x uint64 is <10 and we're on 64-bit, uint(x) < 10
  • If x uint is <10, byte(x) < 10
  • If x int is non-negative and <10, uint(x) < 10

/cc @aclements @rasky

@mvdan

This comment has been minimized.

Member

mvdan commented Jul 9, 2018

Austin's comment from https://go-review.googlesource.com/c/go/+/122695:

Possibly, though it's a bit tricky since these are conditional. There's actually no place in prove right now where we walk through non-control values with facts for a block (and doing so is potentially tricky because the values aren't ordered). That's why this CL adds uncondtional equality facts up-front before doing the rest of the prove pass.

But maybe we should walk through the other values in each block and forward-derive facts? I worry a bit about the performance of that, and how value ordering would affect it. We could make a pre-pass to mark only the values that ultimately affect control values, so we could forward-derive facts only for those values.

@mvdan mvdan added the Performance label Jul 9, 2018

@ianlancetaylor ianlancetaylor added this to the Go1.12 milestone Jul 11, 2018

@randall77

This comment has been minimized.

Contributor

randall77 commented Dec 12, 2018

Punting to 1.13, too late for anything major in 1.12.

@randall77 randall77 modified the milestones: Go1.12, Go1.13 Dec 12, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment