memory: unroll is_dereferenceable check and use it to trim pointer size
this helps reducing stores to e.g. (ite cond x null) -> x
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -324,26 +324,51 @@ expr Pointer::is_aligned(unsigned align, bool exact) const {
return exact ? blk_align == bits : blk_align.uge(bits);
}
-// When bytes is 0, pointer is always derefenceable
-void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
- bool iswrite) {
- expr block_sz = block_size();
- expr offset = get_offset();
- expr bytes = bytes0.zextOrTrunc(bits_size_t);
+static pair<expr, expr> is_dereferenceable(const Pointer &p, const expr &bytes,
+ unsigned align, bool iswrite) {
+ expr block_sz = p.block_size();
+ expr offset = p.get_offset();
// check that offset is within bounds and that arith doesn't overflow
expr cond = (offset + bytes).ule(block_sz);
cond &= offset.add_no_uoverflow(bytes);
- cond &= is_block_alive();
+ cond &= p.is_block_alive();
if (iswrite)
- cond &= is_writable();
+ cond &= p.is_writable();
- m.state->addUB(bytes.uge(1).implies(cond));
+ return { move(cond), p.is_aligned(align) };
+}
+
+// When bytes is 0, pointer is always derefenceable
+void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
+ bool iswrite) {
+ 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)) {
+ Pointer ptr(m, ptr_expr);
+ auto [ub, aligned] = ::is_dereferenceable(ptr, bytes, align, iswrite);
+
+ // record pointer if not definitely unfeasible
+ if (!ub.isFalse() && !aligned.isFalse())
+ all_ptrs.add(ptr_expr, domain);
+
+ UB.add(move(ub), domain);
+ is_aligned.add(move(aligned), domain);
+ }
+
+ m.state->addUB(bytes == 0 || *UB());
// address must be always aligned regardless of access size
- m.state->addUB(is_aligned(align));
+ m.state->addUB(*is_aligned());
+
+ // trim set of valid ptrs
+ if (auto ptrs = all_ptrs())
+ p = *ptrs;
+ else
+ p = mkNullPointer(m).p;
}
void Pointer::is_dereferenceable(unsigned bytes, unsigned align, bool iswrite) {
@@ -730,8 +755,6 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
: p.is_writable());
non_local_block_liveness
= non_local_block_liveness.store(short_bid, allocated);
- // TODO: benchmark; the following line is redundant
- state->addAxiom(mk_liveness_array().load(short_bid) == allocated);
state->addAxiom(p.block_size() == size_zext);
state->addAxiom(p.is_aligned(align, true));
state->addAxiom(p.get_alloc_type() == alloc_ty);

MODIFY
smt/exprs.cpp
smt/exprs.cpp
#include "smt/exprs.h"
#include "util/compiler.h"
+#include <vector>
using namespace std;
@@ -45,6 +46,24 @@ ostream &operator<<(ostream &os, const OrExpr &e) {
}
+template<> DisjointExpr<expr>::DisjointExpr(const expr &e, bool unpack_ite) {
+ assert(unpack_ite);
+ vector<pair<expr, expr>> worklist = { {e, true} };
+ expr cond, then, els;
+
+ do {
+ auto [v, c] = worklist.back();
+ worklist.pop_back();
+ if (v.isIf(cond, then, els)) {
+ worklist.emplace_back(move(then), c && cond);
+ worklist.emplace_back(move(els), c && !cond);
+ } else {
+ add(move(v), move(c));
+ }
+ } while (!worklist.empty());
+}
+
+
void FunctionExpr::add(const expr &key, expr &&val) {
ENSURE(fn.emplace(key, move(val)).second);
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -43,6 +43,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);
template <typename V, typename D>
void add(V &&val, D &&domain) {
@@ -71,6 +72,9 @@ public:
return *default_val;
return {};
}
+
+ auto begin() const { return vals.begin(); }
+ auto end() const { return vals.end(); }
};

memory: unroll is_dereferenceable check and use it to trim pointer size
this helps reducing stores to e.g. (ite cond x null) -> x