memory: track undef variables of data stored in memory explicitly
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1969,7 +1969,7 @@ StateValue Calloc::toSMT(State &s) const {
nonnull);
expr calloc_sz = expr::mkIf(allocated, size, expr::mkUInt(0, sz.bits()));
- s.getMemory().memset(p, { expr::mkUInt(0, 8), true }, calloc_sz, align);
+ s.getMemory().memset(p, { expr::mkUInt(0, 8), true }, calloc_sz, align, {});
return { move(p), move(np) };
}
@@ -2206,7 +2206,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], val->getType(), align);
+ s.getMemory().store(p, s[*val], val->getType(), align, s.getUndefVars());
return {};
}
@@ -2239,7 +2239,8 @@ StateValue Memset::toSMT(State &s) const {
auto &[vbytes, np_bytes] = s[*bytes];
s.addUB((vbytes != 0).implies(np_ptr));
s.addUB(np_bytes);
- s.getMemory().memset(vptr, s[*val].zextOrTrunc(8), vbytes, align);
+ s.getMemory().memset(vptr, s[*val].zextOrTrunc(8), vbytes, align,
+ s.getUndefVars());
return {};
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1464,11 +1464,14 @@ unsigned Memory::getStoreByteSize(const Type &ty) {
}
void Memory::store(const expr &p, const StateValue &v, const Type &type,
- unsigned align, bool deref_check) {
+ unsigned align, const set<expr> &undef_vars0,
+ bool deref_check) {
assert(!memory_unused());
Pointer ptr(*this, p);
unsigned bytesz = bits_byte / 8;
+ undef_vars.insert(undef_vars0.begin(), undef_vars0.end());
+
if (deref_check)
state->addUB(ptr.is_dereferenceable(getStoreByteSize(type), align,
!state->isInitializationPhase()));
@@ -1481,7 +1484,7 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
continue;
auto ptr_i = ptr + byteofs;
auto align_i = gcd(align, byteofs % align);
- store(ptr_i(), aty->extract(v, i), child, align_i, false);
+ store(ptr_i(), aty->extract(v, i), child, align_i, {}, false);
byteofs += getStoreByteSize(child);
}
assert(byteofs == getStoreByteSize(type));
@@ -1533,7 +1536,7 @@ Memory::load(const expr &p, const Type &type, unsigned align) {
}
ret = bytesToValue(*this, loadedBytes, type);
}
- return { state->rewriteUndef(move(ret)), move(ubs) };
+ return { state->rewriteUndef(move(ret), undef_vars), move(ubs) };
}
Byte Memory::load(const Pointer &p) const {
@@ -1553,12 +1556,13 @@ static expr ptr_deref_within(const Pointer &idx, const Pointer &ptr,
}
void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
- unsigned align) {
+ unsigned align, const set<expr> &undef_vars0) {
assert(!memory_unused());
assert(!val.isValid() || val.bits() == 8);
unsigned bytesz = bits_byte / 8;
Pointer ptr(*this, p);
state->addUB(ptr.is_dereferenceable(bytesize, align, true));
+ undef_vars.insert(undef_vars0.begin(), undef_vars0.end());
auto wval = val;
for (unsigned i = 1; i < bytesz; ++i) {
@@ -1728,14 +1732,15 @@ bool Memory::operator<(const Memory &rhs) const {
non_local_block_liveness, local_block_liveness, local_blk_addr,
local_blk_size, local_blk_align, local_blk_kind,
non_local_blk_nonwritable, non_local_blk_size, non_local_blk_align,
- non_local_blk_kind, byval_blks, escaped_local_blks) <
+ non_local_blk_kind, byval_blks, escaped_local_blks, undef_vars) <
tie(rhs.non_local_block_val, rhs.local_block_val,
rhs.initial_non_local_block_val,
rhs.non_local_block_liveness, rhs.local_block_liveness,
rhs.local_blk_addr, rhs.local_blk_size, rhs.local_blk_align,
rhs.local_blk_kind, rhs.non_local_blk_nonwritable,
rhs.non_local_blk_size, rhs.non_local_blk_align,
- rhs.non_local_blk_kind, rhs.byval_blks, rhs.escaped_local_blks);
+ rhs.non_local_blk_kind, rhs.byval_blks, rhs.escaped_local_blks,
+ rhs.undef_vars);
}
#define P(name, expr) do { \

MODIFY
ir/memory.h
ir/memory.h
#include "smt/exprs.h"
#include <optional>
#include <ostream>
+#include <set>
#include <utility>
#include <vector>
@@ -210,6 +211,8 @@ class Memory {
std::vector<unsigned> byval_blks;
std::vector<bool> escaped_local_blks;
+ std::set<smt::expr> undef_vars;
+
void store(const Pointer &p, const smt::expr &val, smt::expr &local,
smt::expr &non_local);
@@ -270,7 +273,8 @@ public:
static unsigned getStoreByteSize(const Type &ty);
void store(const smt::expr &ptr, const StateValue &val, const Type &type,
- unsigned align, bool deref_check = true);
+ unsigned align, const std::set<smt::expr> &undef_vars,
+ bool deref_check = true);
std::pair<StateValue, smt::AndExpr> load(const smt::expr &ptr,
const Type &type, unsigned align);
@@ -278,7 +282,8 @@ public:
Byte load(const Pointer &p) const;
void memset(const smt::expr &ptr, const StateValue &val,
- const smt::expr &bytesize, unsigned align);
+ const smt::expr &bytesize, unsigned align,
+ const std::set<smt::expr> &undef_vars);
void memcpy(const smt::expr &dst, const smt::expr &src,
const smt::expr &bytesize, unsigned align_dst, unsigned align_src,
bool move);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -302,21 +302,18 @@ void State::resetUndefVars() {
undef_vars.clear();
}
-StateValue State::rewriteUndef(StateValue &&val) {
+StateValue State::rewriteUndef(StateValue &&val, const set<expr> &undef_vars) {
+ if (undef_vars.empty())
+ return move(val);
+ if (hit_half_memory_limit())
+ throw AliveException("Out of memory; skipping function.", false);
+
vector<pair<expr, expr>> repls;
- for (auto &var : val.vars()) {
- if (isUndef(var)) {
+ for (auto &var : undef_vars) {
auto newvar = expr::mkFreshVar("undef", var);
repls.emplace_back(var, newvar);
addUndefVar(move(newvar));
}
- }
-
- if (repls.empty())
- return move(val);
- if (hit_half_memory_limit())
- throw AliveException("Out of memory; skipping function.", false);
-
return val.subst(repls);
}

MODIFY
ir/state.h
ir/state.h
@@ -145,9 +145,11 @@ public:
void addQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);
+ auto& getUndefVars() const { return undef_vars; }
void resetUndefVars();
- StateValue rewriteUndef(StateValue &&val);
+ StateValue rewriteUndef(StateValue &&val,
+ const std::set<smt::expr> &undef_vars);
bool isInitializationPhase() const { return is_initialization_phase; }
void finishInitializer();

memory: track undef variables of data stored in memory explicitly