expand fast-math support in binop
implement NSZ for binops
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -45,14 +45,14 @@ expr Instr::getTypeConstraints() const {
BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
- Flags flags)
+ unsigned flags)
: Instr(type, move(name)), lhs(&lhs), rhs(&rhs), op(op), flags(flags) {
switch (op) {
case Add:
case Sub:
case Mul:
case Shl:
- assert((flags & NSWNUW) == flags);
+ assert((flags & (NSW | NUW)) == flags);
break;
case SDiv:
case UDiv:
@@ -65,7 +65,7 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case FMul:
case FDiv:
case FRem:
- assert((flags & NNANNINF) == flags);
+ assert((flags & FastMath) == flags);
break;
case SRem:
case URem:
@@ -133,20 +133,31 @@ void BinOp::print(ostream &os) const {
case FRem: str = "frem "; break;
}
- const char *flag = nullptr;
- switch (flags) {
- case None: flag = " "; break;
- case NSW: flag = " nsw "; break;
- case NUW: flag = " nuw "; break;
- case NSWNUW: flag = " nsw nuw "; break;
- case NNAN: flag = " nnan "; break;
- case NINF: flag = " ninf "; break;
- case NNANNINF: flag = " nnan ninf "; break;
- case Exact: flag = " exact "; break;
- }
+ os << getName() << " = " << str;
- os << getName() << " = " << str << flag << print_type(getType())
- << lhs->getName() << ", " << rhs->getName();
+ if (flags & NSW)
+ os << "nsw ";
+ if (flags & NUW)
+ os << "nuw ";
+ if (flags & Exact)
+ os << "exact ";
+ if ((flags & FastMath) == FastMath) {
+ os << "fast ";
+ } else {
+ if (flags & NNaN)
+ os << "nnan ";
+ if (flags & NInf)
+ os << "ninf ";
+ if (flags & NSZ)
+ os << "nsz ";
+ if (flags & ARCP)
+ os << "arcp ";
+ if (flags & Contract)
+ os << "contract ";
+ if (flags & Reassoc)
+ os << "reassoc ";
+ }
+ os << print_type(getType()) << lhs->getName() << ", " << rhs->getName();
}
static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
@@ -159,13 +170,18 @@ static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
}
static expr fm_poison(const expr &a, const expr &b, const expr &val,
- BinOp::Flags flags) {
+ unsigned flags) {
expr ret = false;
- if (flags & BinOp::NINF)
- ret |= a.isInf() || b.isInf() || val.isInf();
- if (flags & BinOp::NNAN)
+ if (flags & BinOp::NNaN)
ret |= a.isNaN() || b.isNaN() || val.isNaN();
-
+ if (flags & BinOp::NInf)
+ ret |= a.isInf() || b.isInf() || val.isInf();
+ if (flags & BinOp::ARCP)
+ ret |= expr(); // TODO
+ if (flags & BinOp::Contract)
+ ret |= expr(); // TODO
+ if (flags & BinOp::Reassoc)
+ ret |= expr(); // TODO
return ret;
}
@@ -174,6 +190,12 @@ StateValue BinOp::toSMT(State &s) const {
function<StateValue(const expr&, const expr&, const expr&, const expr&)>
fn, scalar_op;
+ auto fm_arg = [&](const expr &val) {
+ if (flags & NSZ)
+ return expr::mkIf(val.isFPNegZero(), expr::mkNumber("0", val), val);
+ return val;
+ };
+
switch (op) {
case Add:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
@@ -372,7 +394,7 @@ StateValue BinOp::toSMT(State &s) const {
case FAdd:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
- auto val = a.fadd(b);
+ auto val = fm_arg(a).fadd(fm_arg(b));
auto non_poison = !fm_poison(a, b, val, flags);
return { move(val), move(non_poison) };
};
@@ -380,7 +402,7 @@ StateValue BinOp::toSMT(State &s) const {
case FSub:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
- auto val = a.fsub(b);
+ auto val = fm_arg(a).fsub(fm_arg(b));
auto non_poison = !fm_poison(a, b, val, flags);
return { move(val), move(non_poison) };
};
@@ -388,7 +410,7 @@ StateValue BinOp::toSMT(State &s) const {
case FMul:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
- auto val = a.fmul(b);
+ auto val = fm_arg(a).fmul(fm_arg(b));
auto non_poison = !fm_poison(a, b, val, flags);
return { move(val), move(non_poison) };
};
@@ -396,7 +418,7 @@ StateValue BinOp::toSMT(State &s) const {
case FDiv:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
- auto val = a.fdiv(b);
+ auto val = fm_arg(a).fdiv(fm_arg(b));
auto non_poison = !fm_poison(a, b, val, flags);
return { move(val), move(non_poison) };
};

MODIFY
ir/instr.h
ir/instr.h
@@ -35,17 +35,19 @@ public:
SMul_Overflow, UMul_Overflow,
FAdd, FSub, FMul, FDiv, FRem,
And, Or, Xor, Cttz, Ctlz };
- enum Flags { None = 0, NSW = 1, NUW = 2, NSWNUW = 3, Exact = 4,
- NNAN = 8, NINF = 16, NNANNINF = 24};
+ enum Flags { None = 0, NSW = 1 << 0, NUW = 1 << 1, Exact = 1 << 2,
+ NNaN = 1 << 3, NInf = 1 << 4, NSZ = 1 << 5, ARCP = 1 << 6,
+ Contract = 1 << 7, Reassoc = 1 << 8,
+ FastMath = NNaN | NInf | NSZ | ARCP | Contract | Reassoc };
private:
Value *lhs, *rhs;
Op op;
- Flags flags;
+ unsigned flags;
public:
BinOp(Type &type, std::string &&name, Value &lhs, Value &rhs, Op op,
- Flags flags = None);
+ unsigned flags = 0);
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -128,23 +128,23 @@ public:
if (isa<llvm::PossiblyExactOperator>(i) && i.isExact())
flags = BinOp::Exact;
- if (isa<llvm::FPMathOperator>(i) && i.getFastMathFlags().noNaNs())
- flags |= BinOp::NNAN;
- if (isa<llvm::FPMathOperator>(i) && i.getFastMathFlags().noInfs())
- flags |= BinOp::NINF;
-
- // TODO: support FP fast-math stuff
- if (isa<llvm::FPMathOperator>(i) && i.getFastMathFlags().any()) {
- auto FMFlag = i.getFastMathFlags();
- if (FMFlag.allowReassoc() || FMFlag.allowReciprocal() ||
- FMFlag.allowContract() || FMFlag.approxFunc() ||
- FMFlag.noSignedZeros () || FMFlag.isFast())
- return error(i);
+ if (isa<llvm::FPMathOperator>(i)) {
+ auto FM = i.getFastMathFlags();
+ if (FM.noNaNs())
+ flags |= BinOp::NNaN;
+ if (FM.noInfs())
+ flags |= BinOp::NInf;
+ if (FM.noSignedZeros())
+ flags |= BinOp::NSZ;
+ if (FM.allowReciprocal())
+ flags |= BinOp::ARCP;
+ if (FM.allowContract())
+ flags |= BinOp::Contract;
+ if (FM.allowReassoc())
+ flags |= BinOp::Reassoc;
}
-
-
RETURN_IDENTIFIER(make_unique<BinOp>(*ty, value_name(i), *a, *b, alive_op,
- (BinOp::Flags)flags));
+ flags));
}
RetTy visitCastInst(llvm::CastInst &i) {

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -701,6 +701,10 @@ expr expr::isFPNeg() const {
return unop_fold(Z3_mk_fpa_is_negative);
}
+expr expr::isFPNegZero() const {
+ return isFPZero() && isFPNeg();
+}
+
// TODO: make rounding mode customizable
expr expr::fadd(const expr &rhs) const {
C(rhs);

MODIFY
smt/expr.h
smt/expr.h
@@ -169,6 +169,7 @@ public:
expr isInf() const;
expr isFPZero() const;
expr isFPNeg() const;
+ expr isFPNegZero() const;
expr fadd(const expr &rhs) const;
expr fsub(const expr &rhs) const;

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -547,13 +547,13 @@ static Value& parse_operand(Type &type) {
UNREACHABLE();
}
-static BinOp::Flags parse_nsw_nuw() {
- BinOp::Flags flags = BinOp::None;
+static unsigned parse_nsw_nuw() {
+ unsigned flags = BinOp::None;
while (true) {
if (tokenizer.consumeIf(NSW)) {
- flags = (BinOp::Flags)(flags | BinOp::NSW);
+ flags |= BinOp::NSW;
} else if (tokenizer.consumeIf(NUW)) {
- flags = (BinOp::Flags)(flags | BinOp::NUW);
+ flags |= BinOp::NUW;
} else {
break;
}
@@ -561,19 +561,19 @@ static BinOp::Flags parse_nsw_nuw() {
return flags;
}
-static BinOp::Flags parse_exact() {
+static unsigned parse_exact() {
if (tokenizer.consumeIf(EXACT))
return BinOp::Exact;
return BinOp::None;
}
-static BinOp::Flags parse_fast_math() {
- BinOp::Flags flags = BinOp::None;
+static unsigned parse_fast_math() {
+ unsigned flags = BinOp::None;
while (true) {
- if (tokenizer.consumeIf(NINF)) {
- flags = (BinOp::Flags)(flags | BinOp::NINF);
- } else if (tokenizer.consumeIf(NNAN)) {
- flags = (BinOp::Flags)(flags | BinOp::NNAN);
+ if (tokenizer.consumeIf(NNAN)) {
+ flags |= BinOp::NNaN;
+ } else if (tokenizer.consumeIf(NINF)) {
+ flags |= BinOp::NInf;
} else {
break;
}
@@ -582,7 +582,7 @@ static BinOp::Flags parse_fast_math() {
}
-static BinOp::Flags parse_binop_flags(token op_token) {
+static unsigned parse_binop_flags(token op_token) {
switch (op_token) {
case ADD:
case SUB:
@@ -624,7 +624,7 @@ static BinOp::Flags parse_binop_flags(token op_token) {
}
static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
- BinOp::Flags flags = parse_binop_flags(op_token);
+ auto flags = parse_binop_flags(op_token);
auto &type = parse_type();
auto &a = parse_operand(type);
parse_comma();

expand fast-math support in binop
implement NSZ for binops