memory: attempt to shrink number of bits for offset whenever GEPs are constant and addresses aren't observed
MODIFY
ir/instr.cpp
ir/instr.cpp
#include <functional>
using namespace smt;
+using namespace util;
using namespace std;
#define RAUW(val) \
@@ -1920,11 +1921,13 @@ StateValue GEP::toSMT(State &s) const {
for (auto &[sz, idx] : offsets) {
auto &[v, np] = idx;
+ assert(ilog2_ceil(sz) <= bits_for_offset);
auto multiplier = expr::mkUInt(sz, bits_for_offset);
auto val = v.sextOrTrunc(bits_for_offset);
auto inc = multiplier * val;
if (inbounds) {
+ non_poison &= val.sextOrTrunc(v.bits()) == v;
non_poison &= multiplier.mul_no_soverflow(val);
non_poison &= ptr.add_no_overflow(inc);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -472,6 +472,7 @@ public:
void addIdx(unsigned obj_size, Value &idx);
Value* getPtr() const { return ptr; }
+ auto& getIdxs() const { return idxs; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -350,8 +350,11 @@ expr Pointer::get_short_bid() const {
}
expr Pointer::get_offset() const {
- return p.extract(bits_for_offset + bits_for_ptrattrs - 1, bits_for_ptrattrs)
- .sextOrTrunc(bits_size_t);
+ return p.extract(bits_for_offset + bits_for_ptrattrs - 1, bits_for_ptrattrs);
+}
+
+expr Pointer::get_offset_sizet() const {
+ return get_offset().sextOrTrunc(bits_size_t);
}
expr Pointer::get_attrs() const {
@@ -395,7 +398,7 @@ expr Pointer::get_address(bool simplify) const {
else
addr = move(non_local);
- return addr + get_offset();
+ return addr + get_offset_sizet();
}
expr Pointer::block_size() const {
@@ -412,8 +415,7 @@ expr Pointer::short_ptr() const {
}
Pointer Pointer::operator+(const expr &bytes) const {
- expr off = (get_offset() + bytes.zextOrTrunc(bits_size_t));
- return { m, get_bid(), off.trunc(bits_for_offset),
+ return { m, get_bid(), get_offset() + bytes.zextOrTrunc(bits_for_offset),
bits_for_ptrattrs ? get_attrs() : expr() };
}
@@ -456,7 +458,7 @@ DEFINE_CMP(ugt)
expr Pointer::inbounds() const {
// equivalent to offset >= 0 && offset <= block_size
// because block_size u<= 0x7FFF..
- return get_offset().ule(block_size());
+ return get_offset_sizet().ule(block_size());
}
expr Pointer::block_alignment() const {
@@ -494,7 +496,7 @@ expr Pointer::is_aligned(unsigned align) const {
static pair<expr, expr> is_dereferenceable(const Pointer &p, const expr &bytes,
unsigned align, bool iswrite) {
expr block_sz = p.block_size();
- expr offset = p.get_offset();
+ expr offset = p.get_offset_sizet();
// check that offset is within bounds and that arith doesn't overflow
expr cond = (offset + bytes).ule(block_sz);
@@ -558,9 +560,9 @@ static expr disjoint(const expr &begin1, const expr &len1, const expr &begin2,
void Pointer::is_disjoint(const expr &len1, const Pointer &ptr2,
const expr &len2) const {
m.state->addUB(get_bid() != ptr2.get_bid() ||
- disjoint(get_offset(),
+ disjoint(get_offset_sizet(),
len1.zextOrTrunc(bits_size_t),
- ptr2.get_offset(),
+ ptr2.get_offset_sizet(),
len2.zextOrTrunc(bits_size_t)));
}
@@ -616,9 +618,9 @@ expr Pointer::refined(const Pointer &other) const {
expr Pointer::fninput_refined(const Pointer &other) const {
expr size = block_size();
- expr off = get_offset();
+ expr off = get_offset_sizet();
expr size2 = other.block_size();
- expr off2 = other.get_offset();
+ expr off2 = other.get_offset_sizet();
expr local
= expr::mkIf(is_heap_allocated(),
@@ -693,7 +695,8 @@ expr Pointer::block_refined(const Pointer &other) const {
is_writable() == other.is_writable() &&
m.state->simplifyWithAxioms(
block_alignment().ule(other.block_alignment())) &&
- (is_block_alive() && get_offset().ult(blk_size)).implies(val_refines);
+ (is_block_alive() && get_offset_sizet().ult(blk_size))
+ .implies(val_refines);
}
expr Pointer::is_writable() const {

MODIFY
ir/memory.h
ir/memory.h
@@ -109,6 +109,7 @@ public:
smt::expr get_bid() const;
smt::expr get_short_bid() const; // same as get_bid but ignoring is_local bit
smt::expr get_offset() const;
+ smt::expr get_offset_sizet() const;
smt::expr get_attrs() const;
smt::expr get_address(bool simplify = true) const;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -446,6 +446,31 @@ static bool returns_nonlocal(const Instr &inst) {
return 0u;
}
+static uint64_t max_gep(const Instr &inst) {
+ if (auto conv = dynamic_cast<const ConversionOp*>(&inst)) {
+ // if addresses are observed, then expose full ptr range
+ if (conv->getOp() == ConversionOp::Int2Ptr ||
+ conv->getOp() == ConversionOp::Ptr2Int)
+ return UINT64_MAX;
+ }
+
+ if (auto gep = dynamic_cast<const GEP*>(&inst)) {
+ int64_t off = 0;
+ for (auto &[mul, v] : gep->getIdxs()) {
+ if (auto i = dynamic_cast<IntConst*>(v)) {
+ if (auto n = i->getInt()) {
+ off += mul * *n;
+ continue;
+ }
+ }
+ return UINT64_MAX;
+ }
+ return abs(off);
+ }
+
+ return 0;
+}
+
static void calculateAndInitConstants(Transform &t) {
const auto &globals_tgt = t.tgt.getGlobalVars();
const auto &globals_src = t.src.getGlobalVars();
@@ -505,6 +530,7 @@ static void calculateAndInitConstants(Transform &t) {
num_max_nonlocals_inst = 0;
// The number of local blocks.
unsigned num_locals_src = 0, num_locals_tgt = 0;
+ uint64_t max_gep_src = 0, max_gep_tgt = 0;
for (auto BB : t.src.getBBs()) {
for (auto &i : BB->instrs()) {
@@ -512,6 +538,7 @@ static void calculateAndInitConstants(Transform &t) {
++num_locals_src;
else
num_max_nonlocals_inst += returns_nonlocal(i);
+ max_gep_src = add_saturate(max_gep_src, max_gep(i));
}
}
for (auto BB : t.tgt.getBBs()) {
@@ -520,6 +547,7 @@ static void calculateAndInitConstants(Transform &t) {
++num_locals_tgt;
else
num_max_nonlocals_inst += returns_nonlocal(i);
+ max_gep_tgt = add_saturate(max_gep_tgt, max_gep(i));
}
}
num_locals = max(num_locals_src, num_locals_tgt);
@@ -592,8 +620,12 @@ static void calculateAndInitConstants(Transform &t) {
bits_for_bid = max(1u, ilog2_ceil(max(num_locals, num_nonlocals)))
+ (num_locals && num_nonlocals);
- // TODO
- bits_for_offset = 64;
+ // reserve a multiple of 4 for the number of offset bits to make SMT &
+ // counterexamples more readable
+ // Allow an extra bit for the sign, and another for power-of-2 cases
+ // e.g. gep(p, 8) -> log(8)=3, but +8 = 01000 (5 bits)
+ auto max_geps = ilog2_ceil(max(max_gep_src, max_gep_tgt)) + 2;
+ bits_for_offset = min(round_up(max(max_geps, 1u), 4), (uint64_t)bits_size_t);
// size of byte
bits_byte = 8 * (does_mem_access ? (unsigned)min_access_size : 1);

MODIFY
util/compiler.cpp
util/compiler.cpp
@@ -62,10 +62,19 @@ unsigned num_trailing_zeros(uint64_t n) {
#endif
}
+uint64_t add_saturate(uint64_t a, uint64_t b) {
+ auto res = a + b;
+ return (res >= a && res >= b) ? res : UINT64_MAX;
+}
+
uint64_t divide_up(uint64_t n, uint64_t amount) {
return (n + amount - 1) / amount;
}
+uint64_t round_up(uint64_t n, uint64_t amount) {
+ return divide_up(n, amount) * amount;
+}
+
uint64_t gcd(uint64_t n, uint64_t m) {
assert(n != 0 || m != 0);
if (n < m) return gcd(m, n);

MODIFY
util/compiler.h
util/compiler.h
@@ -49,6 +49,9 @@ unsigned num_sign_bits(uint64_t n);
unsigned num_leading_zeros(uint64_t n);
unsigned num_trailing_zeros(uint64_t n);
+uint64_t add_saturate(uint64_t a, uint64_t b);
+
uint64_t divide_up(uint64_t n, uint64_t amount); // division with ceiling
+uint64_t round_up(uint64_t n, uint64_t amount);
uint64_t gcd(uint64_t a, uint64_t b);
}

memory: attempt to shrink number of bits for offset whenever GEPs are constant and addresses aren't observed