smt expr: switch all leafs computation to an iterator
this allows early exit
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -907,8 +907,8 @@ ostream& operator<<(ostream &os, const Pointer &p) {
static vector<expr> extract_possible_local_bids(Memory &m, const expr &ptr) {
vector<expr> ret;
expr zero = expr::mkUInt(0, bits_for_offset);
- for (auto ptr_val : expr::allLeafs(ptr)) {
- for (auto bid : expr::allLeafs(Pointer(m, move(ptr_val)).getBid())) {
+ for (auto &ptr_val : allExprLeafs(ptr)) {
+ for (auto &bid : allExprLeafs(Pointer(m, ptr_val).getBid())) {
Pointer ptr(m, bid, zero);
if (!ptr.isLocal().isFalse())
ret.emplace_back(ptr.getShortBid());
@@ -983,7 +983,7 @@ void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
};
// collect over-approximation of possible touched bids
- for (auto &ptr_val : expr::allLeafs(ptr())) {
+ for (auto &ptr_val : allExprLeafs(ptr())) {
Pointer q(*this, expr(ptr_val));
if (has_readnone && q.isReadnone().isTrue())

MODIFY
ir/memory.h
ir/memory.h
@@ -236,6 +236,9 @@ class Memory {
std::vector<unsigned> byval_blks;
std::vector<bool> escaped_local_blks;
+ unsigned numLocals() const;
+ unsigned numNonlocals() const;
+
void mk_nonlocal_val_axioms(bool skip_consts);
bool mayalias(bool local, unsigned bid, const smt::expr &offset,
@@ -369,9 +372,6 @@ public:
smt::expr checkNocapture() const;
void escapeLocalPtr(const smt::expr &ptr);
- unsigned numLocals() const;
- unsigned numNonlocals() const;
-
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);

MODIFY
smt/expr.cpp
smt/expr.cpp
#include <limits>
#include <memory>
#include <string>
-#include <unordered_set>
#include <z3.h>
#define DEBUG_Z3_RC 0
@@ -1720,27 +1719,6 @@ set<expr> expr::vars(const vector<const expr*> &exprs) {
return result;
}
-vector<expr> expr::allLeafs(const expr &e) {
- vector<expr> ret;
- vector<expr> worklist = { e };
- unordered_set<Z3_ast> seen;
- do {
- expr v = worklist.back();
- worklist.pop_back();
- if (!seen.insert(v.isValid() ? v() : nullptr).second)
- continue;
-
- expr cond, then, els;
- if (v.isIf(cond, then, els)) {
- worklist.emplace_back(move(then));
- worklist.emplace_back(move(els));
- } else {
- ret.emplace_back(move(v));
- }
- } while (!worklist.empty());
- return ret;
-}
-
void expr::printUnsigned(ostream &os) const {
os << numeral_string();
}
@@ -1792,4 +1770,29 @@ unsigned expr::hash() const {
return Z3_get_ast_hash(ctx(), ast());
}
+
+ExprLeafIterator::ExprLeafIterator(const expr &init)
+ : worklist({init}), end(false) {
+ ++*this;
+}
+
+void ExprLeafIterator::operator++(void) {
+ assert(!end);
+ while (!worklist.empty()) {
+ val = move(worklist.back());
+ worklist.pop_back();
+ if (!val.isValid() || !seen.insert(val()).second)
+ continue;
+
+ expr cond, then, els;
+ if (val.isIf(cond, then, els)) {
+ worklist.emplace_back(move(then));
+ worklist.emplace_back(move(els));
+ } else {
+ return;
+ }
+ }
+ end = true;
+}
+
}

MODIFY
smt/expr.h
smt/expr.h
#include <ostream>
#include <set>
#include <string>
+#include <unordered_set>
#include <utility>
#include <vector>
@@ -309,9 +310,6 @@ public:
std::set<expr> vars() const;
static std::set<expr> vars(const std::vector<const expr*> &exprs);
- // returns set of all possible leaf expressions (best-effort simplification)
- static std::vector<expr> allLeafs(const expr &e);
-
void printUnsigned(std::ostream &os) const;
void printSigned(std::ostream &os) const;
void printHexadecimal(std::ostream &os) const;
@@ -334,8 +332,37 @@ public:
friend class Solver;
friend class Model;
+ friend class ExprLeafIterator;
+};
+
+
+class ExprLeafIterator {
+ std::vector<expr> worklist;
+ std::unordered_set<Z3_ast> seen;
+ expr val;
+ bool end;
+ ExprLeafIterator() : end(true) {}
+ ExprLeafIterator(const expr &init);
+public:
+ const expr& operator*() const { return val; }
+ void operator++(void);
+ bool operator!=(ExprLeafIterator &rhs) const { return end != rhs.end; }
+ friend class ExprLeafIteratorHelper;
};
+class ExprLeafIteratorHelper {
+ const expr &init;
+public:
+ ExprLeafIteratorHelper(const expr &init ) : init(init) {}
+ ExprLeafIterator begin() const { return { init }; }
+ ExprLeafIterator end() const { return {}; }
+};
+
+// returns set of all possible leaf expressions (best-effort simplification)
+static inline ExprLeafIteratorHelper allExprLeafs(const expr &e) {
+ return { e };
+}
+
#define mkIf_fold(c, a, b) \
mkIf_fold_fn(c, [&]() { return a; }, [&]() { return b; })

smt expr: switch all leafs computation to an iterator
this allows early exit