Let Pointer::is_dereferenceable and Memory::load return UB constraints
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1206,7 +1206,7 @@ static StateValue pack_return(Type &ty, vector<StateValue> &vals,
StateValue FnCall::toSMT(State &s) const {
if (!valid) {
- s.addUB({});
+ s.addUB(expr());
return {};
}
@@ -1671,7 +1671,7 @@ StateValue Switch::toSMT(State &s) const {
}
s.addJump({ move(default_cond), expr(val.non_poison) }, default_target);
- s.addUB(false);
+ s.addUB(expr(false));
return {};
}
@@ -2109,7 +2109,9 @@ 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(), align);
+ auto [sv, ub] = s.getMemory().load(p, getType(), align);
+ s.addUB(move(ub));
+ return sv;
}
expr Load::getTypeConstraints(const Function &f) const {

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -594,7 +594,7 @@ static pair<expr, expr> is_dereferenceable(const Pointer &p,
}
// When bytes is 0, pointer is always derefenceable
-void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
+AndExpr Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
bool iswrite) {
expr bytes_off = bytes0.zextOrTrunc(bits_for_offset);
expr bytes = bytes0.zextOrTrunc(bits_size_t);
@@ -613,24 +613,28 @@ void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
is_aligned.add(move(aligned), domain);
}
- m.state->addUB(bytes == 0 || *UB());
+ AndExpr exprs;
+ exprs.add(bytes == 0 || *UB());
// cannot store more bytes than address space
if (bytes0.bits() > bits_size_t)
- m.state->addUB(bytes0.extract(bytes0.bits() - 1, bits_size_t) == 0);
+ exprs.add(bytes0.extract(bytes0.bits() - 1, bits_size_t) == 0);
// address must be always aligned regardless of access size
- m.state->addUB(*is_aligned());
+ exprs.add(*is_aligned());
// trim set of valid ptrs
if (auto ptrs = all_ptrs())
p = *ptrs;
else
p = expr::mkUInt(0, total_bits());
+
+ return exprs;
}
-void Pointer::is_dereferenceable(unsigned bytes, unsigned align, bool iswrite) {
- is_dereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite);
+AndExpr Pointer::is_dereferenceable(unsigned bytes, unsigned align,
+ bool iswrite) {
+ return is_dereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite);
}
// general disjoint check for unsigned integer
@@ -1398,8 +1402,8 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
unsigned bytesz = bits_byte / 8;
if (deref_check)
- ptr.is_dereferenceable(getStoreByteSize(type), align,
- !state->isInitializationPhase());
+ state->addUB(ptr.is_dereferenceable(getStoreByteSize(type), align,
+ !state->isInitializationPhase()));
if (auto aty = type.getAsAggregateType()) {
unsigned byteofs = 0;
@@ -1427,15 +1431,14 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
}
}
-StateValue Memory::load(const expr &p, const Type &type, unsigned align,
- bool deref_check) {
+pair<StateValue, AndExpr>
+Memory::load(const expr &p, const Type &type, unsigned align) {
assert(!memory_unused());
unsigned bytesz = bits_byte / 8;
unsigned bytecount = getStoreByteSize(type);
Pointer ptr(*this, p);
- if (deref_check)
- ptr.is_dereferenceable(bytecount, align, false);
+ auto ubs = ptr.is_dereferenceable(bytecount, align, false);
StateValue ret;
if (auto aty = type.getAsAggregateType()) {
@@ -1444,7 +1447,7 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
for (unsigned i = 0, e = aty->numElementsConst(); i < e; ++i) {
auto ptr_i = ptr + byteofs;
auto align_i = gcd(align, byteofs % align);
- member_vals.push_back(load(ptr_i(), aty->getChild(i), align_i, false));
+ member_vals.push_back(load(ptr_i(), aty->getChild(i), align_i).first);
byteofs += getStoreByteSize(aty->getChild(i));
}
assert(byteofs == bytecount);
@@ -1462,7 +1465,7 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
}
ret = bytesToValue(*this, loadedBytes, type);
}
- return state->rewriteUndef(move(ret));
+ return { state->rewriteUndef(move(ret)), move(ubs) };
}
Byte Memory::load(const Pointer &p) const {
@@ -1487,7 +1490,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
assert(!val.isValid() || val.bits() == 8);
unsigned bytesz = bits_byte / 8;
Pointer ptr(*this, p);
- ptr.is_dereferenceable(bytesize, align, true);
+ state->addUB(ptr.is_dereferenceable(bytesize, align, true));
auto wval = val;
for (unsigned i = 1; i < bytesz; ++i) {
@@ -1515,8 +1518,8 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
assert(!memory_unused());
assert(bits_byte == 8);
Pointer dst(*this, d), src(*this, s);
- dst.is_dereferenceable(bytesize, align_dst, true);
- src.is_dereferenceable(bytesize, align_src, false);
+ state->addUB(dst.is_dereferenceable(bytesize, align_dst, true));
+ state->addUB(src.is_dereferenceable(bytesize, align_src, false));
if (!is_move)
src.is_disjoint(bytesize, dst, bytesize);

MODIFY
ir/memory.h
ir/memory.h
@@ -147,8 +147,9 @@ public:
smt::expr block_alignment() const; // log(bits)
smt::expr is_block_aligned(unsigned align, bool exact = false) const;
smt::expr is_aligned(unsigned align) const;
- void is_dereferenceable(unsigned bytes, unsigned align, bool iswrite);
- void is_dereferenceable(const smt::expr &bytes, unsigned align, bool iswrite);
+ smt::AndExpr is_dereferenceable(unsigned bytes, unsigned align, bool iswrite);
+ smt::AndExpr is_dereferenceable(const smt::expr &bytes, unsigned align,
+ bool iswrite);
void is_disjoint(const smt::expr &len1, const Pointer &ptr2,
const smt::expr &len2) const;
smt::expr is_block_alive() const;
@@ -267,8 +268,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);
- StateValue load(const smt::expr &ptr, const Type &type, unsigned align,
- bool deref_check = true);
+ std::pair<StateValue, smt::AndExpr> load(const smt::expr &ptr,
+ const Type &type, unsigned align);
// raw load
Byte load(const Pointer &p) const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -160,7 +160,7 @@ void State::addJump(const BasicBlock &dst0, expr &&cond) {
void State::addJump(const BasicBlock &dst) {
addJump(dst, true);
- addUB(false);
+ addUB(expr(false));
}
void State::addJump(StateValue &&cond, const BasicBlock &dst) {
@@ -173,7 +173,7 @@ void State::addCondJump(const StateValue &cond, const BasicBlock &dst_true,
addUB(cond.non_poison);
addJump(dst_true, cond.value == 1);
addJump(dst_false, cond.value == 0);
- addUB(false);
+ addUB(expr(false));
}
void State::addReturn(const StateValue &val) {
@@ -183,7 +183,7 @@ void State::addReturn(const StateValue &val) {
return_undef_vars.insert(undef_vars.begin(), undef_vars.end());
return_undef_vars.insert(domain.undef_vars.begin(), domain.undef_vars.end());
undef_vars.clear();
- addUB(false);
+ addUB(expr(false));
}
void State::addUB(expr &&ub) {
@@ -196,6 +196,11 @@ void State::addUB(const expr &ub) {
domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
}
+void State::addUB(AndExpr &&ubs) {
+ domain.UB.add(ubs);
+ domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
+}
+
const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<pair<StateValue, bool>> &&ptr_inputs,

MODIFY
ir/state.h
ir/state.h
@@ -123,6 +123,7 @@ public:
void addPre(smt::expr &&cond) { precondition.add(std::move(cond)); }
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
+ void addUB(smt::AndExpr &&ubs);
void addOOM(smt::expr &&oom) { ooms.add(std::move(oom)); }
const std::vector<StateValue>

Let Pointer::is_dereferenceable and Memory::load return UB constraints (#301)