add support for noalias function calls
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -728,8 +728,8 @@ bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
if (auto algn = (local ? local_blk_align : non_local_blk_align).lookup(bid)) {
int64_t offset = 0;
uint64_t blk_align;
- ENSURE(algn->isUInt(blk_align));
- if (align > (1ull << blk_align) &&
+ if (algn->isUInt(blk_align) &&
+ align > (1ull << blk_align) &&
(!observesAddresses() || offset0.isInt(offset)))
return false;
}
@@ -1241,8 +1241,55 @@ expr Memory::PtrInput::operator==(const PtrInput &rhs) const {
return val == rhs.val;
}
-expr Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
+Memory::FnRetData Memory::FnRetData::mkIf(const expr &cond, const FnRetData &a,
+ const FnRetData &b) {
+ return { expr::mkIf(cond, a.size, b.size),
+ expr::mkIf(cond, a.align, b.align),
+ expr::mkIf(cond, a.var, b.var) };
+}
+
+pair<expr,Memory::FnRetData>
+Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs,
+ bool is_local, const FnRetData *data) {
assert(has_fncall);
+
+ // can return local block or null (on address space 0 only FIXME)
+ if (is_local) {
+ auto bid = next_local_bid++;
+ assert(bid < numLocals());
+
+ expr size = data ? data->size
+ : expr::mkFreshVar((name + string("#size")).c_str(),
+ expr::mkUInt(0, bits_size_t-1)).zext(1);
+ expr align = data ? data->align
+ : expr::mkFreshVar((name + string("#align")).c_str(),
+ expr::mkUInt(0, 6));
+
+ expr var
+ = data ? data->var
+ : expr::mkFreshVar(name, expr::mkUInt(0, 2 + bits_for_offset));
+ auto is_null = var.extract(0, 0) == 0;
+ auto alloc_ty = var.extract(1, 1);
+ auto offset = var.extract(bits_for_offset+2-1, 2);
+ auto allocated = !is_null;
+
+ auto p_bid = expr::mkUInt(bid, Pointer::bitsShortBid());
+ p_bid = Pointer::mkLongBid(p_bid, true);
+ Pointer ptr(*this, p_bid, offset);
+
+ auto short_bid = ptr.getShortBid();
+ mkLocalDisjAddrAxioms(allocated, short_bid, size, align, 0);
+ store_bv(ptr, allocated, local_block_liveness, non_local_block_liveness);
+ local_blk_size.add(short_bid, expr(size));
+ local_blk_align.add(short_bid, expr(align));
+
+ assert((Pointer::MALLOC & 2) == 2 && (Pointer::CXX_NEW & 2) == 2);
+ local_blk_kind.add(short_bid, expr::mkUInt(1, 1).concat(alloc_ty));
+
+ return { expr::mkIf(is_null, Pointer::mkNullPointer(*this)(), ptr()),
+ { move(size), move(align), move(var) } };
+ }
+
bool has_local = hasEscapedLocals();
unsigned bits_bid = has_local ? bits_for_bid : Pointer::bitsShortBid();
@@ -1268,7 +1315,7 @@ expr Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
ptr_alias.emplace(p.getBid(), move(alias));
state->addAxiom(expr::mkIf(p.isLocal(), local, nonlocal));
- return p.release();
+ return { p.release(), {} };
}
Memory::CallState Memory::CallState::mkIf(const expr &cond,
@@ -1389,6 +1436,46 @@ static expr disjoint_local_blocks(const Memory &m, const expr &addr,
return disj;
}
+void Memory::mkLocalDisjAddrAxioms(const expr &allocated, const expr &short_bid,
+ const expr &size, const expr &align,
+ unsigned align_bits) {
+ if (!observesAddresses())
+ return;
+
+ unsigned var_bw = bits_ptr_address - align_bits - Pointer::hasLocalBit();
+ auto addr_var = expr::mkFreshVar("local_addr", expr::mkUInt(0, var_bw));
+ state->addQuantVar(addr_var);
+
+ expr blk_addr = addr_var.concat_zeros(align_bits);
+ expr full_addr = Pointer::hasLocalBit()
+ ? expr::mkUInt(1, 1).concat(blk_addr) : blk_addr;
+
+ if (align_bits == 0) {
+ auto shift = expr::mkUInt(bits_ptr_address, full_addr) -
+ align.zextOrTrunc(bits_ptr_address);
+ state->addPre((full_addr << shift) == 0);
+ }
+
+ // addr + size only overflows for one case when obj is aligned
+ expr no_ovfl;
+ if (size.ule(align.zextOrTrunc(bits_size_t)).isTrue())
+ no_ovfl = addr_var != expr::mkInt(-1, addr_var);
+ else
+ no_ovfl
+ = blk_addr.add_no_uoverflow(
+ size.zextOrTrunc(bits_ptr_address - Pointer::hasLocalBit()));
+ state->addPre(allocated.implies(no_ovfl));
+
+ // Disjointness of block's address range with other local blocks
+ state->addPre(
+ allocated.implies(
+ disjoint_local_blocks(*this, full_addr,
+ size.zextOrTrunc(bits_ptr_address),
+ align, local_blk_addr)));
+
+ local_blk_addr.add(short_bid, move(blk_addr));
+}
+
pair<expr, expr>
Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
const expr &precond, const expr &nonnull,
@@ -1436,34 +1523,8 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
bool is_null = !is_local && has_null_block && bid == 0;
if (is_local) {
- if (observesAddresses()) {
- unsigned var_bw = bits_ptr_address - align_bits - Pointer::hasLocalBit();
- auto addr_var = expr::mkFreshVar("local_addr", expr::mkUInt(0, var_bw));
- state->addQuantVar(addr_var);
-
- expr blk_addr = addr_var.concat_zeros(align_bits);
- expr full_addr = Pointer::hasLocalBit()
- ? expr::mkUInt(1, 1).concat(blk_addr) : blk_addr;
-
- // addr + size only overflows for one case when obj is aligned
- expr no_ovfl;
- if (size.ule(align).isTrue())
- no_ovfl = addr_var != expr::mkInt(-1, addr_var);
- else
- no_ovfl
- = blk_addr.add_no_uoverflow(
- size_zext.zextOrTrunc(bits_ptr_address - Pointer::hasLocalBit()));
- state->addPre(allocated.implies(no_ovfl));
-
- // Disjointness of block's address range with other local blocks
- state->addPre(
- allocated.implies(
- disjoint_local_blocks(*this, full_addr,
- size_zext.zextOrTrunc(bits_ptr_address),
- align_expr, local_blk_addr)));
-
- local_blk_addr.add(short_bid, move(blk_addr));
- }
+ mkLocalDisjAddrAxioms(allocated, short_bid, size_zext, align_expr,
+ align_bits);
} else {
state->addAxiom(p.blockSize() == size_zext);
state->addAxiom(p.isBlockAligned(align, true));

MODIFY
ir/memory.h
ir/memory.h
@@ -201,6 +201,11 @@ class Memory {
smt::expr blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid,
std::set<smt::expr> &undef) const;
+ void mkLocalDisjAddrAxioms(const smt::expr &allocated,
+ const smt::expr &short_bid,
+ const smt::expr &size, const smt::expr &align,
+ unsigned align_bits);
+
public:
enum BlockKind {
MALLOC, CXX_NEW, STACK, GLOBAL, CONSTGLOBAL
@@ -242,7 +247,19 @@ public:
auto operator<=>(const PtrInput &rhs) const = default;
};
- smt::expr mkFnRet(const char *name, const std::vector<PtrInput> &ptr_inputs);
+ struct FnRetData {
+ smt::expr size;
+ smt::expr align;
+ smt::expr var;
+
+ static FnRetData mkIf(const smt::expr &cond, const FnRetData &a,
+ const FnRetData &b);
+ auto operator<=>(const FnRetData &rhs) const = default;
+ };
+
+ std::pair<smt::expr,FnRetData>
+ mkFnRet(const char *name, const std::vector<PtrInput> &ptr_inputs,
+ bool is_local, const FnRetData *data = nullptr);
CallState mkCallState(const std::string &fnname,
const std::vector<PtrInput> *ptr_inputs, bool nofree);
void setState(const CallState &st);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -729,6 +729,8 @@ State::FnCallOutput State::FnCallOutput::mkIf(const expr &cond,
for (unsigned i = 0, e = a.retvals.size(); i != e; ++i) {
ret.retvals.emplace_back(
StateValue::mkIf(cond, a.retvals[i], b.retvals[i]));
+ ret.ret_data.emplace_back(
+ Memory::FnRetData::mkIf(cond, a.ret_data[i], b.ret_data[i]));
}
return ret;
}
@@ -753,6 +755,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
bool noret = attrs.has(FnAttrs::NoReturn);
bool willret = attrs.has(FnAttrs::WillReturn);
bool noundef = attrs.has(FnAttrs::NoUndef);
+ bool noalias = attrs.has(FnAttrs::NoAlias);
assert(!noret || !willret);
@@ -790,32 +793,36 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
if (inserted) {
auto mk_val = [&](const Type &t, const string &name) {
- return t.isPtrType()
- ? memory.mkFnRet(name.c_str(), I->first.args_ptr)
- : expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
+ if (t.isPtrType())
+ return memory.mkFnRet(name.c_str(), I->first.args_ptr, noalias);
+
+ return make_pair(
+ expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value),
+ Memory::FnRetData());
};
vector<StateValue> values;
+ vector<Memory::FnRetData> ret_data;
string valname = name + "#val";
string npname = name + "#np";
for (auto t : out_types) {
+ auto [val, data] = mk_val(*t, valname);
values.emplace_back(
- mk_val(*t, valname),
+ move(val),
noundef ? expr(true) : expr::mkFreshVar(npname.c_str(), false));
+ ret_data.emplace_back(move(data));
}
- string ub_name = name + "#ub";
- string noret_name = name + "#noreturn";
I->second
- = { move(values), expr::mkFreshVar(ub_name.c_str(), false),
+ = { move(values), expr::mkFreshVar((name + "#ub").c_str(), false),
(noret || willret)
? expr(noret)
- : expr::mkFreshVar(noret_name.c_str(), false),
+ : expr::mkFreshVar((name + "#noreturn").c_str(), false),
writes_memory
? memory.mkCallState(name,
argmemonly ? &I->first.args_ptr : nullptr,
attrs.has(FnAttrs::NoFree))
- : Memory::CallState() };
+ : Memory::CallState(), move(ret_data) };
// add equality constraints between source's function calls
for (auto II = calls_fn.begin(), E = calls_fn.end(); II != E; ++II) {
@@ -849,7 +856,23 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
addUB(move(domain));
addUB(move(d.ub));
addNoReturn(move(d.noreturns));
+
+ if (noalias) {
+ // no alias functions in tgt must allocate a local block on each call
+ // bid may be different from that of src
+ unsigned i = 0;
+ for (auto t : out_types) {
+ retval.emplace_back(
+ t->isPtrType()
+ ? StateValue(memory.mkFnRet(name.c_str(), ptr_inputs, noalias,
+ &d.ret_data[i]).first,
+ move(d.retvals[i].non_poison))
+ : move(d.retvals[i]));
+ ++i;
+ }
+ } else
retval = move(d.retvals);
+
if (writes_memory)
memory.setState(d.callstate);

MODIFY
ir/state.h
ir/state.h
@@ -158,6 +158,7 @@ private:
smt::expr ub;
smt::expr noreturns;
Memory::CallState callstate;
+ std::vector<Memory::FnRetData> ret_data;
static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then,
const FnCallOutput &els);

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -1174,6 +1174,7 @@ public:
continue;
switch (llvmattr.getKindAsEnum()) {
+ case llvm::Attribute::NoAlias: attrs.set(FnAttrs::NoAlias); break;
case llvm::Attribute::NonNull: attrs.set(FnAttrs::NonNull); break;
case llvm::Attribute::NoUndef: attrs.set(FnAttrs::NoUndef); break;

ADD
tests/alive-tv/attrs/noalias-fn.srctgt.ll
+define i8 @src() {
+ %p = call i8* @alloc()
+ store i8 3, i8* %p
+ call void @xpto()
+ %r = load i8, i8* %p
+ ret i8 %r
+}
+
+define i8 @tgt() {
+ %p = call i8* @alloc()
+ store i8 3, i8* %p
+ call void @xpto()
+ ret i8 3
+}
+
+declare noalias i8* @alloc()
+declare void @xpto()

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -562,10 +562,13 @@ static unsigned num_ptrs(const Type &ty) {
}
static bool returns_local(const Value &v) {
+ // no alias fns return local block
+ if (auto call = dynamic_cast<const FnCall*>(&v))
+ return call->getAttributes().has(FnAttrs::NoAlias);
+
return dynamic_cast<const Alloc*>(&v) ||
dynamic_cast<const Malloc*>(&v) ||
dynamic_cast<const Calloc*>(&v);
- // TODO: add noalias fn
}
static Value *get_base_ptr(Value *ptr) {

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -54,8 +54,12 @@ void sym_exec(State &s) {
auto &[val, ub, uvars] = s.exec(i);
auto &name = i.getName();
- if (config::symexec_print_each_value && name[0] == '%')
- dbg() << name << " = " << val << " / UB=" << ub << '\n';
+ if (config::symexec_print_each_value) {
+ dbg() << name;
+ if (name[0] == '%')
+ dbg() << " = " << val << " /";
+ dbg() << " UB=" << ub << '\n';
+ }
}
first = false;

add support for noalias function calls