diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 78cad40f2bb..6b60512abfc 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -205,6 +205,83 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) { // useful to implement that). } +namespace { + +// Do an OR of a pair of constraints where the terms are known to be equal. If +// we can't find a good way to express their ORing, return nullopt. +std::optional approximateOrTermEqualPair(const Abstract::Op aOp, + const Abstract::Op bOp, + const Term& term) { + using namespace Abstract; + + // x == C || x > C === x >= C + if (aOp == Eq && bOp == GtS) { + return Constraint{GeS, term}; + } + + // TODO: all the rest + + return {}; +} + +// Do an OR of a pair of constraints. If we can't find a good way to express +// their ORing, return nullopt. +std::optional approximateOrPair(const Constraint& a, + const Constraint& b, + bool recursing = false) { + if (a.term == b.term) { + if (auto result = approximateOrTermEqualPair(a.op, b.op, a.term)) { + return result; + } + } + + // If a proves b, e.g. x = 5 proves x >= 0 is true, then the OR is b. + if (provesPair(a, b) == True) { + return b; + } + + // TODO: more smarts + + if (!recursing) { + // The flipped form may be recognized. + return approximateOrPair(b, a, true); + } + + return {}; +} + +// Do an OR in full detail, looking at every constraint in each of the given +// sets. +AndedConstraintSet detailedApproximateOr(const AndedConstraintSet& a, + const AndedConstraintSet& b) { + // We can process this in full detail by looking at all the combinations of + // individual constraints, because of the distributive property: + // + // (A & B) | (C & D) == ((A & B) | C) & ((A & B) | D) + // == (A | C) & (B | C) & (A | D) & (B | D) + // + // This is quadratic, but constraint sets are limited to a very small size, + // making this reasonable. + // + // Also, note that we don't need to worry about new contradictions here: ORing + // things never leads to a contradiction, and we can assume the inputs are + // not contradictions. + assert(!a.provesEverything() && !b.provesEverything()); + + auto result = AndedConstraintSet::makeProvesNothing(); + for (auto& ac : a) { + for (auto& bc : b) { + if (auto combined = approximateOrPair(ac, bc)) { + // We found something useful by ORing them, keep it. + result.approximateAnd(*combined); + } + } + } + return result; +} + +} // anonymous namespace + bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) { // If one proves everything, the only thing that matters is the other. if (other.provesEverything()) { @@ -226,12 +303,11 @@ bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) { return true; } - // TODO smarts: handle <= > and so forth - - // Otherwise, we don't know how to nicely OR these things, and expand to the - // trivial set of no constraints. - clear(); - return true; + // For more complex cases, do a detailed analysis. + auto result = detailedApproximateOr(*this, other); + auto changed = (result != *this); + *this = result; + return changed; } std::optional LocalConstraint::parse(Expression* curr) { diff --git a/src/ir/constraint.h b/src/ir/constraint.h index 4412c53a21b..9fea231fbc7 100644 --- a/src/ir/constraint.h +++ b/src/ir/constraint.h @@ -92,6 +92,14 @@ struct AndedConstraintSet : inplace_vector { // until something changes. bool isContradiction = true; + AndedConstraintSet() = default; + AndedConstraintSet(std::initializer_list constraints) { + isContradiction = false; + for (auto& c : constraints) { + approximateAnd(c); + } + } + // Proving everything (even contradictions) is equivalent to being a // contradiction. (This and provesNothing can be seen as the top/bottom of a // poset, if one wants to think of things that way.) diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index ea3fc10167c..ce25048f59b 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -240,5 +240,103 @@ TEST(ConstraintTest, TestDeredundancy) { EXPECT_EQ(t[0], eq0); } -// TODO: test an approximateOr of { x = 10 } and { x >= 0 }, once we support -// inequalities +static void checkOr(const AndedConstraintSet& a, + const AndedConstraintSet& b, + const AndedConstraintSet& result) { + auto ored = a; + ored.approximateOr(b); + EXPECT_EQ(ored, result); + + ored = b; + ored.approximateOr(a); + EXPECT_EQ(ored, result); +} + +TEST(ConstraintTest, TestOrInequality) { + // x == 5 || x >= 0 => x >= 0 + AndedConstraintSet eq5{Constraint{Eq, {Literal(int32_t(5))}}}; + AndedConstraintSet ge0{Constraint{GeU, {Literal(int32_t(0))}}}; + checkOr(eq5, ge0, ge0); + + // x == 5 || x > 5 => x >= 5 + AndedConstraintSet gts5{Constraint{GtS, {Literal(int32_t(5))}}}; + AndedConstraintSet ges5{Constraint{GeS, {Literal(int32_t(5))}}}; + checkOr(eq5, gts5, ges5); + + // x == 5 || x >= 5 => x >= 5 + checkOr(eq5, ges5, ges5); +} + +TEST(ConstraintTest, TestOrLoop) { + // Check common loop patterns: + // { x == A } || { x > A && x <= B } ==> { x >= A && x <= B } + + // { x == 5 } || { x > 5 && x <= 42 } ==> { x >= 5 && x <= 42 } + AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}}; + AndedConstraintSet right( + {{GtS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}}); + AndedConstraintSet result( + {{GeS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}}); + checkOr(left, right, result); + + // Changes to constants: + + // Change 5 on the left to 7: + // { x == 7 } || { x > 5 && x <= 42 } ==> { x > 5 && x <= 42} + AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}}; + checkOr(left7, right, right); + + // Change 5 on the left to 99: + // { x == 99 } || { x > 5 && x <= 42 } ==> { x > 5 } + // TODO: we could emit a range (5, 99] + AndedConstraintSet left99{Constraint{Eq, {Literal(int32_t(99))}}}; + AndedConstraintSet rightOnly5{Constraint{GtS, {Literal(int32_t(5))}}}; + checkOr(left99, right, rightOnly5); + + // Change 5 on the left to 4: + // { x == 4 } || { x > 5 && x <= 42 } ==> { x <= 42 } + // TODO: we could emit a range [4, 42] + AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}}; + AndedConstraintSet rightOnly42({{LeS, {Literal(int32_t(42))}}}); + checkOr(left4, right, rightOnly42); + + // Change 5 on the right to 6: + // { x == 5 } || { x > 6 && x <= 42 } ==> { x <= 42 } + AndedConstraintSet right6( + {{GtS, {Literal(int32_t(6))}}, {LeS, {Literal(int32_t(42))}}}); + checkOr(left, right6, rightOnly42); + + // Changes to operations: + + // Change the Eq on the left to Ne. We fail to find anything for the OR. + // { x != 5 } || { x > 5 && x <= 42 } ==> {} + // TODO: we could emit x != 5 + AndedConstraintSet leftNe{Constraint{Ne, {Literal(int32_t(5))}}}; + auto empty = AndedConstraintSet::makeProvesNothing(); + checkOr(leftNe, right, empty); + + // Change the GtS on the right to GtU: + // { x == 5 } || { x >U 5 && x <= 42 } ==> { x <= 42 } + AndedConstraintSet rightGtU( + {{GtU, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}}); + checkOr(left, rightGtU, rightOnly42); + + // Change the LeS on the right to LeU: + // { x == 5 } || { x > 5 && x <=U 42 } ==> { x >= 5 && x <=U 42 } + AndedConstraintSet rightLeU( + {{GtS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}}); + AndedConstraintSet rightGesLeU( + {{GeS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}}); + checkOr(left, rightLeU, rightGesLeU); + + // Add an operation on the right, x != 21: + // { x == 5 } || { x > 5 && x <= 42 && x != 21 } ==> + // { x >= 5 && x <= 42 && x != 21 } + AndedConstraintSet rightAdded({{GtS, {Literal(int32_t(5))}}, + {LeS, {Literal(int32_t(42))}}, + {Ne, {Literal(int32_t(21))}}}); + AndedConstraintSet resultAdded({{GeS, {Literal(int32_t(5))}}, + {LeS, {Literal(int32_t(42))}}, + {Ne, {Literal(int32_t(21))}}}); + checkOr(left, rightAdded, resultAdded); +} diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast new file mode 100644 index 00000000000..5d90de1096f --- /dev/null +++ b/test/lit/passes/constraint-analysis-loops.wast @@ -0,0 +1,229 @@ +;; NOTE: Assertions have been generated by update_lit_checks.py and should not be edited. + +;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s + +(module + ;; CHECK: (import "a" "b" (func $import (type $1) (result i32))) + (import "a" "b" (func $import (result i32))) + + ;; CHECK: (func $bound (type $0) + ;; CHECK-NEXT: (local $x i32) + ;; CHECK-NEXT: (loop $loop + ;; CHECK-NEXT: (drop + ;; CHECK-NEXT: (i32.const 1) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (drop + ;; CHECK-NEXT: (i32.const 1) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (local.set $x + ;; CHECK-NEXT: (call $import) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (if + ;; CHECK-NEXT: (i32.gt_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (i32.const 0) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (then + ;; CHECK-NEXT: (if + ;; CHECK-NEXT: (i32.le_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (i32.const 100) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (then + ;; CHECK-NEXT: (br $loop) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + (func $bound + (local $x i32) + (loop $loop + ;; We arrive at the loop top with {x == 0} || {x > 0 && x <= 100}. Those + ;; OR into {x >= 0 && x <= 100} - that is, the x == 0 and x > 0 combine + ;; into x >= 0. + (drop + (i32.ge_s + (local.get $x) + (i32.const 0) + ) + ) + (drop + (i32.le_s + (local.get $x) + (i32.const 100) + ) + ) + ;; Set $x to an unknown value before applying the constraints below on the + ;; way back to the loop top. + (local.set $x + (call $import) + ) + (if + (i32.gt_s + (local.get $x) + (i32.const 0) + ) + (then + (if + (i32.le_s + (local.get $x) + (i32.const 100) + ) + (then + (br $loop) + ) + ) + ) + ) + ) + ) + + ;; CHECK: (func $bound-flipped-ifs (type $0) + ;; CHECK-NEXT: (local $x i32) + ;; CHECK-NEXT: (loop $loop + ;; CHECK-NEXT: (drop + ;; CHECK-NEXT: (i32.const 1) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (drop + ;; CHECK-NEXT: (i32.const 1) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (local.set $x + ;; CHECK-NEXT: (call $import) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (if + ;; CHECK-NEXT: (i32.le_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (i32.const 100) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (then + ;; CHECK-NEXT: (if + ;; CHECK-NEXT: (i32.gt_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (i32.const 0) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (then + ;; CHECK-NEXT: (br $loop) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + (func $bound-flipped-ifs + (local $x i32) + ;; As above, but with the ifs flipped. We optimize the same way. + (loop $loop + (drop + (i32.ge_s + (local.get $x) + (i32.const 0) + ) + ) + (drop + (i32.le_s + (local.get $x) + (i32.const 100) + ) + ) + (local.set $x + (call $import) + ) + (if + (i32.le_s + (local.get $x) + (i32.const 100) + ) + (then + (if + (i32.gt_s + (local.get $x) + (i32.const 0) + ) + (then + (br $loop) + ) + ) + ) + ) + ) + ) + + ;; CHECK: (func $bound-nonconstant-no (type $2) (param $p i32) + ;; CHECK-NEXT: (local $x i32) + ;; CHECK-NEXT: (loop $loop + ;; CHECK-NEXT: (drop + ;; CHECK-NEXT: (i32.ge_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (local.get $p) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (drop + ;; CHECK-NEXT: (i32.le_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (local.get $p) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (local.set $x + ;; CHECK-NEXT: (call $import) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (if + ;; CHECK-NEXT: (i32.gt_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (local.get $p) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (then + ;; CHECK-NEXT: (if + ;; CHECK-NEXT: (i32.le_s + ;; CHECK-NEXT: (local.get $x) + ;; CHECK-NEXT: (i32.const 100) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: (then + ;; CHECK-NEXT: (br $loop) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + ;; CHECK-NEXT: ) + (func $bound-nonconstant-no (param $p i32) + (local $x i32) + ;; As above, but rather than zero we have an unknown param $p. + (loop $loop + ;; We can infer nothing here, as p is unknown, and x might be 0 or <= 100. + (drop + (i32.ge_s + (local.get $x) + (local.get $p) + ) + ) + (drop + (i32.le_s + (local.get $x) + (local.get $p) + ) + ) + (local.set $x + (call $import) + ) + (if + (i32.gt_s + (local.get $x) + (local.get $p) + ) + (then + (if + (i32.le_s + (local.get $x) + (i32.const 100) + ) + (then + (br $loop) + ) + ) + ) + ) + ) + ) +)