stub support for constrained FP binops
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -212,4 +212,30 @@ ostream& operator<<(ostream &os, const FastMathFlags &fm) {
return os;
}
+
+smt::expr FpRoundingMode::toSMT() const {
+ switch (mode) {
+ case FpRoundingMode::Dynamic: UNREACHABLE();
+ case FpRoundingMode::RNE: return expr::rne();
+ case FpRoundingMode::RNA: return expr::rna();
+ case FpRoundingMode::RTP: return expr::rtp();
+ case FpRoundingMode::RTN: return expr::rtn();
+ case FpRoundingMode::RTZ: return expr::rtz();
+ }
+ UNREACHABLE();
+}
+
+ostream& operator<<(std::ostream &os, FpRoundingMode rounding) {
+ const char *str;
+ switch (rounding.mode) {
+ case FpRoundingMode::Dynamic: str = "dynamic"; break;
+ case FpRoundingMode::RNE: str = "tonearest"; break;
+ case FpRoundingMode::RNA: str = "tonearestaway"; break;
+ case FpRoundingMode::RTP: str = "upward"; break;
+ case FpRoundingMode::RTN: str = "downward"; break;
+ case FpRoundingMode::RTZ: str = "towardzero"; break;
+ }
+ return os << str;
+}
+
}

MODIFY
ir/attrs.h
ir/attrs.h
@@ -95,4 +95,12 @@ struct FastMathFlags final {
friend std::ostream& operator<<(std::ostream &os, const FastMathFlags &fm);
};
+
+struct FpRoundingMode final {
+ enum Mode { Dynamic, RNE, RNA, RTP, RTN, RTZ } mode;
+ FpRoundingMode(Mode mode) : mode(mode) {}
+ smt::expr toSMT() const;
+ friend std::ostream& operator<<(std::ostream &os, FpRoundingMode rounding);
+};
+
}

MODIFY
ir/fast_math.cpp
ir/fast_math.cpp
@@ -28,7 +28,6 @@ struct Node {
enum { Add, Sub, Mul, Div, Neg, Leaf } operation;
unsigned op1 = -1u, op2 = -1u;
expr leaf;
- // FIXME: we currently ignore rounding
expr rounding;
unsigned flags = 0;
@@ -245,16 +244,16 @@ public:
expr val;
switch (node->operation) {
case Node::Add:
- val = exprs[node->op1]->fadd(*exprs[node->op2]);
+ val = exprs[node->op1]->fadd(*exprs[node->op2], node->rounding);
break;
case Node::Sub:
- val = exprs[node->op1]->fsub(*exprs[node->op2]);
+ val = exprs[node->op1]->fsub(*exprs[node->op2], node->rounding);
break;
case Node::Mul:
- val = exprs[node->op1]->fmul(*exprs[node->op2]);
+ val = exprs[node->op1]->fmul(*exprs[node->op2], node->rounding);
break;
case Node::Div:
- val = exprs[node->op1]->fdiv(*exprs[node->op2]);
+ val = exprs[node->op1]->fdiv(*exprs[node->op2], node->rounding);
break;
case Node::Neg:
val = exprs[node->op1]->fneg();

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -597,7 +597,8 @@ void FpBinOp::print(ostream &os) const {
case FMaximum: str = "fmaximum "; break;
case FMinimum: str = "fminimum "; break;
}
- os << getName() << " = " << str << fmath << *lhs << ", " << rhs->getName();
+ os << getName() << " = " << str << fmath << *lhs << ", " << rhs->getName()
+ << ", rounding=" << rm;
}
static expr any_fp_zero(State &s, const expr &v) {
@@ -701,7 +702,7 @@ StateValue FpBinOp::toSMT(State &s) const {
case FAdd:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
return fm_poison(s, a, ap, b, bp,
- [](expr &a, expr &b) { return a.fadd(b); },
+ [&](expr &a, expr &b) { return a.fadd(b, rm.toSMT()); },
fmath, false);
};
break;
@@ -709,7 +710,7 @@ StateValue FpBinOp::toSMT(State &s) const {
case FSub:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
return fm_poison(s, a, ap, b, bp,
- [](expr &a, expr &b) { return a.fsub(b); },
+ [&](expr &a, expr &b) { return a.fsub(b, rm.toSMT()); },
fmath, false);
};
break;
@@ -717,7 +718,7 @@ StateValue FpBinOp::toSMT(State &s) const {
case FMul:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
return fm_poison(s, a, ap, b, bp,
- [](expr &a, expr &b) { return a.fmul(b); },
+ [&](expr &a, expr &b) { return a.fmul(b, rm.toSMT()); },
fmath, false);
};
break;
@@ -725,7 +726,7 @@ StateValue FpBinOp::toSMT(State &s) const {
case FDiv:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
return fm_poison(s, a, ap, b, bp,
- [](expr &a, expr &b) { return a.fdiv(b); },
+ [&](expr &a, expr &b) { return a.fdiv(b, rm.toSMT()); },
fmath, false);
};
break;
@@ -908,19 +909,22 @@ StateValue UnaryOp::toSMT(State &s) const {
case Round:
fn = [&](auto v, auto np) -> StateValue {
return fm_poison(s, v, np,
- [](expr &v) { return v.roundna(); }, fmath, true);
+ [](expr &v) { return v.round(expr::rna()); },
+ fmath, true);
};
break;
case RoundEven:
fn = [&](auto v, auto np) -> StateValue {
return fm_poison(s, v, np,
- [](expr &v) { return v.roundne(); }, fmath, true);
+ [](expr &v) { return v.round(expr::rne()); },
+ fmath, true);
};
break;
case Trunc:
fn = [&](auto v, auto np) -> StateValue {
return fm_poison(s, v, np,
- [](expr &v) { return v.roundtz(); }, fmath, true);
+ [](expr &v) { return v.round(expr::rtz()); },
+ fmath, true);
};
break;
case Sqrt:
@@ -1260,7 +1264,7 @@ StateValue ConversionOp::toSMT(State &s) const {
expr bv = val.fp2sint(to_type.bits());
expr fp2 = bv.sint2fp(val);
// -0.xx is converted to 0 and then to 0.0, though -0.xx is ok to convert
- expr valrtz = val.roundtz();
+ expr valrtz = val.round(expr::rtz());
return { move(bv), valrtz.isFPZero() || fp2 == valrtz };
};
break;
@@ -1269,7 +1273,7 @@ StateValue ConversionOp::toSMT(State &s) const {
expr bv = val.fp2uint(to_type.bits());
expr fp2 = bv.uint2fp(val);
// -0.xx must be converted to 0, not poison.
- expr valrtz = val.roundtz();
+ expr valrtz = val.round(expr::rtz());
return { move(bv), valrtz.isFPZero() || fp2 == valrtz };
};
break;

MODIFY
ir/instr.h
ir/instr.h
@@ -64,11 +64,13 @@ private:
Value *lhs, *rhs;
Op op;
FastMathFlags fmath;
+ FpRoundingMode rm;
public:
FpBinOp(Type &type, std::string &&name, Value &lhs, Value &rhs, Op op,
- FastMathFlags fmath)
- : Instr(type, std::move(name)), lhs(&lhs), rhs(&rhs), op(op), fmath(fmath) {}
+ FastMathFlags fmath, FpRoundingMode rm = FpRoundingMode::RNE)
+ : Instr(type, std::move(name)), lhs(&lhs), rhs(&rhs), op(op), fmath(fmath),
+ rm(rm) {}
std::vector<Value*> operands() const override;
bool propagatesPoison() const override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -28,6 +28,19 @@ using llvm::LLVMContext;
namespace {
+FpRoundingMode parse_rounding(llvm::Instruction &i) {
+ auto *fp = cast<llvm::ConstrainedFPIntrinsic>(&i);
+ switch (fp->getRoundingMode().getValue()) {
+ case llvm::RoundingMode::Dynamic: return FpRoundingMode::Dynamic;
+ case llvm::RoundingMode::NearestTiesToAway: return FpRoundingMode::RNA;
+ case llvm::RoundingMode::NearestTiesToEven: return FpRoundingMode::RNE;
+ case llvm::RoundingMode::TowardNegative: return FpRoundingMode::RTN;
+ case llvm::RoundingMode::TowardPositive: return FpRoundingMode::RTP;
+ case llvm::RoundingMode::TowardZero: return FpRoundingMode::RTZ;
+ default: UNREACHABLE();
+ }
+}
+
unsigned constexpr_idx;
unsigned copy_idx;
unsigned alignopbundle_idx;
@@ -911,6 +924,25 @@ public:
RETURN_IDENTIFIER(make_unique<FpBinOp>(*ty, value_name(i), *a, *b, op,
parse_fmath(i)));
}
+ case llvm::Intrinsic::experimental_constrained_fadd:
+ case llvm::Intrinsic::experimental_constrained_fsub:
+ case llvm::Intrinsic::experimental_constrained_fmul:
+ case llvm::Intrinsic::experimental_constrained_fdiv:
+ {
+ PARSE_BINOP();
+ FpBinOp::Op op;
+ switch (i.getIntrinsicID()) {
+ case llvm::Intrinsic::experimental_constrained_fadd: op = FpBinOp::FAdd; break;
+ case llvm::Intrinsic::experimental_constrained_fsub: op = FpBinOp::FSub; break;
+ case llvm::Intrinsic::experimental_constrained_fmul: op = FpBinOp::FMul; break;
+ case llvm::Intrinsic::experimental_constrained_fdiv: op = FpBinOp::FDiv; break;
+ default: UNREACHABLE();
+ }
+ // TODO: missing support for exceptions
+ RETURN_IDENTIFIER(
+ make_unique<FpBinOp>(*ty, value_name(i), *a, *b, op, parse_fmath(i),
+ parse_rounding(i)));
+ }
case llvm::Intrinsic::lifetime_start:
case llvm::Intrinsic::lifetime_end:
{

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -999,29 +999,44 @@ expr expr::isFPNegZero() const {
return isFPZero() && isFPNegative();
}
-// TODO: make rounding mode customizable
-expr expr::fadd(const expr &rhs) const {
- C(rhs);
- auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
- return simplify_const(Z3_mk_fpa_add(ctx(), rm, ast(), rhs()), *this, rhs);
+expr expr::rne() {
+ return Z3_mk_fpa_rne(ctx());
}
-expr expr::fsub(const expr &rhs) const {
- C(rhs);
- auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
- return simplify_const(Z3_mk_fpa_sub(ctx(), rm, ast(), rhs()), *this, rhs);
+expr expr::rna() {
+ return Z3_mk_fpa_rna(ctx());
}
-expr expr::fmul(const expr &rhs) const {
- C(rhs);
- auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
- return simplify_const(Z3_mk_fpa_mul(ctx(), rm, ast(), rhs()), *this, rhs);
+expr expr::rtp() {
+ return Z3_mk_fpa_rtp(ctx());
}
-expr expr::fdiv(const expr &rhs) const {
- C(rhs);
- auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
- return simplify_const(Z3_mk_fpa_div(ctx(), rm, ast(), rhs()), *this, rhs);
+expr expr::rtn() {
+ return Z3_mk_fpa_rtn(ctx());
+}
+
+expr expr::rtz() {
+ return Z3_mk_fpa_rtz(ctx());
+}
+
+expr expr::fadd(const expr &rhs, const expr &rm) const {
+ C(rhs, rm);
+ return simplify_const(Z3_mk_fpa_add(ctx(), rm(), ast(), rhs()), *this, rhs);
+}
+
+expr expr::fsub(const expr &rhs, const expr &rm) const {
+ C(rhs, rm);
+ return simplify_const(Z3_mk_fpa_sub(ctx(), rm(), ast(), rhs()), *this, rhs);
+}
+
+expr expr::fmul(const expr &rhs, const expr &rm) const {
+ C(rhs, rm);
+ return simplify_const(Z3_mk_fpa_mul(ctx(), rm(), ast(), rhs()), *this, rhs);
+}
+
+expr expr::fdiv(const expr &rhs, const expr &rm) const {
+ C(rhs, rm);
+ return simplify_const(Z3_mk_fpa_div(ctx(), rm(), ast(), rhs()), *this, rhs);
}
expr expr::fabs() const {
@@ -1045,38 +1060,17 @@ expr expr::fma(const expr &a, const expr &b, const expr &c) {
}
expr expr::ceil() const {
- C();
- return
- simplify_const(
- Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rtp(ctx()), ast()), *this);
+ return round(rtp());
}
expr expr::floor() const {
- C();
- return
- simplify_const(
- Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rtn(ctx()), ast()), *this);
+ return round(rtn());
}
-expr expr::roundna() const {
- C();
- return
- simplify_const(
- Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rna(ctx()), ast()), *this);
-}
-
-expr expr::roundne() const {
- C();
- return
- simplify_const(
- Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rne(ctx()), ast()), *this);
-}
-
-expr expr::roundtz() const {
- C();
+expr expr::round(const expr &rm) const {
+ C(rm);
return
- simplify_const(
- Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rtz(ctx()), ast()), *this);
+ simplify_const(Z3_mk_fpa_round_to_integral(ctx(), rm(), ast()), *this);
}
expr expr::foeq(const expr &rhs) const {

MODIFY
smt/expr.h
smt/expr.h
@@ -211,10 +211,16 @@ public:
expr isFPNegative() const;
expr isFPNegZero() const;
- expr fadd(const expr &rhs) const;
- expr fsub(const expr &rhs) const;
- expr fmul(const expr &rhs) const;
- expr fdiv(const expr &rhs) const;
+ static expr rne();
+ static expr rna();
+ static expr rtp();
+ static expr rtn();
+ static expr rtz();
+
+ expr fadd(const expr &rhs, const expr &rm) const;
+ expr fsub(const expr &rhs, const expr &rm) const;
+ expr fmul(const expr &rhs, const expr &rm) const;
+ expr fdiv(const expr &rhs, const expr &rm) const;
expr fabs() const;
expr fneg() const;
expr sqrt() const;
@@ -223,9 +229,7 @@ public:
expr ceil() const;
expr floor() const;
- expr roundna() const;
- expr roundne() const;
- expr roundtz() const;
+ expr round(const expr &rm) const;
expr foeq(const expr &rhs) const;
expr fogt(const expr &rhs) const;

ADD
tests/alive-tv/fp/fadd-fail.srctgt.ll
+define float @src(float noundef %a) {
+ %ret = call float @llvm.experimental.constrained.fsub.f32(float %a, float 0.0, metadata !"round.downward", metadata !"fpexcept.strict")
+ ret float %ret
+}
+
+define float @tgt(float noundef %a) {
+ ret float %a
+}
+
+declare float @llvm.experimental.constrained.fsub.f32(float, float, metadata, metadata)

ADD
tests/alive-tv/fp/fadd.srctgt.ll
+define float @src(float %a) {
+ %ret = call float @llvm.experimental.constrained.fsub.f32(float %a, float 0.0, metadata !"round.upward", metadata !"fpexcept.strict")
+ ret float %ret
+}
+
+define float @tgt(float %a) {
+ ret float %a
+}
+
+declare float @llvm.experimental.constrained.fsub.f32(float, float, metadata, metadata)

stub support for constrained FP binops (#773)