simplify initial memory
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -11,6 +11,9 @@ using namespace util;
namespace IR {
+Pointer::Pointer(Memory &m, const char *var_name)
+ : m(m), p(expr::mkVar(var_name, total_bits())) {}
+
Pointer::Pointer(Memory &m, unsigned bid, bool local) : m(m) {
expr bid_expr;
if (local)
@@ -25,6 +28,10 @@ Pointer::Pointer(Memory &m, const expr &offset, const expr &local_bid,
const expr &nonlocal_bid)
: m(m), p(offset.concat(local_bid).concat(nonlocal_bid)) {}
+unsigned Pointer::total_bits() const {
+ return bits_for_bids() + m.bits_for_offset;
+}
+
unsigned Pointer::bits_for_bids() const {
return m.bits_for_local_bid + m.bits_for_nonlocal_bid;
}
@@ -162,22 +169,16 @@ expr Memory::mk_val_array(const char *name) const {
}
Memory::Memory(State &state) : state(&state) {
- auto val_name = mkName("blks_val");
- blocks_val = mk_val_array(val_name.c_str());
-
- assert(bits_for_offset <= bits_size_t);
+ blocks_val = mk_val_array("blks_val");
+ {
+ // initialize all local blocks as poison
+ Pointer idx(*this, "#idx0");
+ expr poison = expr::mkUInt(0, 9);
+ expr val = expr::mkIf(idx.is_local(), poison, blocks_val.load(idx()));
+ blocks_val = expr::mkLambda({ idx() }, move(val));
}
-expr Memory::mk_axioms() {
- expr offset = expr::mkVar("offset", bits_for_offset);
- expr bid = expr::mkVar("bid", bits_for_nonlocal_bid);
- Pointer ptr(*this, offset, expr::mkUInt(0, bits_for_local_bid), bid);
-
- auto val_src_name = mkName("blks_val", true);
- auto val_tgt_name = mkName("blks_val", false);
- auto val_src = mk_val_array(val_src_name.c_str()).load(ptr());
- auto val_tgt = mk_val_array(val_tgt_name.c_str()).load(ptr());
- return expr::mkForAll({ offset, bid }, val_src == val_tgt);
+ assert(bits_for_offset <= bits_size_t);
}
pair<expr, vector<expr>> Memory::mkInput(const char *name) {
@@ -195,7 +196,6 @@ expr Memory::alloc(const expr &bytes, unsigned align, bool local) {
expr size = bytes.zextOrTrunc(bits_size_t);
state->addPre(p.block_size() == size);
- memset(p(), { expr::mkUInt(0, 8), false }, size, align);
return p();
}
@@ -289,7 +289,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,
}
} else {
string name = "#idx_" + to_string(last_idx_ptr++);
- Pointer idx(*this, expr::mkVar(name.c_str(), ptr.bits()));
+ Pointer idx(*this, name.c_str());
expr cond = idx.uge(ptr).both() && idx.ult(ptr + bytes).both();
expr val = expr::mkIf(cond, store_val, blocks_val.load(idx()));

MODIFY
ir/memory.h
ir/memory.h
@@ -22,9 +22,11 @@ class Pointer {
// TODO: missing support for address space
smt::expr p;
+ unsigned total_bits() const;
unsigned bits_for_bids() const;
public:
+ Pointer(Memory &m, const char *var_name);
Pointer(Memory &m, smt::expr p) : m(m), p(std::move(p)) {}
Pointer(Memory &m, unsigned bid, bool local);
Pointer(Memory &m, const smt::expr &offset, const smt::expr &local_bid,
@@ -92,8 +94,6 @@ class Memory {
public:
Memory(State &state);
- smt::expr mk_axioms();
-
std::pair<smt::expr, std::vector<smt::expr>> mkInput(const char *name);
smt::expr alloc(const smt::expr &bytes, unsigned align, bool local);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -16,9 +16,6 @@ State::State(const Function &f, bool source)
predecessor_data[&f.getFirstBB()].try_emplace(nullptr,
DomainTy(true, set<expr>()),
*this);
-
- if (source)
- addPre(getMemory().mk_axioms());
}
const StateValue& State::exec(const Value &v) {

simplify initial memory