memory: constant propagate data for non-local bids
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -204,10 +204,17 @@ expr Pointer::get_offset() const {
return p.extract(bits_for_offset - 1, 0).sextOrTrunc(bits_size_t);
}
-expr Pointer::get_value(const char *name, const FunctionExpr &fn,
+expr Pointer::get_value(const char *name, const FunctionExpr &local_fn,
+ const FunctionExpr &nonlocal_fn,
const expr &ret_type) const {
+ auto local = is_local();
auto bid = get_short_bid();
- return expr::mkIf(is_local(), fn(bid), expr::mkUF(name, { bid }, ret_type));
+
+ if (local.isFalse()) {
+ if (auto val = nonlocal_fn.lookup(bid))
+ return *val;
+ }
+ return expr::mkIf(local, local_fn(bid), expr::mkUF(name, { bid }, ret_type));
}
expr Pointer::get_address(bool simplify) const {
@@ -226,18 +233,13 @@ expr Pointer::get_address(bool simplify) const {
expr::mkUInt(0, 1).concat(expr::mkUF("blk_addr", { bid }, retty)));
}
-expr Pointer::block_size(bool simplify) const {
+expr Pointer::block_size() const {
// ASSUMPTION: programs can only allocate up to half of address space
// so the first bit of size is always zero.
// We need this assumption to support negative offsets.
-
- // fast path for null ptrs
- if (simplify && (get_bid() == 0).isTrue())
- return expr::mkUInt(0, bits_size_t);
-
- expr range = expr::mkUInt(0, bits_size_t - 1);
return expr::mkUInt(0, 1)
- .concat(get_value("blk_size", m.local_blk_size, range));
+ .concat(get_value("blk_size", m.local_blk_size, m.non_local_blk_size,
+ expr::mkUInt(0, bits_size_t - 1)));
}
expr Pointer::short_ptr() const {
@@ -290,9 +292,15 @@ expr Pointer::inbounds() const {
}
expr Pointer::is_aligned(unsigned align) const {
- if (auto bits = ilog2(align))
- return get_address().extract(bits-1, 0) == 0;
+ if (align <= 1)
return true;
+
+ auto bits = ilog2(align);
+ if (is_local().isFalse()) {
+ if (auto val = m.non_local_blk_align.lookup(get_short_bid()))
+ return val->uge(bits);
+ }
+ return get_address().extract(bits-1, 0) == 0;
}
// When bytes is 0, pointer is always derefenceable
@@ -345,7 +353,8 @@ expr Pointer::is_block_alive() const {
}
expr Pointer::get_alloc_type() const {
- return get_value("blk_kind", m.local_blk_kind, expr::mkUInt(0, 2));
+ return get_value("blk_kind", m.local_blk_kind, m.non_local_blk_kind,
+ expr::mkUInt(0, 2));
}
expr Pointer::is_heap_allocated() const {
@@ -398,7 +407,14 @@ expr Pointer::block_refined(const Pointer &other) const {
}
expr Pointer::is_readonly() const {
- return !is_local() && expr::mkUF("blk_readonly", { get_short_bid() }, false);
+ auto local = is_local();
+ auto bid = get_short_bid();
+
+ if (local.isFalse()) {
+ if (auto val = m.non_local_blk_readonly.lookup(bid))
+ return *val;
+ }
+ return !local && expr::mkUF("blk_readonly", { bid }, false);
}
Pointer Pointer::mkNullPointer(const Memory &m) {
@@ -521,15 +537,10 @@ Memory::Memory(State &state)
// value.
local_avail_space = expr::mkVar("local_avail_space", bits_size_t - 1);
- if (state.isSource()) {
- auto nullp = Pointer::mkNullPointer(*this);
- state.addAxiom(nullp.block_size(false) == 0);
- state.addAxiom(!nullp.is_block_alive());
- }
+ // Initialize a memory block for null pointer.
+ alloc(expr::mkUInt(0, bits_size_t), 1, GLOBAL, 0, nullptr, false);
if (state.isSource() && observes_addresses()) {
- // Initialize a memory block for null pointer.
- // TODO: in twin memory model, this is not needed.
state.addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);
// Non-local blocks are disjoint.
@@ -630,10 +641,10 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
unsigned alloc_ty = blockKind == HEAP ? Pointer::MALLOC : Pointer::NON_HEAP;
- if (is_local) {
assert(align != 0);
auto align_bits = ilog2(align);
+ if (is_local) {
// MSB of local block area's address is 1.
auto addr_var
= expr::mkFreshVar("local_addr",
@@ -660,9 +671,9 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
state->addPre(allocated.implies(disj));
}
- local_blk_addr.add(expr(short_bid), move(blk_addr));
- local_blk_size.add(expr(short_bid), size_zext.trunc(bits_size_t - 1));
- local_blk_kind.add(expr(short_bid), expr::mkUInt(alloc_ty, 2));
+ local_blk_addr.add(short_bid, move(blk_addr));
+ local_blk_size.add(short_bid, size_zext.trunc(bits_size_t - 1));
+ local_blk_kind.add(short_bid, expr::mkUInt(alloc_ty, 2));
local_block_liveness = local_block_liveness.store(short_bid, allocated);
@@ -681,10 +692,15 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
state->addAxiom(blockKind == CONSTGLOBAL ? p.is_readonly()
: !p.is_readonly());
// The memory block was initially alive.
- state->addAxiom(allocated.implies(mk_liveness_array().load(short_bid) &&
- p.is_aligned(align) &&
- p.block_size() == size_zext));
+ state->addAxiom(mk_liveness_array().load(short_bid) == allocated);
+ state->addAxiom(p.block_size() == size_zext);
+ state->addAxiom(p.is_aligned(align));
state->addAxiom(p.get_alloc_type() == alloc_ty);
+
+ non_local_blk_readonly.add(short_bid, blockKind == CONSTGLOBAL);
+ non_local_blk_size.add(short_bid, size_zext.trunc(bits_size_t - 1));
+ non_local_blk_align.add(short_bid, expr::mkUInt(align_bits, 8));
+ non_local_blk_kind.add(short_bid, expr::mkUInt(alloc_ty, 2));
}
return expr::mkIf(allocated, p(), Pointer::mkNullPointer(*this)());
}
@@ -821,6 +837,10 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
ret.local_blk_addr.add(els.local_blk_addr);
ret.local_blk_size.add(els.local_blk_size);
ret.local_blk_kind.add(els.local_blk_kind);
+ ret.non_local_blk_readonly.add(els.non_local_blk_readonly);
+ ret.non_local_blk_size.add(els.non_local_blk_size);
+ ret.non_local_blk_align.add(els.non_local_blk_align);
+ ret.non_local_blk_kind.add(els.non_local_blk_kind);
ret.did_pointer_store |= els.did_pointer_store;
return ret;
}
@@ -830,11 +850,15 @@ bool Memory::operator<(const Memory &rhs) const {
return
tie(did_pointer_store, non_local_block_val, local_block_val,
non_local_block_liveness, local_block_liveness, local_blk_addr,
- local_blk_size, local_blk_kind, local_avail_space) <
+ local_blk_size, local_blk_kind, local_avail_space,
+ non_local_blk_readonly, non_local_blk_size, non_local_blk_align,
+ non_local_blk_kind) <
tie(rhs.did_pointer_store, rhs.non_local_block_val, rhs.local_block_val,
rhs.non_local_block_liveness, rhs.local_block_liveness,
rhs.local_blk_addr, rhs.local_blk_size, rhs.local_blk_kind,
- rhs.local_avail_space);
+ rhs.local_avail_space, rhs.non_local_blk_readonly,
+ rhs.non_local_blk_size, rhs.non_local_blk_align,
+ rhs.non_local_blk_kind);
}
}

MODIFY
ir/memory.h
ir/memory.h
@@ -35,7 +35,8 @@ class Pointer {
unsigned total_bits() const;
- smt::expr get_value(const char *name, const smt::FunctionExpr &fn,
+ smt::expr get_value(const char *name, const smt::FunctionExpr &local_fn,
+ const smt::FunctionExpr &nonlocal_fn,
const smt::expr &ret_type) const;
public:
@@ -52,7 +53,7 @@ public:
smt::expr get_offset() const;
smt::expr get_address(bool simplify = true) const;
- smt::expr block_size(bool simplify = true) const;
+ smt::expr block_size() const;
const smt::expr& operator()() const { return p; }
smt::expr short_ptr() const;
@@ -123,6 +124,11 @@ class Memory {
smt::FunctionExpr local_blk_size;
smt::FunctionExpr local_blk_kind;
+ smt::FunctionExpr non_local_blk_readonly;
+ smt::FunctionExpr non_local_blk_size;
+ smt::FunctionExpr non_local_blk_align;
+ smt::FunctionExpr non_local_blk_kind;
+
smt::expr mk_val_array() const;
smt::expr mk_liveness_array() const;

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -41,6 +41,12 @@ ostream *out;
const llvm::DataLayout *DL;
+template <typename T>
+unsigned alignment(const T &i, llvm::Type *ty) {
+ auto a = i.getAlignment();
+ return a != 0 ? a : DL->getABITypeAlignment(ty);
+}
+
}
namespace llvm_util {
@@ -213,9 +219,9 @@ Value* get_operand(llvm::Value *v,
return nullptr;
}
- int size = DL->getTypeAllocSize(gv->getValueType());
- int align = gv->getAlignment();
- auto name = "@" + gv->getName().str();
+ unsigned size = DL->getTypeAllocSize(gv->getValueType());
+ unsigned align = alignment(*gv, gv->getValueType());
+ string name = '@' + gv->getName().str();
auto val = make_unique<GlobalVariable>(*ty, move(name), size, align,
gv->isConstant());
gvar = val.get();

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -8,8 +8,8 @@ using namespace std;
namespace smt {
-void FunctionExpr::add(expr &&key, expr &&val) {
- ENSURE(fn.emplace(move(key), move(val)).second);
+void FunctionExpr::add(const expr &key, expr &&val) {
+ ENSURE(fn.emplace(key, move(val)).second);
}
void FunctionExpr::add(const FunctionExpr &other) {
@@ -20,7 +20,7 @@ void FunctionExpr::del(const expr &key) {
fn.erase(key);
}
-expr FunctionExpr::operator()(expr &key) const {
+expr FunctionExpr::operator()(const expr &key) const {
DisjointExpr disj(default_val);
for (auto &[k, v] : fn) {
disj.add(v, k == key);
@@ -28,6 +28,11 @@ expr FunctionExpr::operator()(expr &key) const {
return disj();
}
+const expr* FunctionExpr::lookup(const expr &key) const {
+ auto I = fn.find(key);
+ return I != fn.end() ? &I->second : nullptr;
+}
+
bool FunctionExpr::operator<(const FunctionExpr &rhs) const {
return tie(fn, default_val) < tie(rhs.fn, rhs.default_val);
}

MODIFY
smt/exprs.h
smt/exprs.h
#include "smt/expr.h"
#include <map>
-#include <set>
#include <utility>
namespace smt {
@@ -53,10 +52,13 @@ class FunctionExpr {
public:
FunctionExpr() {}
FunctionExpr(expr &&default_val) : default_val(std::move(default_val)) {}
- void add(expr &&key, expr &&val);
+ void add(const expr &key, expr &&val);
void add(const FunctionExpr &other);
void del(const expr &key);
- expr operator()(expr &key) const;
+
+ expr operator()(const expr &key) const;
+ const expr* lookup(const expr &key) const;
+
auto begin() const { return fn.begin(); }
auto end() const { return fn.end(); }

memory: constant propagate data for non-local bids