track noreturn information per var and use it to improve counterexamples
Now we can differentiate between a call not returning and a cal triggering UB
MODIFY
ir/state.cpp
ir/state.cpp
@@ -150,9 +150,11 @@ void State::resetGlobals() {
const State::ValTy& State::exec(const Value &v) {
assert(undef_vars.empty());
+ domain.noreturn = false;
auto val = v.toSMT(*this);
ENSURE(values_map.try_emplace(&v, (unsigned)values.size()).second);
- values.emplace_back(&v, ValTy{std::move(val), domain.UB(), std::move(undef_vars)});
+ values.emplace_back(&v, ValTy{std::move(val), domain.noreturn, domain.UB(),
+ std::move(undef_vars)});
analysis.unused_vars.insert(&v);
// cleanup potentially used temporary values due to undef rewriting
@@ -386,7 +388,7 @@ StateValue* State::no_more_tmp_slots() {
const StateValue& State::operator[](const Value &val) {
auto &[var, val_uvars] = values[values_map.at(&val)];
- auto &[sval, _ub, uvars] = val_uvars;
+ auto &[sval, _retdom, _ub, uvars] = val_uvars;
auto undef_itr = analysis.non_undef_vals.find(&val);
bool is_non_undef = undef_itr != analysis.non_undef_vals.end();
@@ -661,6 +663,7 @@ void State::addUB(AndExpr &&ubs) {
void State::addNoReturn(const expr &cond) {
if (cond.isFalse())
return;
+ domain.noreturn = cond;
return_memory.add(memory, domain.path && cond);
function_domain.add(domain() && cond);
return_undef_vars.insert(undef_vars.begin(), undef_vars.end());

MODIFY
ir/state.h
ir/state.h
@@ -28,6 +28,7 @@ class State {
public:
struct ValTy {
StateValue val;
+ smt::expr return_domain;
smt::expr domain;
std::set<smt::expr> undef_vars;
};
@@ -36,6 +37,7 @@ private:
struct CurrentDomain {
smt::expr path = true; // path from fn entry
smt::AndExpr UB;
+ smt::expr noreturn;
std::set<smt::expr> undef_vars;
smt::expr operator()() const;
@@ -250,12 +252,12 @@ public:
const auto& getQuantVars() const { return quantified_vars; }
const auto& getFnQuantVars() const { return fn_call_qvars; }
- auto& functionDomain() const { return function_domain; }
smt::expr sinkDomain() const;
Memory returnMemory() const { return *return_memory(); }
ValTy returnVal() const {
- return { *return_val(), return_domain(), return_undef_vars };
+ return { *return_val(), return_domain(), function_domain(),
+ return_undef_vars };
}
smt::expr getJumpCond(const BasicBlock &src, const BasicBlock &dst) const;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -209,6 +209,16 @@ static bool error(Errors &errs, const State &src_state, const State &tgt_state,
}
}
+ if (auto call = dynamic_cast<const FnCall*>(var)) {
+ if (m.eval(val.return_domain).isTrue()) {
+ s << *var << " = function did not return!\n";
+ break;
+ } else if (var->isVoid()) {
+ s << "Function " << call->getFnName() << " returned\n";
+ continue;
+ }
+ }
+
if (!dynamic_cast<const Return*>(var) && // domain always false after exec
!m.eval(val.domain).isTrue()) {
s << *var << " = UB triggered!\n";
@@ -380,11 +390,12 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
static void
check_refinement(Errors &errs, const Transform &t, const State &src_state,
const State &tgt_state, const Value *var, const Type &type,
- const expr &fndom_a, const State::ValTy &ap,
- const expr &fndom_b, const State::ValTy &bp,
+ const State::ValTy &ap, const State::ValTy &bp,
bool check_each_var) {
- auto &dom_a = ap.domain;
- auto &dom_b = bp.domain;
+ auto &fndom_a = ap.domain;
+ auto &fndom_b = bp.domain;
+ auto &retdom_a = ap.return_domain;
+ auto &retdom_b = bp.return_domain;
auto &a = ap.val;
auto &b = bp.val;
@@ -483,10 +494,10 @@ check_refinement(Errors &errs, const Transform &t, const State &src_state,
// 2. Check return domain (noreturn check)
{
expr dom_constr;
- if (dom_a.eq(fndom_a) && dom_b.eq(fndom_b)) { // A /\ B /\ A != B
+ if (retdom_a.eq(fndom_a) && retdom_b.eq(fndom_b)) { // A /\ B /\ A != B
dom_constr = false;
} else {
- dom_constr = (fndom_a && fndom_b) && dom_a != dom_b;
+ dom_constr = (fndom_a && fndom_b) && retdom_a != retdom_b;
}
CHECK(std::move(dom_constr),
@@ -503,7 +514,7 @@ check_refinement(Errors &errs, const Transform &t, const State &src_state,
};
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
- expr dom = dom_a && dom_b;
+ expr dom = retdom_a && retdom_b;
CHECK(dom && !poison_cnstr,
print_value, "Target is more poisonous than source");
@@ -1194,16 +1205,14 @@ Errors TransformVerify::verify() const {
auto &val_tgt = tgt_state->at(*tgt_instrs.at(name));
check_refinement(errs, t, *src_state, *tgt_state, var, var->getType(),
- val.domain, val, val_tgt.domain, val_tgt,
- check_each_var);
+ val, val_tgt, check_each_var);
if (errs)
return errs;
}
}
check_refinement(errs, t, *src_state, *tgt_state, nullptr, t.src.getType(),
- src_state->functionDomain()(), src_state->returnVal(),
- tgt_state->functionDomain()(), tgt_state->returnVal(),
+ src_state->returnVal(), tgt_state->returnVal(),
check_each_var);
} catch (AliveException e) {
return std::move(e);

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -51,14 +51,16 @@ void sym_exec(State &s) {
for (auto &i : bb->instrs()) {
if (first && dynamic_cast<const JumpInstr *>(&i))
s.finishInitializer();
- auto &[val, ub, uvars] = s.exec(i);
+ auto &val = s.exec(i);
auto &name = i.getName();
if (config::symexec_print_each_value) {
dbg() << name;
if (name[0] == '%')
- dbg() << " = " << val << " /";
- dbg() << " UB=" << ub << '\n';
+ dbg() << " = " << val.val << " /";
+ dbg() << " UB=" << val.domain << '\n';
+ if (!val.return_domain.isFalse())
+ dbg() << " RET=" << val.return_domain << '\n';
}
}
@@ -67,8 +69,8 @@ void sym_exec(State &s) {
if (config::symexec_print_each_value) {
auto ret = s.returnVal();
- dbg() << "domain = " << s.functionDomain()
- << "\nreturn domain = " << ret.domain
+ dbg() << "domain = " << ret.domain
+ << "\nreturn domain = " << ret.return_domain
<< "\nreturn = " << ret.val
<< s.returnMemory() << "\n\n";
}

track noreturn information per var and use it to improve counterexamples
Now we can differentiate between a call not returning and a cal triggering UB