fix encoding of dereferenceable attrs
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -181,7 +181,8 @@ static expr
encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
uint64_t derefOrNullBytes, uint64_t align, bool nonnull,
bool nocapture, const expr &deref_expr) {
- Pointer p(s.getMemory(), ptrvalue);
+ auto &m = s.getMemory();
+ Pointer p(m, ptrvalue);
expr non_poison(true);
if (nonnull)
@@ -192,13 +193,17 @@ encodePtrAttrs(State &s, const expr &ptrvalue, uint64_t derefBytes,
if (derefBytes || derefOrNullBytes || deref_expr.isValid()) {
// dereferenceable, byval (ParamAttrs), dereferenceable_or_null
if (derefBytes)
- s.addUB(p.isDereferenceable(derefBytes, align));
+ s.addUB(Pointer(m, ptrvalue).isDereferenceable(derefBytes, align));
if (derefOrNullBytes)
- s.addUB(p.isDereferenceable(derefOrNullBytes, align)() || p.isNull());
+ s.addUB(
+ Pointer(m, ptrvalue).isDereferenceable(derefOrNullBytes, align)() ||
+ p.isNull());
if (deref_expr.isValid())
- s.addUB(p.isDereferenceable(deref_expr, align, false)() || p.isNull());
+ s.addUB(
+ Pointer(m, ptrvalue).isDereferenceable(deref_expr, align, false)() ||
+ p.isNull());
} else if (align > 1)
- non_poison &= p.isAligned(align);
+ non_poison &= Pointer(m, ptrvalue).isAligned(align);
// TODO: handle alloc align

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2309,7 +2309,8 @@ StateValue FnCall::toSMT(State &s) const {
if (attrs.has(AllocKind::Alloc) || attrs.has(AllocKind::Realloc)) {
auto [size, np_size] = attrs.computeAllocSize(s, args);
- expr nonnull = expr::mkBoolVar("malloc_never_fails");
+ expr nonnull = attrs.isNonNull() ? expr(true)
+ : expr::mkBoolVar("malloc_never_fails");
// FIXME: alloc-family below
auto [p_new, allocated]
= m.alloc(size, getAlign(), Memory::MALLOC, np_size, nonnull);
@@ -2317,12 +2318,7 @@ StateValue FnCall::toSMT(State &s) const {
expr nullp = Pointer::mkNullPointer(m)();
expr ret = expr::mkIf(allocated, p_new, nullp);
- if (attrs.isNonNull()) {
// TODO: In C++ we need to throw an exception if the allocation fails.
- s.addPre(std::move(allocated));
- allocated = true;
- ret = p_new;
- }
if (attrs.has(AllocKind::Realloc)) {
auto &[allocptr, np_ptr] = s.getAndAddUndefs(get_alloc_ptr());

MODIFY
ir/pointer.h
ir/pointer.h
@@ -85,11 +85,14 @@ public:
smt::expr inbounds(bool simplify_ptr = false, bool strict = false);
smt::expr blockAlignment() const; // log(bits)
smt::expr isBlockAligned(uint64_t align, bool exact = false) const;
+
+ // WARNING: these modify the pointer in place
smt::expr isAligned(uint64_t align);
smt::AndExpr isDereferenceable(uint64_t bytes, uint64_t align,
bool iswrite = false);
smt::AndExpr isDereferenceable(const smt::expr &bytes, uint64_t align,
bool iswrite);
+
void isDisjointOrEqual(const smt::expr &len1, const Pointer &ptr2,
const smt::expr &len2) const;
smt::expr isBlockAlive() const;

fix encoding of dereferenceable attrs