gep inbounds: simplify pointer value, not just np constraint
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1977,7 +1977,7 @@ StateValue GEP::toSMT(State &s) const {
non_poison.add(ptrval.non_poison);
if (inbounds)
- non_poison.add(ptr.inbounds());
+ non_poison.add(ptr.inbounds(true));
for (auto &[sz, idx] : offsets) {
auto &[v, np] = idx;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -494,11 +494,24 @@ static expr inbounds(const Pointer &p) {
return p.get_offset_sizet().ule(p.block_size());
}
-expr Pointer::inbounds() const {
- DisjointExpr<expr> ret(expr(false));
+expr Pointer::inbounds(bool simplify_ptr) {
+ if (!simplify_ptr)
+ return ::inbounds(*this);
+
+ DisjointExpr<expr> ret(expr(false)), all_ptrs;
for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, true, true)) {
- ret.add(::inbounds(Pointer(m, ptr_expr)), domain);
+ expr inb = ::inbounds(Pointer(m, ptr_expr));
+ if (!inb.isFalse())
+ all_ptrs.add(ptr_expr, domain);
+ ret.add(move(inb), domain);
}
+
+ // trim set of valid ptrs
+ if (auto ptrs = all_ptrs())
+ p = *ptrs;
+ else
+ p = expr::mkUInt(0, total_bits());
+
return *ret();
}

MODIFY
ir/memory.h
ir/memory.h
@@ -142,7 +142,7 @@ public:
StateValue uge(const Pointer &rhs) const;
StateValue ugt(const Pointer &rhs) const;
- smt::expr inbounds() const;
+ smt::expr inbounds(bool simplify_ptr = false);
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;

gep inbounds: simplify pointer value, not just np constraint