fixes to fastmath over-approximations
we were getting some false positives because the check for cex impact wasnt conservative enough
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -320,15 +320,19 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, expr b,
non_poison &= !val.isInf();
}
if (fmath.flags & FastMathFlags::ARCP) {
+ val = expr::mkUF("arcp", { val }, val);
s.doesApproximation("arcp", val);
}
if (fmath.flags & FastMathFlags::Contract) {
+ val = expr::mkUF("contract", { val }, val);
s.doesApproximation("contract", val);
}
if (fmath.flags & FastMathFlags::Reassoc) {
+ val = expr::mkUF("reassoc", { val }, val);
s.doesApproximation("reassoc", val);
}
if (fmath.flags & FastMathFlags::AFN) {
+ val = expr::mkUF("afn", { val }, val);
s.doesApproximation("afn", val);
}
if (fmath.flags & FastMathFlags::NSZ && !only_input)
@@ -1285,9 +1289,7 @@ StateValue ConversionOp::toSMT(State &s) const {
break;
case Int2Ptr:
fn = [&](auto &&val, auto &to_type) -> StateValue {
- auto ret = s.getMemory().int2ptr(val);
- s.doesApproximation("inttoptr", ret);
- return { move(ret), true };
+ return { s.getMemory().int2ptr(val), true };
};
break;
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1620,7 +1620,9 @@ expr Memory::int2ptr(const expr &val) const {
assert(!memory_unused());
// TODO
expr null = Pointer::mkNullPointer(*this).release();
- return expr::mkIf(val == 0, null, expr::mkUF("int2ptr", { val }, null));
+ expr fn = expr::mkUF("int2ptr", { val }, null);
+ state->doesApproximation("inttoptr", fn);
+ return expr::mkIf(val == 0, null, fn);
}
expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -128,8 +128,7 @@ Z3_sort expr::sort() const {
Z3_decl expr::decl() const {
auto app = isApp();
- assert(app);
- return Z3_get_app_decl(ctx(), app);
+ return app ? Z3_get_app_decl(ctx(), app) : nullptr;
}
Z3_app expr::isApp() const {
@@ -217,7 +216,7 @@ expr expr::mkNumber(const char *n, const expr &type) {
return Z3_mk_numeral(ctx(), n, type.sort());
}
-expr expr::mkConst(Z3_func_decl decl) {
+expr expr::mkConst(Z3_decl decl) {
return Z3_mk_app(ctx(), decl, 0, {});
}

MODIFY
smt/expr.h
smt/expr.h
@@ -17,7 +17,6 @@ typedef struct _Z3_func_decl* Z3_decl;
typedef struct _Z3_app* Z3_app;
typedef struct _Z3_ast* Z3_ast;
typedef struct _Z3_sort* Z3_sort;
-typedef struct _Z3_func_decl* Z3_func_decl;
namespace smt {
@@ -64,7 +63,7 @@ class expr {
static Z3_ast mkFalse();
static expr mkUInt(uint64_t n, Z3_sort sort);
static expr mkInt(int64_t n, Z3_sort sort);
- static expr mkConst(Z3_func_decl decl);
+ static expr mkConst(Z3_decl decl);
bool isBinOp(expr &a, expr &b, int z3op) const;
@@ -358,7 +357,6 @@ public:
friend class Solver;
friend class Model;
- friend class ExprLeafIterator;
};

MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -185,6 +185,11 @@ int64_t Model::getInt(const expr &var) const {
return n;
}
+bool Model::hasFnModel(const expr &fn) const {
+ auto fn_decl = fn.decl();
+ return fn_decl ? Z3_model_has_interp(ctx(), m, fn_decl) : false;
+}
+
pair<expr, expr> Model::iterator::operator*(void) const {
auto decl = Z3_model_get_const_decl(ctx(), m, idx);
return { expr::mkConst(decl), Z3_model_get_const_interp(ctx(), m, decl) };

MODIFY
smt/solver.h
smt/solver.h
@@ -36,6 +36,7 @@ public:
expr eval(const expr &var, bool complete = false) const;
uint64_t getUInt(const expr &var) const;
int64_t getInt(const expr &var) const;
+ bool hasFnModel(const expr &fn) const;
class iterator {
Z3_model m;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -141,7 +141,7 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
for (auto *v : { &src_state.getApproximations(),
&tgt_state.getApproximations() }) {
for (auto &[msg, var] : *v) {
- if (!var || m.eval(*var).isConst())
+ if (!var || m.hasFnModel(*var))
approx.emplace(msg);
}
}

fixes to fastmath over-approximations
we were getting some false positives because the check for cex impact wasnt conservative enough