Add support for fma intrinsic
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -196,24 +196,28 @@ static expr any_fp_zero(State &s, expr v) {
v);
}
-static StateValue fm_poison(State &s, expr a, expr b,
- function<expr(expr&,expr&)> fn,
- FastMathFlags fmath, bool only_input) {
+static StateValue fm_poison(State &s, expr a, expr b, expr c,
+ function<expr(expr&,expr&,expr&)> fn,
+ FastMathFlags fmath, bool only_input,
+ bool is_ternary = true){
if (fmath.flags & FastMathFlags::NSZ) {
a = any_fp_zero(s, move(a));
b = any_fp_zero(s, move(b));
+ if (is_ternary) c = any_fp_zero(s, move(c));
}
- expr val = fn(a, b);
+ expr val = fn(a, b, c);
expr non_poison(true);
if (fmath.flags & FastMathFlags::NNaN) {
non_poison &= !a.isNaN() && !b.isNaN();
+ if (is_ternary) non_poison &= !c.isNaN();
if (!only_input)
non_poison &= !val.isNaN();
}
if (fmath.flags & FastMathFlags::NInf) {
non_poison &= !a.isInf() && !b.isInf();
+ if (is_ternary) non_poison &= !c.isInf();
if (!only_input)
non_poison &= !val.isInf();
}
@@ -231,6 +235,14 @@ static StateValue fm_poison(State &s, expr a, expr b,
return { move(val), move(non_poison) };
}
+static StateValue fm_poison(State &s, expr a, expr b,
+ function<expr(expr&,expr&)> fn,
+ FastMathFlags fmath, bool only_input) {
+ return fm_poison(s, move(a), move(b), expr(),
+ [&](expr &a, expr &b, expr &c) { return fn(a, b); },
+ fmath, only_input, false);
+}
+
StateValue BinOp::toSMT(State &s) const {
bool vertical_zip = false;
function<StateValue(const expr&, const expr&, const expr&, const expr&)>
@@ -680,6 +692,18 @@ unique_ptr<Instr> UnaryOp::dup(const string &suffix) const {
return make_unique<UnaryOp>(getType(), getName() + suffix, *val, op, fmath);
}
+TernaryOp::TernaryOp(Type &type, string &&name, Value &a, Value &b, Value &c,
+ Op op, FastMathFlags fmath)
+ : Instr(type, move(name)), a(&a), b(&b), c(&c), op(op), fmath(fmath) {
+ switch (op) {
+ case FShr:
+ case FShl:
+ assert(fmath.isNone());
+ break;
+ case FMA:
+ break;
+ }
+}
vector<Value*> TernaryOp::operands() const {
return { a, b, c };
@@ -700,26 +724,37 @@ void TernaryOp::print(ostream &os) const {
case FShr:
str = "fshr ";
break;
+ case FMA:
+ str = "fma ";
+ break;
}
- os << getName() << " = " << str << *a << ", " << *b << ", " << *c;
+ os << getName() << " = " << str << fmath << *a << ", " << *b << ", " << *c;
}
StateValue TernaryOp::toSMT(State &s) const {
auto &av = s[*a];
auto &bv = s[*b];
auto &cv = s[*c];
- function<expr(const expr&, const expr&, const expr&)> fn;
+ function<StateValue(const expr&, const expr&, const expr&)> fn;
switch (op) {
case FShl:
- fn = [](auto a, auto b, auto c) {
- return expr::fshl(a, b, c);
+ fn = [](auto a, auto b, auto c) -> StateValue {
+ return { expr::fshl(a, b, c), true };
};
break;
+
case FShr:
- fn = [](auto a, auto b, auto c) {
- return expr::fshr(a, b, c);
+ fn = [](auto a, auto b, auto c) -> StateValue {
+ return { expr::fshr(a, b, c), true };
+ };
+ break;
+
+ case FMA:
+ fn = [&](auto a, auto b, auto c) -> StateValue {
+ return fm_poison(s, a, b, c, [](expr &a, expr &b, expr &c) {
+ return expr::fma(a, b, c); }, fmath, false);
};
break;
}
@@ -727,25 +762,36 @@ StateValue TernaryOp::toSMT(State &s) const {
if (getType().isVectorType()) {
vector<StateValue> vals;
auto ty = getType().getAsAggregateType();
+
for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
auto ai = ty->extract(av, i);
auto bi = ty->extract(bv, i);
auto ci = ty->extract(cv, i);
- vals.emplace_back(fn(ai.value, bi.value, ci.value),
- ai.non_poison && bi.non_poison && ci.non_poison);
+ auto [v, np] = fn(ai.value, bi.value, ci.value);
+ vals.emplace_back(move(v), ai.non_poison && bi.non_poison
+ && ci.non_poison && np);
}
return ty->aggregateVals(vals);
}
- return { fn(av.value, bv.value, cv.value),
- av.non_poison && bv.non_poison && cv.non_poison };
+ auto [v, np] = fn(av.value, bv.value, cv.value);
+ return { move(v), av.non_poison && bv.non_poison && cv.non_poison && np };
}
expr TernaryOp::getTypeConstraints(const Function &f) const {
- return Value::getTypeConstraints() &&
- getType().enforceIntOrVectorType() &&
+ expr instrconstr = Value::getTypeConstraints() &&
getType() == a->getType() &&
getType() == b->getType() &&
getType() == c->getType();
+ switch(op) {
+ case FShl:
+ case FShr:
+ instrconstr &= getType().enforceIntOrVectorType();
+ break;
+ case FMA:
+ instrconstr &= getType().enforceFloatOrVectorType();
+ break;
+ }
+ return instrconstr;
}
unique_ptr<Instr> TernaryOp::dup(const string &suffix) const {

MODIFY
ir/instr.h
ir/instr.h
@@ -94,15 +94,16 @@ public:
class TernaryOp final : public Instr {
public:
- enum Op { FShl, FShr };
+ enum Op { FShl, FShr, FMA };
private:
Value *a, *b, *c;
Op op;
+ FastMathFlags fmath;
public:
- TernaryOp(Type &type, std::string &&name, Value &a, Value &b, Value &c, Op op)
- : Instr(type, std::move(name)), a(&a), b(&b), c(&c), op(op) {}
+ TernaryOp(Type &type, std::string &&name, Value &a, Value &b, Value &c, Op op,
+ FastMathFlags fmath = {});
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -596,16 +596,18 @@ public:
}
case llvm::Intrinsic::fshl:
case llvm::Intrinsic::fshr:
+ case llvm::Intrinsic::fma:
{
PARSE_TRIOP();
TernaryOp::Op op;
switch (i.getIntrinsicID()) {
case llvm::Intrinsic::fshl: op = TernaryOp::FShl; break;
case llvm::Intrinsic::fshr: op = TernaryOp::FShr; break;
+ case llvm::Intrinsic::fma: op = TernaryOp::FMA; break;
default: UNREACHABLE();
}
RETURN_IDENTIFIER(make_unique<TernaryOp>(*ty, value_name(i), *a, *b, *c,
- op));
+ op, parse_fmath(i)));
}
case llvm::Intrinsic::lifetime_start:
{

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -834,6 +834,12 @@ expr expr::fdiv(const expr &rhs) const {
return Z3_mk_fpa_div(ctx(), rm, ast(), rhs());
}
+expr expr::fma(const expr &a, const expr &b, const expr &c) {
+ C2(a, b, c);
+ auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+ return Z3_mk_fpa_fma(ctx(), rm, a(), b(), c());
+}
+
expr expr::fneg() const {
return unop_fold(Z3_mk_fpa_neg);
}

MODIFY
smt/expr.h
smt/expr.h
@@ -164,6 +164,7 @@ public:
static expr fshl(const expr &a, const expr &b, const expr &c);
static expr fshr(const expr &a, const expr &b, const expr &c);
+ static expr fma(const expr &a, const expr &b, const expr &c);
expr shl_no_soverflow(const expr &rhs) const;
expr shl_no_uoverflow(const expr &rhs) const;

ADD
tests/unit/fp/fma-error-mismatch.opt
+Name: value mismatch (2.0 * 4.0) + 1.0 => 8.0
+; ERROR: Value mismatch for float %t
+%t = fma float 2.0, float 4.0, float 1.0
+ =>
+%t = 8.0
\ No newline at end of file

ADD
tests/unit/fp/fma-poison-error.opt
+Name: target more poisonous than source
+; ERROR: Target is more poisonous than source for float %t
+%t = fma float %a, float %b, float %c
+ =>
+%t = poison

ADD
tests/unit/fp/fma-poison.opt
+Name: add poison
+%t = fma float %a, float %b, float poison
+ =>
+%t = poison
+
+Name: mul poison
+%t = fma float poison, float poison, float %c
+ =>
+%t = poison

ADD
tests/unit/fp/fma.opt
+Name: fma, passthrough
+%t = fma float 0.0, float 0.0, float 0.0
+ =>
+%t = 0.0
+
+Name: fma, identical constant
+%t = fma float 1.0, float 2.0, float 3.0
+ =>
+%t = fma float 1.0, float 2.0, float 3.0
+
+Name: fma, constant
+%t = fma float 1.0, float 2.0, float 3.0
+ =>
+%t = 5.0
+
+Name: fma, multiply by zero, add zero
+%t = fma nnan float %a, float 0.0, float 0.0
+ =>
+%t = 0.0
+
+Name: fma, multiply zero, add constant
+%t = fma nnan nsz float 0.0, float %b, float %c
+ =>
+%t = %c
+
+Name: fma, multiply neg zero, add constant
+%t = fma nnan nsz float -0.0, float %b, float 4.0
+ =>
+%t = 4.0
+
+Name: fma, multiply one, add zero
+%t = fma nsz half 1.0, half %b, half 0.0
+ =>
+%t = %b
+
+Name: fma => fadd(fmul(a,b),c)
+%m = fmul half 5.0, half 4.0
+%t = fadd half 2.0, %m
+ =>
+%m = fmul half 5.0, half 4.0
+%t = fma half 5.0, half 4.0, half 2.0

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -233,6 +233,7 @@ space+ {
"free" { return FREE; }
"fshl" { return FSHL; }
"fshr" { return FSHR; }
+"fma" { return FMA; }
"extractelement" { return EXTRACTELEMENT; }
"insertelement" { return INSERTELEMENT; }
"shufflevector" { return SHUFFLEVECTOR; }
@@ -278,6 +279,7 @@ space+ {
"double" { return DOUBLE;}
"nnan" { return NNAN; }
"ninf" { return NINF; }
+"nsz" { return NSZ; }
"unreachable" { return UNREACH; }
[a-zA-Z][a-zA-Z0-9]* {

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -601,6 +601,8 @@ static FastMathFlags parse_fast_math(token op_token) {
fmath.flags |= FastMathFlags::NNaN;
} else if (tokenizer.consumeIf(NINF)) {
fmath.flags |= FastMathFlags::NInf;
+ } else if (tokenizer.consumeIf(NSZ)) {
+ fmath.flags |= FastMathFlags::NSZ;
} else {
break;
}
@@ -613,6 +615,7 @@ static FastMathFlags parse_fast_math(token op_token) {
case FDIV:
case FREM:
case FCMP:
+ case FMA:
break;
default:
if (!fmath.isNone())
@@ -745,14 +748,13 @@ static unique_ptr<Instr> parse_unaryop(string_view name, token op_token) {
}
static unique_ptr<Instr> parse_ternary(string_view name, token op_token) {
+ auto fmath = parse_fast_math(op_token);
+
TernaryOp::Op op;
switch (op_token) {
- case FSHL:
- op = TernaryOp::FShl;
- break;
- case FSHR:
- op = TernaryOp::FShr;
- break;
+ case FSHL: op = TernaryOp::FShl; break;
+ case FSHR: op = TernaryOp::FShr; break;
+ case FMA: op = TernaryOp::FMA; break;
default:
UNREACHABLE();
}
@@ -765,7 +767,7 @@ static unique_ptr<Instr> parse_ternary(string_view name, token op_token) {
parse_comma();
auto &cty = parse_type();
auto &c = parse_operand(cty);
- return make_unique<TernaryOp>(aty, string(name), a, b, c, op);
+ return make_unique<TernaryOp>(aty, string(name), a, b, c, op, fmath);
}
static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
@@ -1018,6 +1020,7 @@ static unique_ptr<Instr> parse_instr(string_view name) {
return parse_unaryop(name, t);
case FSHL:
case FSHR:
+ case FMA:
return parse_ternary(name, t);
case BITCAST:
case SEXT:

MODIFY
tools/tokens.h
tools/tokens.h
@@ -47,6 +47,7 @@ TOKEN(FREE)
TOKEN(FREM)
TOKEN(FSHL)
TOKEN(FSHR)
+TOKEN(FMA)
TOKEN(FSUB)
TOKEN(GLOBAL_NAME)
TOKEN(HALF)
@@ -65,6 +66,7 @@ TOKEN(NAME)
TOKEN(NE)
TOKEN(NINF)
TOKEN(NNAN)
+TOKEN(NSZ)
TOKEN(NSW)
TOKEN(NULLTOKEN)
TOKEN(NUM)

Add support for fma intrinsic (#279)