Rework semantics of function calls
before it was allowing the solver to incorrectly assume that f(2) = f(3) = f(..)
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -679,88 +679,64 @@ void FnCall::print(ostream &os) const {
StateValue FnCall::toSMT(State &s) const {
// TODO: add support for memory
// TODO: add support for global variables
- vector<expr> args_eval;
- const char *suffix = s.isSource() ? "#src" : "#tgt";
+ vector<expr> all_args, value_args;
+ expr all_args_np(true);
for (auto arg : args) {
- auto &[v, p] = s[*arg];
- args_eval.emplace_back(v);
- args_eval.emplace_back(p);
+ auto &[v, np] = s[*arg];
+ all_args.emplace_back(v);
+ all_args.emplace_back(np);
+ value_args.emplace_back(v);
+ all_args_np &= np;
}
- auto add_axiom = [&](string fn, const expr &type,
- expr (expr::*implies)(const expr &) const) {
- if (!s.isSource())
- return;
-
+ auto add_implies_axiom = [&](const string &fn) {
vector<expr> vars_src, vars_tgt;
unsigned i = 0;
- for (auto &arg : args_eval) {
+ 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));
}
- auto name_src = fn + "#src";
- auto name_tgt = fn + "#tgt";
-
- {
- // fns are equal if args are non-poison and equal
- set<expr> vars_set;
- for (unsigned i = 0, e = vars_src.size(); i != e; i += 2) {
- vars_set.insert(vars_src[i]);
- }
-
- vector<expr> v_src, v_tgt;
- for (unsigned i = 0, e = vars_src.size(); i != e; i += 2) {
- v_src.emplace_back(vars_src[i]);
- v_src.emplace_back(true);
- v_tgt.emplace_back(vars_src[i]);
- v_tgt.emplace_back(true);
- }
-
- auto fn_src = expr::mkUF(name_src.c_str(), v_src, type);
- auto fn_tgt = expr::mkUF(name_tgt.c_str(), v_tgt, type);
- s.addPre(expr::mkForAll(vars_set, fn_src == fn_tgt));
- }
-
- {
- // fn src implies fn tgt if source value is poison
+ // 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(false);
+ expr cond(true);
for (unsigned i = 0, e = vars_src.size(); i != e; i += 2) {
- cond |= !vars_src[i + 1];
+ cond &= !vars_src[i + 1] ||
+ (vars_src[i] == vars_tgt[i] && vars_tgt[i+1]);
}
- auto fn_src = expr::mkUF(name_src.c_str(), vars_src, type);
- auto fn_tgt = expr::mkUF(name_tgt.c_str(), vars_tgt, type);
- s.addPre(expr::mkForAll(vars_set,
- cond.implies((fn_src.*implies)(fn_tgt))));
- }
+ auto fn_src = expr::mkUF(fn.c_str(), vars_src, false);
+ auto fn_tgt = expr::mkUF(fn.c_str(), vars_tgt, false);
+ s.addPre(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" + suffix;
- s.addUB(expr::mkUF(ub_name.c_str(), args_eval, false));
-
- add_axiom(fnName + "_ub", false, &expr::implies);
+ auto ub_name = fnName + "#ub";
+ s.addUB(expr::mkUF(ub_name.c_str(), all_args, false));
+ add_implies_axiom(ub_name);
if (dynamic_cast<VoidType*>(&getType()))
return {};
- expr ret_type = getType().getDummyValue();
- add_axiom(fnName, ret_type, &expr::operator==);
- add_axiom(fnName + "_poison", false, &expr::implies);
+ // create a new variable that can take any value if function is poison
+ expr val = expr::mkUF(fnName.c_str(), value_args, getType().getDummyValue());
+ if (!all_args_np.isTrue()) {
+ auto var_name = fnName + '#' + to_string(s.nextFnCallId());
+ auto var = expr::mkVar(var_name.c_str(), getType().getDummyValue());
+ s.addQuantVar(var);
+ val = expr::mkIf(all_args_np, val, var);
+ }
+
+ auto poison_name = fnName + "#poison";
+ add_implies_axiom(poison_name);
- auto val_name = fnName + suffix;
- auto poison_name = fnName + "_poison" + suffix;
- return { expr::mkUF(val_name.c_str(), args_eval, ret_type),
- expr::mkUF(poison_name.c_str(), args_eval, false) };
+ return { move(val), expr::mkUF(poison_name.c_str(), all_args, false) };
}
expr FnCall::getTypeConstraints(const Function &f) const {

MODIFY
ir/state.cpp
ir/state.cpp
@@ -18,6 +18,12 @@ State::State(const Function &f, bool source)
*this);
}
+void State::syncWithSrc(const State &src) {
+ assert(src.isSource());
+ assert(!isSource());
+ next_fn_call_id = src.next_fn_call_id;
+}
+
const StateValue& State::exec(const Value &v) {
assert(undef_vars.empty());
auto val = v.toSMT(*this);

MODIFY
ir/state.h
ir/state.h
@@ -47,6 +47,9 @@ private:
predecessor_data;
std::unordered_set<const BasicBlock*> seen_bbs;
+ // fn call id to be used when an argument is poison
+ unsigned next_fn_call_id = 0;
+
// temp state
DomainTy domain;
Memory memory;
@@ -62,6 +65,8 @@ private:
public:
State(const Function &f, bool source);
+ void syncWithSrc(const State &src);
+
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
const ValTy& at(const Value &val) const;
@@ -80,6 +85,8 @@ public:
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
+ unsigned nextFnCallId() { return next_fn_call_id++; }
+
void addQuantVar(const smt::expr &var);
void addUndefVar(const smt::expr &var);
void resetUndefVars();

ADD
tests/unit/call-error2.opt
+; ERROR: Value mismatch
+%c = call i32 @f(i32 3)
+%d = call i32 @f(i32 4)
+%e = sub %c, %d
+ret %e
+ =>
+%c = call i32 @f(i32 3)
+%d = call i32 @f(i32 4)
+%e = sub %c, %d
+ret 0
+

ADD
tests/unit/call-error3.opt
+; ERROR: Value mismatch
+
+%c = call i32 @f(i32 3)
+%d = call i32 @f(i32 poison)
+%e = call i32 @f(i32 4)
+%f = add %c, %e
+ret %f
+ =>
+%c = call i32 @f(i32 3)
+%d = call i32 @f(i32 3)
+%e = call i32 @f(i32 4)
+%f = add %c, %d
+ret %f

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -22,6 +22,8 @@ using namespace std;
static bool is_undef(const expr &e) {
+ if (e.isConst())
+ return false;
Solver s;
s.add(expr::mkForAll(e.vars(), expr::mkVar("#undef", e) != e));
return s.check().isUnsat();
@@ -230,17 +232,17 @@ static void check_refinement(Errors &errs, Transform &t,
expr pre = src_state.getPre() && tgt_state.getPre();
Solver::check({
- { preprocess(t, qvars, ap.second, pre && dom_a.notImplies(dom_b)),
+ { pre && preprocess(t, qvars, ap.second, dom_a.notImplies(dom_b)),
[&](const Result &r) {
err(r, false, "Source is more defined than target");
}},
- { preprocess(t, qvars, ap.second,
- pre && dom_a && a.non_poison.notImplies(b.non_poison)),
+ { pre && preprocess(t, qvars, ap.second,
+ dom_a && a.non_poison.notImplies(b.non_poison)),
[&](const Result &r) {
err(r, true, "Target is more poisonous than source");
}},
- { preprocess(t, qvars, ap.second,
- pre && dom_a && a.non_poison && a.value != b.value),
+ { pre && preprocess(t, qvars, ap.second,
+ dom_a && a.non_poison && a.value != b.value),
[&](const Result &r) {
err(r, true, "Value mismatch");
}}
@@ -265,6 +267,7 @@ Errors TransformVerify::verify() const {
try {
sym_exec(src_state);
+ tgt_state.syncWithSrc(src_state);
sym_exec(tgt_state);
} catch (LoopInCFGDetected&) {
return "Loops are not supported yet! Skipping function.";

Rework semantics of function calls
before it was allowing the solver to incorrectly assume that f(2) = f(3) = f(..)