further simplifications & memory reductions to refinement check
MODIFY
ir/state.h
ir/state.h
@@ -220,6 +220,7 @@ public:
void finishInitializer();
auto& getFn() const { return f; }
+ auto& getMemory() const { return memory; }
auto& getMemory() { return memory; }
auto& getAxioms() const { return axioms; }
auto& getPre() const { return precondition; }

MODIFY
ir/type.cpp
ir/type.cpp
@@ -289,7 +289,7 @@ void VoidType::fixup(const Model &m) {
}
pair<expr, expr>
-VoidType::refines(State &src_s, State &tgt_s, const StateValue &src,
+VoidType::refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const {
return { true, true };
}
@@ -299,7 +299,7 @@ expr VoidType::mkInput(State &s, const char *name,
UNREACHABLE();
}
-void VoidType::printVal(ostream &os, State &s, const expr &e) const {
+void VoidType::printVal(ostream &os, const State &s, const expr &e) const {
UNREACHABLE();
}
@@ -347,7 +347,7 @@ expr IntType::enforceIntType(unsigned bits) const {
}
pair<expr, expr>
-IntType::refines(State &src_s, State &tgt_s, const StateValue &src,
+IntType::refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const {
return { src.non_poison.implies(tgt.non_poison),
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
@@ -358,7 +358,7 @@ expr IntType::mkInput(State &s, const char *name,
return expr::mkVar(name, bits());
}
-void IntType::printVal(ostream &os, State &s, const expr &e) const {
+void IntType::printVal(ostream &os, const State &s, const expr &e) const {
e.printHexadecimal(os);
os << " (";
e.printUnsigned(os);
@@ -533,8 +533,8 @@ expr FloatType::enforceFloatType() const {
}
pair<expr, expr>
-FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
- const StateValue &tgt) const {
+FloatType::refines(const State &src_s, const State &tgt_s,
+ const StateValue &src, const StateValue &tgt) const {
expr non_poison = src.non_poison && tgt.non_poison;
return { src.non_poison.implies(tgt.non_poison),
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
@@ -552,7 +552,7 @@ expr FloatType::mkInput(State &s, const char *name,
UNREACHABLE();
}
-void FloatType::printVal(ostream &os, State &s, const expr &e) const {
+void FloatType::printVal(ostream &os, const State &s, const expr &e) const {
if (e.isNaN().isTrue()) {
os << "NaN";
return;
@@ -652,7 +652,7 @@ StateValue PtrType::fromInt(StateValue v) const {
}
pair<expr, expr>
-PtrType::refines(State &src_s, State &tgt_s, const StateValue &src,
+PtrType::refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const {
auto sm = src_s.returnMemory(), tm = tgt_s.returnMemory();
Pointer p(sm, src.value);
@@ -672,7 +672,7 @@ PtrType::mkUndefInput(State &s, const ParamAttrs &attrs) const {
return s.getMemory().mkUndefInput(attrs);
}
-void PtrType::printVal(ostream &os, State &s, const expr &e) const {
+void PtrType::printVal(ostream &os, const State &s, const expr &e) const {
os << Pointer(s.getMemory(), e);
}
@@ -926,8 +926,8 @@ StateValue AggregateType::fromInt(StateValue v) const {
}
pair<expr, expr>
-AggregateType::refines(State &src_s, State &tgt_s, const StateValue &src,
- const StateValue &tgt) const {
+AggregateType::refines(const State &src_s, const State &tgt_s,
+ const StateValue &src, const StateValue &tgt) const {
set<expr> poison, value;
for (unsigned i = 0; i < elements; ++i) {
auto [p, v] = children[i]->refines(src_s, tgt_s, extract(src, i),
@@ -954,7 +954,7 @@ unsigned AggregateType::numPointerElements() const {
return count;
}
-void AggregateType::printVal(ostream &os, State &s, const expr &e) const {
+void AggregateType::printVal(ostream &os, const State &s, const expr &e) const {
UNREACHABLE();
}
@@ -1360,8 +1360,8 @@ StateValue SymbolicType::fromInt(StateValue val) const {
}
pair<expr, expr>
-SymbolicType::refines(State &src_s, State &tgt_s, const StateValue &src,
- const StateValue &tgt) const {
+SymbolicType::refines(const State &src_s, const State &tgt_s,
+ const StateValue &src, const StateValue &tgt) const {
DISPATCH(refines(src_s, tgt_s, src, tgt), UNREACHABLE());
}
@@ -1375,7 +1375,7 @@ SymbolicType::mkUndefInput(State &st, const ParamAttrs &attrs) const {
DISPATCH(mkUndefInput(st, attrs), UNREACHABLE());
}
-void SymbolicType::printVal(ostream &os, State &st, const expr &e) const {
+void SymbolicType::printVal(ostream &os, const State &st, const expr &e) const {
DISPATCH(printVal(os, st, e), UNREACHABLE());
}

MODIFY
ir/type.h
ir/type.h
@@ -107,7 +107,7 @@ public:
// returns pair of refinement constraints for <poison, !poison && value>
virtual std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const = 0;
virtual smt::expr
@@ -115,7 +115,7 @@ public:
virtual std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const;
- virtual void printVal(std::ostream &os, State &s,
+ virtual void printVal(std::ostream &os, const State &s,
const smt::expr &e) const = 0;
virtual void print(std::ostream &os) const = 0;
@@ -136,11 +136,12 @@ public:
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
+ void printVal(std::ostream &os, const State &s,
+ const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -163,11 +164,12 @@ public:
bool isIntType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
+ void printVal(std::ostream &os, const State &s,
+ const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -208,11 +210,12 @@ public:
smt::expr fromInt(smt::expr v) const override;
IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
+ void printVal(std::ostream &os, const State &s,
+ const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -240,13 +243,14 @@ public:
smt::expr fromInt(smt::expr v) const override;
IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
+ void printVal(std::ostream &os, const State &s,
+ const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -296,12 +300,13 @@ public:
smt::expr fromInt(smt::expr v) const override;
IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
unsigned numPointerElements() const;
- void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
+ void printVal(std::ostream &os, const State &s,
+ const smt::expr &e) const override;
const AggregateType* getAsAggregateType() const override;
};
@@ -402,14 +407,15 @@ public:
smt::expr fromInt(smt::expr v) const override;
IR::StateValue fromInt(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
- refines(State &src_s, State &tgt_s, const StateValue &src,
+ refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs)
const override;
std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const override;
- void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
+ void printVal(std::ostream &os, const State &s,
+ const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
smt/solver.cpp
smt/solver.cpp
#include <iomanip>
#include <iostream>
#include <optional>
+#include <string_view>
#include <utility>
#include <vector>
#include <z3.h>
@@ -208,15 +209,6 @@ ostream& operator<<(ostream &os, const Model &m) {
}
-SolverPush::SolverPush(Solver &s) : s(s) {
- Z3_solver_push(ctx(), s.s);
-}
-
-SolverPush::~SolverPush() {
- Z3_solver_pop(ctx(), s.s, 1);
-}
-
-
static bool print_queries = false;
void solver_print_queries(bool yes) {
print_queries = yes;
@@ -238,7 +230,9 @@ Solver::~Solver() {
}
void Solver::add(const expr &e) {
- if (e.isValid()) {
+ if (e.isFalse()) {
+ is_unsat = true;
+ } else if (e.isValid()) {
auto ast = e();
Z3_solver_assert(ctx(), s, ast);
tactic->add(ast);
@@ -288,16 +282,21 @@ expr Solver::assertions() const {
}
Result Solver::check() const {
- if (config::skip_smt) {
- ++num_skips;
- return Result::SKIP;
- }
-
if (!valid) {
++num_invalid;
return Result::INVALID;
}
+ if (is_unsat) {
+ ++num_trivial;
+ return Result::UNSAT;
+ }
+
+ if (config::skip_smt) {
+ ++num_skips;
+ return Result::SKIP;
+ }
+
++num_queries;
if (print_queries)
cout << "\nSMT query:\n" << Z3_solver_to_string(ctx(), s) << endl;
@@ -312,48 +311,35 @@ Result Solver::check() const {
++num_sats;
return Z3_solver_get_model(ctx(), s);
case Z3_L_UNDEF: {
- string reason = Z3_solver_get_reason_unknown(ctx(), s);
+ string_view reason = Z3_solver_get_reason_unknown(ctx(), s);
if (reason == "timeout") {
++num_timeout;
return Result::TIMEOUT;
}
++num_errors;
- return { Result::ERROR, move(reason) };
+ return { Result::ERROR, string(reason) };
}
default:
UNREACHABLE();
}
}
-bool Solver::check(expr &&q, std::function<void(const Result &r)> &&error) {
- if (!q.isValid()) {
- ++num_invalid;
- error(Result::INVALID);
- return false;
+Result check_expr(const expr &e) {
+ Solver s;
+ s.add(e);
+ return s.check();
}
- if (q.isFalse()) {
- ++num_trivial;
- return true;
- }
- // TODO: benchmark: reset() or new solver every time?
- Solver s;
- s.add(q);
- auto res = s.check();
- if (!res.isUnsat()) {
- error(res);
- return false;
- }
- return true;
+SolverPush::SolverPush(Solver &s) : s(s) {
+ Z3_solver_push(ctx(), s.s);
}
-Result check_expr(const expr &e) {
- Solver s;
- s.add(e);
- return s.check();
+SolverPush::~SolverPush() {
+ Z3_solver_pop(ctx(), s.s, 1);
}
+
void solver_print_stats(ostream &os) {
float total = num_queries / 100.0;
float trivial_pc = num_queries == 0 ? 0 :

MODIFY
smt/solver.h
smt/solver.h
#include "smt/expr.h"
#include <cassert>
-#include <cstdint>
-#include <functional>
#include <ostream>
#include <string>
#include <utility>
@@ -90,19 +88,11 @@ private:
};
-class Solver;
-
-class SolverPush {
- Solver &s;
-public:
- SolverPush(Solver &s);
- ~SolverPush();
-};
-
-
class Solver {
Z3_solver s;
bool valid = true;
+ bool is_unsat = false;
+
public:
Solver(bool simple = false);
~Solver();
@@ -115,8 +105,6 @@ public:
expr assertions() const;
Result check() const;
- // Return true if the query is successfully proven to be UNSAT
- static bool check(expr &&query, std::function<void(const Result &r)> &&err);
friend class SolverPush;
};
@@ -124,6 +112,14 @@ public:
Result check_expr(const expr &e);
+class SolverPush {
+ Solver &s;
+public:
+ SolverPush(Solver &s);
+ ~SolverPush();
+};
+
+
void solver_print_queries(bool yes);
void solver_tactic_verbose(bool yes);
void solver_print_stats(std::ostream &os);

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -33,7 +33,7 @@ static bool is_arbitrary(const expr &e) {
isUnsat();
}
-static void print_single_varval(ostream &os, State &st, const Model &m,
+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 (!val.isValid()) {
@@ -82,7 +82,7 @@ static void print_single_varval(ostream &os, State &st, const Model &m,
}
}
-static void print_varval(ostream &os, State &st, const Model &m,
+static void print_varval(ostream &os, const State &st, const Model &m,
const Value *var, const Type &type,
const StateValue &val, unsigned child = 0) {
if (!type.isAggregateType()) {
@@ -104,7 +104,7 @@ static void print_varval(ostream &os, State &st, const Model &m,
using print_var_val_ty = function<void(ostream&, const Model&)>;
-static void error(Errors &errs, State &src_state, State &tgt_state,
+static void error(Errors &errs, const State &src_state, const State &tgt_state,
const Result &r, const Value *var,
const char *msg, bool check_each_var,
print_var_val_ty print_var_val) {
@@ -354,8 +354,8 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
}
static void
-check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
- const Value *var, const Type &type,
+check_refinement(Errors &errs, const Transform &t, const State &src_state,
+ const State &tgt_state, const Value *var, const Type &type,
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) {
@@ -433,39 +433,38 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
preprocess(t, qvars, uvars, pre && pre_src_forall.implies(refines));
};
- // 1. Check UB
- auto err = [&](const Result &r, print_var_val_ty print, const char *msg) {
- error(errs, src_state, tgt_state, r, var, msg, check_each_var, print);
+ auto check = [&](expr &&e, auto &&printer, const char *msg) -> bool{
+ e = mk_fml(move(e));
+ auto res = check_expr(e);
+ if (res.isUnsat()) {
+ return true;
+ } else {
+ error(errs, src_state, tgt_state, res, var, msg, check_each_var, printer);
+ return false;
+ }
};
- if (!Solver::check(
- mk_fml(fndom_a.notImplies(fndom_b)),
- [&](const Result &r) {
- err(r, [](ostream&, const Model&){},
- "Source is more defined than target");
- }))
- return;
+#define CHECK(fml, printer, msg) \
+ if (!check(fml, printer, msg)) \
+ return
+
+ // 1. Check UB
+ CHECK(fndom_a.notImplies(fndom_b),
+ [](ostream&, const Model&){}, "Source is more defined than target");
// 2. Check return domain (noreturn check)
+ {
expr dom_constr;
- if (dom_a.eq(fndom_a)) {
- if (dom_b.eq(fndom_b)) // A /\ B /\ A != B
+ if (dom_a.eq(fndom_a) && dom_b.eq(fndom_b)) { // A /\ B /\ A != B
dom_constr = false;
- else // A /\ B /\ A != C
- dom_constr = fndom_a && fndom_b && !dom_b;
- } else if (dom_b.eq(fndom_b)) { // A /\ B /\ C != B
- dom_constr = fndom_a && fndom_b && !dom_a;
} else {
dom_constr = (fndom_a && fndom_b) && dom_a != dom_b;
}
- if (!Solver::check(
- mk_fml(move(dom_constr)),
- [&](const Result &r) {
- err(r, [](ostream&, const Model&){},
+ CHECK(move(dom_constr),
+ [](ostream&, const Model&){},
"Source and target don't have the same return domain");
- }))
- return;
+ }
// 3. Check poison
auto print_value = [&](ostream &s, const Model &m) {
@@ -478,29 +477,15 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
expr dom = dom_a && dom_b;
- if (!Solver::check(
- mk_fml(dom && !move(poison_cnstr)),
- [&](const Result &r) {
- err(r, print_value, "Target is more poisonous than source");
- }))
- return;
+ CHECK(dom && !poison_cnstr,
+ print_value, "Target is more poisonous than source");
// 4. Check undef
- if (!Solver::check(
- mk_fml(dom && encode_undef_refinement(type, ap, bp)),
- [&](const Result &r) {
- err(r, print_value, "Target's return value is more undefined");
- }))
- return;
+ CHECK(dom && encode_undef_refinement(type, ap, bp),
+ print_value, "Target's return value is more undefined");
// 5. Check value
- if (!Solver::check(
- // value_cnstr is used by memrefine, so can't be moved
- mk_fml(dom && !value_cnstr),
- [&](const Result &r) {
- err(r, print_value, "Value mismatch");
- }))
- return;
+ CHECK(dom && !value_cnstr, print_value, "Value mismatch");
// 6. Check memory
auto src_mem = src_state.returnMemory();
@@ -518,12 +503,11 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
<< "\nTarget value: " << Byte(tgt_mem, m[tgt_mem.load(p, undef)()]);
};
- Solver::check(
- mk_fml(dom && !(memory_cnstr0.isTrue() ? memory_cnstr0
- : value_cnstr && memory_cnstr0)),
- [&](const Result &r) {
- err(r, print_ptr_load, "Mismatch in memory");
- });
+ CHECK(dom && !(memory_cnstr0.isTrue() ? memory_cnstr0
+ : value_cnstr && memory_cnstr0),
+ print_ptr_load, "Mismatch in memory");
+
+#undef CHECK
}
static bool has_nullptr(const Value *v) {

further simplifications & memory reductions to refinement check