memory: add fast path for get_address() and remove local block data on free
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -206,8 +206,13 @@ expr Pointer::get_value(const char *name, const FunctionExpr &fn,
return expr::mkIf(is_local(), fn(bid), expr::mkUF(name, { bid }, ret_type));
}
-expr Pointer::get_address() const {
+expr Pointer::get_address(bool simplify) const {
expr offset = get_offset();
+
+ // fast path for null ptrs
+ if (simplify && (get_bid() == 0).isTrue())
+ return offset;
+
return offset + get_value("blk_addr", local_blk_addr, offset);
}
@@ -438,7 +443,7 @@ Memory::Memory(State &state, bool little_endian)
// TODO: in twin memory model, this is not needed.
if (state.isSource()) {
auto nullPtr = Pointer::mkNullPointer(*this);
- state.addAxiom(nullPtr.get_address() == 0);
+ state.addAxiom(nullPtr.get_address(false) == 0);
state.addAxiom(nullPtr.block_size(false) == 0);
}
@@ -539,6 +544,14 @@ void Memory::free(const expr &ptr) {
p.is_block_alive() &&
p.get_alloc_type() == Pointer::MALLOC));
::store(p, false, local_block_liveness, non_local_block_liveness, true);
+
+ // optimization: if this is a local block, remove all associated information
+ if (p.is_local().isTrue() && p.get_short_bid().isConst()) {
+ expr bid = p.get_short_bid();
+ local_blk_addr.del(bid);
+ local_blk_size.del(bid);
+ local_blk_kind.del(bid);
+ }
}
void Memory::store(const expr &p, const StateValue &v, const Type &type,

MODIFY
ir/memory.h
ir/memory.h
@@ -49,7 +49,7 @@ public:
smt::expr get_bid() const;
smt::expr get_short_bid() const; // same as get_bid but ignoring is_local bit
smt::expr get_offset() const;
- smt::expr get_address() const;
+ smt::expr get_address(bool simplify = true) const;
smt::expr block_size(bool simplify = true) const;

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -39,6 +39,10 @@ void FunctionExpr::add(expr &&key, expr &&val) {
ENSURE(fn.emplace(move(key), move(val)).second);
}
+void FunctionExpr::del(const expr &key) {
+ fn.erase(key);
+}
+
void FunctionExpr::clear() {
fn.clear();
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -29,6 +29,7 @@ class FunctionExpr {
public:
void add(expr &&key, expr &&val);
+ void del(const expr &key);
void clear();
void reset(smt::expr &&default_val);
expr operator()(expr &key) const;

memory: add fast path for get_address() and remove local block data on free