Factor out data structures used by fn_call_data as struct FnCallInput/FnCallOutput
MODIFY
ir/state.cpp
ir/state.cpp
@@ -235,7 +235,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
auto mk_val = [&](const Type &t, const string &name) {
if (t.isPtrType())
- return memory.mkFnRet(name.c_str(), get<1>(I->first));
+ return memory.mkFnRet(name.c_str(), I->first.args_ptr);
auto v = expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
return make_pair(v, v);
@@ -257,26 +257,26 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
string ub_name = string(name) + "#ub";
I->second = { move(values), expr::mkFreshVar(ub_name.c_str(), false),
writes_memory
- ? memory.mkCallState(argmemonly ? &get<1>(I->first) : nullptr)
+ ? memory.mkCallState(argmemonly ? &I->first.args_ptr : nullptr)
: Memory::CallState(), true };
} else {
- get<3>(I->second) = true;
+ I->second.used = true;
}
- addUB(get<1>(I->second));
+ addUB(I->second.ub);
if (writes_memory)
- memory.setState(get<2>(I->second));
+ memory.setState(I->second.callstate);
if (all_args_np.isTrue())
- return get<0>(I->second);
+ return I->second.retvals;
// if any of the arguments is poison, yield an arbitrary value, such that
// f(poison) -> f(42) works
vector<StateValue> ret;
auto T = out_types.begin();
auto var_name = name + "#pval";
- for (auto &[v, np] : get<0>(I->second)) {
+ for (auto &[v, np] : I->second.retvals) {
auto [val_poison, var] = mk_val(**T, var_name);
ret.emplace_back(expr::mkIf(all_args_np, v, val_poison), expr(np));
addQuantVar(move(var));
@@ -371,7 +371,7 @@ void State::syncSEdataWithSrc(const State &src) {
(void)fn;
for (auto &[in, data] : map) {
(void)in;
- get<3>(data) = false;
+ data.used = false;
}
}

MODIFY
ir/state.h
ir/state.h
@@ -87,17 +87,25 @@ private:
smt::DisjointExpr<Memory> return_memory;
std::set<smt::expr> return_undef_vars;
- // store data for function calls:
- // inputs: non-ptr arguments, (ptr arguments, is by_val arg?), memory,
- // reads memory?, argmemonly
- // outputs: values, UB, memory state, used in this state?
- std::map<std::string,
- std::map<std::tuple<std::vector<StateValue>,
- std::vector<std::pair<StateValue, bool>>,
- Memory, bool, bool>,
- std::tuple<std::vector<StateValue>, smt::expr,
- Memory::CallState, bool>>>
- fn_call_data;
+ struct FnCallInput {
+ std::vector<StateValue> args_nonptr;
+ // (ptr arguments, is by_val arg?)
+ std::vector<std::pair<StateValue, bool>> args_ptr;
+ Memory m;
+ bool readsmem, argmemonly;
+ bool operator<(const FnCallInput &rhs) const {
+ return std::tie(args_nonptr, args_ptr, m, readsmem, argmemonly) <
+ std::tie(rhs.args_nonptr, rhs.args_ptr, rhs.m, rhs.readsmem,
+ rhs.argmemonly);
+ }
+ };
+ struct FnCallOutput {
+ std::vector<StateValue> retvals;
+ smt::expr ub;
+ Memory::CallState callstate;
+ bool used;
+ };
+ std::map<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;
public:
State(Function &f, bool source);

Factor out data structures used by fn_call_data as struct FnCallInput/FnCallOutput (#323)