diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index a1516280deb..44009e02ec3 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -22,6 +22,86 @@ namespace wasm::constraint { +std::optional> Constraint::getSpan() const { + using namespace Abstract; + + auto* c = std::get_if(&term); + if (!c) { + // Not comparing to a constant, so cannot be a constant span. + return {}; + } + + auto minSigned = c->type == Type::i32 ? std::numeric_limits::min() + : std::numeric_limits::min(); + auto maxSigned = c->type == Type::i32 ? std::numeric_limits::max() + : std::numeric_limits::max(); + auto maxUnsigned = c->type == Type::i32 + ? std::numeric_limits::max() + : std::numeric_limits::max(); + + switch (op) { + case Eq: { + auto x = c->getUnsigned(); + if (x <= uint64_t(maxSigned)) { + // This is in the range of both signed and unsigned values, so there is + // no ambiguity. That is, we cannot convert the bit pattern + // 0xffffffff into a Span, as it might be either uint32_t(-1) + // or actually negative (but a bit pattern like 0x00000001 is + // always fine as it can only ever be "1"). + return Span{x, x}; + } + break; + } + + case LtS: + if (c->getInteger() == minSigned) { + // Less than the lowest possible number is an empty span. + return Span::empty(); + } else { + return Span{minSigned, c->getInteger() - 1}; + } + break; + case LtU: + if (c->getInteger() == 0) { + // Less than the lowest possible number is an empty span. + return Span::empty(); + } else { + return Span{0, c->getUnsigned() - 1}; + } + break; + case LeS: + return Span{minSigned, c->getInteger()}; + case LeU: + return Span{0, c->getUnsigned()}; + + case GtS: + if (c->getInteger() == maxSigned) { + // Greater than the highest possible number is an empty span. + return Span::empty(); + } else { + return Span{c->getInteger() + 1, maxSigned}; + } + break; + case GtU: + if (c->getUnsigned() == maxUnsigned) { + // Greater than the highest possible number is an empty span. + return Span::empty(); + } else { + return Span{c->getUnsigned() + 1, maxUnsigned}; + } + break; + case GeS: + return Span{c->getInteger(), maxSigned}; + case GeU: + return Span{c->getUnsigned(), maxUnsigned}; + + default: { + } + } + + return {}; +} + namespace { Result TrueFalse(bool x) { return x ? True : False; } @@ -78,6 +158,31 @@ Result provesConstantPair(Abstract::Op aOp, } } + // If we can represent both as spans, we can calculate that way. + if (auto aSpan = Constraint{aOp, {aConstant}}.getSpan()) { + if (auto bSpan = Constraint{bOp, {bConstant}}.getSpan()) { + if (aSpan->isEmpty()) { + // An empty span implies a contradiction (e.g. x > MAX_INT), as it means + // no possible number can apply. And contradictions prove anything. + return True; + } + if (bSpan->isEmpty()) { + // Anything that is not a contradiction can prove a contradiction. + return False; + } + if (bSpan->contains(*aSpan)) { + // b's values contains a's, e.g., b = { 0 < x < 10 } and + // a = { 3 < x < 7 }, so a => b. + return True; + } + if (!bSpan->hasOverlap(*aSpan)) { + // There is no overlap at all, e.g., { 0 < x < 10 } vs { 20 < x < 30 }, + // both cannot be true and each proves the other false. + return False; + } + } + } + if (!recursing) { // The flipped operation may tell us something: y ==> !x implies // x ==> y is false (because if not, then x would prove y, and y would @@ -239,6 +344,8 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) { } } + // TODO: use Spans here when possible + if (size() < MaxConstraints) { // Insert into the right place, keeping us sorted. insert(std::upper_bound(begin(), end(), c), c); @@ -400,6 +507,8 @@ bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) { return true; } + // TODO: use Spans here when possible + // For more complex cases, do a detailed analysis. auto result = detailedApproximateOr(*this, other); auto changed = (result != *this); @@ -535,37 +644,49 @@ void BasicBlockConstraintMap::set(Index index, Expression* value) { // Apply a constraint to a value, x = C. if (Properties::isSingleConstantExpression(value)) { auto c = Properties::getLiteral(value); - set(index, Constraint{Abstract::Eq, {c}}); + set(index, Constraint{Eq, {c}}); return; } // Apply a constraint to a local, x = y. if (auto* get = value->dynCast()) { - set(index, Constraint{Abstract::Eq, {get->index}}); + set(index, Constraint{Eq, {get->index}}); return; } if (auto* tee = value->dynCast()) { - set(index, Constraint{Abstract::Eq, {tee->index}}); + set(index, Constraint{Eq, {tee->index}}); return; } // Apply an increment of a local, x = y + 1. Index y; - if (matches(value, binary(Abstract::Add, local(&y), ival(1)))) { - // The local y must have old constraints that we know how to increment. - auto old = get(y); + if (matches(value, binary(Add, local(&y), ival(1)))) { + // The local y must have old constraints that we know how to increment and + // transform into new ones. + const auto old = get(y); + auto new_ = old; + + // If we see an unsigned upper bound but not a lower one, we can add a + // lower one (if we do not overflow). That is, if we see x < 100, x++, then + // we can not only update x < 100 to x <= 100, but also add x > 0 (since 0 + // is impossible after the ++). This is not possible for signed operations, + // since x++ does not prove x > 0 there (0 is not the only value that is + // <= 0). + bool hasUnsignedUpperBound = false; + Type type; // Iterate over the old constraints and increment each one. - for (auto iter = old.begin(); iter != old.end();) { + for (auto iter = new_.begin(); iter != new_.end();) { auto& c = *iter; auto* N = std::get_if(&c.term); if (!N) { // A non-constant term, which we don't know how to increment. Simply // remove it: we are losing proving power here, but doing so is never // invalid. - iter = old.erase(iter); + iter = new_.erase(iter); continue; } + type = N->type; switch (c.op) { // x == N, x++ => x == N+1. @@ -585,32 +706,39 @@ void BasicBlockConstraintMap::set(Index index, Expression* value) { break; case LtU: c.op = LeU; + hasUnsignedUpperBound = true; break; // x <= N, x++ => x <= N+1 if no overflow case LeS: if (N->isSignedMax()) { - iter = old.erase(iter); + iter = new_.erase(iter); continue; } *N = N->add(Literal::makeFromInt32(1, N->type)); break; case LeU: if (N->isUnsignedMax()) { - iter = old.erase(iter); + iter = new_.erase(iter); continue; } *N = N->add(Literal::makeFromInt32(1, N->type)); + hasUnsignedUpperBound = true; break; default: // Something we don't recognize. - iter = old.erase(iter); + iter = new_.erase(iter); continue; } ++iter; } - set(index, old); + if (hasUnsignedUpperBound) { + // We know we did not overflow (we are bounded from above), so add x > 0. + new_.approximateAnd({GtU, {Literal::makeFromInt32(0, type)}}); + } + + set(index, new_); return; } diff --git a/src/ir/constraint.h b/src/ir/constraint.h index c7814effea5..85280dcbd1e 100644 --- a/src/ir/constraint.h +++ b/src/ir/constraint.h @@ -27,6 +27,8 @@ #include "ir/abstract.h" #include "support/inplace_vector.h" +#include "support/iu64.h" +#include "support/span.h" #include "support/utilities.h" #include "wasm.h" @@ -63,6 +65,10 @@ struct Constraint { Constraint negate() const { return Constraint{Abstract::negateRelational(op), term}; } + + // Convert the constraint into a constant span, if possible. For example, + // "<= 100 (unsigned)" turns into the span [0, 100]. + std::optional> getSpan() const; }; // We limit constraints to a low number to ensure good performance even with diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index 36a52220125..47039f1ac0b 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -1,3 +1,5 @@ +#include + #include "ir/constraint.h" #include "ir/abstract.h" #include "gtest/gtest.h" @@ -275,8 +277,14 @@ TEST(ConstraintTest, TestOrInequality) { auto empty = AndedConstraintSet::makeProvesNothing(); checkOr(eq5, ges7, empty); - // x > 5 || x >= 6 => x > 5 - checkOr(gts5, ges6, gts5); + // x > 5 and x >= 6 are equivalent, so ORing them does not change either. + auto ored1 = gts5; + ored1.approximateOr(ges6); + EXPECT_EQ(ored1, gts5); + + auto ored2 = ges6; + ored2.approximateOr(gts5); + EXPECT_EQ(ored2, ges6); // x > 5 || x >= 5 => x >= 5 checkOr(gts5, ges5, ges5); @@ -294,8 +302,8 @@ TEST(ConstraintTest, TestOrInequality) { // x > signed_max || x >= (signed_max + 1 === signed_min) != x > signed_max AndedConstraintSet gtsMax{ {GtS, {Literal(std::numeric_limits::max())}}}; - // TODO: x > signed_max is always false, so this could return a contradiction - checkOr(gtsMax, gesMin, empty); + // x > signed_max is impossible, so it vanishes in the OR. + checkOr(gtsMax, gesMin, gesMin); } TEST(ConstraintTest, TestOrLoop) { @@ -484,9 +492,16 @@ TEST(ConstraintTest, TestAndLoop) { // inputs). checkAnd(le5, lt5U, AndedConstraintSet{le5[0], lt5U[0]}); - // Different constants do not optimize, but could TODO + // Different constants optimize when one implies the other (x <= 5 and x < 6 + // are equivalent). AndedConstraintSet lt6{{LtS, {Literal(int32_t(6))}}}; - checkAnd(le5, lt6, AndedConstraintSet{le5[0], lt6[0]}); + auto anded1 = le5; + anded1.approximateAnd(lt6[0]); + EXPECT_EQ(anded1, le5); + + auto anded2 = lt6; + anded2.approximateAnd(le5[0]); + EXPECT_EQ(anded2, lt6); // A non-constant. // x <= y && x < y => x < y @@ -592,10 +607,13 @@ TEST(ConstraintTest, TestIncrement) { map.set(0, &add); check(map.get(0), {LeS, {Literal(int32_t(5))}}); - // Ditto, unsigned + // Ditto, unsigned. We also add a lower bound here, as after $0++, $0 > 0 + // (due to no overflow, proven by the upper bound). + Constraint gtu0{GtU, {Literal(int32_t(0))}}; map.set(0, {LtU, {Literal(int32_t(5))}}); map.set(0, &add); - check(map.get(0), {LeU, {Literal(int32_t(5))}}); + EXPECT_EQ(map.get(0), + (AndedConstraintSet{{LeU, {Literal(int32_t(5))}}, gtu0})); // $0 <= 5, $0++ => $0 <= 6 (signed) map.set(0, {LeS, {Literal(int32_t(5))}}); @@ -605,7 +623,8 @@ TEST(ConstraintTest, TestIncrement) { // Ditto, unsigned map.set(0, {LeU, {Literal(int32_t(5))}}); map.set(0, &add); - check(map.get(0), {LeU, {Literal(int32_t(6))}}); + EXPECT_EQ(map.get(0), + (AndedConstraintSet{{LeU, {Literal(int32_t(6))}}, gtu0})); // $0 <= max_signed, $0++ => nothing, because it would overflow map.set(0, {LeS, {Literal::makeSignedMax(Type::i32)}}); @@ -621,7 +640,9 @@ TEST(ConstraintTest, TestIncrement) { map.set(0, {LeU, {Literal::makeSignedMax(Type::i32)}}); map.set(0, &add); auto one = Literal::makeFromInt32(1, Type::i32); - check(map.get(0), {LeU, {Literal::makeSignedMax(Type::i32).add(one)}}); + EXPECT_EQ(map.get(0), + (AndedConstraintSet{ + {LeU, {Literal::makeSignedMax(Type::i32).add(one)}}, gtu0})); // Multiple constraints at once: // $0 >= 10 && $0 < 20, $0++ => $0 > 10 && $0 <= 20 @@ -660,3 +681,364 @@ TEST(ConstraintTest, TestEqConstraints) { // having $1 > $0 and needing to look $0 up. check(map.get(1), {GtS, {Literal(int32_t(42))}}); } + +TEST(ConstraintTest, GetSpan) { + const IU64 minI32(std::numeric_limits::min()); + const IU64 maxI32(std::numeric_limits::max()); + const IU64 maxU32(std::numeric_limits::max()); + const IU64 minI64(std::numeric_limits::min()); + const IU64 maxI64(std::numeric_limits::max()); + const IU64 maxU64(std::numeric_limits::max()); + + // Non-literal terms have no constant span. + EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpan()), std::nullopt); + EXPECT_EQ((Constraint{LtS, {Index(1)}}.getSpan()), std::nullopt); + EXPECT_EQ((Constraint{GeU, {Index(2)}}.getSpan()), std::nullopt); + + // Unsupported operations (e.g. Ne) have no constant span. + EXPECT_EQ((Constraint{Ne, {Literal(int32_t(5))}}.getSpan()), std::nullopt); + EXPECT_EQ((Constraint{Ne, {Literal(int32_t(0))}}.getSpan()), std::nullopt); + + // Eq (i32): non-negative values up to int32_t max have an unambiguous span. + EXPECT_EQ((Constraint{Eq, {Literal(int32_t(0))}}.getSpan()), + (Span{0, 0})); + EXPECT_EQ((Constraint{Eq, {Literal(int32_t(1))}}.getSpan()), + (Span{1, 1})); + EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getSpan()), + (Span{42, 42})); + EXPECT_EQ( + (Constraint{Eq, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{maxI32, maxI32})); + + // Eq (i32) with negative or large unsigned values returns nullopt due to + // signed/unsigned ambiguity. + EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-1))}}.getSpan()), std::nullopt); + EXPECT_EQ((Constraint{Eq, {Literal(int32_t(-42))}}.getSpan()), std::nullopt); + EXPECT_EQ( + (Constraint{Eq, {Literal(std::numeric_limits::min())}}.getSpan()), + std::nullopt); + EXPECT_EQ((Constraint{Eq, {Literal(uint32_t(0x80000000u))}}.getSpan()), + std::nullopt); + EXPECT_EQ( + (Constraint{Eq, {Literal(std::numeric_limits::max())}}.getSpan()), + std::nullopt); + + // Eq (i64): non-negative values up to int64_t max have an unambiguous span. + EXPECT_EQ((Constraint{Eq, {Literal(int64_t(0))}}.getSpan()), + (Span{0, 0})); + EXPECT_EQ((Constraint{Eq, {Literal(int64_t(42))}}.getSpan()), + (Span{42, 42})); + EXPECT_EQ( + (Constraint{Eq, {Literal(int64_t(std::numeric_limits::max()) + 1)}} + .getSpan()), + (Span{uint64_t(std::numeric_limits::max()) + 1, + uint64_t(std::numeric_limits::max()) + 1})); + EXPECT_EQ( + (Constraint{Eq, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{maxI64, maxI64})); + + // Eq (i64) with negative or large unsigned values returns nullopt. + EXPECT_EQ((Constraint{Eq, {Literal(int64_t(-1))}}.getSpan()), std::nullopt); + EXPECT_EQ( + (Constraint{Eq, {Literal(std::numeric_limits::min())}}.getSpan()), + std::nullopt); + EXPECT_EQ((Constraint{Eq, {Literal(uint64_t(uint64_t(1) << 63))}}.getSpan()), + std::nullopt); + EXPECT_EQ( + (Constraint{Eq, {Literal(std::numeric_limits::max())}}.getSpan()), + std::nullopt); + + // LtS (i32): [minI32, C - 1] + EXPECT_EQ((Constraint{LtS, {Literal(int32_t(10))}}.getSpan()), + (Span{minI32, IU64(9)})); + EXPECT_EQ((Constraint{LtS, {Literal(int32_t(0))}}.getSpan()), + (Span{minI32, IU64(-1)})); + EXPECT_EQ((Constraint{LtS, {Literal(int32_t(-5))}}.getSpan()), + (Span{minI32, IU64(-6)})); + EXPECT_EQ( + (Constraint{LtS, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{minI32, IU64(std::numeric_limits::max() - 1)})); + // LtS min signed (i32): empty span + auto ltsMin32 = + Constraint{LtS, {Literal(std::numeric_limits::min())}}.getSpan(); + ASSERT_TRUE(ltsMin32.has_value()); + EXPECT_TRUE(ltsMin32->isEmpty()); + EXPECT_EQ(ltsMin32, Span::empty()); + + // LtS (i64): [minI64, C - 1] + EXPECT_EQ((Constraint{LtS, {Literal(int64_t(100))}}.getSpan()), + (Span{minI64, IU64(99)})); + EXPECT_EQ((Constraint{LtS, {Literal(int64_t(0))}}.getSpan()), + (Span{minI64, IU64(-1)})); + EXPECT_EQ( + (Constraint{LtS, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{minI64, IU64(std::numeric_limits::max() - 1)})); + // LtS min signed (i64): empty span + auto ltsMin64 = + Constraint{LtS, {Literal(std::numeric_limits::min())}}.getSpan(); + ASSERT_TRUE(ltsMin64.has_value()); + EXPECT_TRUE(ltsMin64->isEmpty()); + EXPECT_EQ(ltsMin64, Span::empty()); + + // LtU (i32): [0, C - 1] + EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(10))}}.getSpan()), + (Span{IU64(0), IU64(9)})); + EXPECT_EQ((Constraint{LtU, {Literal(uint32_t(1))}}.getSpan()), + (Span{IU64(0), IU64(0)})); + EXPECT_EQ( + (Constraint{LtU, {Literal(std::numeric_limits::max())}} + .getSpan()), + (Span{IU64(0), + IU64(uint64_t(std::numeric_limits::max()) - 1)})); + // LtU 0 (i32): empty span + auto ltuZero32 = Constraint{LtU, {Literal(uint32_t(0))}}.getSpan(); + ASSERT_TRUE(ltuZero32.has_value()); + EXPECT_TRUE(ltuZero32->isEmpty()); + EXPECT_EQ(ltuZero32, Span::empty()); + + // LtU (i64): [0, C - 1] + EXPECT_EQ((Constraint{LtU, {Literal(uint64_t(100))}}.getSpan()), + (Span{IU64(0), IU64(99)})); + EXPECT_EQ( + (Constraint{LtU, {Literal(std::numeric_limits::max())}} + .getSpan()), + (Span{IU64(0), IU64(std::numeric_limits::max() - 1)})); + // LtU 0 (i64): empty span + auto ltuZero64 = Constraint{LtU, {Literal(uint64_t(0))}}.getSpan(); + ASSERT_TRUE(ltuZero64.has_value()); + EXPECT_TRUE(ltuZero64->isEmpty()); + EXPECT_EQ(ltuZero64, Span::empty()); + + // LeS (i32): [minI32, C] + EXPECT_EQ((Constraint{LeS, {Literal(int32_t(10))}}.getSpan()), + (Span{minI32, IU64(10)})); + EXPECT_EQ((Constraint{LeS, {Literal(int32_t(0))}}.getSpan()), + (Span{minI32, IU64(0)})); + EXPECT_EQ((Constraint{LeS, {Literal(int32_t(-5))}}.getSpan()), + (Span{minI32, IU64(-5)})); + EXPECT_EQ( + (Constraint{LeS, {Literal(std::numeric_limits::min())}}.getSpan()), + (Span{minI32, minI32})); + EXPECT_EQ( + (Constraint{LeS, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{minI32, maxI32})); + + // LeS (i64): [minI64, C] + EXPECT_EQ((Constraint{LeS, {Literal(int64_t(10))}}.getSpan()), + (Span{minI64, IU64(10)})); + EXPECT_EQ( + (Constraint{LeS, {Literal(std::numeric_limits::min())}}.getSpan()), + (Span{minI64, minI64})); + EXPECT_EQ( + (Constraint{LeS, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{minI64, maxI64})); + + // LeU (i32): [0, C] + EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(0))}}.getSpan()), + (Span{IU64(0), IU64(0)})); + EXPECT_EQ((Constraint{LeU, {Literal(uint32_t(10))}}.getSpan()), + (Span{IU64(0), IU64(10)})); + EXPECT_EQ((Constraint{LeU, {Literal(std::numeric_limits::max())}} + .getSpan()), + (Span{IU64(0), maxU32})); + + // LeU (i64): [0, C] + EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(0))}}.getSpan()), + (Span{IU64(0), IU64(0)})); + EXPECT_EQ((Constraint{LeU, {Literal(uint64_t(10))}}.getSpan()), + (Span{IU64(0), IU64(10)})); + EXPECT_EQ((Constraint{LeU, {Literal(std::numeric_limits::max())}} + .getSpan()), + (Span{IU64(0), maxU64})); + + // GtS (i32): [C + 1, maxI32] + EXPECT_EQ((Constraint{GtS, {Literal(int32_t(10))}}.getSpan()), + (Span{IU64(11), maxI32})); + EXPECT_EQ((Constraint{GtS, {Literal(int32_t(0))}}.getSpan()), + (Span{IU64(1), maxI32})); + EXPECT_EQ((Constraint{GtS, {Literal(int32_t(-5))}}.getSpan()), + (Span{IU64(-4), maxI32})); + EXPECT_EQ( + (Constraint{GtS, {Literal(std::numeric_limits::min())}}.getSpan()), + (Span{IU64(std::numeric_limits::min() + 1), maxI32})); + EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits::max() - 1)}} + .getSpan()), + (Span{maxI32, maxI32})); + // GtS max signed (i32): empty span + auto gtsMax32 = + Constraint{GtS, {Literal(std::numeric_limits::max())}}.getSpan(); + ASSERT_TRUE(gtsMax32.has_value()); + EXPECT_TRUE(gtsMax32->isEmpty()); + EXPECT_EQ(gtsMax32, Span::empty()); + + // GtS (i64): [C + 1, maxI64] + EXPECT_EQ((Constraint{GtS, {Literal(int64_t(10))}}.getSpan()), + (Span{IU64(11), maxI64})); + EXPECT_EQ((Constraint{GtS, {Literal(int64_t(0))}}.getSpan()), + (Span{IU64(1), maxI64})); + EXPECT_EQ( + (Constraint{GtS, {Literal(std::numeric_limits::min())}}.getSpan()), + (Span{IU64(std::numeric_limits::min() + 1), maxI64})); + EXPECT_EQ((Constraint{GtS, {Literal(std::numeric_limits::max() - 1)}} + .getSpan()), + (Span{maxI64, maxI64})); + // GtS max signed (i64): empty span + auto gtsMax64 = + Constraint{GtS, {Literal(std::numeric_limits::max())}}.getSpan(); + ASSERT_TRUE(gtsMax64.has_value()); + EXPECT_TRUE(gtsMax64->isEmpty()); + EXPECT_EQ(gtsMax64, Span::empty()); + + // GtU (i32): [C + 1, maxU32] + EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(0))}}.getSpan()), + (Span{IU64(1), maxU32})); + EXPECT_EQ((Constraint{GtU, {Literal(uint32_t(10))}}.getSpan()), + (Span{IU64(11), maxU32})); + EXPECT_EQ( + (Constraint{GtU, {Literal(std::numeric_limits::max() - 1)}} + .getSpan()), + (Span{maxU32, maxU32})); + // GtU max unsigned (i32): empty span + auto gtuMax32 = + Constraint{GtU, {Literal(std::numeric_limits::max())}}.getSpan(); + ASSERT_TRUE(gtuMax32.has_value()); + EXPECT_TRUE(gtuMax32->isEmpty()); + EXPECT_EQ(gtuMax32, Span::empty()); + + // GtU (i64): [C + 1, maxU64] + EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(0))}}.getSpan()), + (Span{IU64(1), maxU64})); + EXPECT_EQ((Constraint{GtU, {Literal(uint64_t(10))}}.getSpan()), + (Span{IU64(11), maxU64})); + EXPECT_EQ( + (Constraint{GtU, {Literal(std::numeric_limits::max() - 1)}} + .getSpan()), + (Span{maxU64, maxU64})); + // GtU max unsigned (i64): empty span + auto gtuMax64 = + Constraint{GtU, {Literal(std::numeric_limits::max())}}.getSpan(); + ASSERT_TRUE(gtuMax64.has_value()); + EXPECT_TRUE(gtuMax64->isEmpty()); + EXPECT_EQ(gtuMax64, Span::empty()); + + // GeS (i32): [C, maxI32] + EXPECT_EQ((Constraint{GeS, {Literal(int32_t(10))}}.getSpan()), + (Span{IU64(10), maxI32})); + EXPECT_EQ((Constraint{GeS, {Literal(int32_t(0))}}.getSpan()), + (Span{IU64(0), maxI32})); + EXPECT_EQ((Constraint{GeS, {Literal(int32_t(-5))}}.getSpan()), + (Span{IU64(-5), maxI32})); + EXPECT_EQ( + (Constraint{GeS, {Literal(std::numeric_limits::min())}}.getSpan()), + (Span{minI32, maxI32})); + EXPECT_EQ( + (Constraint{GeS, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{maxI32, maxI32})); + + // GeS (i64): [C, maxI64] + EXPECT_EQ((Constraint{GeS, {Literal(int64_t(10))}}.getSpan()), + (Span{IU64(10), maxI64})); + EXPECT_EQ((Constraint{GeS, {Literal(int64_t(0))}}.getSpan()), + (Span{IU64(0), maxI64})); + EXPECT_EQ( + (Constraint{GeS, {Literal(std::numeric_limits::min())}}.getSpan()), + (Span{minI64, maxI64})); + EXPECT_EQ( + (Constraint{GeS, {Literal(std::numeric_limits::max())}}.getSpan()), + (Span{maxI64, maxI64})); + + // GeU (i32): [C, maxU32] + EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(0))}}.getSpan()), + (Span{IU64(0), maxU32})); + EXPECT_EQ((Constraint{GeU, {Literal(uint32_t(10))}}.getSpan()), + (Span{IU64(10), maxU32})); + EXPECT_EQ((Constraint{GeU, {Literal(std::numeric_limits::max())}} + .getSpan()), + (Span{maxU32, maxU32})); + + // GeU (i64): [C, maxU64] + EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(0))}}.getSpan()), + (Span{IU64(0), maxU64})); + EXPECT_EQ((Constraint{GeU, {Literal(uint64_t(10))}}.getSpan()), + (Span{IU64(10), maxU64})); + EXPECT_EQ((Constraint{GeU, {Literal(std::numeric_limits::max())}} + .getSpan()), + (Span{maxU64, maxU64})); +} + +TEST(ConstraintTest, SpanOptimizations) { + // Using spans, we can optimize things like {x < 100} => {x < 200}. + Constraint lts100{LtS, {Literal(int32_t(100))}}; + Constraint lts200{LtS, {Literal(int32_t(200))}}; + EXPECT_EQ(AndedConstraintSet{lts100}.proves(lts200), True); + + // Mixing signed and unsigned works fine: x in [0, 100] (x <= 100 unsigned) + // proves x in [-MIN_INT, 200] (x < 200 signed) is true. + Constraint leu100{LtU, {Literal(int32_t(100))}}; + EXPECT_EQ(AndedConstraintSet{leu100}.proves(lts200), True); + + // Replacing 100 with 500, we can no longer prove anything. + Constraint leu500{LtU, {Literal(int32_t(500))}}; + EXPECT_EQ(AndedConstraintSet{leu500}.proves(lts200), Unknown); +} + +TEST(ConstraintTest, EmptySpanContradiction) { + // Impossible constraints produce empty spans. + Constraint gtsMax32{GtS, {Literal(std::numeric_limits::max())}}; + Constraint ltsMin32{LtS, {Literal(std::numeric_limits::min())}}; + Constraint ltuZero32{LtU, {Literal(uint32_t(0))}}; + Constraint gtuMax32{GtU, {Literal(std::numeric_limits::max())}}; + + Constraint gtsMax64{GtS, {Literal(std::numeric_limits::max())}}; + Constraint ltsMin64{LtS, {Literal(std::numeric_limits::min())}}; + Constraint ltuZero64{LtU, {Literal(uint64_t(0))}}; + Constraint gtuMax64{GtU, {Literal(std::numeric_limits::max())}}; + + Constraint eq5{Eq, {Literal(int32_t(5))}}; + Constraint ge0{GeS, {Literal(int32_t(0))}}; + Constraint eq100_64{Eq, {Literal(int64_t(100))}}; + + // An impossible constraint proves anything is True. + EXPECT_EQ(AndedConstraintSet{gtsMax32}.proves(eq5), True); + EXPECT_EQ(AndedConstraintSet{ltsMin32}.proves(ge0), True); + EXPECT_EQ(AndedConstraintSet{ltuZero32}.proves(eq5), True); + EXPECT_EQ(AndedConstraintSet{gtuMax32}.proves(ge0), True); + + EXPECT_EQ(AndedConstraintSet{gtsMax64}.proves(eq100_64), True); + EXPECT_EQ(AndedConstraintSet{ltsMin64}.proves(eq100_64), True); + EXPECT_EQ(AndedConstraintSet{ltuZero64}.proves(eq100_64), True); + EXPECT_EQ(AndedConstraintSet{gtuMax64}.proves(eq100_64), True); + + // Impossible constraint proves another impossible constraint is True. + EXPECT_EQ(AndedConstraintSet{gtsMax32}.proves(ltsMin32), True); + EXPECT_EQ(AndedConstraintSet{ltuZero32}.proves(gtuMax32), True); + + // A normal constraint proves an impossible constraint is False. + EXPECT_EQ(AndedConstraintSet{eq5}.proves(gtsMax32), False); + EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltsMin32), False); + EXPECT_EQ(AndedConstraintSet{eq5}.proves(ltuZero32), False); + EXPECT_EQ(AndedConstraintSet{eq5}.proves(gtuMax32), False); + + EXPECT_EQ(AndedConstraintSet{eq100_64}.proves(gtsMax64), False); + EXPECT_EQ(AndedConstraintSet{eq100_64}.proves(ltsMin64), False); + EXPECT_EQ(AndedConstraintSet{eq100_64}.proves(ltuZero64), False); + EXPECT_EQ(AndedConstraintSet{eq100_64}.proves(gtuMax64), False); + + // An impossible constraint in a set proves any condition. + AndedConstraintSet s{gtsMax32}; + EXPECT_EQ(s.proves(eq5), True); + EXPECT_EQ(s.proves(ge0), True); + + // Adding an impossible constraint to a non-empty set proves False and turns + // the set into an explicit contradiction (provesEverything() == true). + AndedConstraintSet s2; + s2.set(eq5); + s2.approximateAnd(ltuZero32); + EXPECT_TRUE(s2.provesEverything()); + + // ORing an impossible constraint (which has no models) with a valid set + // leaves the valid set. + AndedConstraintSet valid{{Eq, {Literal(int32_t(42))}}}; + AndedConstraintSet impossible{gtsMax32}; + checkOr(valid, impossible, valid); +} diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast index 9e503b01e95..5d7f122a69a 100644 --- a/test/lit/passes/constraint-analysis-loops.wast +++ b/test/lit/passes/constraint-analysis-loops.wast @@ -665,7 +665,7 @@ (br $out) ) ) - ;; x > 0 && x <= 100 here (but we need loops mode to get both). + ;; x > 0 && x <= 100 here. (drop (i32.gt_u (local.get $x)