add pointer comparison support for memcmp
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -29,8 +29,7 @@ unsigned bits_byte;
unsigned strlen_unroll_cnt;
unsigned memcmp_unroll_cnt;
bool little_endian;
-bool has_int2ptr;
-bool has_ptr2int;
+bool observes_addresses;
bool has_malloc;
bool has_free;
bool has_alloca;

MODIFY
ir/globals.h
ir/globals.h
@@ -54,9 +54,8 @@ extern unsigned memcmp_unroll_cnt;
extern bool little_endian;
-/// Whether int2ptr or ptr2int are used in either function
-extern bool has_int2ptr;
-extern bool has_ptr2int;
+/// Whether pointer addresses are observed
+extern bool observes_addresses;
/// Whether malloc or free/delete is used in either function
extern bool has_malloc;

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -69,18 +69,16 @@ struct LoopLikeFunctionApproximator {
auto ub = ub_i();
prefix.add(ub_i);
- if (is_last) {
+ if (is_last)
s.addPre(prefix().implies(!continue_i));
- return { move(res_i), move(np_i), move(ub) };
- }
- if (continue_i.isFalse() || ub.isFalse())
+ if (is_last || continue_i.isFalse() || ub.isFalse())
return { move(res_i), move(np_i), move(ub) };
prefix.add(continue_i);
auto [val_next, np_next, ub_next] = _loop(s, prefix, i + 1, unroll_cnt);
return { expr::mkIf(continue_i, move(val_next), move(res_i)),
- expr::mkIf(continue_i, move(np_next), move(np_i)),
+ np_i && continue_i.implies(np_next),
ub && continue_i.implies(ub_next) };
}
};
@@ -2533,16 +2531,14 @@ unique_ptr<Instr> Assume::dup(const string &suffix) const {
}
-MemInstr::ByteAccessInfo
-MemInstr::ByteAccessInfo::intOnly(unsigned bytesz) {
+MemInstr::ByteAccessInfo MemInstr::ByteAccessInfo::intOnly(unsigned bytesz) {
ByteAccessInfo info;
info.byteSize = bytesz;
info.hasIntByteAccess = true;
return info;
}
-MemInstr::ByteAccessInfo
-MemInstr::ByteAccessInfo::anyType(unsigned bytesz) {
+MemInstr::ByteAccessInfo MemInstr::ByteAccessInfo::anyType(unsigned bytesz) {
ByteAccessInfo info;
info.byteSize = bytesz;
return info;
@@ -2559,11 +2555,11 @@ MemInstr::ByteAccessInfo::get(const Type &t, bool store, unsigned align) {
return info;
}
-MemInstr::ByteAccessInfo
-MemInstr::ByteAccessInfo::full(unsigned byteSize) {
- return { true, true, true, byteSize };
+MemInstr::ByteAccessInfo MemInstr::ByteAccessInfo::full(unsigned byteSize) {
+ return { true, true, true, true, byteSize };
}
+
static void eq_bids(OrExpr &acc, Memory &m, const Type &t,
const StateValue &val, const expr &bid) {
if (auto agg = t.getAsAggregateType()) {
@@ -3275,7 +3271,6 @@ uint64_t Memcpy::getMaxAccessSize() const {
}
Memcpy::ByteAccessInfo Memcpy::getByteAccessInfo() const {
- unsigned byteSize = 1;
#if 0
if (auto bytes = get_int(i->getBytes()))
byteSize = gcd(gcd(i->getSrcAlign(), i->getDstAlign()), *bytes);
@@ -3283,7 +3278,9 @@ Memcpy::ByteAccessInfo Memcpy::getByteAccessInfo() const {
// FIXME: memcpy doesn't have multi-byte support
// Memcpy does not have sub-byte access, unless the sub-byte type appears
// at other instructions
- return ByteAccessInfo::full(byteSize);
+ auto info = ByteAccessInfo::full(1);
+ info.observesAddresses = false;
+ return info;
}
vector<Value*> Memcpy::operands() const {
@@ -3351,7 +3348,9 @@ uint64_t Memcmp::getMaxAccessSize() const {
}
Memcmp::ByteAccessInfo Memcmp::getByteAccessInfo() const {
- return ByteAccessInfo::intOnly(1); /* memcmp raises UB on ptr bytes */
+ auto info = ByteAccessInfo::anyType(1);
+ info.observesAddresses = true;
+ return info;
}
vector<Value*> Memcmp::operands() const {
@@ -3385,7 +3384,6 @@ StateValue Memcmp::toSMT(State &s) const {
s.addUB(p2.isDereferenceable(vnum, 1, false));
expr zero = expr::mkUInt(0, 32);
- auto &vn = vnum;
expr result_var, result_var_neg;
if (is_bcmp) {
@@ -3406,30 +3404,41 @@ StateValue Memcmp::toSMT(State &s) const {
auto ith_exec =
[&, this](unsigned i, bool is_last) -> tuple<expr, expr, AndExpr, expr> {
- auto [val1, ub1] = s.getMemory().load((p1 + i)(), IntType("i8", 8), 1);
- auto [val2, ub2] = s.getMemory().load((p2 + i)(), IntType("i8", 8), 1);
-
- AndExpr ub_and;
- ub_and.add(move(ub1));
- ub_and.add(move(ub2));
+ assert(bits_byte == 8); // TODO: remove constraint
+ auto val1 = s.getMemory().raw_load(p1 + i);
+ auto val2 = s.getMemory().raw_load(p2 + i);
+ expr is_ptr1 = val1.isPtr();
+ expr is_ptr2 = val2.isPtr();
expr result_neq;
if (is_bcmp) {
result_neq = result_var;
} else {
- auto pos = val1.value.uge(val2.value);
+ expr pos
+ = mkIf_fold(is_ptr1,
+ val1.ptr().getAddress().uge(val2.ptr().getAddress()),
+ val1.nonptrValue().uge(val2.nonptrValue()));
result_neq = expr::mkIf(pos, result_var, result_var_neg);
}
- auto val_eq = val1.value == val2.value;
+ // allow null <-> 0 comparison
+ expr val_eq =
+ (is_ptr1 == is_ptr2 &&
+ mkIf_fold(is_ptr1,
+ val1.ptr().getAddress() == val2.ptr().getAddress(),
+ val1.nonptrValue() == val2.nonptrValue())) ||
+ (val1.isZero() && val2.isZero());
+
+ expr np
+ = (is_ptr1 == is_ptr2 || val1.isZero() || val2.isZero()) &&
+ !val1.isPoison() && !val2.isPoison();
+
return { expr::mkIf(val_eq, zero, result_neq),
- val1.non_poison && val2.non_poison,
- move(ub_and),
- val_eq && vn.uge(i + 2) };
+ move(np), {},
+ val_eq && vnum.uge(i + 2) };
};
auto [val, np, ub]
= LoopLikeFunctionApproximator(ith_exec).encode(s, memcmp_unroll_cnt);
- s.addUB((vnum != 0).implies(move(ub)));
return { expr::mkIf(vnum == 0, zero, move(val)), (vnum != 0).implies(np) };
}

MODIFY
ir/instr.h
ir/instr.h
@@ -452,6 +452,7 @@ public:
bool hasIntByteAccess = false;
bool doesPtrLoad = false;
bool doesPtrStore = false;
+ bool observesAddresses = false;
// The maximum size of a byte that this instruction can support.
// If zero, this instruction does not read/write bytes.

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -381,7 +381,7 @@ ostream& operator<<(ostream &os, const Byte &byte) {
}
bool Memory::observesAddresses() {
- return has_ptr2int || has_int2ptr;
+ return observes_addresses;
}
int Memory::isInitialMemBlock(const expr &e, bool match_any_init) {
@@ -1658,10 +1658,15 @@ Memory::load(const expr &p, const Type &type, unsigned align) {
return { state->rewriteUndef(move(ret), undef_vars), move(ubs) };
}
-Byte Memory::load(const Pointer &p, set<expr> &undef) {
+Byte Memory::raw_load(const Pointer &p, set<expr> &undef) {
return move(load(p, bits_byte / 8, undef, 1)[0]);
}
+Byte Memory::raw_load(const Pointer &p) {
+ set<expr> undef;
+ return { *this, state->rewriteUndef(raw_load(p, undef)(), undef) };
+}
+
void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
unsigned align, const set<expr> &undef_vars,
bool deref_check) {
@@ -1725,7 +1730,7 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
= expr::mkFreshVar("#off", expr::mkUInt(0, Pointer::bitsShortOffset()));
Pointer ptr_src = src + (offset - dst.getShortOffset());
set<expr> undef;
- auto val = load(ptr_src, undef);
+ auto val = raw_load(ptr_src, undef);
storeLambda(dst, offset, bytesize, move(val)(), undef, align_dst);
}
}

MODIFY
ir/memory.h
ir/memory.h
@@ -273,7 +273,8 @@ public:
load(const smt::expr &ptr, const Type &type, unsigned align);
// raw load; NB: no UB check
- Byte load(const Pointer &p, std::set<smt::expr> &undef_vars);
+ Byte raw_load(const Pointer &p, std::set<smt::expr> &undef_vars);
+ Byte raw_load(const Pointer &p);
void memset(const smt::expr &ptr, const StateValue &val,
const smt::expr &bytesize, unsigned align,

MODIFY
ir/state.cpp
ir/state.cpp
@@ -906,6 +906,10 @@ StateValue State::rewriteUndef(StateValue &&val, const set<expr> &undef_vars) {
return val.subst(repls);
}
+expr State::rewriteUndef(expr &&val, const set<expr> &undef_vars) {
+ return rewriteUndef({move(val), expr()}, undef_vars).value;
+}
+
void State::finishInitializer() {
is_initialization_phase = false;
}

MODIFY
ir/state.h
ir/state.h
@@ -223,6 +223,8 @@ public:
StateValue rewriteUndef(StateValue &&val,
const std::set<smt::expr> &undef_vars);
+ smt::expr rewriteUndef(smt::expr &&val,
+ const std::set<smt::expr> &undef_vars);
bool isInitializationPhase() const { return is_initialization_phase; }
void finishInitializer();

MODIFY
tests/alive-tv/opt-memory/ptrcmp-null-negative.ident.ll
tests/alive-tv/opt-memory/ptrcmp-null-negative.ident.ll
@@ -5,4 +5,4 @@ define i1 @f(i8* %p) {
ret i1 %c
}
-; CHECK: has_ptr2int: 1
+; CHECK: observes_addresses: 1

MODIFY
tests/alive-tv/opt-memory/ptrcmp-null.ident.ll
tests/alive-tv/opt-memory/ptrcmp-null.ident.ll
@@ -6,4 +6,4 @@ define i1 @f(i8* %p) {
}
; CHECK: use_provenance
-; CHECK: has_ptr2int: 0
+; CHECK: observes_addresses: 0

MODIFY
tests/alive-tv/opt-memory/ptrcmp-null2.ident.ll
tests/alive-tv/opt-memory/ptrcmp-null2.ident.ll
@@ -6,4 +6,4 @@ define i1 @f(i8* %p) {
}
; CHECK: use_provenance
-; CHECK: has_ptr2int: 0
+; CHECK: observes_addresses: 0

MODIFY
tests/alive-tv/opt-memory/ptrcmp-sameorigin.ident.ll
tests/alive-tv/opt-memory/ptrcmp-sameorigin.ident.ll
@@ -7,4 +7,4 @@ define i1 @f(i8* %p) {
}
; CHECK: use_provenance
-; CHECK: has_ptr2int: 0
+; CHECK: observes_addresses: 0

MODIFY
tests/alive-tv/opt-memory/ptrcmp-sameorigin2.ident.ll
tests/alive-tv/opt-memory/ptrcmp-sameorigin2.ident.ll
@@ -7,4 +7,4 @@ define i1 @f(i8* %p) {
}
; CHECK: use_provenance
-; CHECK: has_ptr2int: 0
+; CHECK: observes_addresses: 0

MODIFY
tests/alive-tv/opt-memory/ptrcmp-sameorigin3.ident.ll
tests/alive-tv/opt-memory/ptrcmp-sameorigin3.ident.ll
@@ -7,4 +7,4 @@ define i1 @f(i8* %p, i64 %i, i64 %j) {
}
; CHECK: offsetonly
-; CHECK: has_ptr2int: 0
+; CHECK: observes_addresses: 0

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -527,8 +527,8 @@ check_refinement(Errors &errs, const Transform &t, const State &src_state,
set<expr> undef;
Pointer p(src_mem, m[ptr_refinement()]);
s << "\nMismatch in " << p
- << "\nSource value: " << Byte(src_mem, m[src_mem.load(p, undef)()])
- << "\nTarget value: " << Byte(tgt_mem, m[tgt_mem.load(p, undef)()]);
+ << "\nSource value: " << Byte(src_mem, m[src_mem.raw_load(p, undef)()])
+ << "\nTarget value: " << Byte(tgt_mem, m[tgt_mem.raw_load(p, undef)()]);
};
CHECK(dom && !(memory_cnstr0.isTrue() ? memory_cnstr0
@@ -789,8 +789,8 @@ static void calculateAndInitConstants(Transform &t) {
uint64_t min_global_size = UINT64_MAX;
bool nullptr_is_used = false;
- has_int2ptr = false;
- has_ptr2int = false;
+ bool has_int2ptr = false;
+ bool has_ptr2int = false;
has_alloca = false;
has_dead_allocas = false;
has_malloc = false;
@@ -800,6 +800,7 @@ static void calculateAndInitConstants(Transform &t) {
does_ptr_store = false;
does_ptr_mem_access = false;
does_int_mem_access = false;
+ observes_addresses = false;
bool does_any_byte_access = false;
// Mininum access size (in bytes)
@@ -877,6 +878,7 @@ static void calculateAndInitConstants(Transform &t) {
does_ptr_store |= info.doesPtrStore;
does_int_mem_access |= info.hasIntByteAccess;
does_mem_access |= info.doesMemAccess();
+ observes_addresses |= info.observesAddresses;
min_access_size = gcd(min_access_size, info.byteSize);
if (info.doesMemAccess() && !info.hasIntByteAccess &&
!info.doesPtrLoad && !info.doesPtrStore)
@@ -902,8 +904,8 @@ static void calculateAndInitConstants(Transform &t) {
min_access_size = gcd(min_access_size, getCommonAccessSize(t));
} else if (auto *ic = dynamic_cast<const ICmp*>(&i)) {
- has_ptr2int |= ic->isPtrCmp() &&
- (ic->getPtrCmpMode() == ICmp::INTEGRAL);
+ observes_addresses |= ic->isPtrCmp() &&
+ ic->getPtrCmpMode() == ICmp::INTEGRAL;
}
}
}
@@ -944,6 +946,8 @@ static void calculateAndInitConstants(Transform &t) {
num_nonlocals = num_nonlocals_src + num_globals - num_globals_src;
+ observes_addresses |= has_int2ptr || has_ptr2int;
+
if (!does_int_mem_access && !does_ptr_mem_access && has_fncall)
does_int_mem_access = true;
@@ -1025,8 +1029,7 @@ static void calculateAndInitConstants(Transform &t) {
<< "\nmemcmp_unroll_cnt: " << memcmp_unroll_cnt
<< "\nlittle_endian: " << little_endian
<< "\nnullptr_is_used: " << nullptr_is_used
- << "\nhas_int2ptr: " << has_int2ptr
- << "\nhas_ptr2int: " << has_ptr2int
+ << "\nobserves_addresses: " << observes_addresses
<< "\nhas_malloc: " << has_malloc
<< "\nhas_free: " << has_free
<< "\nhas_null_block: " << has_null_block

add pointer comparison support for memcmp (#444)