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: add bounds information from non-control ops to prove pass #25086

josharian opened this Issue Apr 25, 2018 · 4 comments


None yet
3 participants

josharian commented Apr 25, 2018

Probably low priority; I'm not sure.

Some ops have strongly bounded output. For example, Ctz64 is always in [0,64], and Ctz64NonZero is in [0, 63]. Rsh by a constant also provides bounds.

The prove pass seems unaware of this. Does it / should it care? Where/how should it be added?


@josharian josharian added this to the Unplanned milestone Apr 25, 2018


This comment has been minimized.


rasky commented Apr 26, 2018

I would be surprised if it matters much right now.

If you want to try something, I'd try adding it at the end of (*factsTable).update: if v (or w) is OpCtz*, call ft.update recursively adding a relation between v and 64 (in the quick test, just materialize the constant there with parent.NewValue0I). I would do that on top of my CL serie that includes transitive relations, as I can see this information being useful as part of a more complex relation of vars rather than being used directly. That would increase the likeliness of this information being useful.

To check if the code is really helping, check if ft.unsat is true when ft.update returns. If it's true, you're learning something that is helping remove a condition and wasn't known before.


This comment has been minimized.


randall77 commented Apr 26, 2018

Should do this for the And ops as well, they can provide strong bounds info, e.g. a[i & 0xff].
We handle a bunch of cases using rules, but doing it in prove would be more complete.

@rasky rasky self-assigned this Sep 6, 2018


This comment has been minimized.


rasky commented Sep 6, 2018

I'll mail a CL that adds bounds derived from:

  • OpAnd*: z=x&y ⇒ z<=x && <=y (unsigned)
  • OpZeroExt*: z=zext(x) ⇒ z==x (unsigned)
  • OpSignExt*: z=sext(x) ⇒ z==x (signed)
  • OpRsh*: z=x>>y ⇒ z<=x (signed and unsigned)
  • OpRshU*: z=x>>y ⇒ z<=x && z <= (1<<(64-y))-1 (unsigned)

The result in terms of proved ops can be seen here:

It's easy to add Ctz following the lead, but it's not used in the compiler or standard library itself, so I'm not sure how to measure the impact.


This comment has been minimized.


josharian commented Sep 9, 2018

If it is easy, I think it is worth adding the full math/bits intrisincs set, on pain of having to rediscover it later, even if usage is rare; when math/bits is in use people frequently care lots about performance.

I’ll note in passing that we can convert signed ext to zero ext if we can prove non-negative. Not sure if that is very useful in this context, but I can imagine on amd64 that it could eliminate some 32-to-64 extensions by folding them into MOVLs.

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