stub fast-math reassoc verification
This is a very complex property that needs to traverse expressions seen in the past
The code is not wired. DO NOT USE.
The egraph implementation is not complete
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -92,6 +92,7 @@ include_directories(${PROJECT_BINARY_DIR})
set(IR_SRCS
ir/attrs.cpp
ir/constant.cpp
+ ir/fast_math.cpp
ir/function.cpp
ir/globals.cpp
ir/instr.cpp

MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -71,6 +71,11 @@ ostream& operator<<(ostream &os, const FnAttrs &attr) {
return os;
}
+bool ParamAttrs::poisonImpliesUB() const {
+ return has(Dereferenceable) || has(NoUndef) || has(ByVal) ||
+ has(DereferenceableOrNull);
+}
+
bool ParamAttrs::undefImpliesUB() const {
bool ub = has(NoUndef) || has(Dereferenceable) || has(ByVal) ||
has(DereferenceableOrNull);
@@ -160,4 +165,26 @@ FnAttrs::encode(const State &s, const StateValue &val, const Type &ty) const {
return { move(UB), move(new_non_poison) };
}
+
+ostream& operator<<(ostream &os, const FastMathFlags &fm) {
+ if (fm.flags == FastMathFlags::FastMath)
+ return os << "fast ";
+
+ if (fm.flags & FastMathFlags::NNaN)
+ os << "nnan ";
+ if (fm.flags & FastMathFlags::NInf)
+ os << "ninf ";
+ if (fm.flags & FastMathFlags::NSZ)
+ os << "nsz ";
+ if (fm.flags & FastMathFlags::ARCP)
+ os << "arcp ";
+ if (fm.flags & FastMathFlags::Contract)
+ os << "contract ";
+ if (fm.flags & FastMathFlags::Reassoc)
+ os << "reassoc ";
+ if (fm.flags & FastMathFlags::AFN)
+ os << "afn ";
+ return os;
+}
+
}

MODIFY
ir/attrs.h
ir/attrs.h
@@ -32,9 +32,7 @@ public:
void set(Attribute a) { bits |= (unsigned)a; }
// Returns true if it's UB for the argument to be poison / have a poison elem.
- bool poisonImpliesUB() const
- { return has(Dereferenceable) || has(NoUndef) || has(ByVal) ||
- has(DereferenceableOrNull); }
+ bool poisonImpliesUB() const;
// Returns true if it is UB for the argument to be (partially) undef.
bool undefImpliesUB() const;
@@ -82,4 +80,17 @@ public:
encode(const State &s, const StateValue &val, const Type &ty) const;
};
+
+struct FastMathFlags final {
+ enum Flags {
+ None = 0, NNaN = 1 << 0, NInf = 1 << 1, NSZ = 1 << 2, ARCP = 1 << 3,
+ Contract = 1 << 4, Reassoc = 1 << 5, AFN = 1 << 6,
+ FastMath = NNaN | NInf | NSZ | ARCP | Contract | Reassoc | AFN
+ };
+ unsigned flags = None;
+
+ bool isNone() const { return flags == None; }
+ friend std::ostream& operator<<(std::ostream &os, const FastMathFlags &fm);
+};
+
}

ADD
ir/fast_math.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/fast_math.h"
+#include "ir/attrs.h"
+#include "util/unionfind.h"
+#include <map>
+
+#define DEBUG_FMF
+
+#ifdef DEBUG_FMF
+# include <iostream>
+#endif
+
+using namespace IR;
+using namespace smt;
+using namespace util;
+using namespace std;
+
+// Home-made e-graph to represent all possible fast-math reassociations
+
+namespace {
+
+class EGraph;
+
+struct Node {
+ enum { Add, Sub, Mul, Div, Neg, Leaf } operation;
+ unsigned op1 = 0, op2 = 0;
+ expr leaf;
+ // FIXME: we currently ignore rounding
+ expr rounding;
+ unsigned flags = 0;
+
+ auto operator<=>(const Node &other) const = default;
+
+#ifdef DEBUG_FMF
+ void print(ostream &os, EGraph &g) const;
+#endif
+};
+
+
+class EGraph {
+ UnionFind uf;
+ map<Node, unsigned> nodes;
+
+ unsigned get(Node &&n) {
+ auto [I, inserted] = nodes.try_emplace(move(n), 0);
+ if (inserted)
+ I->second = uf.mk();
+ return I->second;
+ }
+
+ void decl_equivalent(Node &&node, unsigned n1) {
+ unsigned n2 = nodes.try_emplace(move(node), n1).first->second;
+ uf.merge(n1, n2);
+ }
+
+public:
+ unsigned root(unsigned n) {
+ return uf.find(n);
+ }
+
+ unsigned get(const expr &e0) {
+ Node n;
+ expr rounding, a, b;
+ bool is_leaf = false;
+
+ expr e = e0;
+
+ while (true) {
+ if (e.isFPAdd(rounding, a, b)) {
+ n.op2 = get(b);
+ n.operation = Node::Add;
+ } else if (e.isFPSub(rounding, a, b)) {
+ n.op2 = get(b);
+ n.operation = Node::Sub;
+ } else if (e.isFPMul(rounding, a, b)) {
+ n.op2 = get(b);
+ n.operation = Node::Mul;
+ } else if (e.isFPDiv(rounding, a, b)) {
+ n.op2 = get(b);
+ n.operation = Node::Div;
+ } else if (e.isFPNeg(a)) {
+ n.operation = Node::Neg;
+ } else if (auto name = e.fn_name(); !name.empty()) {
+ if (name == "reassoc") {
+ n.flags |= FastMathFlags::Reassoc;
+ e = e.getFnArg(0);
+ continue;
+ }
+ is_leaf = true;
+ } else {
+ is_leaf = true;
+ }
+
+ if (is_leaf) {
+ n.operation = Node::Leaf;
+ n.leaf = move(e);
+ } else {
+ n.op1 = get(a);
+ n.rounding = move(rounding);
+ }
+
+ return get(move(n));
+ }
+ }
+
+ void saturate() {
+ while (true) {
+ auto nodes_copy = nodes;
+ for (auto &[node, n] : nodes_copy) {
+ // commutativity: x . y == y . x
+ // Always correct for add & mul regardless of fast-math
+ if (node.operation == Node::Add || node.operation == Node::Mul) {
+ Node nn = node;
+ swap(nn.op1, nn.op2);
+ decl_equivalent(move(nn), n);
+ }
+
+ if (node.flags & FastMathFlags::Reassoc) {
+ // distributivity: x . (y + z) == x . y + x . z
+
+ // associativity (x . y) . z == x . (y . z)
+
+ }
+
+ if (node.flags & FastMathFlags::Contract) {
+ // x / y == x * (1 / y)
+ // TODO
+ }
+ }
+ if (nodes.size() == nodes_copy.size())
+ return;
+ }
+ }
+
+#ifdef DEBUG_FMF
+ friend ostream& operator<<(ostream &os, EGraph &g) {
+ vector<vector<const Node*>> sorted;
+ for (auto &[node, n] : g.nodes) {
+ unsigned r = g.root(n);
+ if (r >= sorted.size())
+ sorted.resize(r + 1);
+ sorted[r].emplace_back(&node);
+ }
+
+ for (unsigned i = 0, e = sorted.size(); i != e; ++i) {
+ auto &nodes = sorted[i];
+ if (!nodes.empty()) {
+ os << "Root " << i << '\n';
+ for (auto *n : nodes) {
+ n->print(os << " ", g);
+ os << '\n';
+ }
+ }
+ }
+ return os;
+ }
+#endif
+};
+
+
+#ifdef DEBUG_FMF
+void Node::print(ostream &os, EGraph &g) const {
+ const char *op;
+ switch (operation) {
+ case Add: op = "add "; break;
+ case Sub: op = "sub "; break;
+ case Mul: op = "mul "; break;
+ case Div: op = "div "; break;
+ case Neg: op = "neg "; break;
+ case Leaf: op = "leaf "; break;
+ }
+ os << op;
+
+ if (operation == Leaf) {
+ os << leaf;
+ return;
+ }
+
+ os << g.root(op1);
+ if (operation != Neg) {
+ os << ", " << g.root(op2);
+ }
+
+ FastMathFlags fmf;
+ fmf.flags = flags;
+ if (!fmf.isNone())
+ os << "\t# " << fmf;
+}
+#endif
+
+}
+
+namespace IR {
+
+expr float_refined(const expr &a, const expr &b) {
+ EGraph g;
+ unsigned na = g.get(a);
+ unsigned nb = g.get(b);
+#ifdef DEBUG_FMF
+ cout << "Before saturate:\n" << g << "Roots: " << na << " / " << nb << "\n\n";
+#endif
+
+ if (na == nb)
+ return true;
+
+ g.saturate();
+
+ na = g.root(na);
+ nb = g.root(nb);
+#ifdef DEBUG_FMF
+ cout << "After saturate:\n" << g << "Roots: " << na << " / " << nb << "\n\n";
+#endif
+ if (na == nb)
+ return true;
+
+ // TODO
+ return false;
+}
+
+}

ADD
ir/fast_math.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "smt/expr.h"
+
+namespace IR {
+
+smt::expr float_refined(const smt::expr &a, const smt::expr &b);
+
+}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -109,28 +109,6 @@ expr Instr::getTypeConstraints() const {
}
-ostream& operator<<(ostream &os, const FastMathFlags &fm) {
- if (fm.flags == FastMathFlags::FastMath)
- return os << "fast ";
-
- if (fm.flags & FastMathFlags::NNaN)
- os << "nnan ";
- if (fm.flags & FastMathFlags::NInf)
- os << "ninf ";
- if (fm.flags & FastMathFlags::NSZ)
- os << "nsz ";
- if (fm.flags & FastMathFlags::ARCP)
- os << "arcp ";
- if (fm.flags & FastMathFlags::Contract)
- os << "contract ";
- if (fm.flags & FastMathFlags::Reassoc)
- os << "reassoc ";
- if (fm.flags & FastMathFlags::AFN)
- os << "afn ";
- return os;
-}
-
-
BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
unsigned flags, FastMathFlags fmath)
: Instr(type, move(name)), lhs(&lhs), rhs(&rhs), op(op), flags(flags),
@@ -650,8 +628,8 @@ StateValue BinOp::toSMT(State &s) const {
auto v = [&](expr &a, expr &b) {
expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
- expr neg_cond = (op == FMinimum) ? a.isFPNeg() || b.isFPNeg()
- : a.isFPNeg() && b.isFPNeg();
+ expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative())
+ : (a.isFPNegative() && b.isFPNegative());
expr e = expr::mkIf(a.isFPZero() && b.isFPZero(),
expr::mkIf(neg_cond, zneg, zpos),
expr::mkIf(cmp, a, b));

MODIFY
ir/instr.h
ir/instr.h
@@ -27,19 +27,6 @@ public:
};
-struct FastMathFlags final {
- enum Flags {
- None = 0, NNaN = 1 << 0, NInf = 1 << 1, NSZ = 1 << 2, ARCP = 1 << 3,
- Contract = 1 << 4, Reassoc = 1 << 5, AFN = 1 << 6,
- FastMath = NNaN | NInf | NSZ | ARCP | Contract | Reassoc | AFN
- };
- unsigned flags = None;
-
- bool isNone() const { return flags == None; }
- friend std::ostream& operator<<(std::ostream &os, const FastMathFlags &fm);
-};
-
-
class BinOp final : public Instr {
public:
enum Op { Add, Sub, Mul, SDiv, UDiv, SRem, URem, Shl, AShr, LShr,

MODIFY
ir/type.cpp
ir/type.cpp
@@ -569,9 +569,9 @@ void FloatType::printVal(ostream &os, const State &s, const expr &e) const {
e.float2BV().printHexadecimal(os);
os << " (";
if (e.isFPZero().isTrue()) {
- os << (e.isFPNeg().isTrue() ? "-0.0" : "+0.0");
+ os << (e.isFPNegative().isTrue() ? "-0.0" : "+0.0");
} else if (e.isInf().isTrue()) {
- os << (e.isFPNeg().isTrue() ? "-oo" : "+oo");
+ os << (e.isFPNegative().isTrue() ? "-oo" : "+oo");
} else {
os << e.float2Real().numeral_string();
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -253,6 +253,14 @@ expr expr::mkConst(Z3_decl decl) {
return Z3_mk_app(ctx(), decl, 0, {});
}
+bool expr::isUnOp(expr &a, int z3op) const {
+ if (auto app = isAppOf(z3op)) {
+ a = Z3_get_app_arg(ctx(), app, 0);
+ return true;
+ }
+ return false;
+}
+
bool expr::isBinOp(expr &a, expr &b, int z3op) const {
if (auto app = isAppOf(z3op)) {
if (Z3_get_app_num_args(ctx(), app) != 2)
@@ -264,6 +272,16 @@ bool expr::isBinOp(expr &a, expr &b, int z3op) const {
return false;
}
+bool expr::isTernaryOp(expr &a, expr &b, expr &c, int z3op) const {
+ if (auto app = isAppOf(z3op)) {
+ a = Z3_get_app_arg(ctx(), app, 0);
+ b = Z3_get_app_arg(ctx(), app, 1);
+ c = Z3_get_app_arg(ctx(), app, 2);
+ return true;
+ }
+ return false;
+}
+
expr expr::mkVar(const char *name, const expr &type) {
C2(type);
return ::mkVar(name, type.sort());
@@ -425,13 +443,7 @@ bool expr::isULE(expr &lhs, expr &rhs) const {
}
bool expr::isIf(expr &cond, expr &then, expr &els) const {
- if (auto app = isAppOf(Z3_OP_ITE)) {
- cond = Z3_get_app_arg(ctx(), app, 0);
- then = Z3_get_app_arg(ctx(), app, 1);
- els = Z3_get_app_arg(ctx(), app, 2);
- return true;
- }
- return false;
+ return isTernaryOp(cond, then, els, Z3_OP_ITE);
}
bool expr::isConcat(expr &a, expr &b) const {
@@ -460,11 +472,7 @@ bool expr::isExtract(expr &e, unsigned &high, unsigned &low) const {
}
bool expr::isSignExt(expr &val) const {
- if (auto app = isAppOf(Z3_OP_SIGN_EXT)) {
- val = Z3_get_app_arg(ctx(), app, 0);
- return true;
- }
- return false;
+ return isUnOp(val, Z3_OP_SIGN_EXT);
}
bool expr::isAnd(expr &a, expr &b) const {
@@ -472,11 +480,7 @@ bool expr::isAnd(expr &a, expr &b) const {
}
bool expr::isNot(expr &neg) const {
- if (auto app = isAppOf(Z3_OP_NOT)) {
- neg = Z3_get_app_arg(ctx(), app, 0);
- return true;
- }
- return false;
+ return isUnOp(neg, Z3_OP_NOT);
}
bool expr::isAdd(expr &a, expr &b) const {
@@ -505,30 +509,35 @@ bool expr::isBasePlusOffset(expr &base, uint64_t &offset) const {
}
bool expr::isConstArray(expr &val) const {
- if (auto app = isAppOf(Z3_OP_CONST_ARRAY)) {
- val = Z3_get_app_arg(ctx(), app, 0);
- return true;
- }
- return false;
+ return isUnOp(val, Z3_OP_CONST_ARRAY);
}
bool expr::isStore(expr &array, expr &idx, expr &val) const {
- if (auto app = isAppOf(Z3_OP_STORE)) { // store(array, idx, val)
- array = Z3_get_app_arg(ctx(), app, 0);
- idx = Z3_get_app_arg(ctx(), app, 1);
- val = Z3_get_app_arg(ctx(), app, 2);
- return true;
- }
- return false;
+ return isTernaryOp(array, idx, val, Z3_OP_STORE);
}
bool expr::isLoad(expr &array, expr &idx) const {
- if (auto app = isAppOf(Z3_OP_SELECT)) {
- array = Z3_get_app_arg(ctx(), app, 0);
- idx = Z3_get_app_arg(ctx(), app, 1);
- return true;
+ return isBinOp(array, idx, Z3_OP_SELECT);
}
- return false;
+
+bool expr::isFPAdd(expr &rounding, expr &lhs, expr &rhs) const {
+ return isTernaryOp(rounding, lhs, rhs, Z3_OP_FPA_ADD);
+}
+
+bool expr::isFPSub(expr &rounding, expr &lhs, expr &rhs) const {
+ return isTernaryOp(rounding, lhs, rhs, Z3_OP_FPA_SUB);
+}
+
+bool expr::isFPMul(expr &rounding, expr &lhs, expr &rhs) const {
+ return isTernaryOp(rounding, lhs, rhs, Z3_OP_FPA_MUL);
+}
+
+bool expr::isFPDiv(expr &rounding, expr &lhs, expr &rhs) const {
+ return isTernaryOp(rounding, lhs, rhs, Z3_OP_FPA_DIV);
+}
+
+bool expr::isFPNeg(expr &val) const {
+ return isUnOp(val, Z3_OP_FPA_NEG);
}
bool expr::isNaNCheck(expr &fp) const {
@@ -540,11 +549,7 @@ bool expr::isNaNCheck(expr &fp) const {
}
bool expr::isfloat2BV(expr &fp) const {
- if (auto app = isAppOf(Z3_OP_FPA_TO_IEEE_BV)) {
- fp = Z3_get_app_arg(ctx(), app, 0);
- return true;
- }
- return false;
+ return isUnOp(fp, Z3_OP_FPA_TO_IEEE_BV);
}
unsigned expr::min_leading_zeros() const {
@@ -967,12 +972,12 @@ expr expr::isFPZero() const {
return unop_fold(Z3_mk_fpa_is_zero);
}
-expr expr::isFPNeg() const {
+expr expr::isFPNegative() const {
return unop_fold(Z3_mk_fpa_is_negative);
}
expr expr::isFPNegZero() const {
- return isFPZero() && isFPNeg();
+ return isFPZero() && isFPNegative();
}
// TODO: make rounding mode customizable
@@ -2029,6 +2034,12 @@ string expr::fn_name() const {
return "";
}
+expr expr::getFnArg(unsigned i) const {
+ auto app = isApp();
+ assert(app && i < Z3_get_app_num_args(ctx(), app));
+ return Z3_get_app_arg(ctx(), app, i);
+}
+
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
@@ -56,7 +56,9 @@ class expr {
static expr mkInt(int64_t n, Z3_sort sort);
static expr mkConst(Z3_decl decl);
+ bool isUnOp(expr &a, int z3op) const;
bool isBinOp(expr &a, expr &b, int z3op) const;
+ bool isTernaryOp(expr &a, expr &b, expr &c, int z3op) const;
public:
expr() : ptr(0) {}
@@ -138,6 +140,11 @@ public:
bool isStore(expr &array, expr &idx, expr &val) const;
bool isLoad(expr &array, expr &idx) const;
+ bool isFPAdd(expr &rounding, expr &lhs, expr &rhs) const;
+ bool isFPSub(expr &rounding, expr &lhs, expr &rhs) const;
+ bool isFPMul(expr &rounding, expr &lhs, expr &rhs) const;
+ bool isFPDiv(expr &rounding, expr &lhs, expr &rhs) const;
+ bool isFPNeg(expr &neg) const;
bool isNaNCheck(expr &fp) const;
bool isfloat2BV(expr &fp) const;
@@ -198,7 +205,7 @@ public:
expr isNaN() const;
expr isInf() const;
expr isFPZero() const;
- expr isFPNeg() const;
+ expr isFPNegative() const;
expr isFPNegZero() const;
expr fadd(const expr &rhs) const;
@@ -333,6 +340,7 @@ public:
void printHexadecimal(std::ostream &os) const;
std::string numeral_string() const;
std::string fn_name() const; // empty if not a function
+ expr getFnArg(unsigned i) const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);
// for container use only

MODIFY
util/unionfind.cpp
util/unionfind.cpp
@@ -14,6 +14,12 @@ UnionFind::UnionFind(unsigned n) {
}
}
+unsigned UnionFind::mk() {
+ unsigned n = id.size();
+ id.push_back(n);
+ return n;
+}
+
unsigned UnionFind::find(unsigned i) {
unsigned root = i;
while (root != id[root])

MODIFY
util/unionfind.h
util/unionfind.h
@@ -10,7 +10,8 @@ namespace util {
class UnionFind final {
std::vector<unsigned> id;
public:
- UnionFind(unsigned n);
+ UnionFind(unsigned n = 0);
+ unsigned mk();
unsigned find(unsigned i);
void merge(unsigned p, unsigned q);
};

stub fast-math reassoc verification
This is a very complex property that needs to traverse expressions seen in the past
The code is not wired. DO NOT USE.
The egraph implementation is not complete