llvm2alive: change lowering of fn call returned argument to copy or bitcast
alive was crashing due to missing bitcast semantics
this lowering reuses all of bitcast code & semantics
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1285,17 +1285,13 @@ 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<StateValue> &returned_val) {
+ vector<pair<StateValue, bool>> &ptr_inputs) {
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, returned_val);
+ inputs, ptr_inputs);
}
} else {
- if (argflag & FnCall::ArgReturned)
- returned_val.emplace_back(value);
-
if (ty.isPtrType()) {
Pointer p(s.getMemory(), value.value);
p.strip_attrs();
@@ -1342,13 +1338,11 @@ 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,
- returned_val);
+ unpack_inputs(s, arg->getType(), flags, s[*arg], inputs, ptr_inputs);
fnName_mangled << '#' << arg->getType().toString();
}
fnName_mangled << '!' << getType();
@@ -1358,7 +1352,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, move(returned_val));
+ flags & ArgMemOnly);
return isVoid() ? StateValue() : pack_return(getType(), ret, flags, idx);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -191,7 +191,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, ArgReturned = 1 << 1 };
+ enum ArgFlags { ArgNone = 0, ArgByVal = 1 << 0 };
private:
std::string fnName;
std::vector<std::pair<Value*, unsigned>> args;
@@ -203,6 +203,8 @@ public:
: Instr(type, std::move(name)), fnName(std::move(fnName)), flags(flags),
valid(valid) {}
void addArg(Value &arg, unsigned flags);
+ const auto& getFnName() const { return fnName; }
+ const auto& getArgs() const { return args; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -209,8 +209,7 @@ 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,
- vector<StateValue> &&returned_val) {
+ bool writes_memory, bool argmemonly) {
// TODO: handle changes to memory due to fn call
// TODO: can read/write=false fn calls be removed?
@@ -247,16 +246,12 @@ 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
@@ -140,8 +140,7 @@ 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,
- std::vector<StateValue> &&returned_val);
+ bool writes_memory, bool argmemonly);
void addQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -266,6 +266,7 @@ public:
string fn_name = '@' + fn->getName().str();
auto call = make_unique<FnCall>(*ty, value_name(i), move(fn_name), flags,
!known);
+ unique_ptr<Instr> ret_val;
auto argI = fn->arg_begin(), argE = fn->arg_end();
for (auto &arg : args) {
unsigned attr = FnCall::ArgNone;
@@ -273,12 +274,33 @@ 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;
+ else if (argI->hasReturnedAttr()) {
+ auto call2
+ = make_unique<FnCall>(Type::voidTy, "", string(call->getFnName()),
+ flags, !known);
+ for (auto &[arg, flags] : call->getArgs()) {
+ call2->addArg(*arg, flags);
+ }
+ call = move(call2);
+
+ // fn may have different type than argument. LLVM assumes there's
+ // an implicit bitcast
+ assert(!ret_val);
+ if (argI->getType() == i.getType())
+ ret_val = make_unique<UnaryOp>(*ty, value_name(i), *arg,
+ UnaryOp::Copy);
+ else
+ ret_val = make_unique<ConversionOp>(*ty, value_name(i), *arg,
+ ConversionOp::BitCast);
+ }
++argI;
}
call->addArg(*arg, attr);
}
+ if (ret_val) {
+ BB->addInstr(move(call));
+ RETURN_IDENTIFIER(move(ret_val));
+ }
RETURN_IDENTIFIER(move(call));
}

llvm2alive: change lowering of fn call returned argument to copy or bitcast
alive was crashing due to missing bitcast semantics
this lowering reuses all of bitcast code & semantics