expriment with manualing instantiating all ty_%input vars (only 3 values each)
MODIFY
ir/function.h
ir/function.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/instr.h"
+#include "ir/value.h"
#include "smt/expr.h"
#include "util/compiler.h"
#include <memory>

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -348,7 +348,7 @@ StateValue Freeze::toSMT(State &s) const {
return { p.isFalse() ?
move(undet) :
- expr::mkIf(p, v, undet),
+ expr::mkIf(p, v, std::move(undet)),
true };
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -77,7 +77,7 @@ const StateValue& State::operator[](const Value &val) {
}
tmp_values[i_tmp_values] =
- { sval.value.replace(repls), sval.non_poison.replace(repls) };
+ { sval.value.subst(repls), sval.non_poison.subst(repls) };
return tmp_values[i_tmp_values++];
}

MODIFY
ir/value.cpp
ir/value.cpp
@@ -87,8 +87,7 @@ void Input::print(std::ostream &os) const {
StateValue Input::toSMT(State &s) const {
// 00: normal, 01: undef, else: poison
- string tyname = "ty_" + getName();
- expr type = expr::mkVar(tyname.c_str(), 2);
+ expr type = getTyVar();
auto bw = bits();
string uname = UndefValue::getFreshName();
@@ -101,4 +100,9 @@ StateValue Input::toSMT(State &s) const {
type.extract(1,1) == expr::mkUInt(0, 1) };
}
+expr Input::getTyVar() const {
+ string tyname = "ty_" + getName();
+ return expr::mkVar(tyname.c_str(), 2);
+}
+
}

MODIFY
ir/value.h
ir/value.h
@@ -76,6 +76,7 @@ public:
Value(type, std::move(name)) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
+ smt::expr getTyVar() const;
};
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -716,7 +716,7 @@ expr expr::mkIf(const expr &cond, const expr &then, const expr &els) {
}
expr expr::mkForAll(const set<expr> &vars, expr &&val) {
- if (vars.empty() || val.isTrue() || val.isFalse())
+ if (vars.empty() || val.isTrue() || val.isFalse() || !val.isValid())
return move(val);
unique_ptr<Z3_app[]> vars_ast(new Z3_app[vars.size()]);
@@ -728,12 +728,19 @@ expr expr::mkForAll(const set<expr> &vars, expr &&val) {
val());
}
-expr expr::replace(vector<pair<expr, expr>> &repls) const {
+expr expr::simplify() const {
+ C();
+ return Z3_simplify(ctx(), ast());
+}
+
+expr expr::subst(vector<pair<expr, expr>> &repls) const {
+ C();
unique_ptr<Z3_ast[]> from(new Z3_ast[repls.size()]);
unique_ptr<Z3_ast[]> to(new Z3_ast[repls.size()]);
unsigned i = 0;
for (auto &p : repls) {
+ C2(p.first, p.second);
from[i] = p.first();
to[i] = p.second();
++i;
@@ -741,6 +748,13 @@ expr expr::replace(vector<pair<expr, expr>> &repls) const {
return Z3_substitute(ctx(), ast(), repls.size(), from.get(), to.get());
}
+expr expr::subst(const expr &from, const expr &to) const {
+ C(from, to);
+ auto f = from();
+ auto t = to();
+ return Z3_substitute(ctx(), ast(), 1, &f, &t);
+}
+
ostream& operator<<(ostream &os, const expr &e) {
return os << (e.isValid() ? Z3_ast_to_string(ctx(), e()) : "(null)");
}

MODIFY
smt/expr.h
smt/expr.h
@@ -166,8 +166,11 @@ public:
static expr mkIf(const expr &cond, const expr &then, const expr &els);
static expr mkForAll(const std::set<expr> &vars, expr &&val);
+ expr simplify() const;
+
// replace v1 -> v2
- expr replace(std::vector<std::pair<expr, expr>> &repls) const;
+ expr subst(std::vector<std::pair<expr, expr>> &repls) const;
+ expr subst(const expr &from, const expr &to) const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);

MODIFY
smt/smt.cpp
smt/smt.cpp
#include "smt/smt.h"
#include "smt/ctx.h"
+#include <cstdint>
#include <z3.h>
namespace smt {
@@ -27,4 +28,16 @@ const char* get_query_timeout() {
return query_timeout;
}
+
+// FIXME make this configurable
+static uint64_t z3_memory_limit = 1ull << 30; // 1 GB
+
+bool hit_memory_limit() {
+ return Z3_get_estimated_alloc_size() >= z3_memory_limit;
+}
+
+bool hit_half_memory_limit() {
+ return Z3_get_estimated_alloc_size() >= (z3_memory_limit / 2);
+}
+
}

MODIFY
smt/smt.h
smt/smt.h
@@ -14,4 +14,7 @@ struct smt_initializer {
void set_query_timeout(const char *ms);
const char* get_query_timeout();
+bool hit_memory_limit();
+bool hit_half_memory_limit();
+
}

MODIFY
smt/solver.cpp
smt/solver.cpp
#include "util/compiler.h"
#include "util/config.h"
#include <iomanip>
+#include <iostream>
#include <z3.h>
using namespace smt;
@@ -75,6 +76,11 @@ SolverPop::~SolverPop() {
}
+static bool print_queries = false;
+void solver_print_queries(bool yes) {
+ print_queries = yes;
+}
+
Solver::Solver() {
// FIXME: implement a tactic
s = Z3_mk_simple_solver(ctx());
@@ -118,10 +124,12 @@ Result Solver::check() const {
if (!valid) {
++num_invalid;
- return Result::UNKNOWN;
+ return Result::INVALID;
}
++num_queries;
+ if (print_queries)
+ cout << "\nSMT query:\n" << Z3_solver_to_string(ctx(), s);
switch (Z3_solver_check(ctx(), s)) {
case Z3_L_FALSE:
@@ -129,7 +137,7 @@ Result Solver::check() const {
return Result::UNSAT;
case Z3_L_TRUE:
++num_sats;
- return { Z3_solver_get_model(ctx(), s), Result::SAT };
+ return Z3_solver_get_model(ctx(), s);
case Z3_L_UNDEF:
++num_unknown;
return Result::UNKNOWN;
@@ -138,28 +146,25 @@ Result Solver::check() const {
}
}
-Result Solver::check(const expr &e) {
- if (!e.isValid()) {
+void Solver::check(initializer_list<E> queries) {
+ for (auto &[q, error] : queries) {
+ if (!q.isValid()) {
++num_invalid;
- return Result::UNKNOWN;
+ error(Result::INVALID);
+ return;
}
- if (e.isFalse()) {
+ if (q.isFalse()) {
++num_trivial;
- return Result::UNSAT;
- }
-
- // FIXME: benchmark: is push/pop the best?
- auto pop = push();
- add(e);
- return check();
+ continue;
}
-void Solver::check(initializer_list<E> queries) {
- for (auto &[q, error] : queries) {
- auto res = check(q);
- if (res.isSat()) {
- error(res.m);
+ // TODO: benchmark: reset() or new solver every time?
+ Solver s;
+ s.add(q);
+ auto res = s.check();
+ if (!res.isUnsat()) {
+ error(res);
return;
}
}

MODIFY
smt/solver.h
smt/solver.h
@@ -54,12 +54,13 @@ public:
class Result {
public:
- enum answer { UNSAT, SAT, UNKNOWN };
+ enum answer { UNSAT, SAT, INVALID, UNKNOWN };
Result() : a(UNKNOWN) {}
bool isSat() const { return a == SAT; }
bool isUnsat() const { return a == UNSAT; }
+ bool isInvalid() const { return a == INVALID; }
bool isUnknown() const { return a == UNKNOWN; }
const Model& getModel() const {
@@ -72,7 +73,7 @@ private:
answer a;
Result(answer a) : a(a) {}
- Result(Z3_model m, answer a) : m(m), a(a) {}
+ Result(Z3_model m) : m(m), a(SAT) {}
friend class Solver;
};
@@ -92,7 +93,7 @@ public:
class Solver {
Z3_solver s;
bool valid = true;
- using E = std::pair<expr, std::function<void(const Model &m)>>;
+ using E = std::pair<expr, std::function<void(const Result &r)>>;
public:
Solver();
~Solver();
@@ -103,13 +104,13 @@ public:
void reset();
Result check() const;
- Result check(const expr &e);
- void check(std::initializer_list<E> queries);
+ static void check(std::initializer_list<E> queries);
friend class SolverPop;
};
+void solver_print_queries(bool yes);
void solver_print_stats(std::ostream &os);

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -25,7 +25,8 @@ static void show_help() {
" -v\t\tVerbose mode\n"
" -smt-stats\tShow SMT statistics\n"
" -smt-to:x\tTimeout for SMT queries in ms\n"
- " -skip-smt\tAssume all SMT queries are UNSAT\n"
+ " -smt-verbose\tPrint all SMT queries\n"
+ " -skip-smt\tSkip all SMT queries\n"
" -h / --help\tShow this help\n";
}
@@ -50,6 +51,8 @@ int main(int argc, char **argv) {
show_smt_stats = true;
else if (arg.compare(0, 8, "-smt-to:") == 0 && arg.size() > 8)
smt::set_query_timeout(arg.substr(8).data());
+ else if (arg == "-smt-verbose")
+ smt::solver_print_queries(true);
else if (arg == "-skip-smt")
config::skip_smt = true;
else if (arg == "-h" || arg == "--help") {

MODIFY
tools/transform.cpp
tools/transform.cpp
#include "tools/transform.h"
#include "ir/state.h"
#include "smt/expr.h"
+#include "smt/smt.h"
#include "smt/solver.h"
#include "util/errors.h"
#include "util/symexec.h"
using namespace IR;
using namespace smt;
+using namespace tools;
using namespace util;
using namespace std;
-static void check_refinement(Solver &s, Errors &errs,
+
+static expr preprocess(Transform &t, const set<expr> &qvars,
+ const set<expr> &undef_qvars, expr && e) {
+ if (qvars.empty() || e.isFalse())
+ return move(e);
+
+ // TODO: maybe try to instantiate undet_xx vars?
+ if (undef_qvars.empty() || hit_half_memory_limit())
+ return expr::mkForAll(qvars, move(e));
+
+ // manually instantiate all ty_%v vars
+ set<expr> instances({ move(e) });
+ set<expr> instances2;
+
+ expr nums[3] = { expr::mkUInt(0, 2), expr::mkUInt(1, 2), expr::mkUInt(2, 2) };
+
+ for (auto &i : t.src.getInputs()) {
+ auto var = static_cast<const Input&>(i).getTyVar();
+
+ for (auto &e : instances) {
+ for (unsigned i = 0; i <= 2; ++i) {
+ expr newexpr = e.subst(var, nums[i]);
+ if (newexpr.eq(e))
+ break;
+
+ newexpr = newexpr.simplify();
+ if (newexpr.isFalse())
+ continue;
+ instances2.emplace(move(newexpr));
+ }
+ }
+ instances = move(instances2);
+ }
+
+ expr insts(false);
+ for (auto &e : instances) {
+ insts |= e;
+ }
+
+ // TODO: try out instantiating the undefs in forall quantifier
+
+ return expr::mkForAll(qvars, move(insts));
+}
+
+
+static void check_refinement(Errors &errs, Transform &t,
const set<expr> &global_qvars,
const expr &dom_a, const State::ValTy &ap,
const expr &dom_b, const State::ValTy &bp) {
@@ -24,15 +71,16 @@ static void check_refinement(Solver &s, Errors &errs,
qvars.insert(ap.second.begin(), ap.second.end());
// TODO: improve error messages
- s.check({
- { expr::mkForAll(qvars, dom_a.notImplies(dom_b)),
- [&](const Model &m) { errs.add("Source is more defined than target"); } },
+ Solver::check({
+ { preprocess(t, qvars, ap.second, dom_a.notImplies(dom_b)),
+ [&](const Result &r) { errs.add("Source is more defined than target"); }},
- { expr::mkForAll(qvars, dom_a && a.non_poison.notImplies(b.non_poison)),
- [&](const Model &m) {errs.add("Target is more poisonous than source"); }},
+ { 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");}},
- { expr::mkForAll(qvars, dom_a && a.non_poison && a.value != b.value),
- [&](const Model &m) { errs.add("value mismatch"); } }
+ { preprocess(t, qvars, ap.second, dom_a && a.non_poison && a.value != b.value),
+ [&](const Result &r) { errs.add("value mismatch"); } }
});
}
@@ -54,7 +102,6 @@ Errors TransformVerify::verify() const {
sym_exec(tgt_state);
Errors errs;
- Solver s;
if (check_each_var) {
for (auto &[var, val] : src_state.getValues()) {
@@ -63,7 +110,7 @@ Errors TransformVerify::verify() const {
continue;
// TODO: add data-flow domain tracking for Alive, but not for TV
- check_refinement(s, errs, src_state.getQuantVars(),
+ check_refinement(errs, t, src_state.getQuantVars(),
true, val, true, tgt_state.at(*tgt_vals.at(name)));
if (errs)
return errs;
@@ -77,7 +124,7 @@ Errors TransformVerify::verify() const {
errs.add("Target returns but source doesn't");
} else if (src_state.fnReturned()) {
- check_refinement(s, errs, src_state.getQuantVars(),
+ check_refinement(errs, t, src_state.getQuantVars(),
src_state.returnDomain(), src_state.returnVal(),
tgt_state.returnDomain(), tgt_state.returnVal());
}

expriment with manualing instantiating all ty_%input vars (only 3 values each)