improvements to refinement check of argmemonly function calls
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1802,7 +1802,8 @@ StateValue FnCall::toSMT(State &s) const {
vector<StateValue> inputs;
vector<Memory::PtrInput> ptr_inputs;
vector<Type*> out_types;
- bool argmemonly = s.getFn().getFnAttrs().has(FnAttrs::ArgMemOnly);
+ bool argmemonly_fn = s.getFn().getFnAttrs().has(FnAttrs::ArgMemOnly);
+ bool argmemonly_call = hasAttribute(FnAttrs::ArgMemOnly);
ostringstream fnName_mangled;
fnName_mangled << fnName;
@@ -1821,7 +1822,7 @@ StateValue FnCall::toSMT(State &s) const {
sv2 = s[*arg];
}
- unpack_inputs(s, *arg, arg->getType(), flags, argmemonly, move(sv),
+ unpack_inputs(s, *arg, arg->getType(), flags, argmemonly_fn, move(sv),
move(sv2), inputs, ptr_inputs);
fnName_mangled << '#' << arg->getType();
}
@@ -1829,12 +1830,20 @@ StateValue FnCall::toSMT(State &s) const {
if (!isVoid())
unpack_ret_ty(out_types, getType());
- auto check_access = [&]() {
- if (argmemonly) {
+ auto check = [&](FnAttrs::Attribute attr) {
+ return s.getFn().getFnAttrs().has(attr) && !hasAttribute(attr);
+ };
+
+ auto check_implies = [&](FnAttrs::Attribute attr) {
+ if (!check(attr))
+ return;
+
+ if (argmemonly_call) {
for (auto &p : ptr_inputs) {
if (!p.byval) {
Pointer ptr(s.getMemory(), p.val.value);
- s.addUB(p.val.non_poison.implies(ptr.isLocal()));
+ s.addUB(p.val.non_poison.implies(
+ ptr.isLocal() || ptr.isConstGlobal()));
}
}
} else {
@@ -1842,23 +1851,12 @@ StateValue FnCall::toSMT(State &s) const {
}
};
- if (!attrs.has(FnAttrs::NoRead)) {
- if (s.getFn().getFnAttrs().has(FnAttrs::NoRead))
- check_access();
- }
-
- if (!attrs.has(FnAttrs::NoWrite)) {
- if (s.getFn().getFnAttrs().has(FnAttrs::NoWrite))
- check_access();
- }
+ check_implies(FnAttrs::NoRead);
+ check_implies(FnAttrs::NoWrite);
+ check_implies(FnAttrs::NoFree);
// Check attributes that calles must have if caller has them
- auto check = [&](FnAttrs::Attribute attr) {
- return s.getFn().getFnAttrs().has(attr) && !attrs.has(attr);
- };
-
if (check(FnAttrs::ArgMemOnly) ||
- check(FnAttrs::NoFree) ||
check(FnAttrs::NoThrow) ||
check(FnAttrs::WillReturn) ||
check(FnAttrs::InaccessibleMemOnly))

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1355,8 +1355,8 @@ expr Memory::CallState::operator==(const CallState &rhs) const {
}
Memory::CallState
-Memory::mkCallState(const string &fnname, const vector<PtrInput> *ptr_inputs,
- bool nofree, bool inaccessiblememonly) {
+Memory::mkCallState(const string &fnname, bool nofree,
+ bool inaccessiblememonly) {
assert(has_fncall);
CallState st;
st.empty = false;
@@ -1364,36 +1364,71 @@ Memory::mkCallState(const string &fnname, const vector<PtrInput> *ptr_inputs,
// TODO: handle havoc of local blocks
auto blk_type = mk_block_val_array(1);
- unsigned num_consts = has_null_block + num_consts_src;
- unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns;
if (inaccessiblememonly) {
st.non_local_block_val.emplace_back(expr::mkFreshVar("blk_val", blk_type));
} else {
+ unsigned num_consts = has_null_block + num_consts_src;
+ unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns;
for (unsigned i = num_consts; i < limit; ++i) {
st.non_local_block_val.emplace_back(
expr::mkFreshVar("blk_val", blk_type));
}
}
- // TODO: this code should be moved to setState as old_val should be the one
- // from the corresponding state, not always from source
- if (ptr_inputs) {
+ st.non_local_liveness = mk_liveness_array();
+ if (num_nonlocals_src && !nofree && !inaccessiblememonly)
+ st.non_local_liveness
+ = expr::mkFreshVar("blk_liveness", st.non_local_liveness);
+
+ return st;
+}
+
+void Memory::setState(const Memory::CallState &st,
+ const vector<PtrInput> *ptr_inputs,
+ unsigned modifies_bid) {
+ assert(has_fncall);
+
+ unsigned num_consts = has_null_block + num_consts_src;
+ unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns;
+
+ // 1) Havoc memory
+
+ // inaccessibleonly fncall
+ if (modifies_bid != -1u) {
+ assert(st.non_local_block_val.size() == 1);
+ unsigned bid
+ = num_nonlocals_src - num_inaccessiblememonly_fns + modifies_bid;
+ assert(bid < num_nonlocals_src);
+ assert(non_local_block_val[bid].undef.empty());
+ non_local_block_val[bid].val = st.non_local_block_val[0];
+ }
+ // argmemonly fncall
+ else if (ptr_inputs) {
for (unsigned bid = num_consts; bid < limit - has_write_fncall; ++bid) {
expr modifies(false);
for (auto &ptr_in : *ptr_inputs) {
if (!ptr_in.byval && bid < next_nonlocal_bid) {
- modifies |= Pointer(*this, ptr_in.val.value).getBid() == bid;
+ modifies |= ptr_in.val.non_poison &&
+ Pointer(*this, ptr_in.val.value).getBid() == bid;
}
}
auto &new_val = st.non_local_block_val[bid - num_consts];
- auto &old_val = non_local_block_val[bid].val;
- new_val = expr::mkIf(modifies, new_val, old_val);
+ auto &cur_val = non_local_block_val[bid].val;
+ cur_val = expr::mkIf(modifies, new_val, cur_val);
+ if (modifies.isTrue())
+ non_local_block_val[bid].undef.clear();
+ }
+ // generic fncall
+ } else {
+ for (unsigned bid = num_consts; bid < limit; ++bid) {
+ non_local_block_val[bid].val = st.non_local_block_val[bid - num_consts];
+ non_local_block_val[bid].undef.clear();
}
}
- if (num_nonlocals_src && !nofree && !inaccessiblememonly) {
+ if (!st.non_local_liveness.isAllOnes()) {
expr one = expr::mkUInt(1, num_nonlocals);
expr zero = expr::mkUInt(0, num_nonlocals);
expr mask = has_null_block ? one : zero;
@@ -1403,48 +1438,21 @@ Memory::mkCallState(const string &fnname, const vector<PtrInput> *ptr_inputs,
may_free = false;
for (auto &ptr_in : *ptr_inputs) {
if (!ptr_in.byval && bid < next_nonlocal_bid)
- may_free |= Pointer(*this, ptr_in.val.value).getBid() == bid;
+ may_free |= ptr_in.val.non_poison &&
+ Pointer(*this, ptr_in.val.value).getBid() == bid;
}
}
expr heap = Pointer(*this, bid, false).isHeapAllocated();
mask = mask | expr::mkIf(heap && may_free && !is_fncall_mem(bid),
zero,
- one << expr::mkUInt(bid, num_nonlocals));
+ one << expr::mkUInt(bid, one));
}
- if (mask.isAllOnes()) {
- st.non_local_liveness = non_local_block_liveness;
- } else {
- auto liveness_var = expr::mkFreshVar("blk_liveness", mk_liveness_array());
// functions can free an object, but cannot bring a dead one back to live
- st.non_local_liveness = non_local_block_liveness & (liveness_var | mask);
- }
- } else {
- st.non_local_liveness = non_local_block_liveness;
- }
- return st;
+ non_local_block_liveness
+ = non_local_block_liveness & (st.non_local_liveness | mask);
}
-void Memory::setState(const Memory::CallState &st, unsigned modifies_bid) {
- assert(has_fncall);
- if (modifies_bid != -1u) {
- assert(st.non_local_block_val.size() == 1);
- unsigned bid
- = num_nonlocals_src - num_inaccessiblememonly_fns + modifies_bid;
- assert(bid < num_nonlocals_src);
- assert(non_local_block_val[bid].undef.empty());
- non_local_block_val[bid].val = st.non_local_block_val[0];
- } else {
- auto consts = has_null_block + num_consts_src;
- unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns;
- for (unsigned i = consts; i < limit; ++i) {
- non_local_block_val[i].val = st.non_local_block_val[i - consts];
- if (isInitialMemBlock(non_local_block_val[i].val, true))
- non_local_block_val[i].undef.clear();
- }
- // TODO: this is not ok for functions that can be reordered
- non_local_block_liveness = st.non_local_liveness;
- }
mkNonlocalValAxioms(true);
}

MODIFY
ir/memory.h
ir/memory.h
@@ -260,10 +260,10 @@ public:
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,
+ CallState mkCallState(const std::string &fnname, bool nofree,
bool inaccessiblememonly);
- void setState(const CallState &st, unsigned modifies_bid);
+ void setState(const CallState &st, const std::vector<PtrInput> *ptr_inputs,
+ unsigned modifies_bid);
// Allocates a new memory block and returns (pointer expr, allocated).
// If bid is not specified, it creates a fresh block id by increasing

MODIFY
ir/state.cpp
ir/state.cpp
@@ -54,13 +54,13 @@ void State::ValueAnalysis::meet_with(const State::ValueAnalysis &other) {
}
void State::ValueAnalysis::FnCallRanges::inc(const std::string &name,
- bool inaccessiblememonly) {
+ bool inaccessible_or_args_memonly) {
auto [I, inserted] = try_emplace(name);
if (inserted) {
I->second.first.emplace(1);
- I->second.second = inaccessiblememonly;
+ I->second.second = inaccessible_or_args_memonly;
} else {
- assert(I->second.second == inaccessiblememonly);
+ assert(I->second.second == inaccessible_or_args_memonly);
set<unsigned> new_set;
for (unsigned n : I->second.first) {
new_set.emplace(n+1);
@@ -822,7 +822,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
.first->second;
State::ValueAnalysis::FnCallRanges call_ranges;
- if (reads_memory)
+ if (reads_memory && !argmemonly)
call_ranges = inaccessiblememonly
? analysis.ranges_fn_calls.project(name)
: analysis.ranges_fn_calls;
@@ -867,7 +867,6 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
: expr::mkFreshVar((name + "#noreturn").c_str(), false),
writes_memory
? memory.mkCallState(name,
- argmemonly ? &I->first.args_ptr : nullptr,
attrs.has(FnAttrs::NoFree),
inaccessiblememonly)
: Memory::CallState(), move(ret_data) };
@@ -886,7 +885,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
addNoReturn(I->second.noreturns);
retval = I->second.retvals;
if (writes_memory)
- memory.setState(I->second.callstate, modifies_bid);
+ memory.setState(I->second.callstate,
+ argmemonly ? &I->first.args_ptr : nullptr,
+ modifies_bid);
}
else {
// target: this fn call must match one from the source, otherwise it's UB
@@ -922,7 +923,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
retval = move(d.retvals);
if (writes_memory)
- memory.setState(d.callstate, modifies_bid);
+ memory.setState(d.callstate,
+ argmemonly ? &ptr_inputs : nullptr,
+ modifies_bid);
fn_call_pre &= pre;
if (qvar.isValid())
@@ -936,7 +939,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
}
if (writes_memory)
- analysis.ranges_fn_calls.inc(name, inaccessiblememonly);
+ analysis.ranges_fn_calls.inc(name, argmemonly | inaccessiblememonly);
return retval;
}

MODIFY
ir/state.h
ir/state.h
@@ -52,9 +52,9 @@ private:
// Possible number of calls per function name that occurred so far
// This is an over-approximation, union over all predecessors
struct FnCallRanges
- // bool records whether fn only accesses inaccessible memory only
+ // bool records whether fn only accesses inaccessible/args memory only
: public std::map<std::string, std::pair<std::set<unsigned>, bool>> {
- void inc(const std::string &name, bool inaccessiblememonly);
+ void inc(const std::string &name, bool inaccessible_or_args_memonly);
bool overlaps(const FnCallRanges &other) const;
// remove all ranges but name
FnCallRanges project(const std::string &name) const;

ADD
tests/alive-tv/attrs/argmemonly2.srctgt.ll
+@x = constant i8 0
+@y = constant i8 1
+
+define void @src() {
+ call void @f(i8* @x)
+ call void @f(i8* @y)
+ ret void
+}
+
+define void @tgt() {
+ call void @f(i8* @y)
+ call void @f(i8* @x)
+ ret void
+}
+
+declare void @f(i8*) argmemonly willreturn

ADD
tests/alive-tv/attrs/argmemonly3.srctgt.ll
+@x = constant i8 0
+
+define void @src() {
+ call void @f(i8* @x)
+ ret void
+}
+
+define void @tgt() readnone {
+ call void @f(i8* @x)
+ ret void
+}
+
+declare void @f(i8*) argmemonly

improvements to refinement check of argmemonly function calls