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.