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: add reverse proof to prove pass? #48469

Open
JAicewizard opened this issue Sep 19, 2021 · 3 comments
Open

cmd/compile: add reverse proof to prove pass? #48469

JAicewizard opened this issue Sep 19, 2021 · 3 comments
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. NeedsDecision Feedback is required from experts, contributors, and/or the community before a change can be made.
Milestone

Comments

@JAicewizard
Copy link

What version of Go are you using (go version)?

$ go version
1.17.1

Does this issue reproduce with the latest release?

yes

I dont know if there are propper terms for these. I call the current way the prove pass works forwards, as it proves from what it knows, whereas I call what I propose backwards because it goes the opposite way. (trying to find out what knowlege is needed to prove the branch).

While seeing what happens in some cases I recently reported, I found that essentially that trying to improve the ft.update function might be a simple solution for proving things, but its also one-way. It tries to proof things from what it already knows. However in some cases it is actually almost trivial to do this in reverse. Look at what condition you're branching on, and then see what you need to prove this.

Adding more of the forward rules will grow exponentially, because each rule will trigger another etc. Adding a backwards rule would only grow the complexity linearly. Of course its affect is also smaller, but adding forward rules will eventually hit diminishing returns as maybe only 1% of the rules applied actually end up being useful.

@JAicewizard
Copy link
Author

JAicewizard commented Sep 19, 2021

see https://github.com/JAicewizard/go/tree/add_backwards_checks_ssa for my current implementation. Along with the backwards rules, I also added some other improvements to make sure my own issue is fixed.
One thing to note that I initially forgot, is that these are specific cases, not general rules. like "if this value was negated, and before that it was incremented and is was smaller than 0 then we know it is now bigger than or equal to 0", more like rewrite rules.

@randall77
Copy link
Contributor

It's an interesting idea. The prove pass certainly proves a lot of things to itself that it doesn't end up using.

The prove pass is currently very delicate, error-prone code. I think at this point I'm much more concerned about the complexity of the code itself than the amount of work it does at compile time. So I think I'm not that excited about making the prove pass more efficient. If this rework makes it more obviously correct, that would make me excited.

@JAicewizard
Copy link
Author

My code doesnt really touch the existing code in the prove pass. What I have right now is sort of like a pattern matching function that tries to match a pattern of values, sees if it the required facts are known, and if so adds a conclusion fact. I think it makes most sense for complex logic that the prove pass would never be able to prove due to the nature of information it stores. eg: it only stores the range a value can be in as a min/max, but what if we know if its between -x and MinInt-x? this doesn't get stored at all, and doing so would make the code even more complex.

Assuming this pattern matching function is correct, the tricky part would be getting correct patterns and facts, not the code itself.

We could also make something like how the current update function works, but this would be just as complex as update and wouldn't be able to prove something like the example above (although it would certainly be interesting! ).

@ALTree ALTree added the NeedsDecision Feedback is required from experts, contributors, and/or the community before a change can be made. label Sep 20, 2021
@ALTree ALTree added this to the Unplanned milestone Sep 20, 2021
@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
Labels
compiler/runtime Issues related to the Go compiler and/or runtime. NeedsDecision Feedback is required from experts, contributors, and/or the community before a change can be made.
Projects
None yet
Development

No branches or pull requests

4 participants