ConstraintAnalysis: Add inequality parsing#8891
Conversation
| for (auto op : {Abstract::Eq, | ||
| Abstract::Ne, | ||
| Abstract::LtS, | ||
| Abstract::LtU, | ||
| Abstract::LeS, | ||
| Abstract::LeU, | ||
| Abstract::GtS, | ||
| Abstract::GtU, | ||
| Abstract::GeS, | ||
| Abstract::GeU}) { |
There was a problem hiding this comment.
Instead of guess-and-check to see if the binary operation is one we support, can we instead have a function in abstract.h to switch over binary->op and return the corresponding Abstract op, if any? Then we can very efficiently skip operations that don't correspond to any abstract op.
There was a problem hiding this comment.
I can measure this and look for an optimization. Maybe as an NFC followup?
(The challenge is avoiding code duplication - the current way avoids writing the mapping of opcodes twice.)
| ) | ||
| ) | ||
|
|
||
| ;; CHECK: (func $local-changes (type $3) (param $x i32) (param $y i32) (param $z i32) |
There was a problem hiding this comment.
I assume local-changes was not changed?
There was a problem hiding this comment.
Yes, I verified it did not change. Just unfortunate git diffing...
| ;; OPTIN: (func $inequalities-lt_u (type $0) (param $x i32) | ||
| ;; OPTIN-NEXT: (drop | ||
| ;; OPTIN-NEXT: (i32.eq | ||
| ;; OPTIN-NEXT: (i32.lt_u |
There was a problem hiding this comment.
Can we add something simple to the tests to prevent the if-elses from being optimized out by OptimizeInstructions?
There was a problem hiding this comment.
We could, but I'm not sure it would help - it would make the test longer but not add anything in these cases?
There was a problem hiding this comment.
Well the stated purpose of the OPTIN tests is to ensure that we still optimize canonicalized IR after optimize-instructions runs, and right now the tests are not showing that.
There was a problem hiding this comment.
Yeah, this matters mostly in the early tests where there are realistic conversions of things. I don't think these later ones need it. I could split out the test files if you think that's better?
There was a problem hiding this comment.
Makes sense. Splitting might make sense, but it doesn't seem urgent.
2 participants
We now parse
i32.lt_sand so forth.This does not include full range analysis yet, so we don't infer
ties between
<=and<for example, but this is already enough to inferthe precise inequalities we see, and their negations. This can handle
the simplest kinds of software bounds checks, more will be added later.
Also add proper printing of these opcodes.