Add support for the fast math flags NNaN and NInf
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -39,6 +39,13 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case LShr:
assert((flags & Exact) == flags);
break;
+ case FAdd:
+ case FSub:
+ case FMul:
+ case FDiv:
+ case FRem:
+ assert((flags & NNANNINF) == flags);
+ break;
case SRem:
case URem:
case SAdd_Sat:
@@ -56,12 +63,6 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case USub_Overflow:
case SMul_Overflow:
case UMul_Overflow:
- // TODO: add support for fast-math flags
- case FAdd:
- case FSub:
- case FMul:
- case FDiv:
- case FRem:
assert(flags == 0);
break;
}
@@ -108,6 +109,9 @@ void BinOp::print(ostream &os) const {
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;
}
@@ -123,6 +127,17 @@ static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
s.addUB((ap && a != expr::IntSMin(bits)) || b != expr::mkInt(-1, bits));
}
+static expr fm_poison(const expr &a, const expr &b, const expr &val,
+ BinOp::Flags flags) {
+ expr ret = false;
+ if (flags & BinOp::NINF)
+ ret |= a.isInf() || b.isInf() || val.isInf();
+ if (flags & BinOp::NNAN)
+ ret |= a.isNaN() || b.isNaN() || val.isNaN();
+
+ return ret;
+}
+
StateValue BinOp::toSMT(State &s) const {
auto &[a, ap] = s[lhs];
auto &[b, bp] = s[rhs];
@@ -277,18 +292,22 @@ StateValue BinOp::toSMT(State &s) const {
case FAdd:
val = a.fadd(b);
+ not_poison &= !fm_poison(a, b, val, flags);
break;
case FSub:
val = a.fsub(b);
+ not_poison &= !fm_poison(a, b, val, flags);
break;
case FMul:
val = a.fmul(b);
+ not_poison &= !fm_poison(a, b, val, flags);
break;
case FDiv:
val = a.fdiv(b);
+ not_poison &= !fm_poison(a, b, val, flags);
break;
case FRem:
@@ -934,7 +953,7 @@ StateValue Freeze::toSMT(State &s) const {
return { expr(v), expr(p) };
auto name = "nondet_" + fresh_id();
- expr nondet = expr::mkVar(name.c_str(), bits());
+ expr nondet = expr::mkVar(name.c_str(), getType().getDummyValue());
s.addQuantVar(nondet);
return { expr::mkIf(p, v, move(nondet)), true };

MODIFY
ir/instr.h
ir/instr.h
@@ -33,7 +33,8 @@ 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 };
+ enum Flags { None = 0, NSW = 1, NUW = 2, NSWNUW = 3, Exact = 4,
+ NNAN = 8, NINF = 16, NNANNINF = 24};
private:
Value &lhs, &rhs;

MODIFY
ir/value.cpp
ir/value.cpp
@@ -65,7 +65,7 @@ void PoisonValue::print(ostream &os) const {
}
StateValue PoisonValue::toSMT(State &s) const {
- return { expr::mkUInt(0, bits()), false };
+ return { getType().getDummyValue(), false };
}

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -274,9 +274,20 @@ 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())
+ 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);
+ }
+
RETURN_IDENTIFIER(make_unique<BinOp>(*ty, value_name(i), *a, *b, alive_op,
(BinOp::Flags)flags));

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -240,6 +240,8 @@ re2c:yyfill:check = 0;
"half" { return HALF;}
"float" { return FLOAT;}
"double" { return DOUBLE;}
+"nnan" { return NNAN; }
+"ninf" { return NINF; }
"unreachable" { return UNREACH; }
[a-zA-Z][a-zA-Z0-9]* {

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -404,6 +404,21 @@ static BinOp::Flags parse_exact() {
return BinOp::None;
}
+static BinOp::Flags parse_fast_math() {
+ BinOp::Flags 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);
+ } else {
+ break;
+ }
+ }
+ return flags;
+}
+
+
static BinOp::Flags parse_binop_flags(token op_token) {
switch (op_token) {
case ADD:
@@ -416,6 +431,12 @@ static BinOp::Flags parse_binop_flags(token op_token) {
case LSHR:
case ASHR:
return parse_exact();
+ case FADD:
+ case FSUB:
+ case FMUL:
+ case FDIV:
+ case FREM:
+ return parse_fast_math();
case SREM:
case UREM:
case UADD_SAT:
@@ -433,11 +454,6 @@ static BinOp::Flags parse_binop_flags(token op_token) {
case USUB_OVERFLOW:
case SMUL_OVERFLOW:
case UMUL_OVERFLOW:
- case FADD:
- case FSUB:
- case FMUL:
- case FDIV:
- case FREM:
return BinOp::None;
default:
UNREACHABLE();

MODIFY
tools/tokens.h
tools/tokens.h
@@ -51,6 +51,8 @@ TOKEN(LSHR)
TOKEN(MUL)
TOKEN(NAME)
TOKEN(NE)
+TOKEN(NINF)
+TOKEN(NNAN)
TOKEN(NSW)
TOKEN(NUM)
TOKEN(NUM_STR)

Add support for the fast math flags NNaN and NInf (#76)