Add support for returned attribute
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1173,13 +1173,18 @@ void FnCall::print(ostream &os) const {
static void unpack_inputs(State&s, Type &ty, unsigned argflag,
const StateValue &value, vector<StateValue> &inputs,
- vector<pair<StateValue, bool>> &ptr_inputs) {
+ vector<pair<StateValue, bool>> &ptr_inputs,
+ vector<StateValue> &returned_val) {
if (auto agg = ty.getAsAggregateType()) {
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
unpack_inputs(s, agg->getChild(i), argflag, agg->extract(value, i),
- inputs, ptr_inputs);
+ inputs, ptr_inputs, returned_val);
}
- } else if (ty.isPtrType()) {
+ } else {
+ if (argflag & FnCall::ArgReturned)
+ returned_val.emplace_back(value);
+
+ if (ty.isPtrType()) {
Pointer p(s.getMemory(), value.value);
p.strip_attrs();
ptr_inputs.emplace_back(StateValue(p.release(), expr(value.non_poison)),
@@ -1188,6 +1193,7 @@ static void unpack_inputs(State&s, Type &ty, unsigned argflag,
inputs.emplace_back(value);
}
}
+}
static void unpack_ret_ty (vector<Type*> &out_types, Type &ty) {
if (auto agg = ty.getAsAggregateType()) {
@@ -1224,11 +1230,13 @@ StateValue FnCall::toSMT(State &s) const {
vector<StateValue> inputs;
vector<pair<StateValue, bool>> ptr_inputs;
vector<Type*> out_types;
+ vector<StateValue> returned_val;
ostringstream fnName_mangled;
fnName_mangled << fnName;
for (auto &[arg, flags] : args) {
- unpack_inputs(s, arg->getType(), flags, s[*arg], inputs, ptr_inputs);
+ unpack_inputs(s, arg->getType(), flags, s[*arg], inputs, ptr_inputs,
+ returned_val);
fnName_mangled << "#" << arg->getType().toString();
}
fnName_mangled << '!' << getType();
@@ -1238,7 +1246,7 @@ StateValue FnCall::toSMT(State &s) const {
unsigned idx = 0;
auto ret = s.addFnCall(fnName_mangled.str(), move(inputs), move(ptr_inputs),
out_types, !(flags & NoRead), !(flags & NoWrite),
- flags & ArgMemOnly);
+ flags & ArgMemOnly, move(returned_val));
return isVoid() ? StateValue() : pack_return(getType(), ret, flags, idx);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -174,7 +174,7 @@ class FnCall final : public Instr {
public:
enum Flags { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1, ArgMemOnly = 1 << 2,
NNaN = 1 << 3 };
- enum ArgFlags { ArgNone = 0, ArgByVal = 1 << 0 };
+ enum ArgFlags { ArgNone = 0, ArgByVal = 1 << 0, ArgReturned = 1 << 1 };
private:
std::string fnName;
std::vector<std::pair<Value*, unsigned>> args;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -205,7 +205,8 @@ const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<pair<StateValue, bool>> &&ptr_inputs,
const vector<Type*> &out_types, bool reads_memory,
- bool writes_memory, bool argmemonly) {
+ bool writes_memory, bool argmemonly,
+ vector<StateValue> &&returned_val) {
// TODO: handle changes to memory due to fn call
// TODO: can read/write=false fn calls be removed?
@@ -242,12 +243,16 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
if (inserted) {
vector<StateValue> values;
+ if (!returned_val.empty())
+ values = move(returned_val);
+ else {
string valname = name + "#val";
string npname = name + "#np";
for (auto t : out_types) {
values.emplace_back(mk_val(*t, valname).first,
expr::mkFreshVar(npname.c_str(), false));
}
+ }
string ub_name = string(name) + "#ub";
I->second = { move(values), expr::mkFreshVar(ub_name.c_str(), false),

MODIFY
ir/state.h
ir/state.h
@@ -131,7 +131,8 @@ public:
addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
std::vector<std::pair<StateValue, bool>> &&ptr_inputs,
const std::vector<Type*> &out_types, bool reads_memory,
- bool writes_memory, bool argmemonly);
+ bool writes_memory, bool argmemonly,
+ std::vector<StateValue> &&returned_val);
void addQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -273,6 +273,8 @@ public:
// Check whether arg itr finished early because it was var arg
if (argI->hasByValAttr())
attr |= FnCall::ArgByVal;
+ else if (argI->hasReturnedAttr())
+ attr |= FnCall::ArgReturned;
++argI;
}
call->addArg(*arg, attr);

ADD
tests/alive-tv/returned-fail.srctgt.ll
+declare i8 @f(i8 returned)
+
+define i8 @src(i8 %t) {
+ %v = call i8 @f(i8 %t)
+ ret i8 %v
+}
+
+define i8 @tgt(i8 %t) {
+ call i8 @f(i8 %t)
+ ret i8 0
+}
+
+; ERROR: Value mismatch

ADD
tests/alive-tv/returned.src.ll
+declare i8 @f(i8 returned)
+declare i8* @f2(i8* returned)
+
+define i8 @g(i8 %t) {
+ %v = call i8 @f(i8 %t)
+ ret i8 %v
+}
+
+define i8* @g2(i8* %p) {
+ %p2 = call i8* @f2(i8* %p)
+ ret i8* %p2
+}
+
+define i8 @g3() {
+ %t = call i8 @f(i8 0)
+ ret i8 %t
+}
+
+define void @g4(i8* %p) {
+ %p2 = call i8* @f2(i8* %p)
+ store i8 0, i8* %p2
+ ret void
+}
+
+define i8 @g5(i8* readonly %p) {
+ %p2 = call i8* @f2(i8* %p)
+ %v = load i8, i8* %p2
+ ret i8 %v
+}
+
+define void @g6(i8* readonly %p) {
+ %p2 = call i8* @f2(i8* %p)
+ store i8 0, i8* %p2 ; should be UB
+ ret void
+}

ADD
tests/alive-tv/returned.tgt.ll
+declare i8 @f(i8 returned)
+declare i8* @f2(i8* returned)
+
+define i8 @g(i8 %t) {
+ call i8 @f(i8 %t)
+ ret i8 %t
+}
+
+define i8* @g2(i8* %p) {
+ call i8* @f2(i8* %p)
+ ret i8* %p
+}
+
+define i8 @g3() {
+ call i8 @f(i8 0)
+ ret i8 0
+}
+
+define void @g4(i8* %p) {
+ call i8* @f2(i8* %p)
+ store i8 0, i8* %p
+ ret void
+}
+
+define i8 @g5(i8* readonly %p) {
+ call i8* @f2(i8* %p)
+ %v = load i8, i8* %p
+ ret i8 %v
+}
+
+define void @g6(i8* readonly %p) {
+ call i8* @f2(i8* %p)
+ store i8 0, i8* %p ; should be UB
+ ret void
+}

Add support for returned attribute (#310)