-
Notifications
You must be signed in to change notification settings - Fork 1.3k
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
PCC: check facts on loaded and stored values, infer facts where needed, and add a basic vmctx/memory example. #7231
Conversation
Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>
Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>
Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
- Allow any fact at all to subsume a trivially-true range fact that states a bitslice is within the maximum range for its width. - Clamp the maximum value of a bitslice at the maximum value for the slice's width.
The test failures exposed two issues surfaced by the new "default facts" (e.g., width-8 value is always <= 255), so I had to add a bit more reasoning. @fitzgen mind taking a look at the last commit? |
Ah -- automerge was still on and this went in with your r+, @fitzgen; still happy to take feedback on the approach in the last commit if you have any! |
// Any value on the LHS subsumes a minimal (always-true) | ||
// fact about the max value of a given bitwidth on the | ||
// RHS: e.g., no matter the value, the bottom 8 bits will | ||
// always be <= 255. | ||
(_, Fact::ValueMax { bit_width, max }) if *max == max_value_for_width(*bit_width) => { | ||
true | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think this is technically wrong but it feels like a footgun to allow a Mem
fact to subsume a minimal ValueMax
fact.
Would it be a problem to limit this to ValueMax
LHSes? I guess that is what would happen if this case wasn't here, due to the match arm just below this one. Can you explain in more detail why we need this kind of cross-fact-kind subsumption then?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It seems that that narrower rule is indeed sufficient, at least for our test cases. The new rule is still necessary (not covered by the rule below) because of the remaining difference: it doesn't require matching bit-widths.
All of this is a bit of awkward fallout of the way default facts are working now though, so I'm going to see if I can try again to eliminate them and make subsume
take the type instead. If not, I'll update as you suggest!
This removes the need for the awkward "max-range fact is subsumed by anything" rule noted by @fitzgen in [this comment](bytecodealliance#7231 (comment)). It also makes checking a little more efficient and logically clear, as only the facts that the frontend/producer added are verified, rather than all default facts as well.
This removes the need for the awkward "max-range fact is subsumed by anything" rule noted by @fitzgen in [this comment](#7231 (comment)). It also makes checking a little more efficient and logically clear, as only the facts that the frontend/producer added are verified, rather than all default facts as well.
This PR incorporates a few more steps in PCC's development:
With all of these together, we can validate a simple "mock
vmctx
" example that looks a lot like what static memory accesses in Wasmtime do:In theory, once we propagate facts during aegraph rewriting (we don't currently; opts are off in all tests), this should be enough for end-to-end checking of static memories by emitting the right facts in
cranelift-wasm
. Those two steps (opts, then Wasm frontend) are next!Co-authored-by: Nick Fitzgerald fitzgen@gmail.com