Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

int2ptr support #988

Merged
merged 4 commits into from
Sep 6, 2024
Merged

int2ptr support #988

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
06d67f5
int2ptr support
nunoplopes Aug 14, 2024
8f3b127
fix crash
nunoplopes Sep 4, 2024
7cc3831
fix crash
nunoplopes Sep 4, 2024
60f61d6
optimize the toLogical() function which is only needed for local addrs
nunoplopes Sep 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions ir/globals.cpp
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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