limit DisjointExpr recursion depth
for some test cases it was taking many minutes to come back
MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -269,7 +269,7 @@ expr Pointer::inbounds(bool simplify_ptr, bool strict) {
return ::inbounds(*this, strict);
DisjointExpr<expr> ret(expr(false)), all_ptrs;
- for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, true, true)) {
+ for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) {
expr inb = ::inbounds(Pointer(m, ptr_expr), strict);
if (!inb.isFalse())
all_ptrs.add(ptr_expr, domain);
@@ -362,7 +362,7 @@ AndExpr Pointer::isDereferenceable(const expr &bytes0, unsigned align,
expr bytes = bytes0.zextOrTrunc(bits_size_t);
DisjointExpr<expr> UB(expr(false)), is_aligned(expr(false)), all_ptrs;
- for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, true, true)) {
+ for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) {
Pointer ptr(m, ptr_expr);
auto [ub, aligned] = ::is_dereferenceable(ptr, bytes_off, bytes, align,
iswrite);

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -85,9 +85,13 @@ ostream &operator<<(ostream &os, const OrExpr &e) {
}
-template<> DisjointExpr<expr>::DisjointExpr(const expr &e, bool unpack_ite,
- bool unpack_concat) {
- assert(unpack_ite);
+template<>
+DisjointExpr<expr>::DisjointExpr(const expr &e, unsigned depth_limit) {
+ if (depth_limit-- == 0) {
+ add(e, expr(true));
+ return;
+ }
+
vector<pair<expr, expr>> worklist = { {e, true} };
expr cond, then, els, a, b;
unsigned high, low;
@@ -109,9 +113,9 @@ template<> DisjointExpr<expr>::DisjointExpr(const expr &e, bool unpack_ite,
worklist.emplace_back(move(then), c && cond);
worklist.emplace_back(move(els), c && !cond);
}
- else if (unpack_concat && v.isConcat(a, b)) {
- DisjointExpr<expr> lhs(a, unpack_ite, unpack_concat);
- DisjointExpr<expr> rhs(b, unpack_ite, unpack_concat);
+ else if (v.isConcat(a, b)) {
+ DisjointExpr<expr> lhs(a, depth_limit);
+ DisjointExpr<expr> rhs(b, depth_limit);
if (lhs.size() == 1 && rhs.size() == 1) {
add(move(v), move(c));
continue;
@@ -134,8 +138,8 @@ template<> DisjointExpr<expr>::DisjointExpr(const expr &e, bool unpack_ite,
}
}
}
- else if (unpack_concat && v.isExtract(a, high, low)) {
- DisjointExpr<expr> vals(a, unpack_ite, true);
+ else if (v.isExtract(a, high, low)) {
+ DisjointExpr<expr> vals(a, depth_limit);
if (vals.size() == 1) {
add(move(v), move(c));
continue;

MODIFY
smt/exprs.h
smt/exprs.h
@@ -57,7 +57,7 @@ public:
DisjointExpr(const T &default_val) : default_val(default_val) {}
DisjointExpr(const std::optional<T> &default_val) : default_val(default_val){}
DisjointExpr(T &&default_val) : default_val(std::move(default_val)) {}
- DisjointExpr(const expr &e, bool unpack_ite, bool unpack_concat = false);
+ DisjointExpr(const expr &e, unsigned depth_limit);
template <typename V, typename D>
void add(V &&val, D &&domain) {

limit DisjointExpr recursion depth
for some test cases it was taking many minutes to come back