Add support for nocapture arg attribute
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1640,8 +1640,47 @@ void Return::print(ostream &os) const {
os << val->getName();
}
+static void addUBForNoCaptureRet(State &s, const vector<expr> &nonpoisons,
+ const vector<expr> &bids, const StateValue &svret, const Type &t) {
+ auto &[vret, npret] = svret;
+ if (t.isPtrType()) {
+ for (unsigned i = 0, e = nonpoisons.size(); i != e; ++i) {
+ s.addUB((nonpoisons[i] && npret).implies(
+ Pointer(s.getMemory(), vret).get_bid() != bids[i]));
+ }
+ return;
+ }
+
+ if (auto agg = t.getAsAggregateType()) {
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ addUBForNoCaptureRet(s, nonpoisons, bids, agg->extract(svret, i),
+ agg->getChild(i));
+ }
+ }
+}
+
StateValue Return::toSMT(State &s) const {
- s.addReturn(s[*val]);
+ // Encode nocapture semantics.
+ vector<expr> nonpoisons;
+ vector<expr> bids;
+ for (const auto &I: s.getFn().getInputs()) {
+ auto inp = dynamic_cast<const Input *>(&I);
+ if (!inp->getType().isPtrType() ||
+ !inp->hasAttribute(Input::NoCapture))
+ continue;
+
+ auto &[v1, np1] = s[I];
+ auto bid = Pointer(s.getMemory(), v1).get_bid();
+ nonpoisons.emplace_back(np1);
+ bids.emplace_back(bid);
+ }
+ auto &retval = s[*val];
+ if (bids.size() != 0) {
+ addUBForNoCaptureRet(s, nonpoisons, bids, retval, val->getType());
+ s.addUB(s.getMemory().has_noptrbyte(nonpoisons, bids));
+ }
+ s.addReturn(retval);
+
return {};
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1233,6 +1233,26 @@ pair<expr,Pointer> Memory::refined(const Memory &other) const {
move(ptr) };
}
+expr Memory::has_noptrbyte(const vector<expr> &conds,
+ const vector<expr> &bids) const {
+ assert(conds.size() != 0 && conds.size() == bids.size());
+ expr res(true);
+ auto ofs = expr::mkFreshVar("ofs", expr::mkUInt(0, bits_for_offset));
+
+ for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
+ Pointer p(*this, expr::mkUInt(bid, bits_for_bid), ofs);
+ Byte b(*this, non_local_block_val.load(p.short_ptr()));
+ Pointer loadp(*this, b.ptr_value());
+
+ expr c(true);
+ for (unsigned i = 0, e = bids.size(); i < e; ++i)
+ c &= conds[i].implies(loadp.get_bid() != bids[i]);
+ res &= p.is_block_alive().implies(
+ expr::mkForAll({ ofs }, (b.is_ptr() && b.ptr_nonpoison()).implies(c)));
+ }
+ return res;
+}
+
Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
assert(then.state == els.state);
Memory ret(then);

MODIFY
ir/memory.h
ir/memory.h
@@ -238,6 +238,11 @@ public:
std::pair<smt::expr,Pointer> refined(const Memory &other) const;
+ // Encodes existence of a pointer byte, bid of which is one of bids.
+ // If conds[i] is false, bids[i] is ignored.
+ smt::expr has_noptrbyte(const std::vector<smt::expr> &conds,
+ const std::vector<smt::expr> &bids) const;
+
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);

MODIFY
ir/value.cpp
ir/value.cpp
@@ -154,6 +154,8 @@ static string attr_str(unsigned attributes) {
string ret;
if (attributes & Input::NonNull)
ret += "nonnull ";
+ if (attributes & Input::NoCapture)
+ ret += "nocapture ";
return ret;
}

MODIFY
ir/value.h
ir/value.h
@@ -109,7 +109,7 @@ public:
class Input final : public Value {
public:
- enum Attributes { None = 0, NonNull = 1<<0 };
+ enum Attributes { None = 0, NonNull = 1<<0, NoCapture = 1<<1 };
private:
std::string smt_name;
unsigned attributes;
@@ -117,6 +117,7 @@ public:
Input(Type &type, std::string &&name, unsigned attributes = 0);
void copySMTName(const Input &other);
void print(std::ostream &os) const override;
+ bool hasAttribute(Attributes a) const { return (attributes & a) != 0; }
StateValue toSMT(State &s) const override;
smt::expr getTyVar() const;
};

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -742,6 +742,10 @@ public:
attrs |= Input::NonNull;
continue;
+ case llvm::Attribute::NoCapture:
+ attrs |= Input::NoCapture;
+ continue;
+
default:
*out << "ERROR: Unsupported attribute: " << attr.getAsString() << '\n';
return {};

ADD
tests/alive-tv/attrs/nocapture.src.ll
+@x = global i8* null
+
+define void @f1(i8* nocapture %p) {
+ store i8* %p, i8** @x
+ ret void
+}
+
+define void @f2(i8* nocapture %p0) {
+ %p = getelementptr i8, i8* %p0, i32 1
+ store i8* %p, i8** @x
+ ret void
+}
+
+define i8* @f3(i8* nocapture %p) {
+ ret i8* %p
+}
+
+define i8* @f4(i8* nocapture %p) {
+ %p2 = getelementptr i8, i8* %p, i32 1
+ ret i8* %p2
+}
+
+define <2 x i8*> @f5(i8* nocapture %p) {
+ %v = insertelement <2 x i8*> undef, i8* %p, i32 1
+ ret <2 x i8*> %v
+}
+

ADD
tests/alive-tv/attrs/nocapture.tgt.ll
+@x = global i8* null
+
+define void @f1(i8* nocapture %p) {
+ %poison = getelementptr inbounds i8, i8* null, i64 1
+ store i8* %poison, i8** @x
+ ret void
+}
+
+define void @f2(i8* nocapture %p) {
+ %poison = getelementptr inbounds i8, i8* null, i64 1
+ store i8* %poison, i8** @x
+ ret void
+}
+
+define i8* @f3(i8* nocapture %p) {
+ %poison = getelementptr inbounds i8, i8* null, i64 1
+ ret i8* %poison
+}
+
+define i8* @f4(i8* nocapture %p) {
+ %poison = getelementptr inbounds i8, i8* null, i64 1
+ ret i8* %poison
+}
+
+define <2 x i8*> @f5(i8* nocapture %p) {
+ %poison = getelementptr inbounds i8, i8* null, i64 1
+ %v = insertelement <2 x i8*> undef, i8* %poison, i32 1
+ ret <2 x i8*> %v
+}

Add support for nocapture arg attribute (#245)