handle overflows in the IESolver

CHANGES.md

@@ -13,6 +13,7 @@
   * fix parsing of hexadecimal numbers (#421)
   * fix assignment aggregates (#436)
   * fix build scripts for Python 3.12 (#452)
+  * fix overflows in IESolver (#462)
   * make sure `clingo_control_ground` is re-entrant (#418)
   * update clasp and dependencies
 

libgringo/gringo/term.hh

@@ -259,14 +259,10 @@ public:
     void compute();
 
 private:
+    enum class UpdateResult { changed, unchanged, overflow };
     using SubSolvers = std::forward_list<IESolver>;
-    template<typename I>
-    static I floordiv_(I n, I m);
-    template<typename I>
-    static I ceildiv_(I n, I m);
-    static int div_(bool positive, int a, int b);
-    bool update_bound_(IETerm const &term, int slack, int num_unbounded);
-    void update_slack_(IETerm const &term, int &slack, int &num_unbounded);
+    UpdateResult update_bound_(IETerm const &term, int64_t slack, int num_unbounded);
+    bool update_slack_(IETerm const &term, int64_t &slack, int &num_unbounded);
 
     IESolver *parent_;
     IEContext &ctx_;

libgringo/src/ground/literals.cc

@@ -294,7 +294,7 @@ class AssignBinder : public Binder {
 
 } // namespace
 
-// {{{1 definition of PredicateLiteral
+// {{{1 definition of RangeLiteral
 
 RangeLiteral::RangeLiteral(UTerm assign, UTerm left, UTerm right)
 : assign_(std::move(assign))
@@ -333,7 +333,7 @@ Literal::Score RangeLiteral::score(Term::VarSet const &bound, Logger &log) {
         bool undefined = false;
         Symbol l(range_.first->eval(undefined, log));
         Symbol r(range_.second->eval(undefined, log));
-        return (l.type() == SymbolType::Num && r.type() == SymbolType::Num) ? r.num() - l.num() : -1;
+        return (l.type() == SymbolType::Num && r.type() == SymbolType::Num) ? static_cast<double>(r.num()) - l.num() : -1.0;
     }
     return 0;
 }

libgringo/src/term.cc

@@ -27,6 +27,7 @@
 #include "gringo/logger.hh"
 #include "gringo/graph.hh"
 #include <cmath>
+#include <cstddef>
 
 // #define CLINGO_DEBUG_INEQUALITIES
 
@@ -351,10 +352,16 @@ void IESolver::compute() {
     while (changed) {
         changed = false;
         for (auto const &ie : ies_) {
-            int slack = ie.bound;
+            int64_t slack = ie.bound;
             int num_unbounded = 0;
             for (auto const &term : ie.terms) {
-                update_slack_(term, slack, num_unbounded);
+                // In case the slack cannot be updated due to an overflow, no bounds are calculated.
+                if (!update_slack_(term, slack, num_unbounded)) {
+#ifdef CLINGO_DEBUG_INEQUALITIES
+                    std::cerr << "  overflow updating slack of " << ie << std::endl;
+#endif
+                    return;
+                }
             }
             if (num_unbounded == 0 && slack > 0) {
                 // we simply set all bounds to empty intervals
@@ -369,17 +376,20 @@ void IESolver::compute() {
             }
             if (num_unbounded <= 1) {
                 for (auto const &term : ie.terms) {
+                    auto res = update_bound_(term, slack, num_unbounded);
+                    if (res == UpdateResult::changed) {
 #ifdef CLINGO_DEBUG_INEQUALITIES
-                    bool bound_changed = update_bound_(term, slack, num_unbounded);
-                    if (bound_changed) {
-                        bool comma = false;
                         std::cerr << "  update bound using " << ie << std::endl;
                         std::cerr << "    the new bound for " << *term.variable << " is "<< bounds_[term.variable] << std::endl;
+#endif
+                        changed = true;
                     }
-                    changed = bound_changed || changed;
-#else
-                    changed = update_bound_(term, slack, num_unbounded) || changed;
+                    if (res == UpdateResult::overflow) {
+#ifdef CLINGO_DEBUG_INEQUALITIES
+                        std::cerr << "  overflow updating bound of " << *term.variable << std::endl;
 #endif
+                        return;
+                    }
                 }
             }
         }
@@ -400,8 +410,10 @@ void IESolver::add(IEContext &context) {
     subSolvers_.emplace_front(context, this);
 }
 
+namespace {
+
 template<typename I>
-I IESolver::floordiv_(I n, I m) {
+I floordiv(I n, I m) {
     using std::div;
     auto a = div(n, m);
     if (((n < 0) ^ (m < 0)) && a.rem != 0) {
@@ -411,7 +423,7 @@ I IESolver::floordiv_(I n, I m) {
 }
 
 template<typename I>
-I IESolver::ceildiv_(I n, I m) {
+I ceildiv(I n, I m) {
     using std::div;
     auto a = div(n, m);
     if (((n < 0) ^ (m < 0)) && a.rem != 0) {
@@ -420,32 +432,130 @@ I IESolver::ceildiv_(I n, I m) {
     return a.quot;
 }
 
-int IESolver::div_(bool positive, int a, int b) {
-    return positive ? floordiv_(a, b) : ceildiv_(a, b);
+template<typename I>
+I div(bool positive, I a, I b) {
+    return positive ? floordiv(a, b) : ceildiv(a, b);
+}
+
+int clamp_div(bool positive, int64_t a, int64_t b) {
+    if (a == std::numeric_limits<int64_t>::min() && b == -1) {
+        return std::numeric_limits<int>::max();
+    }
+    auto c = div<int64_t>(positive, a, b);
+    if (c > std::numeric_limits<int>::max()) {
+        return std::numeric_limits<int>::max();
+    }
+    if (c < std::numeric_limits<int>::min()) {
+        return std::numeric_limits<int>::min();
+    }
+    return static_cast<int>(c);
 }
 
-bool IESolver::update_bound_(IETerm const &term, int slack, int num_unbounded) {
+template <class T, class S>
+inline bool check_cast(S in, T &out) {
+    if (sizeof(T) < sizeof(S) && (in < std::numeric_limits<T>::min() || in > std::numeric_limits<T>::max())) {
+        return  false;
+    }
+    out = static_cast<T>(in);
+    return  true;
+}
+
+#ifdef __GNUC__
+
+template <class S> inline bool check_add(S a, S b, S &c) {
+    return !__builtin_add_overflow(a, b, &c);
+}
+
+template <class S> inline bool check_sub(S a, S b, S &c) {
+    return !__builtin_sub_overflow(a, b, &c);
+}
+
+template <class S> inline bool check_mul(S a, S b, S &c) {
+    return !__builtin_mul_overflow(a, b, &c);
+}
+
+#else
+
+inline bool check_add(int32_t a, int32_t b, int32_t &c) {
+    return check_cast<int32_t>(static_cast<int64_t>(a) + b, c);
+}
+
+template <class S> inline bool check_add(S a, S b, S &c) {
+    using U = std::make_unsigned_t<S>;
+    c = static_cast<S>(static_cast<U>(a) + static_cast<U>(b));
+    return (a < 0 || b < 0 || c >= a) && (a >= 0 || b >= 0 || c <= a);
+}
+
+inline bool check_sub(int32_t a, int32_t b, int32_t &c) {
+    return check_cast<int32_t>(static_cast<int64_t>(a) - b, c);
+}
+
+template <class S> inline bool check_sub(S a, S b, S &c) {
+    using U = std::make_unsigned_t<S>;
+    c = static_cast<S>(static_cast<U>(a) - static_cast<U>(b));
+    return (a < 0 || b >= 0 || c >= a) && (b < 0 || c <= a);
+}
+
+template <class S> inline bool check_mul(S a, S b, S &c) {
+    if (a > 0 && b > 0 && a > std::numeric_limits<S>::max() / b) {
+        return false;
+    }
+    if (a < 0 && b < 0 && b < std::numeric_limits<S>::max() / a) {
+        return false;
+    }
+    if (a > 0 && b < 0 && b < std::numeric_limits<S>::min() / a) {
+        return false;
+    }
+    if (a < 0 && b > 0 && a < std::numeric_limits<S>::min() / b) {
+        return false;
+    }
+    c = a * b;
+    return true;
+}
+
+#endif
+
+} // namespace
+
+IESolver::UpdateResult IESolver::update_bound_(IETerm const &term, int64_t slack, int num_unbounded) {
     bool positive = term.coefficient > 0;
     auto type = positive ? IEBound::Upper : IEBound::Lower;
     if (num_unbounded == 0) {
-        slack += term.coefficient * bounds_[term.variable].get(type);
+        int64_t val = 0;
+        if (!check_mul<int64_t>(term.coefficient, bounds_[term.variable].get(type), val)) {
+            return UpdateResult::overflow;
+        }
+        if (!check_add(slack, val, slack)) {
+            return UpdateResult::overflow;
+        }
     }
     else if (num_unbounded > 1 || bounds_[term.variable].isSet(type)) {
-        return false;
+        return UpdateResult::unchanged;
     }
 
-    auto value = div_(positive, slack, term.coefficient);
-    return bounds_[term.variable].refine(positive ? IEBound::Lower : IEBound::Upper, value);
+
+    auto value = clamp_div(positive, slack, term.coefficient);
+    if (bounds_[term.variable].refine(positive ? IEBound::Lower : IEBound::Upper, value)) {
+        return UpdateResult::changed;
+    }
+    return UpdateResult::unchanged;
 }
 
-void IESolver::update_slack_(IETerm const &term, int &slack, int &num_unbounded) {
+bool IESolver::update_slack_(IETerm const &term, int64_t &slack, int &num_unbounded) {
     auto type = term.coefficient > 0 ? IEBound::Upper : IEBound::Lower;
     if (bounds_[term.variable].isSet(type)) {
-        slack -= term.coefficient * bounds_[term.variable].get(type);
+        int64_t val = 0;
+        if (!check_mul<int64_t>(term.coefficient, bounds_[term.variable].get(type), val)) {
+            return false;
+        }
+        if (!check_sub(slack, val, slack)) {
+            return false;
+        }
     }
     else {
         ++num_unbounded;
     }
+    return true;
 }
 
 // }}}

libgringo/tests/input/program.cc

@@ -359,6 +359,49 @@ TEST_CASE("input-program", "[input]") {
         REQUIRE("#external p(X):[#inc_base].[X]#external p(X):[#inc_base].[Y]#external p(Y):[#inc_base].[X]#external p(Y):[#inc_base].[Y]" == rewrite(parse("#external p(X;Y). [(X;Y)]")));
     }
 
+    SECTION("iesolver") {
+        // no overflow
+        REQUIRE("q(5)."
+                "p(S):-"
+                "#range(Y,0,1);"
+                "#range(X,0,1);"
+                "#range(S,0,2147483647);"
+                "#range(#Arith0,0,2147483647);"
+                "q(B);"
+                "0<=Y;"
+                "Y<=2147483647;"
+                "0<=X;"
+                "X<=2147483647;"
+                "S=((2147483647*X)+(2147483647*Y));"
+                "#Arith0=((2147483647*X)+(2147483647*Y));"
+                "#Arith0=S;"
+                "S<=B." == rewrite(parse("q(5). "
+                                         "p(S) :- q(B), "
+                                         "S<=B, "
+                                         "0<=X<=0x7FFFFFFF, "
+                                         "0<=Y<=0x7FFFFFFF, "
+                                         "S=0x7FFFFFFF*X+0x7FFFFFFF*Y.")));
+        // overflow
+        REQUIRE("q(5)."
+                "p(S):-q(B);"
+                "#Arith0=S;"
+                "#Arith0=(((2147483647*X)+(2147483647*Y))+(2147483647*Z));"
+                "S=(((2147483647*X)+(2147483647*Y))+(2147483647*Z));"
+                "Z<=2147483647;"
+                "0<=Z;"
+                "Y<=2147483647;"
+                "0<=Y;"
+                "X<=2147483647;"
+                "0<=X;"
+                "S<=B." == rewrite(parse("q(5). "
+                                         "p(S) :- q(B), "
+                                         "S<=B, "
+                                         "0<=X<=0x7FFFFFFF, "
+                                         "0<=Y<=0x7FFFFFFF, "
+                                         "0<=Z<=0x7FFFFFFF, "
+                                         "S=0x7FFFFFFF*X+0x7FFFFFFF*Y+0x7FFFFFFF*Z.")));
+    }
+
     SECTION("theory") {
         REQUIRE("#theory x{}." == rewrite(parse("#theory x{  }.")));
         REQUIRE("#theory x{node{};&edge/0:node,directive}." == rewrite(parse("#theory x{ node{}; &edge/0: node, directive }.")));

libgringo/tests/output/lparse.cc

@@ -1132,7 +1132,25 @@ TEST_CASE("output-lparse", "[output]") {
                 "a(6) :- not not { }.\n"
                 , {"a("})));
     }
+    SECTION("IESolver") {
+        // clean
+        REQUIRE(
+            "([[p(1),p(a),q]],[])" ==
+            IO::to_string(solve(
+                "p(1).\n"
+                "p(a).\n"
+                "q :- p(X), -0x7FFFFFFF-1 <= X <= 0x7FFFFFFF.\n"
+                , {"p", "q"})));
+        // relies on two's complemenet
+        REQUIRE(
+            "([[p(1),p(a),q]],[])" ==
+            IO::to_string(solve(
+                "p(1).\n"
+                "p(a).\n"
+                "q :- p(X), 0x80000000 <= X <= 0x7FFFFFFF.\n"
+                , {"p", "q"})));
+    }
+
 }
 
 } } } // namespace Test Output Gringo
-