smt exprs: add simplifications for AndExpr(and) & extract of concat
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1973,8 +1973,7 @@ StateValue GEP::toSMT(State &s) const {
auto scalar = [&](const StateValue &ptrval,
vector<pair<unsigned, StateValue>> &offsets) -> StateValue {
Pointer ptr(s.getMemory(), ptrval.value);
- AndExpr non_poison;
- non_poison.add(ptrval.non_poison);
+ AndExpr non_poison(ptrval.non_poison);
if (inbounds)
non_poison.add(ptr.inbounds(true));

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -387,6 +387,17 @@ bool expr::isExtract(expr &e, unsigned &high, unsigned &low) const {
return false;
}
+bool expr::isAnd(expr &a, expr &b) const {
+ if (auto app = isAppOf(Z3_OP_AND)) {
+ if (Z3_get_domain_size(ctx(), decl()) != 2)
+ return false;
+ a = Z3_get_app_arg(ctx(), app, 0);
+ b = Z3_get_app_arg(ctx(), app, 1);
+ return true;
+ }
+ return false;
+}
+
bool expr::isNot(expr &neg) const {
if (auto app = isAppOf(Z3_OP_NOT)) {
neg = Z3_get_app_arg(ctx(), app, 0);
@@ -1300,6 +1311,8 @@ expr expr::extract(unsigned high, unsigned low) const {
return b.extract(high, low);
if (low >= b_bw)
return a.extract(high - b_bw, low - b_bw);
+ if (low == 0)
+ return a.extract(high - b_bw, 0).concat(b);
}
}
{

MODIFY
smt/expr.h
smt/expr.h
@@ -125,6 +125,7 @@ public:
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;
+ bool isAnd(expr &a, expr &b) const;
bool isNot(expr &neg) const;
bool isConstArray(expr &val) const;
bool isStore(expr &array, expr &idx, expr &val) const;

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -10,12 +10,28 @@ using namespace std;
namespace smt {
void AndExpr::add(const expr &e) {
- if (!e.isTrue())
+ if (e.isTrue())
+ return;
+
+ expr a, b;
+ if (e.isAnd(a, b)) {
+ add(move(a));
+ add(move(b));
+ return;
+ }
exprs.insert(e);
}
void AndExpr::add(expr &&e) {
- if (!e.isTrue())
+ if (e.isTrue())
+ return;
+
+ expr a, b;
+ if (e.isAnd(a, b)) {
+ add(move(a));
+ add(move(b));
+ return;
+ }
exprs.insert(move(e));
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -15,6 +15,10 @@ class AndExpr {
std::set<expr> exprs;
public:
+ AndExpr() {}
+ template <typename T>
+ AndExpr(T &&e) { add(std::forward<T>(e)); }
+
void add(const expr &e);
void add(expr &&e);
void add(const AndExpr &other);

smt exprs: add simplifications for AndExpr(and) & extract of concat