From f14f67433131db2bbff1f1598db9bfede0915c45 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 21 Aug 2026 12:30:23 -0700 Subject: [PATCH 1/4] work --- src/ir/constraint.cpp | 153 +++++++++++++++++++++++++------------- src/ir/constraint.h | 12 ++- test/gtest/constraint.cpp | 85 +++++++++++++++++++++ 3 files changed, 199 insertions(+), 51 deletions(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 6e7c8ce81f2..3d38bf99230 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -22,26 +22,58 @@ namespace wasm::constraint { -std::optional> Constraint::getSpan() const { +namespace { + +std::optional> +getSpanInternal(const Constraint& c, std::optional type, bool exact) { using namespace Abstract; - auto* c = std::get_if(&term); - if (!c) { - // Not comparing to a constant, so cannot be a constant span. - return {}; + auto* cc = std::get_if(&c.term); + if (cc) { + // If passed in, the type must be right. + assert(!type || *type == cc->type); + + type = cc->type; } - 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 + auto minSigned = type && *type == Type::i32 + ? std::numeric_limits::min() + : std::numeric_limits::min(); + auto maxSigned = type && *type == Type::i32 + ? std::numeric_limits::max() + : std::numeric_limits::max(); + auto maxUnsigned = type && *type == Type::i32 ? std::numeric_limits::max() : std::numeric_limits::max(); - switch (op) { + if (!cc) { + // Not comparing to a constant, so we can't infer anything exact, but might + // if we just need something we can prove, and if we know the type. + if (!exact && type) { + switch (c.op) { + // x < y, i.e., x is less than *something*, proves x < MAX_INT. + case LtS: + return Span{minSigned, maxSigned - 1}; + case LtU: + return Span{0, maxUnsigned - 1}; + + // Similarly, x > y proves x > MIN_INT. + case GtS: + return Span{minSigned + 1, maxSigned}; + case GtU: + return Span{1, maxUnsigned}; + + default: { + } + } + } + + return {}; + } + + switch (c.op) { case Eq: { - auto x = c->getUnsigned(); + auto x = cc->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 @@ -54,46 +86,46 @@ std::optional> Constraint::getSpan() const { } case LtS: - if (c->getInteger() == minSigned) { + if (cc->getInteger() == minSigned) { // Less than the lowest possible number is an empty span. return Span::empty(); } else { - return Span{minSigned, c->getInteger() - 1}; + return Span{minSigned, cc->getInteger() - 1}; } break; case LtU: - if (c->getInteger() == 0) { + if (cc->getInteger() == 0) { // Less than the lowest possible number is an empty span. return Span::empty(); } else { - return Span{0, c->getUnsigned() - 1}; + return Span{0, cc->getUnsigned() - 1}; } break; case LeS: - return Span{minSigned, c->getInteger()}; + return Span{minSigned, cc->getInteger()}; case LeU: - return Span{0, c->getUnsigned()}; + return Span{0, cc->getUnsigned()}; case GtS: - if (c->getInteger() == maxSigned) { + if (cc->getInteger() == maxSigned) { // Greater than the highest possible number is an empty span. return Span::empty(); } else { - return Span{c->getInteger() + 1, maxSigned}; + return Span{cc->getInteger() + 1, maxSigned}; } break; case GtU: - if (c->getUnsigned() == maxUnsigned) { + if (cc->getUnsigned() == maxUnsigned) { // Greater than the highest possible number is an empty span. return Span::empty(); } else { - return Span{c->getUnsigned() + 1, maxUnsigned}; + return Span{cc->getUnsigned() + 1, maxUnsigned}; } break; case GeS: - return Span{c->getInteger(), maxSigned}; + return Span{cc->getInteger(), maxSigned}; case GeU: - return Span{c->getUnsigned(), maxUnsigned}; + return Span{cc->getUnsigned(), maxUnsigned}; default: { } @@ -102,6 +134,17 @@ std::optional> Constraint::getSpan() const { return {}; } +} // anonymous namespace + +std::optional> Constraint::getSpan(std::optional type) const { + return getSpanInternal(*this, type, true); +} + +std::optional> +Constraint::getProvenSpan(std::optional type) const { + return getSpanInternal(*this, type, false); +} + namespace { Result TrueFalse(bool x) { return x ? True : False; } @@ -158,31 +201,6 @@ 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 @@ -212,7 +230,42 @@ Result provesPair(const Constraint& a, const Constraint& b) { auto* aConstant = std::get_if(&a.term); auto* bConstant = std::get_if(&b.term); if (aConstant && bConstant) { - return provesConstantPair(a.op, *aConstant, b.op, *bConstant); + auto result = provesConstantPair(a.op, *aConstant, b.op, *bConstant); + if (result != Unknown) { + return result; + } + } + + // If we can represent both as spans, we can calculate that way. At least one + // must be a constant in this case, so that we know the type. + if (aConstant || bConstant) { + auto type = aConstant ? aConstant->type : bConstant->type; + // Use a proven span for a, and an exact one for b. This allows us to do + // a => proven span for a => exact span for b => b. + if (auto aSpan = a.getProvenSpan(type)) { + if (auto bSpan = b.getSpan(type)) { + 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; + } + } + } } return Unknown; diff --git a/src/ir/constraint.h b/src/ir/constraint.h index 85280dcbd1e..ced8edd0b46 100644 --- a/src/ir/constraint.h +++ b/src/ir/constraint.h @@ -68,7 +68,17 @@ struct Constraint { // Convert the constraint into a constant span, if possible. For example, // "<= 100 (unsigned)" turns into the span [0, 100]. - std::optional> getSpan() const; + // + // An optional type may be passed in. If not, the type is inferred from the + // term, when possible. + std::optional> getSpan(std::optional type = {}) const; + + // Get a span we can prove. This is less precise than getSpan, which gets an + // *exact* span to represent the Constraint. Here we only return a span we can + // prove is true. For example, x < y cannot be represented exactly using a + // span (y is not a constant), but that x is smaller than *something* proves + // x is not MAX_INT, so we can return the span [MIN_INT, MAX_INT - 1]. + std::optional> getProvenSpan(std::optional type = {}) 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 47039f1ac0b..7e8423f7d04 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -39,6 +39,9 @@ TEST(ConstraintTest, TestEq) { // x != 5: we can infer false. EXPECT_EQ(s.proves(Constraint{Ne, {Literal(int32_t(5))}}), False); + + // x > y: we can infer nothing. + EXPECT_EQ(s.proves(Constraint{GtS, {Index(1)}}), Unknown); } TEST(ConstraintTest, TestNe) { @@ -682,6 +685,24 @@ TEST(ConstraintTest, TestEqConstraints) { check(map.get(1), {GtS, {Literal(int32_t(42))}}); } +TEST(ConstraintTest, ComplexOrRegression) { + // $0 == 0 + BasicBlockConstraintMap left; + left.setReachable(); + left.set(0, {Eq, {Literal(int32_t(0))}}); + + // $0 <= 100, $0 > $1 + BasicBlockConstraintMap right; + right.setReachable(); + right.set(0, {{LeS, {Literal(int32_t(100))}}, {GtS, {Index(1)}}}); + + // $0 == 0 || $0 <= 100 => $0 <= 100 (0 is included in <= 100), but the + // other constraint, $0 > $1, was only on one side, and vanishes. + right.approximateOr(left); + check(right.get(0), {LeS, {Literal(int32_t(100))}}); + EXPECT_TRUE(right.get(1).empty()); +} + TEST(ConstraintTest, GetSpan) { const IU64 minI32(std::numeric_limits::min()); const IU64 maxI32(std::numeric_limits::max()); @@ -966,6 +987,70 @@ TEST(ConstraintTest, GetSpan) { (Span{maxU64, maxU64})); } +TEST(ConstraintTest, GetSpanType) { + const IU64 minI32(std::numeric_limits::min()); + const IU64 minI32Plus1(std::numeric_limits::min() + 1); + + const IU64 maxI32(std::numeric_limits::max()); + const IU64 maxI32Minus1(std::numeric_limits::max() - 1); + + const IU64 maxU32(std::numeric_limits::max()); + const IU64 maxU32Minus1(std::numeric_limits::max() - 1); + + const IU64 minI64(std::numeric_limits::min()); + const IU64 minI64Plus1(std::numeric_limits::min() + 1); + + const IU64 maxI64(std::numeric_limits::max()); + const IU64 maxI64Minus1(std::numeric_limits::max() - 1); + + const IU64 maxU64(std::numeric_limits::max()); + const IU64 maxU64Minus1(std::numeric_limits::max() - 1); + + // Providing the type to getSpan() doesn't help with certain things. + EXPECT_EQ((Constraint{Eq, {Index(0)}}.getSpan(Type::i32)), std::nullopt); + EXPECT_EQ((Constraint{Ne, {Index(1)}}.getSpan(Type::i64)), std::nullopt); + EXPECT_EQ((Constraint{GeU, {Index(2)}}.getSpan(Type::i32)), std::nullopt); + EXPECT_EQ((Constraint{GeS, {Index(0)}}.getSpan(Type::i64)), std::nullopt); + EXPECT_EQ((Constraint{LeU, {Index(1)}}.getSpan(Type::i64)), std::nullopt); + EXPECT_EQ((Constraint{LeS, {Index(2)}}.getSpan(Type::i32)), std::nullopt); + + // But it does help with others: x < y means x cannot be MAX_INT, so we can + // report a *proven* span, if not an exact one. + EXPECT_EQ((Constraint{LtS, {Index(0)}}.getProvenSpan(Type::i32)), + (Span{minI32, maxI32Minus1})); + EXPECT_EQ((Constraint{LtS, {Index(1)}}.getProvenSpan(Type::i64)), + (Span{minI64, maxI64Minus1})); + + EXPECT_EQ((Constraint{LtU, {Index(2)}}.getProvenSpan(Type::i32)), + (Span{0, maxU32Minus1})); + EXPECT_EQ((Constraint{LtU, {Index(0)}}.getProvenSpan(Type::i64)), + (Span{0, maxU64Minus1})); + + EXPECT_EQ((Constraint{GtS, {Index(1)}}.getProvenSpan(Type::i32)), + (Span{minI32Plus1, maxI32})); + EXPECT_EQ((Constraint{GtS, {Index(2)}}.getProvenSpan(Type::i64)), + (Span{minI64Plus1, maxI64})); + + EXPECT_EQ((Constraint{GtU, {Index(0)}}.getProvenSpan(Type::i32)), + (Span{1, maxU32})); + EXPECT_EQ((Constraint{GtU, {Index(1)}}.getProvenSpan(Type::i64)), + (Span{1, maxU64})); + + // But all the last things are impossible with an exact span. + EXPECT_EQ((Constraint{LtS, {Index(0)}}.getSpan(Type::i32)), std::nullopt); + EXPECT_EQ((Constraint{LtS, {Index(1)}}.getSpan(Type::i64)), std::nullopt); + EXPECT_EQ((Constraint{LtU, {Index(2)}}.getSpan(Type::i32)), std::nullopt); + EXPECT_EQ((Constraint{LtU, {Index(0)}}.getSpan(Type::i64)), std::nullopt); + EXPECT_EQ((Constraint{GtS, {Index(1)}}.getSpan(Type::i32)), std::nullopt); + EXPECT_EQ((Constraint{GtS, {Index(2)}}.getSpan(Type::i64)), std::nullopt); + EXPECT_EQ((Constraint{GtU, {Index(0)}}.getSpan(Type::i32)), std::nullopt); + EXPECT_EQ((Constraint{GtU, {Index(1)}}.getSpan(Type::i64)), std::nullopt); + + // Proven spans are otherwise like normal ones. + EXPECT_EQ((Constraint{Eq, {Literal(int32_t(42))}}.getProvenSpan()), + (Span{42, 42})); +} + TEST(ConstraintTest, SpanOptimizations) { // Using spans, we can optimize things like {x < 100} => {x < 200}. Constraint lts100{LtS, {Literal(int32_t(100))}}; From 48cddc7ee85ead19424b67c4e48617562f4ab064 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 21 Aug 2026 12:36:25 -0700 Subject: [PATCH 2/4] fix --- src/ir/constraint.cpp | 55 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 6e7c8ce81f2..d0ba04d88ab 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -314,6 +314,55 @@ std::optional fusedApproximateAndPair(const Constraint& a, return {}; } +bool isImmediateContradiction(const Constraint& c) { + using namespace Abstract; + + auto* cc = std::get_if(&c.term); + if (!cc) { + // Only operations on constants can be immediate contradictions. + return false; + } + + auto minSigned = cc->type == Type::i32 ? std::numeric_limits::min() + : std::numeric_limits::min(); + auto maxSigned = cc->type == Type::i32 ? std::numeric_limits::max() + : std::numeric_limits::max(); + auto maxUnsigned = cc->type == Type::i32 + ? std::numeric_limits::max() + : std::numeric_limits::max(); + + switch (c.op) { + case LtS: + if (cc->getInteger() == minSigned) { + // Less than the lowest possible number. + return true; + } + break; + case LtU: + if (cc->getInteger() == 0) { + // Less than the lowest possible number. + return true; + } + break; + case GtS: + if (cc->getInteger() == maxSigned) { + // Greater than the highest possible number. + return true; + } + break; + case GtU: + if (cc->getUnsigned() == maxUnsigned) { + // Greater than the highest possible number. + return true; + } + break; + default: { + } + } + + return false; +} + } // anonymous namespace void AndedConstraintSet::approximateAnd(const Constraint& c) { @@ -322,6 +371,12 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) { return; } + // We don't store contradictions: identify them and mark us as such. + if (isImmediateContradiction(c)) { + setProvesEverything(); + return; + } + auto result = proves(c); if (result == True) { // We already prove c to be true, so it adds nothing. From 344ac09786537b9d78d9ca3c3aabe3d37e0f113c Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 21 Aug 2026 16:08:16 -0700 Subject: [PATCH 3/4] oops, do not error on non-numbers in getSpan --- src/ir/constraint.cpp | 5 +++++ test/gtest/constraint.cpp | 6 ++++++ 2 files changed, 11 insertions(+) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 2a342cd5716..f769a2acf60 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -36,6 +36,11 @@ getSpanInternal(const Constraint& c, std::optional type, bool exact) { type = cc->type; } + if (type && !type->isNumber()) { + // References etc. do not convert to spans. + return {}; + } + auto minSigned = type && *type == Type::i32 ? std::numeric_limits::min() : std::numeric_limits::min(); diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index 7e8423f7d04..b9ec2712b70 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -1127,3 +1127,9 @@ TEST(ConstraintTest, EmptySpanContradiction) { AndedConstraintSet impossible{gtsMax32}; checkOr(valid, impossible, valid); } + +TEST(ConstraintTest, GetSpanGC) { + // Reference types do not cause errors. + EXPECT_EQ((Constraint{Eq, {Literal::makeNull(HeapType::eq)}}.getSpan()), + std::nullopt); +} From a5c09a08689ad0ff11d936f6b7d3ccdbf1837b40 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 21 Aug 2026 16:18:51 -0700 Subject: [PATCH 4/4] floats too --- src/ir/constraint.cpp | 2 +- test/gtest/constraint.cpp | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index f769a2acf60..18f090b67aa 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -36,7 +36,7 @@ getSpanInternal(const Constraint& c, std::optional type, bool exact) { type = cc->type; } - if (type && !type->isNumber()) { + if (type && !type->isInteger()) { // References etc. do not convert to spans. return {}; } diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index b9ec2712b70..2feb0c12fb7 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -1128,6 +1128,12 @@ TEST(ConstraintTest, EmptySpanContradiction) { checkOr(valid, impossible, valid); } +TEST(ConstraintTest, GetSpanFloat) { + // Non-integer types do not cause errors. + EXPECT_EQ((Constraint{Eq, {Literal(float(3.14159))}}.getSpan()), + std::nullopt); +} + TEST(ConstraintTest, GetSpanGC) { // Reference types do not cause errors. EXPECT_EQ((Constraint{Eq, {Literal::makeNull(HeapType::eq)}}.getSpan()),