memory: exploit operations that ensure that pointers are aligned
to index memory using zeroed offsets. This enables us to do more store forwarding
e.g. (p aligned to 4) cannot alias (q aligned to 4) + 1
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -584,7 +584,7 @@ expr Pointer::isBlockAligned(unsigned align, bool exact) const {
return exact ? blk_align == bits : blk_align.uge(bits);
}
-expr Pointer::isAligned(unsigned align) const {
+expr Pointer::isAligned(unsigned align) {
assert(align >= bits_byte / 8);
if (align == 1)
return true;
@@ -597,16 +597,24 @@ expr Pointer::isAligned(unsigned align) const {
expr blk_align = isBlockAligned(align);
- if (!observes_addresses() || blk_align.isConst())
+ if (!observes_addresses() || blk_align.isConst()) {
// This is stricter than checking getAddress(), but as addresses are not
// observed, program shouldn't be able to distinguish this from checking
// getAddress()
- return blk_align && offset.extract(bits - 1, 0) == 0;
+ auto zero = expr::mkUInt(0, bits);
+ auto newp = p.extract(totalBits() - 1, bits_for_ptrattrs + bits)
+ .concat(zero);
+ if (bits_for_ptrattrs)
+ newp = newp.concat(getAttrs());
+ p = move(newp);
+ assert(!p.isValid() || p.bits() == totalBits());
+ return { blk_align && offset.extract(bits - 1, 0) == zero };
+ }
return getAddress().extract(bits - 1, 0) == 0;
}
-static pair<expr, expr> is_dereferenceable(const Pointer &p,
+static pair<expr, expr> is_dereferenceable(Pointer &p,
const expr &bytes_off,
const expr &bytes,
unsigned align, bool iswrite) {
@@ -646,7 +654,7 @@ AndExpr Pointer::isDereferenceable(const expr &bytes0, unsigned align,
// record pointer if not definitely unfeasible
if (!ub.isFalse() && !aligned.isFalse() && !ptr.blockSize().isZero())
- all_ptrs.add(ptr_expr, domain);
+ all_ptrs.add(ptr.release(), domain);
UB.add(move(ub), domain);
is_aligned.add(move(aligned), domain);

MODIFY
ir/memory.h
ir/memory.h
@@ -151,7 +151,7 @@ public:
smt::expr inbounds(bool simplify_ptr = false, bool strict = false);
smt::expr blockAlignment() const; // log(bits)
smt::expr isBlockAligned(unsigned align, bool exact = false) const;
- smt::expr isAligned(unsigned align) const;
+ smt::expr isAligned(unsigned align);
smt::AndExpr isDereferenceable(unsigned bytes, unsigned align = bits_byte / 8,
bool iswrite = false);
smt::AndExpr isDereferenceable(const smt::expr &bytes, unsigned align,

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -539,6 +539,14 @@ expr expr::unop_fold(Z3_ast(*op)(Z3_context, Z3_ast)) const {
z3app)
expr expr::operator+(const expr &rhs) const {
+ expr a, b;
+ // (concat x const) + rhs -> (concat const+rhs) if no overflow happens
+ if (rhs.isConst() && isConcat(a, b) && b.isConst()) {
+ auto rhs2 = rhs.trunc(b.bits());
+ if (rhs2.zextOrTrunc(rhs.bits()).eq(rhs) &&
+ b.add_no_uoverflow(rhs2).isTrue())
+ return a.concat(b + rhs2);
+ }
return binopc(Z3_mk_bvadd, operator+, Z3_OP_BADD, isZero, alwaysFalse);
}
@@ -1343,11 +1351,16 @@ expr expr::zextOrTrunc(unsigned tobw) const {
}
expr expr::concat(const expr &rhs) const {
- expr a, b;
+ expr a, b, c, d;
unsigned h, l, h2, l2;
- if (isExtract(a, h, l) && rhs.isExtract(b, h2, l2) && a.eq(b) && l == h2+1)
+ if (isExtract(a, h, l)) {
+ if (rhs.isExtract(b, h2, l2) && l == h2+1 && a.eq(b))
return a.extract(h, l2);
+ // extract_l concat (concat extract_r foo)
+ if (rhs.isConcat(b, c) && b.isExtract(d, h2, l2) && l == h2+1 && a.eq(d))
+ return a.extract(h, l2).concat(c);
+ }
return binop_fold(rhs, Z3_mk_concat);
}

memory: exploit operations that ensure that pointers are aligned
to index memory using zeroed offsets. This enables us to do more store forwarding
e.g. (p aligned to 4) cannot alias (q aligned to 4) + 1