alive-exec: add line-by-line results now that state has enough info
If there are undef or input values, the SMT solver will just pick zero for those
MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -351,11 +351,13 @@ Result check_expr(const expr &e) {
}
-SolverPush::SolverPush(Solver &s) : s(s) {
+SolverPush::SolverPush(Solver &s) : s(s), valid(s.valid), is_unsat(s.is_unsat) {
Z3_solver_push(ctx(), s.s);
}
SolverPush::~SolverPush() {
+ s.valid = valid;
+ s.is_unsat = is_unsat;
Z3_solver_pop(ctx(), s.s, 1);
}

MODIFY
smt/solver.h
smt/solver.h
@@ -114,6 +114,7 @@ Result check_expr(const expr &e);
class SolverPush {
Solver &s;
+ bool valid, is_unsat;
public:
SolverPush(Solver &s);
~SolverPush();

MODIFY
tools/alive-exec.cpp
tools/alive-exec.cpp
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "ir/type.h"
#include "llvm_util/llvm2alive.h"
#include "smt/expr.h"
#include "smt/smt.h"
#include "llvm/Support/Signals.h"
#include "llvm/Support/SourceMgr.h"
#include "llvm/Transforms/IPO/PassManagerBuilder.h"
-#include "llvm/Transforms/Utils/Cloning.h"
#include <fstream>
#include <iostream>
#include <utility>
+using namespace IR;
using namespace llvm_util;
using namespace smt;
using namespace tools;
@@ -97,68 +98,107 @@ void execFunction(llvm::Function &F, llvm::TargetLibraryInfoWrapperPass &TLI,
assert(types.hasSingleTyping());
}
+ auto error = [&](const Result &r) {
+ if (r.isSat() || r.isUnsat())
+ return false;
+
+ if (r.isInvalid()) {
+ cout << "ERROR: invalid expression\n";
+ } else if (r.isError()) {
+ cout << "ERROR: Error in SMT solver: " << r.getReason() << '\n';
+ } else if (r.isTimeout()) {
+ cout << "ERROR: SMT solver timedout\n";
+ } else if (r.isSkip()) {
+ cout << "ERROR: SMT queries disabled";
+ } else {
+ UNREACHABLE();
+ }
+ ++errorCount;
+ return true;
+ };
+
smt_init->reset();
try {
auto p = verifier.exec();
- auto &state = *p.first;
+ const auto &state = *p.first;
+ const auto &fn = t.src;
+ const auto *bb = &fn.getFirstBB();
+
+ Solver s(true);
+
+ for (auto &[var, val] : state.getValues()) {
+ auto &name = var->getName();
+ auto *i = dynamic_cast<const Instr*>(var);
+ if (!i || &fn.bbOf(*i) != bb)
+ continue;
- auto [ret_val, ret_domain, ret_undefs] = state.returnVal();
- auto ret = expr::mkVar("ret_val", ret_val.value);
- auto ret_np = expr::mkVar("ret_np", ret_val.non_poison);
+ if (auto *jmp = dynamic_cast<const JumpInstr*>(var)) {
+ bool jumped = false;
+ expr cond;
+ for (auto &dst : jmp->targets()) {
+ cond = state.getJumpCond(*bb, dst);
- Solver s;
- s.add(ret_domain);
+ SolverPush push(s);
+ s.add(cond);
auto r = s.check();
- if (r.isUnsat()) {
- cout << "ERROR: Function doesn't reach a return statement\n";
- ++errorCount;
- return;
- }
- if (r.isInvalid()) {
- cout << "ERROR: invalid expression\n";
- ++errorCount;
+ if (error(r))
return;
+
+ if ((jumped = r.isSat())) {
+ cout << " >> Jump to " << dst.getName() << "\n\n";
+ bb = &dst;
+ break;
}
- if (r.isError()) {
- cout << "ERROR: Error in SMT solver: " << r.getReason() << '\n';
- ++errorCount;
- return;
}
- if (r.isTimeout()) {
- cout << "ERROR: SMT solver timedout\n";
- ++errorCount;
+
+ if (jumped) {
+ s.add(cond);
+ continue;
+ } else {
+ cout << "UB triggered on " << name << "\n\n";
+ ++successCount;
return;
}
- if (r.isSkip()) {
- cout << "ERROR: SMT queries disabled";
- ++errorCount;
- return;
}
- if (r.isSat()) {
- auto &m = r.getModel();
- cout << "Return value: ";
- // TODO: add support for aggregates
- if (m.eval(ret_val.non_poison, true).isFalse()) {
- cout << "poison\n\n";
- } else {
- t.src.getType().printVal(cout, state, m.eval(ret_val.value, true));
- s.block(m);
- if (s.check().isSat()) {
- cout << "\n\nWARNING: There are multiple return values";
- }
+ if (dynamic_cast<const Return*>(var)) {
+ const auto &ret = state.returnVal();
+ s.add(ret.domain);
+ auto r = s.check();
+ if (error(r))
+ return;
+ cout << "Returned: ";
+ print_model_val(cout, state, r.getModel(), var, fn.getType(), ret.val);
cout << "\n\n";
+ ++successCount;
+ return;
}
+
+ s.add(val.domain);
+ auto r = s.check();
+ if (error(r))
+ return;
+
+ if (r.isUnsat()) {
+ cout << *var << " = UB triggered!\n\n";
++successCount;
return;
}
- UNREACHABLE();
+ if (name[0] != '%')
+ continue;
+
+ cout << *var << " = ";
+ print_model_val(cout, state, r.getModel(), var, var->getType(), val.val);
+ cout << '\n';
+ continue;
+ }
} catch (const AliveException &e) {
cout << "ERROR: " << e.msg << '\n';
++errorCount;
return;
}
+ ++successCount;
}
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -38,6 +38,11 @@ static bool is_arbitrary(const expr &e) {
static void print_single_varval(ostream &os, const State &st, const Model &m,
const Value *var, const Type &type,
const StateValue &val, unsigned child) {
+ if (dynamic_cast<const VoidType*>(&type)) {
+ os << "void";
+ return;
+ }
+
if (!val.isValid()) {
os << "(invalid expr)";
return;
@@ -82,9 +87,9 @@ static void print_single_varval(ostream &os, const State &st, const Model &m,
}
}
-static void print_varval(ostream &os, const State &st, const Model &m,
+void tools::print_model_val(ostream &os, const State &st, const Model &m,
const Value *var, const Type &type,
- const StateValue &val, unsigned child = 0) {
+ const StateValue &val, unsigned child) {
if (!type.isAggregateType()) {
print_single_varval(os, st, m, var, type, val, child);
return;
@@ -95,8 +100,8 @@ static void print_varval(ostream &os, const State &st, const Model &m,
for (unsigned i = 0, e = agg->numElementsConst(); i < e; ++i) {
if (i != 0)
os << ", ";
- print_varval(os, st, m, var, agg->getChild(i), agg->extract(val, i),
- child + i);
+ tools::print_model_val(os, st, m, var, agg->getChild(i),
+ agg->extract(val, i), child + i);
}
os << (type.isStructType() ? " }" : " >");
}
@@ -168,7 +173,7 @@ static bool error(Errors &errs, const State &src_state, const State &tgt_state,
!dynamic_cast<const ConstantInput*>(var))
continue;
s << *var << " = ";
- print_varval(s, src_state, m, var, var->getType(), val.val);
+ print_model_val(s, src_state, m, var, var->getType(), val.val);
s << '\n';
}
@@ -208,7 +213,7 @@ static bool error(Errors &errs, const State &src_state, const State &tgt_state,
if (jumped) {
continue;
} else {
- s << "UB triggered on " << var->getName() << '\n';
+ s << "UB triggered on " << name << '\n';
break;
}
}
@@ -223,7 +228,8 @@ static bool error(Errors &errs, const State &src_state, const State &tgt_state,
continue;
s << *var << " = ";
- print_varval(s, const_cast<State&>(*st), m, var, var->getType(), val.val);
+ print_model_val(s, const_cast<State&>(*st), m, var, var->getType(),
+ val.val);
s << '\n';
}
@@ -497,9 +503,9 @@ check_refinement(Errors &errs, const Transform &t, const State &src_state,
// 3. Check poison
auto print_value = [&](ostream &s, const Model &m) {
s << "Source value: ";
- print_varval(s, src_state, m, var, type, a);
+ print_model_val(s, src_state, m, var, type, a);
s << "\nTarget value: ";
- print_varval(s, tgt_state, m, var, type, b);
+ print_model_val(s, tgt_state, m, var, type, b);
};
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);

MODIFY
tools/transform.h
tools/transform.h
@@ -60,4 +60,9 @@ public:
void fixupTypes(const TypingAssignments &ty);
};
+
+void print_model_val(std::ostream &os, const IR::State &st, const smt::Model &m,
+ const IR::Value *var, const IR::Type &type,
+ const IR::StateValue &val, unsigned child = 0);
+
}

alive-exec: add line-by-line results now that state has enough info
If there are undef or input values, the SMT solver will just pick zero for those