Add support for noreturn
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1314,6 +1314,8 @@ void FnCall::print(ostream &os) const {
os << " argmemonly";
if (flags & NNaN)
os << " NNaN";
+ if (flags & NoReturn)
+ os << " noreturn";
if (!valid)
os << "\t; WARNING: unknown known function";
@@ -1389,6 +1391,12 @@ StateValue FnCall::toSMT(State &s) const {
auto ret = s.addFnCall(fnName_mangled.str(), move(inputs), move(ptr_inputs),
out_types, !(flags & NoRead), !(flags & NoWrite),
flags & ArgMemOnly);
+
+ if (flags & NoReturn) {
+ // TODO: Even if a function call doesn't have noreturn, it can possibly
+ // exit. Relevant bug: https://bugs.llvm.org/show_bug.cgi?id=27953
+ s.addNoReturn();
+ }
return isVoid() ? StateValue() : pack_return(getType(), ret, flags, idx);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -190,7 +190,7 @@ public:
class FnCall final : public Instr {
public:
enum Flags { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1, ArgMemOnly = 1 << 2,
- NNaN = 1 << 3 };
+ NNaN = 1 << 3, NoReturn = 1 << 4 };
enum ArgFlags { ArgNone = 0, ArgByVal = 1 << 0 };
private:
std::string fnName;
@@ -206,6 +206,7 @@ public:
const auto& getFnName() const { return fnName; }
const auto& getArgs() const { return args; }
+ bool hasFlag(unsigned i) const { return flags & i; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -182,6 +182,7 @@ void State::addReturn(const StateValue &val) {
return_val.add(val, domain.path);
return_memory.add(memory, domain.path);
return_domain.add(domain());
+ function_domain.add(domain());
return_undef_vars.insert(undef_vars.begin(), undef_vars.end());
return_undef_vars.insert(domain.undef_vars.begin(), domain.undef_vars.end());
undef_vars.clear();
@@ -205,6 +206,11 @@ void State::addUB(AndExpr &&ubs) {
domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
}
+void State::addNoReturn() {
+ function_domain.add(domain());
+ addUB(expr(false));
+}
+
const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<pair<StateValue, bool>> &&ptr_inputs,

MODIFY
ir/state.h
ir/state.h
@@ -83,6 +83,8 @@ private:
// return_domain: a boolean expression describing return condition
smt::OrExpr return_domain;
+ // function_domain: a condition for function having well-defined behavior
+ smt::OrExpr function_domain;
smt::DisjointExpr<StateValue> return_val;
smt::DisjointExpr<Memory> return_memory;
std::set<smt::expr> return_undef_vars;
@@ -134,6 +136,7 @@ public:
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
void addUB(smt::AndExpr &&ubs);
+ void addNoReturn();
void addOOM(smt::expr &&oom) { ooms.add(std::move(oom)); }
const std::vector<StateValue>
@@ -163,6 +166,7 @@ public:
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }
+ auto& functionDomain() const { return function_domain; }
auto& returnDomain() const { return return_domain; }
smt::expr sinkDomain() const;
Memory returnMemory() const { return *return_memory(); }

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -258,6 +258,8 @@ public:
flags |= FnCall::NoRead;
if (i.hasFnAttr(llvm::Attribute::ArgMemOnly))
flags |= FnCall::ArgMemOnly;
+ if (i.hasFnAttr(llvm::Attribute::NoReturn))
+ flags |= FnCall::NoReturn;
if (auto op = dyn_cast<llvm::FPMathOperator>(&i)) {
if (op->hasNoNaNs())
flags |= FnCall::NNaN;

ADD
tests/alive-tv/attrs/noreturn-2.srctgt.ll
+declare void @f() noreturn
+
+define void @src(i1 %cond) {
+ br i1 %cond, label %A, label %B
+A:
+ unreachable
+B:
+ call void @f()
+ ret void
+}
+
+define void @tgt(i1 %cond) {
+ call void @f()
+ ret void
+}

ADD
tests/alive-tv/attrs/noreturn-3.srctgt.ll
+declare void @f() noreturn
+declare void @g()
+
+; This should hold, because src has tgt's behavior
+define i8 @src() {
+ %c = freeze i1 undef
+ br i1 %c, label %A, label %B
+A:
+ call void @g()
+ ret i8 0
+B:
+ call void @f()
+ ret i8 0
+}
+
+define i8 @tgt() {
+ call void @f()
+ ret i8 0
+}

ADD
tests/alive-tv/attrs/noreturn-fail-2.srctgt.ll
+declare void @f()
+
+define i8 @src() {
+ call void @f() noreturn
+ ret i8 0
+}
+
+define i8 @tgt() {
+ call void @f()
+ ret i8 0
+}
+
+; ERROR: Target or source may never return

ADD
tests/alive-tv/attrs/noreturn-fail-3.srctgt.ll
+declare void @f() noreturn
+declare void @g()
+
+define i8 @src(i8* %p) {
+ call void @f()
+ %v = load i8, i8* %p
+ ret i8 %v
+}
+
+define i8 @tgt(i8* %p) {
+ %v = load i8, i8* %p
+ call void @f()
+ ret i8 %v
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/attrs/noreturn-fail-4.srctgt.ll
+declare void @f()
+
+define i8 @src() {
+ call void @f()
+ ret i8 0
+}
+
+define i8 @tgt() {
+ call void @f() noreturn
+ ret i8 0
+}
+
+; ERROR: Target or source may never return

ADD
tests/alive-tv/attrs/noreturn-fail-5.srctgt.ll
+declare void @f() noreturn
+declare void @g() noreturn
+
+define void @src() {
+ call void @f()
+ ret void
+}
+
+define void @tgt() {
+ call void @g()
+ ret void
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/attrs/noreturn-fail.srctgt.ll
+declare void @f() noreturn
+
+define void @src() {
+ call void @f()
+ ret void
+}
+
+define void @tgt() {
+ unreachable
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/attrs/noreturn.srctgt.ll
+declare void @f() noreturn
+
+define void @src() {
+ call void @f()
+ call void @f()
+ ret void
+}
+
+define void @tgt() {
+ call void @f()
+ unreachable
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -260,11 +260,11 @@ static expr preprocess(Transform &t, const set<expr> &qvars0,
}
-static void check_refinement(Errors &errs, Transform &t,
- State &src_state, State &tgt_state,
+static void
+check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
const Value *var, const Type &type,
- const expr &dom_a, const State::ValTy &ap,
- const expr &dom_b, const State::ValTy &bp,
+ const expr &dom_a, const expr &fndom_a, const State::ValTy &ap,
+ const expr &dom_b, const expr &fndom_b, const State::ValTy &bp,
bool check_each_var) {
auto &a = ap.first;
auto &b = bp.first;
@@ -358,11 +358,16 @@ static void check_refinement(Errors &errs, Transform &t,
};
Solver::check({
- { mk_fml(dom_a.notImplies(dom_b)),
+ { mk_fml(fndom_a.notImplies(fndom_b)),
[&](const Result &r) {
err(r, [](ostream&, const Model&){},
"Source is more defined than target");
}},
+ { mk_fml(fndom_a && ((!dom_a && dom_b) || (dom_a && !dom_b))),
+ [&](const Result &r) {
+ err(r, [](ostream&, const Model&){},
+ "Target or source may never return");
+ }},
{ mk_fml(dom && !poison_cnstr),
[&](const Result &r) {
err(r, print_value, "Target is more poisonous than source");
@@ -961,7 +966,8 @@ Errors TransformVerify::verify() const {
// TODO: add data-flow domain tracking for Alive, but not for TV
check_refinement(errs, t, src_state, tgt_state, var, var->getType(),
- true, val, true, tgt_state.at(*tgt_instrs.at(name)),
+ true, true, val,
+ true, true, tgt_state.at(*tgt_instrs.at(name)),
check_each_var);
if (errs)
return errs;
@@ -969,8 +975,10 @@ Errors TransformVerify::verify() const {
}
check_refinement(errs, t, src_state, tgt_state, nullptr, t.src.getType(),
- src_state.returnDomain()(), src_state.returnVal(),
- tgt_state.returnDomain()(), tgt_state.returnVal(),
+ src_state.returnDomain()(), src_state.functionDomain()(),
+ src_state.returnVal(),
+ tgt_state.returnDomain()(), tgt_state.functionDomain()(),
+ tgt_state.returnVal(),
check_each_var);
return errs;

Add support for noreturn (#309)