add initial counterexample printing support
MODIFY
ir/state.cpp
ir/state.cpp
@@ -28,19 +28,20 @@ State::State(const Function &f) : f(f) {
const StateValue& State::exec(const Value &v) {
assert(undef_vars.empty());
auto val = v.toSMT(*this);
- auto p = values.try_emplace(&v, move(val), move(undef_vars));
+ auto p = values_map.try_emplace(&v, (unsigned)values.size());
assert(p.second);
+ values.emplace_back(&v, ValTy(move(val), move(undef_vars)));
// cleanup potentially used temporary values due to undef rewriting
while (i_tmp_values > 0) {
tmp_values[--i_tmp_values] = StateValue();
}
- return p.first->second.first;
+ return values.back().second.first;
}
const StateValue& State::operator[](const Value &val) {
- auto &[sval, uvars] = values.at(&val);
+ auto &[sval, uvars] = values[values_map.at(&val)].second;
if (uvars.empty())
return sval;
@@ -82,7 +83,7 @@ const StateValue& State::operator[](const Value &val) {
}
const State::ValTy& State::at(const Value &val) const {
- return values.at(&val);
+ return values[values_map.at(&val)].second;
}
bool State::startBB(const BasicBlock &bb) {

MODIFY
ir/state.h
ir/state.h
#include <set>
#include <unordered_map>
#include <utility>
+#include <vector>
namespace IR {
@@ -37,8 +38,11 @@ public:
private:
const Function &f;
std::set<smt::expr> quantified_vars;
+
// var -> ((value, not_poison), undef_vars)
- std::unordered_map<const Value*, ValTy> values;
+ std::unordered_map<const Value*, unsigned> values_map;
+ std::vector<std::pair<const Value*, ValTy>> values;
+
std::unordered_map<const BasicBlock*, smt::expr> domain_bbs;
// temp state

MODIFY
tools/transform.cpp
tools/transform.cpp
#include "smt/solver.h"
#include "util/errors.h"
#include "util/symexec.h"
+#include <set>
+#include <sstream>
using namespace IR;
using namespace smt;
@@ -16,6 +18,77 @@ using namespace util;
using namespace std;
+static void print_varval(ostream &s, const Model &m, const StateValue &val) {
+ if (m[val.non_poison].isFalse()) {
+ s << "poison";
+ return;
+ }
+
+ expr e = m[val.value];
+ uint64_t n;
+ ENSURE(e.isUInt(n));
+ auto bw = e.bits();
+ s << "0x" << hex << n << dec;
+ s << " (" << n;
+ if (n != 0 && num_leading_zeros(n) == (64 - bw)) {
+ s << ", " << ((int64_t)(n << (64 - bw)) >> (64 - bw));
+ }
+ s << ')';
+}
+
+
+static void error(Errors &errs, State &src_state, State &tgt_state,
+ const Result &r, bool print_var, const Value *var,
+ const StateValue &src, const StateValue &tgt,
+ const char *msg) {
+
+ if (r.isInvalid()) {
+ errs.add("Invalid expr");
+ return;
+ }
+
+ if (r.isUnknown()) {
+ errs.add("Timeout");
+ return;
+ }
+
+ stringstream s;
+ string empty;
+ auto &var_name = var ? var->getName() : empty;
+ auto &m = r.getModel();
+
+ s << msg;
+ if (!var_name.empty())
+ s << " for " << *var;
+ s << "\n\nExample:\n";
+
+ set<string> seen_vars;
+ for (auto &vs : { src_state.getValues(), tgt_state.getValues() }) {
+ for (auto &[var, val] : vs) {
+ auto &name = var->getName();
+ if (name == var_name)
+ break;
+
+ if (name[0] != '%' || !seen_vars.insert(name).second)
+ continue;
+
+ s << *var << " = ";
+ print_varval(s, m, val.first);
+ s << '\n';
+ }
+ }
+
+ if (print_var) {
+ s << "Source value: ";
+ print_varval(s, m, src);
+ s << "\nTarget value: ";
+ print_varval(s, m, tgt);
+ }
+
+ errs.add(s.str());
+}
+
+
static expr preprocess(Transform &t, const set<expr> &qvars,
const set<expr> &undef_qvars, expr && e) {
if (qvars.empty() || e.isFalse())
@@ -43,6 +116,8 @@ static expr preprocess(Transform &t, const set<expr> &qvars,
newexpr = newexpr.simplify();
if (newexpr.isFalse())
continue;
+
+ newexpr &= var == nums[i]; // keep for counterexample printing
instances2.emplace(move(newexpr));
}
}
@@ -61,29 +136,39 @@ static expr preprocess(Transform &t, const set<expr> &qvars,
static void check_refinement(Errors &errs, Transform &t,
- const set<expr> &global_qvars,
+ State &src_state, State &tgt_state,
+ const Value *var,
const expr &dom_a, const State::ValTy &ap,
const expr &dom_b, const State::ValTy &bp) {
auto &a = ap.first;
auto &b = bp.first;
- auto qvars = global_qvars;
+ auto qvars = src_state.getQuantVars();
qvars.insert(ap.second.begin(), ap.second.end());
- // TODO: improve error messages
+ auto err = [&](const Result &r, bool print_var, const char *msg) {
+ error(errs, src_state, tgt_state, r, print_var, var, a, b, msg);
+ };
+
Solver::check({
{ preprocess(t, qvars, ap.second, dom_a.notImplies(dom_b)),
- [&](const Result &r) { errs.add("Source is more defined than target"); }},
-
+ [&](const Result &r) {
+ err(r, false, "Source is more defined than target");
+ }},
{ preprocess(t, qvars, ap.second,
dom_a && a.non_poison.notImplies(b.non_poison)),
- [&](const Result &r) {errs.add("Target is more poisonous than source");}},
-
- { preprocess(t, qvars, ap.second, dom_a && a.non_poison && a.value != b.value),
- [&](const Result &r) { errs.add("value mismatch"); } }
+ [&](const Result &r) {
+ err(r, true, "Target is more poisonous than source");
+ }},
+ { preprocess(t, qvars, ap.second,
+ dom_a && a.non_poison && a.value != b.value),
+ [&](const Result &r) {
+ err(r, true, "Value mismatch");
+ }}
});
}
+
namespace tools {
TransformVerify::TransformVerify(Transform &t, bool check_each_var) :
@@ -110,7 +195,7 @@ Errors TransformVerify::verify() const {
continue;
// TODO: add data-flow domain tracking for Alive, but not for TV
- check_refinement(errs, t, src_state.getQuantVars(),
+ check_refinement(errs, t, src_state, tgt_state, var,
true, val, true, tgt_state.at(*tgt_instrs.at(name)));
if (errs)
return errs;
@@ -124,7 +209,7 @@ Errors TransformVerify::verify() const {
errs.add("Target returns but source doesn't");
} else if (src_state.fnReturned()) {
- check_refinement(errs, t, src_state.getQuantVars(),
+ check_refinement(errs, t, src_state, tgt_state, nullptr,
src_state.returnDomain(), src_state.returnVal(),
tgt_state.returnDomain(), tgt_state.returnVal());
}

MODIFY
util/compiler.cpp
util/compiler.cpp
@@ -36,4 +36,12 @@ unsigned num_sign_bits(uint64_t n) {
#endif
}
+unsigned num_leading_zeros(uint64_t n) {
+#if defined(__GNUC__)
+ return __builtin_clzll(n);
+#else
+# error Unknown compiler
+#endif
+}
+
}

MODIFY
util/compiler.h
util/compiler.h
@@ -42,5 +42,6 @@ struct const_strip_unique_ptr {
unsigned ilog2(uint64_t n);
unsigned num_sign_bits(uint64_t n);
+unsigned num_leading_zeros(uint64_t n);
}

MODIFY
util/errors.cpp
util/errors.cpp
@@ -7,13 +7,13 @@ using namespace std;
namespace util {
-void Errors::add(const char *str) {
+void Errors::add(string &&str) {
errs.emplace_back(str);
}
ostream& operator<<(ostream &os, const Errors &errs) {
for (auto &err : errs.errs) {
- os << "Error: " << err << '\n';
+ os << "ERROR: " << err << '\n';
}
return os;
}

MODIFY
util/errors.h
util/errors.h
@@ -13,7 +13,7 @@ class Errors {
std::vector<std::string> errs;
public:
- void add(const char *str);
+ void add(std::string &&str);
explicit operator bool() const { return !errs.empty(); }
friend std::ostream& operator<<(std::ostream &os, const Errors &e);

add initial counterexample printing support