2x speedup for when handling large load expressions with undef
MODIFY
ir/state.cpp
ir/state.cpp
#include "smt/smt.h"
#include "util/errors.h"
#include <cassert>
-#include <sstream>
#include <string_view>
using namespace smt;
@@ -269,31 +268,22 @@ void State::resetUndefVars() {
undef_vars.clear();
}
-static void collectUndefVars(State &s, set<expr> &undef_vars,
- vector<pair<expr,expr>> &repls, const expr &val) {
+StateValue State::rewriteUndef(StateValue &&val) {
+ vector<pair<expr, expr>> repls;
for (auto &var : val.vars()) {
- ostringstream ss;
- ss << var;
- auto name = ss.str();
- if (string_view(name).substr(0, 6) == "undef!" &&
- undef_vars.emplace(var).second) {
+ if (string_view(var.fn_name()).substr(0, 6) == "undef!") {
auto newvar = expr::mkFreshVar("undef", var);
repls.emplace_back(var, newvar);
- s.addUndefVar(move(newvar));
- }
+ addUndefVar(move(newvar));
}
}
-StateValue State::rewriteUndef(StateValue &&val) {
- set<expr> undef_vars;
- vector<pair<expr, expr>> repls;
- collectUndefVars(*this, undef_vars, repls, val.value);
- collectUndefVars(*this, undef_vars, repls, val.non_poison);
- if (undef_vars.empty())
+ if (repls.empty())
return move(val);
if (hit_half_memory_limit())
throw AliveException("Out of memory; skipping function.", false);
- return { val.value.subst(repls), val.non_poison.subst(repls) };
+
+ return val.subst(repls);
}
void State::finishInitializer() {

MODIFY
ir/state_value.cpp
ir/state_value.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/state_value.h"
+#include "util/compiler.h"
#include <tuple>
using namespace smt;
@@ -43,8 +44,28 @@ bool StateValue::eq(const StateValue &other) const {
return value.eq(other.value) && non_poison.eq(other.non_poison);
}
+set<expr> StateValue::vars() const {
+ return expr::vars({ &value, &non_poison });
+}
+
StateValue StateValue::subst(const vector<pair<expr, expr>> &repls) const {
+ if (!value.isValid() || !non_poison.isValid())
return { value.subst(repls), non_poison.subst(repls) };
+
+ // create dummy expr so we can do a single subst (more efficient than 2)
+ expr v1 = expr::mkVar("#1", value);
+ expr v2 = expr::mkVar("#2", non_poison);
+ expr val = expr::mkIf(non_poison == v2, value, v1).subst(repls);
+
+ expr cond, then, els, a, b, np;
+ ENSURE(val.isIf(cond, then, els));
+ if (cond.isEq(a, b)) {
+ np = a.eq(v2) ? move(b) : move(a);
+ } else {
+ assert(non_poison.isBool() && non_poison.isConst());
+ np = non_poison;
+ }
+ return { then.eq(v1) ? move(els) : move(then), move(np) };
}
bool StateValue::operator<(const StateValue &rhs) const {

MODIFY
ir/state_value.h
ir/state_value.h
@@ -31,6 +31,7 @@ struct StateValue {
bool eq(const StateValue &other) const;
+ std::set<smt::expr> vars() const;
StateValue
subst(const std::vector<std::pair<smt::expr, smt::expr>> &repls) const;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -343,6 +343,15 @@ bool expr::isInt(int64_t &n) const {
return true;
}
+bool expr::isEq(expr &lhs, expr &rhs) {
+ if (auto app = isAppOf(Z3_OP_EQ)) {
+ lhs = Z3_get_app_arg(ctx(), app, 0);
+ rhs = Z3_get_app_arg(ctx(), app, 1);
+ return true;
+ }
+ return false;
+}
+
bool expr::isIf(expr &cond, expr &then, expr &els) const {
if (auto app = isAppOf(Z3_OP_ITE)) {
cond = Z3_get_app_arg(ctx(), app, 0);
@@ -1214,6 +1223,11 @@ expr expr::zextOrTrunc(unsigned tobw) const {
}
expr expr::concat(const expr &rhs) const {
+ expr a, b;
+ unsigned h, l, h2, l2;
+ if (isExtract(a, h, l) && rhs.isExtract(b, h2, l2) && a.eq(b) && l == h2+1)
+ return a.extract(h, l2);
+
return binop_fold(rhs, Z3_mk_concat);
}
@@ -1492,15 +1506,24 @@ expr expr::subst(const expr &from, const expr &to) const {
}
set<expr> expr::vars() const {
- C();
+ return vars({ this });
+}
+
+set<expr> expr::vars(const vector<const expr*> &exprs) {
set<expr> result;
- unordered_set<Z3_ast> todo{ ast() };
- unordered_set<Z3_ast> seen = todo;
+ vector<Z3_ast> todo;
+ unordered_set<Z3_ast> seen;
+
+ for (auto e : exprs) {
+ C2(*e);
+ auto ast = e->ast();
+ if (seen.emplace(ast).second)
+ todo.emplace_back(ast);
+ }
do {
- auto I = todo.begin();
- auto ast = *I;
- todo.erase(I);
+ auto ast = todo.back();
+ todo.pop_back();
switch (Z3_get_ast_kind(ctx(), ast)) {
case Z3_VAR_AST:
@@ -1510,7 +1533,7 @@ set<expr> expr::vars() const {
case Z3_QUANTIFIER_AST: {
auto body = Z3_get_quantifier_body(ctx(), ast);
if (seen.emplace(body).second)
- todo.emplace(body);
+ todo.emplace_back(body);
break;
}
@@ -1529,7 +1552,7 @@ set<expr> expr::vars() const {
for (unsigned i = 0; i < num_args; ++i) {
auto arg = Z3_get_app_arg(ctx(), app, i);
if (seen.emplace(arg).second)
- todo.emplace(arg);
+ todo.emplace_back(arg);
}
break;
}

MODIFY
smt/expr.h
smt/expr.h
@@ -119,6 +119,7 @@ public:
bool isUInt(uint64_t &n) const;
bool isInt(int64_t &n) const;
+ bool isEq(expr &lhs, expr &rhs);
bool isIf(expr &cond, expr &then, expr &els) const;
bool isConcat(expr &a, expr &b) const;
bool isExtract(expr &e, unsigned &high, unsigned &low) const;
@@ -284,6 +285,7 @@ public:
expr subst(const expr &from, const expr &to) const;
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);

MODIFY
tests/alive-tv/memory/memset-large.src.ll
tests/alive-tv/memory/memset-large.src.ll
-; TEST-ARGS: -smt-to=10000 -disable-undef-input
+; TEST-ARGS: -smt-to=10000
declare void @llvm.memset.p0i8.i128(i8*, i8, i128, i1)

2x speedup for when handling large load expressions with undef