implement argmemonly in function calls
fixes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1690,14 +1690,42 @@ void FnCall::print(ostream &os) const {
os << ')' << attrs;
}
+static void eq_bids(OrExpr &acc, Memory &m, const Type &t,
+ const StateValue &val, const expr &bid) {
+ if (auto agg = t.getAsAggregateType()) {
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ eq_bids(acc, m, agg->getChild(i), agg->extract(val, i), bid);
+ }
+ return;
+ }
+
+ if (t.isPtrType()) {
+ acc.add(val.non_poison && Pointer(m, val.value).getBid() == bid);
+ }
+}
+
+static expr ptr_only_args(State &s, const Pointer &p) {
+ expr bid = p.getBid();
+ auto &m = s.getMemory();
+
+ OrExpr e;
+ for (auto &in : s.getFn().getInputs()) {
+ if (hasPtr(in.getType()))
+ eq_bids(e, m, in.getType(), s[in], bid);
+ }
+ return e();
+}
+
static void unpack_inputs(State &s, Value &argv, Type &ty,
- const ParamAttrs &argflag, StateValue value,
- StateValue value2, vector<StateValue> &inputs,
+ const ParamAttrs &argflag, bool argmemonly,
+ StateValue value, StateValue value2,
+ vector<StateValue> &inputs,
vector<Memory::PtrInput> &ptr_inputs) {
if (auto agg = ty.getAsAggregateType()) {
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
- unpack_inputs(s, argv, agg->getChild(i), argflag, agg->extract(value, i),
- agg->extract(value2, i), inputs, ptr_inputs);
+ unpack_inputs(s, argv, agg->getChild(i), argflag, argmemonly,
+ agg->extract(value, i), agg->extract(value2, i), inputs,
+ ptr_inputs);
}
return;
}
@@ -1708,6 +1736,10 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
value.non_poison = move(new_non_poison);
if (ty.isPtrType()) {
+ if (argmemonly)
+ value.non_poison
+ &= ptr_only_args(s, Pointer(s.getMemory(), value.value));
+
ptr_inputs.emplace_back(move(value),
argflag.blockSize,
argflag.has(ParamAttrs::NoCapture));
@@ -1768,6 +1800,7 @@ StateValue FnCall::toSMT(State &s) const {
vector<StateValue> inputs;
vector<Memory::PtrInput> ptr_inputs;
vector<Type*> out_types;
+ bool argmemonly = attrs.has(FnAttrs::ArgMemOnly);
ostringstream fnName_mangled;
fnName_mangled << fnName;
@@ -1786,8 +1819,8 @@ StateValue FnCall::toSMT(State &s) const {
sv2 = s[*arg];
}
- unpack_inputs(s, *arg, arg->getType(), flags, move(sv), move(sv2), inputs,
- ptr_inputs);
+ unpack_inputs(s, *arg, arg->getType(), flags, argmemonly, move(sv),
+ move(sv2), inputs, ptr_inputs);
fnName_mangled << '#' << arg->getType();
}
fnName_mangled << '!' << getType();
@@ -1795,7 +1828,7 @@ StateValue FnCall::toSMT(State &s) const {
unpack_ret_ty(out_types, getType());
auto check_access = [&]() {
- if (attrs.has(FnAttrs::ArgMemOnly)) {
+ if (argmemonly) {
for (auto &p : ptr_inputs) {
if (!p.byval) {
Pointer ptr(s.getMemory(), p.val.value);
@@ -1822,7 +1855,8 @@ StateValue FnCall::toSMT(State &s) const {
return s.getFn().getFnAttrs().has(attr) && !attrs.has(attr);
};
- if (check(FnAttrs::NoFree) ||
+ if (check(FnAttrs::ArgMemOnly) ||
+ check(FnAttrs::NoFree) ||
check(FnAttrs::NoThrow) ||
check(FnAttrs::WillReturn))
s.addUB(expr(false));
@@ -2560,32 +2594,6 @@ MemInstr::ByteAccessInfo MemInstr::ByteAccessInfo::full(unsigned byteSize) {
}
-static void eq_bids(OrExpr &acc, Memory &m, const Type &t,
- const StateValue &val, const expr &bid) {
- if (auto agg = t.getAsAggregateType()) {
- for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
- eq_bids(acc, m, agg->getChild(i), agg->extract(val, i), bid);
- }
- return;
- }
-
- if (t.isPtrType()) {
- acc.add(val.non_poison && Pointer(m, val.value).getBid() == bid);
- }
-}
-
-static expr ptr_only_args(State &s, const Pointer &p) {
- expr bid = p.getBid();
- auto &m = s.getMemory();
-
- OrExpr e;
- for (auto &in : s.getFn().getInputs()) {
- if (hasPtr(in.getType()))
- eq_bids(e, m, in.getType(), s[in], bid);
- }
- return e();
-}
-
static void check_can_load(State &s, const expr &p0) {
auto &attrs = s.getFn().getFnAttrs();
Pointer p(s.getMemory(), p0);

ADD
tests/alive-tv/attrs/argmemonly-poison.srctgt.ll
+@glb = external global i8
+
+define void @src(i8 *%p) argmemonly {
+ load i8, i8* %p
+ %c = icmp eq i8* %p, @glb
+ br i1 %c, label %true, label %false
+
+true:
+ br label %end
+
+false:
+ call void @f(i8* @glb)
+ br label %end
+
+end:
+ ret void
+}
+
+define void @tgt(i8 *%p) argmemonly {
+ %c = icmp eq i8* %p, @glb
+ br i1 %c, label %true, label %false
+
+true:
+ br label %end
+
+false:
+ call void @f(i8* poison)
+ br label %end
+
+end:
+ ret void
+}
+
+declare void @f(i8*) argmemonly

ADD
tests/alive-tv/attrs/argmemonly-ub.srctgt.ll
+@glb = external global i8
+
+define void @src(i8 *%p) argmemonly {
+ call void @f(i8* %p)
+ ret void
+}
+
+define void @tgt(i8 *%p) argmemonly {
+ unreachable
+}
+
+declare void @f(i8*)

ADD
tests/alive-tv/attrs/argmemonly.srctgt.ll
+define i8 @src(i8 *%p) argmemonly {
+ %p2 = getelementptr i8, i8* %p, i32 0
+ %v = call i8 @f(i8* %p2)
+ ret i8 %v
+}
+
+define i8 @tgt(i8 *%p) argmemonly {
+ %v = call i8 @f(i8* %p)
+ ret i8 %v
+}
+
+declare i8 @f(i8*) argmemonly

implement argmemonly in function calls
fixes #670