From c32a8707d50df32b97135e681099218f2fb6bad8 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Thu, 30 Jul 2026 12:39:18 -0700 Subject: [PATCH 1/4] ConstraintAnalysis: Add more simple inequalities --- src/ir/constraint.cpp | 38 ++++++++++++++++++++++++++++++++++++++ test/gtest/constraint.cpp | 15 +++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index eb4f65e9a9d..2c60bdc1cd9 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -266,6 +266,32 @@ std::optional approximateOrTermEqualPair(const Abstract::Op aOp, return Constraint{GeS, term}; } + // x >= C || x > C === x >= C + if (aOp == GtS && bOp == GeS) { + return Constraint{GeS, term}; + } + + // TODO: all the rest + + return {}; +} + +// Do an OR of a pair of constraints where the terms are adjacent constants: a +// operations on C, and b on C+1. +std::optional approximateOrAdjacentConstantPair( + const Abstract::Op aOp, const Literal& aConstant, const Abstract::Op bOp) { + using namespace Abstract; + + // x == C || x >= C+1 === x >= C + if (aOp == Eq && bOp == GeS) { + return Constraint{GeS, aConstant}; + } + + // x > C || x >= C+1 === x > C + if (aOp == GtS && bOp == GeS) { + return Constraint{GtS, aConstant}; + } + // TODO: all the rest return {}; @@ -282,6 +308,18 @@ std::optional approximateOrPair(const Constraint& a, } } + // See if we operate on constants N, N+1. + if (auto* ac = std::get_if(&a.term)) { + if (auto* bc = std::get_if(&b.term)) { + if (ac->type == bc->type && ac->type.isInteger() && + ac->add(Literal::makeFromInt32(1, ac->type)) == *bc) { + if (auto result = approximateOrAdjacentConstantPair(a.op, *ac, b.op)) { + 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; diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index c1e23650dd6..51e58499575 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -265,6 +265,21 @@ TEST(ConstraintTest, TestOrInequality) { // x == 5 || x >= 5 => x >= 5 checkOr(eq5, ges5, ges5); + + // x == 5 || x >= 6 => x >= 5 + AndedConstraintSet ges6{{GeS, {Literal(int32_t(6))}}}; + checkOr(eq5, ges6, ges5); + + // TODO: x == 5 || x >= 7 => x >= 5 TODO + AndedConstraintSet ges7{{GeS, {Literal(int32_t(7))}}}; + auto empty = AndedConstraintSet::makeProvesNothing(); + checkOr(eq5, ges7, empty); + + // x > 5 || x >= 6 => x > 5 + checkOr(gts5, ges6, gts5); + + // x > 5 || x >= 5 => x >= 5 + checkOr(gts5, ges5, ges5); } TEST(ConstraintTest, TestOrLoop) { From 3118ba0ad2f65330ed23c615dec889f44a41cc24 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Thu, 30 Jul 2026 12:42:24 -0700 Subject: [PATCH 2/4] fix --- src/ir/constraint.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index 2c60bdc1cd9..d0828c8bce6 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -266,7 +266,7 @@ std::optional approximateOrTermEqualPair(const Abstract::Op aOp, return Constraint{GeS, term}; } - // x >= C || x > C === x >= C + // x > C || x >= C === x >= C if (aOp == GtS && bOp == GeS) { return Constraint{GeS, term}; } From d61d1d44779a9ebc150a812aebabbc3443730563 Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Thu, 30 Jul 2026 12:51:45 -0700 Subject: [PATCH 3/4] fix warning --- src/ir/constraint.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index d0828c8bce6..c0b1e315e82 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -284,12 +284,12 @@ std::optional approximateOrAdjacentConstantPair( // x == C || x >= C+1 === x >= C if (aOp == Eq && bOp == GeS) { - return Constraint{GeS, aConstant}; + return Constraint{GeS, {aConstant}}; } // x > C || x >= C+1 === x > C if (aOp == GtS && bOp == GeS) { - return Constraint{GtS, aConstant}; + return Constraint{GtS, {aConstant}}; } // TODO: all the rest From 48354874ef7d41c650c0d51c4de8b4c71639ec7e Mon Sep 17 00:00:00 2001 From: Alon Zakai Date: Fri, 31 Jul 2026 09:30:58 -0700 Subject: [PATCH 4/4] handle overflow --- src/ir/constraint.cpp | 10 +++++----- test/gtest/constraint.cpp | 16 ++++++++++++++++ 2 files changed, 21 insertions(+), 5 deletions(-) diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp index c0b1e315e82..afe76703a91 100644 --- a/src/ir/constraint.cpp +++ b/src/ir/constraint.cpp @@ -277,18 +277,18 @@ std::optional approximateOrTermEqualPair(const Abstract::Op aOp, } // Do an OR of a pair of constraints where the terms are adjacent constants: a -// operations on C, and b on C+1. +// operates on C, and b on C+1. std::optional approximateOrAdjacentConstantPair( const Abstract::Op aOp, const Literal& aConstant, const Abstract::Op bOp) { using namespace Abstract; - // x == C || x >= C+1 === x >= C - if (aOp == Eq && bOp == GeS) { + // x == C || x >= C+1 === x >= C, if C+1 does not overflow. + if (aOp == Eq && bOp == GeS && !aConstant.isSignedMax()) { return Constraint{GeS, {aConstant}}; } - // x > C || x >= C+1 === x > C - if (aOp == GtS && bOp == GeS) { + // x > C || x >= C+1 === x > C, if C+1 does not overflow. + if (aOp == GtS && bOp == GeS && !aConstant.isSignedMax()) { return Constraint{GtS, {aConstant}}; } diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp index 51e58499575..da1f05f2f66 100644 --- a/test/gtest/constraint.cpp +++ b/test/gtest/constraint.cpp @@ -280,6 +280,22 @@ TEST(ConstraintTest, TestOrInequality) { // x > 5 || x >= 5 => x >= 5 checkOr(gts5, ges5, ges5); + + // Careful of overflow: + // x == signed_max || x >= (signed_max + 1 === signed_min) != x >= signed_max + AndedConstraintSet eqMax{ + {Eq, {Literal(std::numeric_limits::max())}}}; + AndedConstraintSet gesMin{ + {GeS, {Literal(std::numeric_limits::min())}}}; + // TODO: x >= signed_min is always true, so this could be empty + checkOr(eqMax, gesMin, gesMin); + + // Careful of overflow: + // 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); } TEST(ConstraintTest, TestOrLoop) {