memory: allow folding of block data when we are sure the block isn't local
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -184,10 +184,10 @@ Pointer::Pointer(const Memory &m, const char *var_name, const expr &local)
: m(m), p(local.toBVBool().concat(
expr::mkFreshVar(var_name, expr::mkUInt(0, total_bits()-1)))) {}
-Pointer::Pointer(const Memory &m, unsigned bid, bool local) : m(m) {
- expr bid_expr = expr::mkUInt(bid, bits_for_bid - 1);
- p = expr::mkUInt(local, 1).concat(bid_expr)
- .concat(expr::mkUInt(0, bits_for_offset));
+Pointer::Pointer(const Memory &m, unsigned bid, bool local)
+ : m(m), p(expr::mkUInt(local, 1).concat(expr::mkUInt(bid, bits_for_bid - 1))
+ .concat(expr::mkUInt(0, bits_for_offset))) {
+ assert((local && bid < num_locals) || (!local && bid < num_nonlocals));
}
Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset)
@@ -225,7 +225,9 @@ expr Pointer::get_value(const char *name, const FunctionExpr &local_fn,
else
non_local = expr::mkUF(name, { bid }, ret_type);
- return expr::mkIf(is_local(), local_fn(bid), non_local);
+ if (auto local = local_fn(bid))
+ return expr::mkIf(is_local(), *local, non_local);
+ return non_local;
}
expr Pointer::get_address(bool simplify) const {
@@ -236,13 +238,17 @@ expr Pointer::get_address(bool simplify) const {
// fast path for null ptrs
auto non_local
= simplify && bid.isZero() ? zero : expr::mkUF("blk_addr", { bid }, zero);
+ // Non-local block area is the lower half
+ non_local = expr::mkUInt(0, 1).concat(non_local);
+ expr addr;
+ if (auto local = m.local_blk_addr(bid))
// Local block area is the upper half of the memory
- // Non-local block area is the lower half
- return get_offset() +
- expr::mkIf(is_local(),
- expr::mkUInt(1, 1).concat(m.local_blk_addr(bid)),
- expr::mkUInt(0, 1).concat(non_local));
+ addr = expr::mkIf(is_local(), expr::mkUInt(1, 1).concat(*local), non_local);
+ else
+ addr = move(non_local);
+
+ return addr + get_offset();
}
expr Pointer::block_size() const {
@@ -524,13 +530,7 @@ static bool memory_unused() {
!observes_addresses();
}
-Memory::Memory(State &state)
- : state(&state),
- local_blk_addr(expr::mkUInt(0, bits_size_t - 1)),
- local_blk_size(expr::mkUInt(0, bits_size_t - 1)),
- local_blk_align(expr::mkUInt(0, 8)),
- local_blk_kind(expr::mkUInt(0, 2)) {
-
+Memory::Memory(State &state) : state(&state) {
if (memory_unused())
return;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -108,7 +108,7 @@ bool State::startBB(const BasicBlock &bb) {
if (domain.first.isFalse())
return false;
- memory = in_memory();
+ memory = *in_memory();
return true;
}

MODIFY
ir/state.h
ir/state.h
@@ -105,10 +105,10 @@ public:
const auto& getQuantVars() const { return quantified_vars; }
auto& returnDomain() const { return return_domain; }
- Memory returnMemory() const { return return_memory(); }
+ Memory returnMemory() const { return *return_memory(); }
std::pair<StateValue, const std::set<smt::expr>&> returnVal() const {
- return { return_val(), return_undef_vars };
+ return { *return_val(), return_undef_vars };
}
void startParsingPre() { disable_undef_rewrite = true; }

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -52,7 +52,7 @@ void FunctionExpr::del(const expr &key) {
fn.erase(key);
}
-expr FunctionExpr::operator()(const expr &key) const {
+optional<expr> FunctionExpr::operator()(const expr &key) const {
DisjointExpr disj(default_val);
for (auto &[k, v] : fn) {
disj.add(v, k == key);

MODIFY
smt/exprs.h
smt/exprs.h
@@ -40,6 +40,7 @@ class DisjointExpr {
public:
DisjointExpr() {}
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)) {}
template <typename V, typename D>
@@ -55,7 +56,7 @@ public:
I->second |= std::forward<D>(domain);
}
- T operator()() const {
+ std::optional<T> operator()() const {
std::optional<T> ret;
for (auto &[val, domain] : vals) {
if (domain.isTrue())
@@ -63,14 +64,18 @@ public:
ret = ret ? T::mkIf(domain, val, *ret) : val;
}
- return ret ? *ret : *default_val;
+ if (ret)
+ return *ret;
+ if (default_val)
+ return *default_val;
+ return {};
}
};
class FunctionExpr {
std::map<expr, expr> fn; // key -> val
- expr default_val;
+ std::optional<expr> default_val;
public:
FunctionExpr() {}
@@ -79,7 +84,7 @@ public:
void add(const FunctionExpr &other);
void del(const expr &key);
- expr operator()(const expr &key) const;
+ std::optional<expr> operator()(const expr &key) const;
const expr* lookup(const expr &key) const;
auto begin() const { return fn.begin(); }

memory: allow folding of block data when we are sure the block isn't local