Add support for llvm.is.fpclass intrinsic
Missing quiet/signaling nan distinction
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1322,6 +1322,97 @@ unique_ptr<Instr> FpTernaryOp::dup(const string &suffix) const {
}
+vector<Value*> TestOp::operands() const {
+ return { lhs, rhs };
+}
+
+bool TestOp::propagatesPoison() const {
+ return true;
+}
+
+void TestOp::rauw(const Value &what, Value &with) {
+ RAUW(lhs);
+ RAUW(rhs);
+}
+
+void TestOp::print(ostream &os) const {
+ const char *str = nullptr;
+ switch (op) {
+ case Is_FPClass: str = "is.fpclass "; break;
+ }
+
+ os << getName() << " = " << str << *lhs << ", " << *rhs;
+}
+
+StateValue TestOp::toSMT(State &s) const {
+ auto &a = s[*lhs];
+ auto &b = s[*rhs];
+ function<expr(const expr&)> fn;
+
+ switch (op) {
+ case Is_FPClass:
+ fn = [&](const expr &a) -> expr {
+ uint64_t n;
+ if (!b.value.isUInt(n) || !b.non_poison.isTrue()) {
+ s.addUB(expr(false));
+ return {};
+ }
+ OrExpr result;
+ // TODO: distinguish between quiet and signaling NaNs
+ if (n & (1 << 0))
+ result.add(a.isNaN());
+ if (n & (1 << 1))
+ result.add(a.isNaN());
+ if (n & (1 << 2))
+ result.add(a.isFPNegative() && a.isInf());
+ if (n & (1 << 3))
+ result.add(a.isFPNegative() && a.isFPNormal());
+ if (n & (1 << 4))
+ result.add(a.isFPNegative() && a.isFPSubNormal());
+ if (n & (1 << 5))
+ result.add(a.isFPNegZero());
+ if (n & (1 << 6))
+ result.add(a.isFPZero() && !a.isFPNegative());
+ if (n & (1 << 7))
+ result.add(!a.isFPNegative() && a.isFPSubNormal());
+ if (n & (1 << 8))
+ result.add(!a.isFPNegative() && a.isFPNormal());
+ if (n & (1 << 9))
+ result.add(!a.isFPNegative() && a.isInf());
+ return result().toBVBool();
+ };
+ break;
+ }
+
+ auto scalar = [&](const StateValue &v) -> StateValue {
+ return { fn(v.value), expr(v.non_poison) };
+ };
+
+ if (getType().isVectorType()) {
+ vector<StateValue> vals;
+ auto ty = lhs->getType().getAsAggregateType();
+
+ for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
+ vals.emplace_back(scalar(ty->extract(a, i)));
+ }
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
+ return scalar(a);
+}
+
+expr TestOp::getTypeConstraints(const Function &f) const {
+ return Value::getTypeConstraints() &&
+ lhs->getType().enforceFloatOrVectorType() &&
+ rhs->getType().enforceIntType(32) &&
+ getType().enforceIntOrVectorType(1) &&
+ getType().enforceVectorTypeEquiv(lhs->getType());
+}
+
+unique_ptr<Instr> TestOp::dup(const string &suffix) const {
+ return make_unique<TestOp>(getType(), getName() + suffix, *lhs, *rhs, op);
+}
+
+
vector<Value*> ConversionOp::operands() const {
return { val };
}

MODIFY
ir/instr.h
ir/instr.h
@@ -216,6 +216,28 @@ public:
};
+class TestOp final : public Instr {
+public:
+ enum Op { Is_FPClass };
+
+private:
+ Value *lhs, *rhs;
+ Op op;
+
+public:
+ TestOp(Type &type, std::string &&name, Value &lhs, Value &rhs, Op op)
+ : Instr(type, std::move(name)), lhs(&lhs), rhs(&rhs), op(op) {}
+
+ std::vector<Value*> operands() const override;
+ bool propagatesPoison() const override;
+ void rauw(const Value &what, Value &with) override;
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
+
class ConversionOp final : public Instr {
public:
enum Op { SExt, ZExt, Trunc, BitCast, Ptr2Int, Int2Ptr };

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -833,8 +833,7 @@ public:
case llvm::Intrinsic::smin: op = BinOp::SMin; break;
case llvm::Intrinsic::smax: op = BinOp::SMax; break;
case llvm::Intrinsic::abs: op = BinOp::Abs; break;
- default:
- UNREACHABLE();
+ default: UNREACHABLE();
}
RETURN_IDENTIFIER(make_unique<BinOp>(*ty, value_name(i), *a, *b, op));
}
@@ -1028,13 +1027,22 @@ public:
case llvm::Intrinsic::experimental_constrained_lround:
case llvm::Intrinsic::llround:
case llvm::Intrinsic::experimental_constrained_llround: op = FpConversionOp::LRound; break;
- default:
- return error(i);
+ default: UNREACHABLE();
}
RETURN_IDENTIFIER(make_unique<FpConversionOp>(*ty, value_name(i), *val,
op, parse_rounding(i),
parse_exceptions(i)));
}
+ case llvm::Intrinsic::is_fpclass:
+ {
+ PARSE_BINOP();
+ TestOp::Op op;
+ switch (i.getOpcode()) {
+ case llvm::Intrinsic::is_fpclass: op = TestOp::Is_FPClass; break;
+ default: UNREACHABLE();
+ }
+ RETURN_IDENTIFIER(make_unique<TestOp>(*ty, value_name(i), *a, *b, op));
+ }
case llvm::Intrinsic::lifetime_start:
case llvm::Intrinsic::lifetime_end:
{

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1013,6 +1013,14 @@ expr expr::isFPNegZero() const {
return isFPZero() && isFPNegative();
}
+expr expr::isFPNormal() const {
+ return unop_fold(Z3_mk_fpa_is_normal);
+}
+
+expr expr::isFPSubNormal() const {
+ return unop_fold(Z3_mk_fpa_is_subnormal);
+}
+
expr expr::rne() {
return Z3_mk_fpa_rne(ctx());
}

MODIFY
smt/expr.h
smt/expr.h
@@ -211,6 +211,8 @@ public:
expr isFPZero() const;
expr isFPNegative() const;
expr isFPNegZero() const;
+ expr isFPNormal() const;
+ expr isFPSubNormal() const;
static expr rne();
static expr rna();

ADD
tests/alive-tv/is_fpclass.srctgt.ll
+define <2 x i1> @src(<2 x float> %x) {
+entry:
+ %0 = tail call <2 x i1> @llvm.is.fpclass.v2f32(<2 x float> <float -0.0, float 1.0>, i32 256) ; is pos
+ ret <2 x i1> %0
+}
+
+define <2 x i1> @tgt(<2 x float> %x) {
+ ret <2 x i1> <i1 false, i1 true>
+}
+
+declare <2 x i1> @llvm.is.fpclass.v2f32(<2 x float>, i32)

Add support for llvm.is.fpclass intrinsic
Missing quiet/signaling nan distinction