Skip to content

Commit

Permalink
Merge pull request #462 from potassco/fix/overflow-iesolver
Browse files Browse the repository at this point in the history 
handle overflows in the IESolver

Variables with large domains could lead to overflows in the IESolver. To prevent this, a 64bit type is used to sum up values. In case there are still overflows, computed bounds are simply ignored.
  • Loading branch information
@rkaminsk
rkaminsk authored Oct 17, 2023
2 parents 3b4b4a3 + d1ef16f commit d8f3fab
Show file tree
Hide file tree
Showing 6 changed files with 197 additions and 29 deletions.
1 change: 1 addition & 0 deletions CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
10 changes: 3 additions & 7 deletions libgringo/gringo/term.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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_;
Expand Down
4 changes: 2 additions & 2 deletions libgringo/src/ground/literals.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down Expand Up @@ -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;
}
Expand Down
148 changes: 129 additions & 19 deletions libgringo/src/term.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
#include "gringo/logger.hh"
#include "gringo/graph.hh"
#include <cmath>
#include <cstddef>

// #define CLINGO_DEBUG_INEQUALITIES

Expand Down Expand Up @@ -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
Expand All @@ -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;
}
}
}
}
Expand All @@ -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) {
Expand All @@ -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) {
Expand All @@ -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;
}

// }}}
Expand Down
43 changes: 43 additions & 0 deletions libgringo/tests/input/program.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 }.")));
Expand Down
20 changes: 19 additions & 1 deletion libgringo/tests/output/lparse.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit d8f3fab

Please sign in to comment.