further work on memory model
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -9,34 +9,47 @@ using namespace smt;
using namespace std;
using namespace util;
-namespace {
-struct Pointer {
- IR::Memory &m;
- // [offset, local_bid, nonlocal_bid]
- const expr &p;
+namespace IR {
- Pointer(IR::Memory *m, const expr &p) : m(*m), p(p) {}
+Pointer::Pointer(Memory &m, unsigned bid, bool local) : m(m) {
+ expr bid;
+ if (local)
+ bid = expr::mkUInt((uint64_t)bid << m.bits_for_nonlocal_bid,
+ bits_for_bids());
+ else
+ bid = expr::mkUInt(bid, bits_for_bids());
+ p = expr::mkUInt(0, m.bits_for_offset).concat(bid);
+}
- expr get_offset() const {
- // FIXME
- return p.extract(0, 0);
+unsigned Pointer::bits_for_bids() const {
+ return m.bits_for_local_bid + m.bits_for_nonlocal_bid;
}
- const expr& operator()() const {
- return p;
+expr Pointer::get_bid() const {
+ return p.extract(bits_for_bids() - 1, 0);
}
- void operator++(void) {
- // TODO
+expr Pointer::get_offset() const {
+ return p.extract(bits_for_bids() + m.bits_for_offset - 1, bits_for_bids());
}
- void is_dereferenceable(unsigned bytes) {
- // TODO
+void Pointer::operator++(void) {
+ p = (get_offset() + expr::mkUInt(1, m.bits_for_offset)).concat(get_bid());
}
-};
+
+void Pointer::is_dereferenceable(unsigned bytes) {
+ expr block_sz = m.blocks_size.load(get_bid());
+ expr offset = get_offset();
+ expr length = expr::mkUInt(bytes, m.bits_for_offset);
+
+ // 1) check that offset is within bounds and that arith doesn't overflow
+ m.state.addUB((offset + length).ult(block_sz));
+ m.state.addUB(offset.add_no_uoverflow(length));
+
+ // 2) check block is alive
+ // TODO
}
-namespace IR {
Memory::Memory(State &state) : state(state) {
unsigned bits_bids = bits_for_local_bid + bits_for_nonlocal_bid;
@@ -46,30 +59,37 @@ Memory::Memory(State &state) : state(state) {
blocks_val = expr::mkArray("blks_val",
expr::mkUInt(0, bits_bids + bits_for_offset),
- expr::mkUInt(0, 8 + 1)); // 1 byte + 1 bit poison
+ expr::mkUInt(0, byte_size + 1)); // val+poison bit
+}
+
+expr Memory::alloc(const expr &bytes, bool local) {
+ Pointer p(*this, last_bid++, local);
+ blocks_size = blocks_size.store(p(), bytes.zextOrTrunc(bits_size_t));
+ memset(p(), { expr::mkUInt(0, byte_size), false }, bytes);
+ return p();
}
void Memory::store(const expr &p, const StateValue &v) {
unsigned bits = v.value.bits();
- unsigned bytes = divide_up(bits, 8);
+ unsigned bytes = divide_up(bits, byte_size);
- Pointer ptr(this, p);
+ Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes);
expr poison = v.non_poison.toBVBool();
- expr val = v.value.zext(bytes * 8 - bits);
+ expr val = v.value.zext(bytes * byte_size - bits);
for (unsigned i = 0; i < bytes; ++i) {
// FIXME: right now we store in little-endian; consider others?
- blocks_val = blocks_val.store(ptr(),
- poison.concat(val.extract((i+1)*8 - 1, i*8)));
+ expr data = val.extract((i + 1) * byte_size - 1, i * byte_size);
+ blocks_val = blocks_val.store(ptr(), poison.concat(data));
++ptr;
}
}
StateValue Memory::load(const expr &p, unsigned bits) {
- unsigned bytes = divide_up(bits, 8);
- Pointer ptr(this, p);
+ unsigned bytes = divide_up(bits, byte_size);
+ Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes);
expr val, non_poison;
@@ -77,8 +97,8 @@ StateValue Memory::load(const expr &p, unsigned bits) {
for (unsigned i = 0; i < bytes; ++i) {
expr pair = blocks_val.load(ptr());
- expr v = pair.extract(7, 0);
- expr p = pair.extract(8, 8) == expr::mkUInt(1, 1);
+ expr v = pair.extract(byte_size-1, 0);
+ expr p = pair.extract(byte_size, byte_size) == expr::mkUInt(1, 1);
if (first) {
val = move(v);
@@ -94,9 +114,27 @@ StateValue Memory::load(const expr &p, unsigned bits) {
return { val.trunc(bits), move(non_poison) };
}
-Memory Memory::ite(const expr &cond, const Memory &then, const Memory &els) {
+void Memory::memset(const expr &ptr, const StateValue &val, const expr &bytes) {
// TODO
- return then;
+}
+
+void Memory::memcpy(const expr &dst, const expr &src, const expr &bytes) {
+ // TODO
+}
+
+Memory Memory::ite(const expr &cond, const Memory &then, const Memory &els) {
+ assert(&then.state == &els.state);
+ Memory ret(then.state);
+ ret.bits_for_offset = then.bits_for_offset;
+ ret.bits_for_local_bid = then.bits_for_local_bid;
+ ret.bits_for_nonlocal_bid = then.bits_for_nonlocal_bid;
+ ret.bits_size_t = then.bits_size_t;
+ ret.byte_size = then.byte_size;
+
+ ret.blocks_size = expr::mkIf(cond, then.blocks_size, els.blocks_size);
+ ret.blocks_val = expr::mkIf(cond, then.blocks_val, els.blocks_val);
+ ret.last_bid = max(then.last_bid, els.last_bid);
+ return ret;
}
}

MODIFY
ir/memory.h
ir/memory.h
namespace IR {
+class Memory;
class State;
+class Pointer {
+ Memory &m;
+ // [offset, local_bid, nonlocal_bid]
+ smt::expr p;
+
+ unsigned bits_for_bids() const;
+
+public:
+ Pointer(Memory &m, smt::expr p) : m(m), p(std::move(p)) {}
+ Pointer(Memory &m, unsigned bid, bool local);
+
+ smt::expr get_bid() const;
+ smt::expr get_offset() const;
+
+ const smt::expr& operator()() const { return p; }
+
+ void operator++(void);
+
+ void is_dereferenceable(unsigned bytes);
+};
+
+
class Memory {
State &state;
@@ -18,18 +41,28 @@ class Memory {
unsigned bits_for_local_bid = 8;
unsigned bits_for_nonlocal_bid = 8;
unsigned bits_size_t = 64;
+ unsigned byte_size = 8;
smt::expr blocks_size; // array: bid -> size in bytes
smt::expr blocks_val; // array: (bid, offset) -> StateValue
+ unsigned last_bid = 0;
public:
Memory(State &state);
+ smt::expr alloc(const smt::expr &bytes, bool local);
void store(const smt::expr &ptr, const StateValue &val);
StateValue load(const smt::expr &ptr, unsigned bits);
+ void memset(const smt::expr &ptr, const StateValue &val,
+ const smt::expr &bytes);
+ void memcpy(const smt::expr &dst, const smt::expr &src,
+ const smt::expr &bytes);
+
static Memory ite(const smt::expr &cond, const Memory &then,
const Memory &els);
+
+ friend class Pointer;
};
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -942,6 +942,11 @@ expr expr::trunc(unsigned tobw) const {
return extract(tobw-1, 0);
}
+expr expr::zextOrTrunc(unsigned tobw) const {
+ auto bw = bits();
+ return bw < tobw ? zext(tobw - bw) : trunc(tobw);
+}
+
expr expr::concat(const expr &rhs) const {
C(rhs);
return Z3_mk_concat(ctx(), ast(), rhs());

MODIFY
smt/expr.h
smt/expr.h
@@ -185,6 +185,7 @@ public:
expr sext(unsigned amount) const;
expr zext(unsigned amount) const;
expr trunc(unsigned tobw) const;
+ expr zextOrTrunc(unsigned tobw) const;
expr concat(const expr &rhs) const;
expr extract(unsigned high, unsigned low) const;

further work on memory model