track memory through branches
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -943,7 +943,7 @@ void Load::print(std::ostream &os) const {
StateValue Load::toSMT(State &s) const {
auto &[p, np] = s[ptr];
s.addUB(np);
- return s.getMemory().load(p, getType().bits());
+ return s.getMemory().load(p, getType().bits(), align);
}
expr Load::getTypeConstraints(const Function &f) const {
@@ -963,7 +963,7 @@ void Store::print(std::ostream &os) const {
StateValue Store::toSMT(State &s) const {
auto &[p, np] = s[ptr];
s.addUB(np);
- s.getMemory().store(p, s[val]);
+ s.getMemory().store(p, s[val], align);
return {};
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -43,15 +43,15 @@ void Pointer::is_dereferenceable(unsigned bytes) {
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).zextOrTrunc(m.bits_size_t).ult(block_sz));
- m.state.addUB(offset.add_no_uoverflow(length));
+ m.state->addUB((offset + length).zextOrTrunc(m.bits_size_t).ult(block_sz));
+ m.state->addUB(offset.add_no_uoverflow(length));
// 2) check block is alive
// TODO
}
-Memory::Memory(State &state) : state(state) {
+Memory::Memory(State &state) : state(&state) {
unsigned bits_bids = bits_for_local_bid + bits_for_nonlocal_bid;
blocks_size = expr::mkArray("blks_size",
expr::mkUInt(0, bits_bids),
@@ -60,6 +60,8 @@ Memory::Memory(State &state) : state(state) {
blocks_val = expr::mkArray("blks_val",
expr::mkUInt(0, bits_bids + bits_for_offset),
expr::mkUInt(0, byte_size + 1)); // val+poison bit
+
+ assert(bits_for_offset <= bits_size_t);
}
expr Memory::alloc(const expr &bytes, unsigned align, bool local) {
@@ -74,11 +76,12 @@ void Memory::free(const expr &ptr) {
// TODO
}
-void Memory::store(const expr &p, const StateValue &v) {
+void Memory::store(const expr &p, const StateValue &v, unsigned align) {
unsigned bits = v.value.bits();
unsigned bytes = divide_up(bits, byte_size);
Pointer ptr(*this, p);
+ // TODO: handle alignment
ptr.is_dereferenceable(bytes);
expr poison = v.non_poison.toBVBool();
@@ -92,9 +95,10 @@ void Memory::store(const expr &p, const StateValue &v) {
}
}
-StateValue Memory::load(const expr &p, unsigned bits) {
+StateValue Memory::load(const expr &p, unsigned bits, unsigned align) {
unsigned bytes = divide_up(bits, byte_size);
Pointer ptr(*this, p);
+ // TODO: handle alignment
ptr.is_dereferenceable(bytes);
expr val, non_poison;
@@ -127,15 +131,9 @@ 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;
-
+Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
+ assert(then.state == els.state);
+ Memory ret(then);
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);

MODIFY
ir/memory.h
ir/memory.h
@@ -34,7 +34,7 @@ public:
class Memory {
- State &state;
+ State *state;
// FIXME: these should be tuned per function
unsigned bits_for_offset = 32;
@@ -53,15 +53,15 @@ public:
smt::expr alloc(const smt::expr &bytes, unsigned align, bool local);
void free(const smt::expr &ptr);
- void store(const smt::expr &ptr, const StateValue &val);
- StateValue load(const smt::expr &ptr, unsigned bits);
+ void store(const smt::expr &ptr, const StateValue &val, unsigned align);
+ StateValue load(const smt::expr &ptr, unsigned bits, unsigned align);
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,
+ static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);
friend class Pointer;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -12,7 +12,9 @@ using namespace std;
namespace IR {
State::State(const Function &f) : f(f), memory(*this) {
- predecessor_domain[&f.getFirstBB()].try_emplace(nullptr, true, set<expr>());
+ predecessor_data[&f.getFirstBB()].try_emplace(nullptr,
+ DomainTy(true, set<expr>()),
+ *this);
}
const StateValue& State::exec(const Value &v) {
@@ -61,9 +63,9 @@ const State::ValTy& State::at(const Value &val) const {
}
const expr* State::jumpCondFrom(const BasicBlock &bb) const {
- auto &pres = predecessor_domain.at(current_bb);
+ auto &pres = predecessor_data.at(current_bb);
auto I = pres.find(&bb);
- return I == pres.end() ? nullptr : &I->second.first;
+ return I == pres.end() ? nullptr : &I->second.first.first;
}
bool State::startBB(const BasicBlock &bb) {
@@ -71,18 +73,27 @@ bool State::startBB(const BasicBlock &bb) {
ENSURE(seen_bbs.emplace(&bb).second);
current_bb = &bb;
- auto I = predecessor_domain.find(&bb);
- if (I == predecessor_domain.end())
+ auto I = predecessor_data.find(&bb);
+ if (I == predecessor_data.end())
return false;
domain.first = false;
domain.second.clear();
+ bool first = true;
for (auto &[src, data] : I->second) {
(void)src;
- auto &[d, vars] = data;
- domain.first |= d;
+ auto &[dom, mem] = data;
+ auto &[cond, vars] = dom;
+ domain.first |= cond;
domain.second.insert(vars.begin(), vars.end());
+
+ if (first) {
+ memory = mem;
+ first = false;
+ } else {
+ memory = Memory::mkIf(cond, mem, memory);
+ }
}
return !domain.first.isFalse();
}
@@ -92,13 +103,17 @@ void State::addJump(const BasicBlock &dst, expr &&cond) {
throw LoopInCFGDetected();
cond &= domain.first;
- auto p = predecessor_domain[&dst].try_emplace(current_bb, move(cond),
- undef_vars);
+ auto p = predecessor_data[&dst].try_emplace(current_bb, DomainTy({}, {}),
+ memory);
if (!p.second) {
- p.first->second.first |= move(cond);
- p.first->second.second.insert(undef_vars.begin(), undef_vars.end());
+ p.first->second.second = Memory::mkIf(cond, memory, p.first->second.second);
+ p.first->second.first.first |= move(cond);
+ p.first->second.first.second.insert(undef_vars.begin(), undef_vars.end());
+ } else {
+ p.first->second.first.first = move(cond);
+ p.first->second.first.second = undef_vars;
}
- p.first->second.second.insert(domain.second.begin(), domain.second.end());
+ p.first->second.first.second.insert(domain.second.begin(), domain.second.end());
}
void State::addJump(const BasicBlock &dst) {

MODIFY
ir/state.h
ir/state.h
@@ -37,10 +37,11 @@ private:
std::unordered_map<const Value*, unsigned> values_map;
std::vector<std::pair<const Value*, ValTy>> values;
- // dst BB -> src BB -> domain data
+ // dst BB -> src BB -> (domain data, memory)
std::unordered_map<const BasicBlock*,
- std::unordered_map<const BasicBlock*, DomainTy>>
- predecessor_domain;
+ std::unordered_map<const BasicBlock*,
+ std::pair<DomainTy, Memory>>>
+ predecessor_data;
std::unordered_set<const BasicBlock*> seen_bbs;
// temp state

track memory through branches