refactor handling of function calls in preparation for supporting ptrs & memory
add preliminary support for fn calls with aggregated i/o
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1088,88 +1088,63 @@ void FnCall::print(ostream &os) const {
os << "\t; WARNING: unknown known function";
}
-StateValue FnCall::toSMT(State &s) const {
- if (!valid) {
- s.addUB({});
- return {};
+static void unpack_inputs(Type &ty, const StateValue &value,
+ vector<StateValue> &inputs,
+ vector<StateValue> &ptr_inputs) {
+ if (auto agg = ty.getAsAggregateType()) {
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ unpack_inputs(agg->getChild(i), agg->extract(value, i), inputs,
+ ptr_inputs);
}
-
- // TODO: add support for memory
- // TODO: add support for global variables
- vector<expr> all_args, value_args;
- expr all_args_np(true);
-
- for (auto arg : args) {
- auto &[v, np] = s[*arg];
- all_args.emplace_back(v);
- all_args.emplace_back(np);
- value_args.emplace_back(v);
- all_args_np &= np;
+ } else {
+ (ty.isPtrType() ? ptr_inputs : inputs).emplace_back(value);
}
-
- auto add_implies_axiom = [&](const string &fn) {
- vector<expr> vars_src, vars_tgt;
- unsigned i = 0;
- for (auto &arg : all_args) {
- auto name = "v" + to_string(i++);
- vars_src.emplace_back(expr::mkVar(name.c_str(), arg));
- name = "v" + to_string(i++);
- vars_tgt.emplace_back(expr::mkVar(name.c_str(), arg));
}
- // fn src implies fn tgt if each src arg is poison or it's equal to tgt
- set<expr> vars_set(vars_src.begin(), vars_src.end());
- vars_set.insert(vars_tgt.begin(), vars_tgt.end());
-
- expr cond(true);
- for (unsigned i = 0, e = vars_src.size(); i != e; i += 2) {
- cond &= !vars_src[i + 1] ||
- (vars_src[i] == vars_tgt[i] && vars_tgt[i+1]);
+static void unpack_ret_ty (vector<Type*> &out_types, Type &ty) {
+ if (auto agg = ty.getAsAggregateType()) {
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ unpack_ret_ty(out_types, agg->getChild(i));
+ }
+ } else {
+ out_types.emplace_back(&ty);
+ }
}
- auto fn_src = expr::mkUF(fn.c_str(), vars_src, false);
- auto fn_tgt = expr::mkUF(fn.c_str(), vars_tgt, false);
- s.addAxiom(expr::mkForAll(vars_set, cond.implies(fn_src.implies(fn_tgt))));
- };
-
- // impact of the function on the domain of the program
- // TODO: constraint when certain attributes are on
- auto ub_name = fnName + "#ub";
- s.addUB(expr::mkUF(ub_name.c_str(), all_args, false));
- add_implies_axiom(ub_name);
+static StateValue pack_return(Type &ty, vector<StateValue> &vals,
+ unsigned &idx) {
+ if (auto agg = ty.getAsAggregateType()) {
+ vector<StateValue> vs;
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ vs.emplace_back(pack_return(agg->getChild(i), vals, idx));
+ }
+ return agg->aggregateVals(vs);
+ }
+ return vals[idx++];
+}
- if (dynamic_cast<VoidType*>(&getType()))
+StateValue FnCall::toSMT(State &s) const {
+ if (!valid) {
+ s.addUB({});
return {};
-
- // create a new variable that can take any value if function is poison
- StateValue ret_type = getType().getDummyValue(true);
- expr val = expr::mkUF(fnName.c_str(), value_args, ret_type.value);
- if (!all_args_np.isTrue()) {
- auto var_name = fnName + "_val";
- auto var = expr::mkFreshVar(var_name.c_str(), ret_type.value);
- s.addQuantVar(var);
- val = expr::mkIf(all_args_np, val, var);
}
- // FIXME: broken for functions that return aggregate types
- if (getType().isAggregateType())
- return {};
+ vector<StateValue> inputs, ptr_inputs;
+ vector<Type*> out_types;
- auto poison_name = fnName + "#poison";
- add_implies_axiom(poison_name);
+ for (auto arg : args) {
+ unpack_inputs(arg->getType(), s[*arg], inputs, ptr_inputs);
+ }
+ unpack_ret_ty(out_types, getType());
- return { move(val), expr::mkUF(poison_name.c_str(), all_args, false) };
+ unsigned idx = 0;
+ auto ret = s.addFnCall(fnName, move(inputs), move(ptr_inputs), out_types);
+ return pack_return(getType(), ret, idx);
}
expr FnCall::getTypeConstraints(const Function &f) const {
// TODO : also need to name each arg type smt var uniquely
- auto r = Value::getTypeConstraints();
- // TODO: add aggregate support
- for (auto arg : args) {
- r &= !arg->getType().enforceStructType();
- r &= !arg->getType().enforceVectorType();
- }
- return r;
+ return Value::getTypeConstraints();
}
unique_ptr<Instr> FnCall::dup(const string &suffix) const {

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -661,7 +661,6 @@ Memory::Memory(State &state) : state(&state) {
auto bid = ptr_val.ptr().get_bid().extract(bits_for_bid - 2, 0);
state.addAxiom(expr::mkForAll({ idx }, bid.ule(num_nonlocals - 1)));
}
- }
#else
non_local_block_val
= expr::mkArray("blk_val",

MODIFY
ir/state.cpp
ir/state.cpp
@@ -171,6 +171,51 @@ void State::addUB(const expr &ub) {
domain.second.insert(undef_vars.begin(), undef_vars.end());
}
+const vector<StateValue>
+State::addFnCall(const string &name, vector<StateValue> &&inputs,
+ vector<StateValue> &&ptr_inputs,
+ const vector<Type*> &out_types) {
+ expr all_args_np(true);
+ for (auto &v : inputs) {
+ all_args_np &= v.non_poison;
+ }
+ for (auto &v : ptr_inputs) {
+ all_args_np &= v.non_poison;
+ }
+
+ auto [I, inserted]
+ = fn_call_data[name].try_emplace({move(inputs), move(ptr_inputs), memory});
+
+ if (inserted) {
+ vector<StateValue> values;
+ string valname = name + "#val";
+ string npname = name + "#np";
+ for (auto t : out_types) {
+ values.emplace_back(
+ expr::mkFreshVar(valname.c_str(), t->getDummyValue(false).value),
+ expr::mkFreshVar(npname.c_str(), false));
+ }
+
+ string ub_name = string(name) + "#ub";
+ I->second = { move(values), expr::mkFreshVar(ub_name.c_str(), false) };
+ }
+
+ addUB(I->second.second);
+ if (all_args_np.isTrue())
+ return I->second.first;
+
+ // if any of the arguments is poison, yield an arbitrary value, such that
+ // f(poison) -> f(42) works
+ vector<StateValue> ret;
+ auto var_name = name + "#pval";
+ for (auto &[v, np] : I->second.first) {
+ auto var = expr::mkFreshVar(var_name.c_str(), v);
+ ret.emplace_back(expr::mkIf(all_args_np, v, var), expr(np));
+ addQuantVar(var);
+ }
+ return ret;
+}
+
void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}
@@ -232,14 +277,51 @@ void State::markGlobalAsAllocated(const string &glbvar) {
itr->second.second = true;
}
-void State::copyGlobalVarBidsFromSrc(const State &src) {
+void State::syncSEdataWithSrc(const State &src) {
assert(glbvar_bids.empty());
- assert(src.isSource());
+ assert(src.isSource() && !isSource());
glbvar_bids = src.glbvar_bids;
for (auto &itm : glbvar_bids)
itm.second.second = false;
+ fn_call_data = src.fn_call_data;
+
Memory::resetLocalBids();
}
+void State::mkAxioms(const State &tgt) {
+ assert(isSource() && !tgt.isSource());
+ memory.mkAxioms();
+
+ // axioms for function calls
+ // TODO: handle refinement of pointers & memory
+ for (auto &[fn, data] : tgt.fn_call_data) {
+ (void)fn;
+ for (auto I = data.begin(), E = data.end(); I != E; ++I) {
+ auto &[ins, ptr_ins, mem] = I->first;
+ auto &[rets, ub] = I->second;
+
+ for (auto I2 = data.begin(); I2 != E; ++I2) {
+ auto &[ins2, ptr_ins2, mem2] = I2->first;
+ auto &[rets2, ub2] = I2->second;
+
+ expr refines(true), is_val_eq(true);
+ for (unsigned i = 0, e = ins.size(); i != e; ++i) {
+ expr eq_val = ins[i].value == ins2[i].value;
+ is_val_eq &= eq_val;
+ refines &= !ins[i].non_poison || (eq_val && ins2[i].non_poison);
+ }
+
+ expr ref_expr(true), eq_expr(true);
+ for (unsigned i = 0, e = rets.size(); i != e; ++i) {
+ eq_expr &= rets[i].value == rets2[i].value;
+ ref_expr &= rets[i].non_poison.implies(rets2[i].non_poison);
+ }
+ addAxiom(is_val_eq.implies(eq_expr));
+ addAxiom(refines.implies(ref_expr && ub.implies(ub2)));
+ }
+ }
+ }
+}
+
}

MODIFY
ir/state.h
ir/state.h
#include "smt/expr.h"
#include "smt/exprs.h"
#include <array>
+#include <map>
#include <ostream>
#include <set>
+#include <string>
#include <tuple>
#include <unordered_map>
#include <unordered_set>
@@ -66,6 +68,15 @@ private:
smt::DisjointExpr<Memory> return_memory;
std::set<smt::expr> return_undef_vars;
+ // store data for function calls:
+ // inputs: non-ptr arguments, ptr arguments, memory
+ // outputs: values, UB
+ std::map<std::string,
+ std::map<std::tuple<std::vector<StateValue>, std::vector<StateValue>,
+ Memory>,
+ std::pair<std::vector<StateValue>, smt::expr>>>
+ fn_call_data;
+
public:
State(const Function &f, bool source);
@@ -90,6 +101,11 @@ public:
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
+ const std::vector<StateValue>
+ addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
+ std::vector<StateValue> &&ptr_inputs,
+ const std::vector<Type*> &out_types);
+
void addQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);
void resetUndefVars();
@@ -124,7 +140,9 @@ public:
bool hasGlobalVarBid(const std::string &glbvar, unsigned &bid,
bool &allocated) const;
void markGlobalAsAllocated(const std::string &glbvar);
- void copyGlobalVarBidsFromSrc(const State &src);
+ void syncSEdataWithSrc(const State &src);
+
+ void mkAxioms(const State &tgt);
private:
void addJump(const BasicBlock &dst, smt::expr &&domain);

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -591,8 +591,9 @@ Errors TransformVerify::verify() const {
try {
sym_exec(src_state);
- tgt_state.copyGlobalVarBidsFromSrc(src_state);
+ tgt_state.syncSEdataWithSrc(src_state);
sym_exec(tgt_state);
+ src_state.mkAxioms(tgt_state);
} catch (AliveException e) {
return move(e);
}

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -23,7 +23,6 @@ void sym_exec(State &s) {
}
s.exec(Value::voidVal);
- s.getMemory().mkAxioms();
bool first = true;
if (f.getFirstBB().getName() != "#init") {

refactor handling of function calls in preparation for supporting ptrs & memory
add preliminary support for fn calls with aggregated i/o