Skip to content

Commit

Permalink
Add initial support for physical pointers and int2ptr casts (#988)
Browse files Browse the repository at this point in the history
  • Loading branch information
@nunoplopes
nunoplopes authored Sep 6, 2024
1 parent 68e0b98 commit 582f881
Show file tree
Hide file tree
Showing 14 changed files with 448 additions and 242 deletions.
1 change: 1 addition & 0 deletions ir/globals.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ unsigned strlen_unroll_cnt = 8;
unsigned memcmp_unroll_cnt = 8;
bool little_endian = true;
bool observes_addresses = true;
bool has_int2ptr = true;
bool has_alloca = true;
bool has_fncall = true;
bool has_write_fncall = true;
Expand Down
1 change: 1 addition & 0 deletions ir/globals.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@ extern bool little_endian;

/// Whether pointer addresses are observed
extern bool observes_addresses;
extern bool has_int2ptr;

/// Whether there is an alloca
extern bool has_alloca;
Expand Down
1 change: 1 addition & 0 deletions ir/instr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3803,6 +3803,7 @@ StateValue GEP::toSMT(State &s) const {
AndExpr inbounds_np;
AndExpr idx_all_zeros;

// FIXME: not implemented for physical pointers
if (inbounds)
inbounds_np.add(ptr.inbounds());

Expand Down
174 changes: 40 additions & 134 deletions ir/memory.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -441,7 +441,7 @@ expr Byte::refined(const Byte &other) const {
if (asm_mode) {
extra = !is_ptr2 &&
other.boolNonptrNonpoison() &&
castPtrToInt() == v2;
castPtrToInt() == other.nonptrValue();
}
ptr_cnstr = ptrNonpoison().implies(
(other.ptrNonpoison() &&
Expand Down Expand Up @@ -869,19 +869,15 @@ weak_ordering Memory::MemBlock::operator<=>(const MemBlock &rhs) const {
static set<Pointer> all_leaf_ptrs(const Memory &m, const expr &ptr) {
set<Pointer> ptrs;
for (auto &ptr_val : ptr.leafs()) {
Pointer p(m, ptr_val);
auto offset = p.getOffset();
for (auto &bid : p.getBid().leafs()) {
ptrs.emplace(m, bid, offset);
}
ptrs.emplace(m, ptr_val);
}
return ptrs;
}

static set<expr> extract_possible_local_bids(Memory &m, const expr &eptr) {
set<expr> ret;
for (auto &ptr : all_leaf_ptrs(m, eptr)) {
if (!ptr.isLocal().isFalse())
if (!ptr.isLocal().isFalse() && !ptr.isLogical().isFalse())
ret.emplace(ptr.getShortBid());
}
return ret;
Expand All @@ -906,13 +902,17 @@ unsigned Memory::numNonlocals() const {
}

expr Memory::isBlockAlive(const expr &bid, bool local) const {
uint64_t bid_n;
if (!local && bid.isUInt(bid_n) && always_alive(bid_n))
return true;

return
load_bv(local ? local_block_liveness : non_local_block_liveness, bid) &&
(!local && has_null_block && !null_is_dereferenceable ? bid != 0 : true);
}

bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
unsigned bytes, uint64_t align, bool write) const {
const expr &bytes, uint64_t align, bool write) const {
if (local && bid0 >= next_local_bid)
return false;

Expand Down Expand Up @@ -969,19 +969,14 @@ bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
} else if (local) // allocated in another branch
return false;

if (local || !always_alive(bid0)) {
if ((local ? local_block_liveness : non_local_block_liveness)
.extract(bid0, bid0).isZero())
return false;
}
if (isBlockAlive(bid, local).isFalse())
return false;

return true;
}

Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, unsigned bytes,
Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, const expr &bytes,
uint64_t align, bool write) const {
assert(bytes % (bits_byte/8) == 0);

AliasSet aliasing(*this);
auto sz_local = next_local_bid;
auto sz_nonlocal = aliasing.size(false);
Expand All @@ -1004,7 +999,7 @@ Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, unsigned bytes,
AliasSet this_alias = aliasing;
auto is_local = p.isLocal();
auto shortbid = p.getShortBid();
expr offset = p.getOffset();
expr offset = p.getOffset();
uint64_t bid;
if (shortbid.isUInt(bid) && (!isAsmMode() || p.isInbounds(true).isTrue())) {
if (!is_local.isFalse() && bid < sz_local)
Expand Down Expand Up @@ -1054,9 +1049,10 @@ Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, unsigned bytes,
return aliasing;
}

void Memory::access(const Pointer &ptr, unsigned bytes, uint64_t align,
void Memory::access(const Pointer &ptr, const expr &bytes, uint64_t align,
bool write, const
function<void(MemBlock&, const Pointer&, expr&&)> &fn) {
assert(!ptr.isLogical().isFalse());
auto aliasing = computeAliasing(ptr, bytes, align, write);
unsigned has_local = aliasing.numMayAlias(true);
unsigned has_nonlocal = aliasing.numMayAlias(false);
Expand All @@ -1072,25 +1068,17 @@ void Memory::access(const Pointer &ptr, unsigned bytes, uint64_t align,
auto sz_local = aliasing.size(true);
auto sz_nonlocal = aliasing.size(false);

#define call_fn(block, local, cond_log) \
Pointer this_ptr(*this, i, local); \
fn(block, this_ptr + offset, is_singleton ? expr(true) : (cond_log));

for (unsigned i = 0; i < sz_local; ++i) {
if (!aliasing.mayAlias(true, i))
continue;

Pointer this_ptr(*this, i, true);
expr cond_eq;

if (isAsmMode() && !ptr.isInbounds(true).isTrue()) {
// in asm mode, all pointers have full provenance
cond_eq = ptr.isInboundsOf(this_ptr, bytes);
this_ptr += addr - this_ptr.getAddress();
} else {
auto n = expr::mkUInt(i, Pointer::bitsShortBid());
cond_eq
= has_local == 1 ? is_local : (bid == (has_both ? one.concat(n) : n));
this_ptr += offset;
}

fn(local_block_val[i], ptr, is_singleton ? expr(true) : std::move(cond_eq));
auto n = expr::mkUInt(i, Pointer::bitsShortBid());
call_fn(local_block_val[i], true,
has_local == 1 ? is_local : (bid == (has_both ? one.concat(n) : n)))
}

for (unsigned i = 0; i < sz_nonlocal; ++i) {
Expand All @@ -1102,20 +1090,9 @@ void Memory::access(const Pointer &ptr, unsigned bytes, uint64_t align,
// If aliasing info says it can, either imprecise analysis or incorrect
// block id encoding is happening.
assert(!is_fncall_mem(i));
Pointer this_ptr(*this, i, false);
expr cond_eq;

if (isAsmMode() && !ptr.isInbounds(true).isTrue()) {
// in asm mode, all pointers have full provenance
cond_eq = ptr.isInboundsOf(this_ptr, bytes);
this_ptr += addr - this_ptr.getAddress();
} else {
cond_eq = has_nonlocal == 1 ? !is_local : bid == i;
this_ptr += offset;
}

fn(non_local_block_val[i], this_ptr,
is_singleton ? expr(true) : std::move(cond_eq));
call_fn(non_local_block_val[i], false,
has_nonlocal == 1 ? !is_local : bid == i)
}
}

Expand Down Expand Up @@ -1169,7 +1146,7 @@ vector<Byte> Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
}
};

access(ptr, bytes, align, false, fn);
access(ptr, expr::mkUInt(bytes, bits_size_t), align, false, fn);

vector<Byte> ret;
for (auto &disj : loaded) {
Expand Down Expand Up @@ -1261,7 +1238,8 @@ void Memory::store(const Pointer &ptr,
blk.undef.insert(undef.begin(), undef.end());
};

access(ptr, bytes, align, !state->isInitializationPhase(), fn);
access(ptr, expr::mkUInt(bytes, bits_size_t), align,
!state->isInitializationPhase(), fn);
}

void Memory::storeLambda(const Pointer &ptr, const expr &offset,
Expand Down Expand Up @@ -1309,10 +1287,7 @@ void Memory::storeLambda(const Pointer &ptr, const expr &offset,
blk.undef.insert(undef.begin(), undef.end());
};

uint64_t size = bits_byte / 8;
bytes.isUInt(size);

access(ptr, size, align, true, fn);
access(ptr, bytes.zextOrTrunc(bits_size_t), align, true, fn);
}

static bool memory_unused() {
Expand Down Expand Up @@ -1640,6 +1615,9 @@ expr Memory::mkInput(const char *name, const ParamAttrs &attrs0) {
unsigned max_bid = has_null_block + num_globals_src + next_ptr_input++;
assert(max_bid < num_nonlocals_src);

// FIXME: doesn't consider physical ptrs
// consider how to do POR?

auto attrs = attrs0;
attrs.set(ParamAttrs::IsArg);
Pointer p(*this, name, attrs);
Expand Down Expand Up @@ -2395,7 +2373,7 @@ void Memory::copy(const Pointer &src, const Pointer &dst) {
dst_blk.type |= blk.type;
has_bv_val |= 1u << blk.val.isBV();
};
access(src, bits_byte/8, bits_byte/8, false, fn);
access(src, expr::mkUInt(bits_byte/8, bits_size_t), bits_byte/8, false, fn);

// if we have mixed array/non-array blocks, switch them all to array
if (has_bv_val == 3) {
Expand All @@ -2415,93 +2393,18 @@ void Memory::fillPoison(const expr &bid) {
std::move(blksz), bits_byte / 8, {}, false);
}

expr Memory::ptr2int(const expr &ptr) const {
expr Memory::ptr2int(const expr &ptr) {
assert(!memory_unused() && observesAddresses());
Pointer p(*this, ptr);
observesAddr(p);
state->addUB(!p.isNocapture());
return p.getAddress();
}

Pointer Memory::searchPointer(const expr &val0) const {
DisjointExpr<Pointer> ret;
expr val = val0.zextOrTrunc(bits_ptr_address);

auto add = [&](unsigned limit, bool local) {
for (unsigned i = 0; i != limit; ++i) {
Pointer p(*this, i, local);
Pointer p_end = p + p.blockSize();
ret.add(p + (val - p.getAddress()),
!local && i == 0 && has_null_block
? val == 0
: val.uge(p.getAddress()) && val.ult(p_end.getAddress()));
}
};
add(numLocals(), true);
add(numNonlocals(), false);
return *std::move(ret)();
}

expr Memory::int2ptr(const expr &val0) const {
expr Memory::int2ptr(const expr &val) const {
assert(!memory_unused() && observesAddresses());
if (isAsmMode()) {
DisjointExpr<expr> ret(Pointer::mkNullPointer(*this).release());
expr val = val0;
OrExpr domain;
bool processed_all = true;

// Try to optimize the conversion
// Note that the result of int2ptr is always used to dereference the ptr
// Hence we can throw away null & OOB pointers
// Also, these pointers must have originated from ptr->int type punning
// so they must have a (blk_addr bid) expression in them (+ some offset)
for (auto [e, cond] : DisjointExpr<expr>(val, 5)) {
auto blks = e.get_apps_of("blk_addr", "local_addr!");
if (blks.empty()) {
expr subst = false;
if (cond.isNot(cond))
subst = true;
val = val.subst(cond, subst);
continue;
}
// There's only one possible bid in this expression
if (blks.size() == 1) {
auto &fn = *blks.begin();
expr bid;
if (fn.fn_name().starts_with("local_addr!")) {
for (auto &[bid0, addr] : local_blk_addr) {
auto blks = addr.get_apps_of("blk_addr", "local_addr!");
assert(blks.size() == 1);
if (blks.begin()->eq(fn)) {
bid = Pointer::mkLongBid(bid0, true);
break;
}
}
} else {
// non-local block
assert(fn.fn_name() == "blk_addr");
bid = Pointer::mkLongBid(fn.getFnArg(0), false);
}
assert(bid.isValid());
Pointer base(*this, bid, expr::mkUInt(0, bits_for_offset));
expr offset = (e - base.getAddress()).sextOrTrunc(bits_for_offset);
ret.add(Pointer(*this, bid, offset).release(), cond);
} else {
processed_all = false;
}
domain.add(std::move(cond));
}
state->addUB(std::move(domain)());

if (processed_all)
return std::move(ret)()->simplify();

return searchPointer(val.simplify()).release();
}

expr null = Pointer::mkNullPointer(*this).release();
expr fn = expr::mkUF("int2ptr", { val0 }, null);
state->doesApproximation("inttoptr", fn);
return expr::mkIf(val0 == 0, null, fn);
return
Pointer::mkPhysical(*this, val.zextOrTrunc(bits_ptr_address)).release();
}

expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
Expand Down Expand Up @@ -2599,12 +2502,15 @@ Memory::refined(const Memory &other, bool fncall,

AliasSet block_alias(*this, other);
auto min_read_sz = bits_byte / 8;
expr min_read_sz_expr = expr::mkUInt(min_read_sz, bits_size_t);

auto sets = { make_pair(this, set_ptrs), make_pair(&other, set_ptrs2) };
for (const auto &[mem, set] : sets) {
if (set) {
for (auto &it: *set_ptrs) {
block_alias.unionWith(computeAliasing(Pointer(*mem, it.val.value),
min_read_sz, min_read_sz, false));
min_read_sz_expr, min_read_sz,
false));
}
} else {
if (mem->next_nonlocal_bid > 0)
Expand Down
12 changes: 6 additions & 6 deletions ir/memory.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,12 +191,13 @@ class Memory {
void mkNonlocalValAxioms(bool skip_consts) const;

bool mayalias(bool local, unsigned bid, const smt::expr &offset,
unsigned bytes, uint64_t align, bool write) const;
const smt::expr &bytes, uint64_t align, bool write) const;

AliasSet computeAliasing(const Pointer &ptr, unsigned bytes, uint64_t align,
bool write) const;
AliasSet computeAliasing(const Pointer &ptr, const smt::expr &bytes,
uint64_t align, bool write) const;

void access(const Pointer &ptr, unsigned btyes, uint64_t align, bool write,
void access(const Pointer &ptr, const smt::expr &bytes, uint64_t align,
bool write,
const std::function<void(MemBlock&, const Pointer&,
smt::expr&&)> &fn);

Expand Down Expand Up @@ -353,9 +354,8 @@ class Memory {

void fillPoison(const smt::expr &bid);

smt::expr ptr2int(const smt::expr &ptr) const;
smt::expr ptr2int(const smt::expr &ptr);
smt::expr int2ptr(const smt::expr &val) const;
Pointer searchPointer(const smt::expr &val) const;

std::tuple<smt::expr, Pointer, std::set<smt::expr>>
refined(const Memory &other, bool fncall,
Expand Down
Loading

0 comments on commit 582f881

Please sign in to comment.