opt calloc -> memset call
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2322,9 +2322,9 @@ StateValue Calloc::toSMT(State &s) const {
auto [p, allocated] = s.getMemory().alloc(size, align, Memory::MALLOC,
np && nm.mul_no_uoverflow(sz),
nonnull);
+ p = p.subst(allocated, true).simplify();
- 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 }, size, align, {}, false);
return { move(p), move(np) };
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1580,11 +1580,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, const set<expr> &undef_vars0) {
+ unsigned align, const set<expr> &undef_vars0,
+ bool deref_check) {
assert(!memory_unused());
assert(!val.isValid() || val.bits() == 8);
unsigned bytesz = bits_byte / 8;
Pointer ptr(*this, p);
+ if (deref_check)
state->addUB(ptr.isDereferenceable(bytesize, align, true));
undef_vars.insert(undef_vars0.begin(), undef_vars0.end());

MODIFY
ir/memory.h
ir/memory.h
@@ -297,7 +297,7 @@ public:
void memset(const smt::expr &ptr, const StateValue &val,
const smt::expr &bytesize, unsigned align,
- const std::set<smt::expr> &undef_vars);
+ const std::set<smt::expr> &undef_vars, bool deref_check = true);
void memcpy(const smt::expr &dst, const smt::expr &src,
const smt::expr &bytesize, unsigned align_dst, unsigned align_src,
bool move);

opt calloc -> memset call