Navigation Menu

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

Jump to bottom

cmd/compile: prove misses obvious facts about constants #36889

Open
josharian opened this issue Jan 30, 2020 · 2 comments
Open

cmd/compile: prove misses obvious facts about constants #36889

josharian opened this issue Jan 30, 2020 · 2 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
Backlog

Comments

@josharian
Copy link
Contributor

I noticed that left shifts by a constant are not being marked as bounded by prove. Prove consults ft.limits, but ft.limits doesn't contain limits for constants. Something similar happens for some other ops with easy limits.

This is pretty straightforward to fix: Write a wrapper around ft.limits accesses that generates limits in cases like these.

I have a prototype CL of this, and it mostly helps. But before it can be mailed, I need to investigate and fix a few more minor regressions from it. (The compiler is quite sensitive to the order in which optimizations occur.)

And before doing that, I wanted to check in about whether this was even the right kind of fix here.

cc @zdjones @rasky
@rasky
Copy link
Member

rasky commented Jan 30, 2020

Can you try if my CL https://go-review.googlesource.com/c/go/+/196679 fixes the test case you have in mind? It does add bounds to constants

@josharian
Copy link
Contributor Author

@rasky will do, thanks. I'll have to find it again first, so it may be a little while. :)

@cagedmantis cagedmantis added this to the Backlog milestone Feb 7, 2020
@cagedmantis cagedmantis added the NeedsInvestigation Someone must examine and confirm this is a valid issue and not a duplicate of an existing one. label Feb 7, 2020
@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
Assignees
No one assigned
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
Go Compiler / Runtime
Status: Triage Backlog
Milestone
Backlog
Development

No branches or pull requests
4 participants
@josharian @cagedmantis @rasky @gopherbot