add support for ceil, floor, round, roundeven, trunc
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -841,10 +841,15 @@ void UnaryOp::print(ostream &os) const {
case BSwap: str = "bswap "; break;
case Ctpop: str = "ctpop "; break;
case IsConstant: str = "is.constant "; break;
+ case FAbs: str = "fabs "; break;
case FNeg: str = "fneg "; break;
+ case Ceil: str = "ceil "; break;
+ case Floor: str = "floor "; break;
+ case Round: str = "round "; break;
+ case RoundEven: str = "roundeven "; break;
+ case Trunc: str = "trunc "; break;
case Sqrt: str = "sqrt "; break;
case FFS: str = "ffs "; break;
- case FAbs: str = "fabs "; break;
}
os << getName() << " = " << str << fmath << print_type(getType())
@@ -885,11 +890,44 @@ StateValue UnaryOp::toSMT(State &s) const {
s.addQuantVar(var);
return { move(var), true };
}
+ case FAbs:
+ fn = [&](auto v, auto np) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v) { return v.fabs(); }, fmath, true);
+ };
+ break;
case FNeg:
fn = [&](auto v, auto np) -> StateValue {
return fm_poison(s, v, np, [](expr &v){ return v.fneg(); }, fmath, false);
};
break;
+ case Ceil:
+ fn = [&](auto v, auto np) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v) { return v.ceil(); }, fmath, true);
+ };
+ break;
+ case Floor:
+ fn = [&](auto v, auto np) -> StateValue {
+ return fm_poison(s, v, np, [](expr &v) { return v.floor(); }, fmath, true);
+ };
+ break;
+ case Round:
+ fn = [&](auto v, auto np) -> StateValue {
+ return fm_poison(s, v, np,
+ [](expr &v) { return v.roundna(); }, fmath, true);
+ };
+ break;
+ case RoundEven:
+ fn = [&](auto v, auto np) -> StateValue {
+ return fm_poison(s, v, np,
+ [](expr &v) { return v.roundne(); }, fmath, true);
+ };
+ break;
+ case Trunc:
+ fn = [&](auto v, auto np) -> StateValue {
+ return fm_poison(s, v, np,
+ [](expr &v) { return v.roundtz(); }, fmath, true);
+ };
+ break;
case Sqrt:
fn = [&](auto v, auto np) -> StateValue {
return fm_poison(s, v, np, [](expr &v){ return v.sqrt(); }, fmath, false);
@@ -900,12 +938,6 @@ StateValue UnaryOp::toSMT(State &s) const {
return { v.cttz(expr::mkInt(-1, v)) + expr::mkUInt(1, v), expr(np) };
};
break;
- case FAbs:
- fn = [&](auto v, auto np) -> StateValue {
- auto f = [](expr &v) { return v.fabs(); };
- return fm_poison(s, v, np, f, fmath, true);
- };
- break;
}
auto &v = s[*val];
@@ -941,9 +973,14 @@ expr UnaryOp::getTypeConstraints(const Function &f) const {
case IsConstant:
instrconstr = getType().enforceIntType(1);
break;
+ case FAbs:
case FNeg:
+ case Ceil:
+ case Floor:
+ case Round:
+ case RoundEven:
+ case Trunc:
case Sqrt:
- case FAbs:
instrconstr &= getType().enforceFloatOrVectorType();
break;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -74,7 +74,8 @@ public:
class UnaryOp final : public Instr {
public:
enum Op {
- Copy, BitReverse, BSwap, Ctpop, IsConstant, FNeg, Sqrt, FFS, FAbs
+ Copy, BitReverse, BSwap, Ctpop, IsConstant, FAbs, FNeg,
+ Ceil, Floor, Round, RoundEven, Trunc, Sqrt, FFS
};
private:

MODIFY
llvm_util/known_fns.cpp
llvm_util/known_fns.cpp
@@ -118,11 +118,35 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
make_unique<ConversionOp>(*ty, value_name(i), *Op, ConversionOp::Trunc));
}
case llvm::LibFunc_fabs:
- case llvm::LibFunc_fabsf: {
+ case llvm::LibFunc_fabsf:
RETURN_KNOWN(
- make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::FAbs,
- parse_fmath(i)));
- }
+ make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::FAbs));
+
+ case llvm::LibFunc_ceil:
+ case llvm::LibFunc_ceilf:
+ RETURN_KNOWN(
+ make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Ceil));
+
+ case llvm::LibFunc_floor:
+ case llvm::LibFunc_floorf:
+ RETURN_KNOWN(
+ make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Floor));
+
+ case llvm::LibFunc_round:
+ case llvm::LibFunc_roundf:
+ RETURN_KNOWN(
+ make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Round));
+
+ case llvm::LibFunc_roundeven:
+ case llvm::LibFunc_roundevenf:
+ RETURN_KNOWN(
+ make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::RoundEven));
+
+ case llvm::LibFunc_trunc:
+ case llvm::LibFunc_truncf:
+ RETURN_KNOWN(
+ make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Trunc));
+
case llvm::LibFunc_fwrite: {
auto size = getInt(*args[1]);

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -776,24 +776,34 @@ end:
}
case llvm::Intrinsic::bitreverse:
case llvm::Intrinsic::bswap:
+ case llvm::Intrinsic::ceil:
case llvm::Intrinsic::ctpop:
case llvm::Intrinsic::expect:
case llvm::Intrinsic::expect_with_probability:
case llvm::Intrinsic::fabs:
+ case llvm::Intrinsic::floor:
case llvm::Intrinsic::is_constant:
- case llvm::Intrinsic::sqrt:{
+ case llvm::Intrinsic::round:
+ case llvm::Intrinsic::roundeven:
+ case llvm::Intrinsic::sqrt:
+ case llvm::Intrinsic::trunc: {
PARSE_UNOP();
UnaryOp::Op op;
switch (i.getIntrinsicID()) {
case llvm::Intrinsic::bitreverse: op = UnaryOp::BitReverse; break;
case llvm::Intrinsic::bswap: op = UnaryOp::BSwap; break;
+ case llvm::Intrinsic::ceil: op = UnaryOp::Ceil; break;
case llvm::Intrinsic::ctpop: op = UnaryOp::Ctpop; break;
case llvm::Intrinsic::expect:
case llvm::Intrinsic::expect_with_probability:
op = UnaryOp::Copy; break;
case llvm::Intrinsic::fabs: op = UnaryOp::FAbs; break;
+ case llvm::Intrinsic::floor: op = UnaryOp::Floor; break;
case llvm::Intrinsic::is_constant: op = UnaryOp::IsConstant; break;
+ case llvm::Intrinsic::round: op = UnaryOp::Round; break;
+ case llvm::Intrinsic::roundeven: op = UnaryOp::RoundEven; break;
case llvm::Intrinsic::sqrt: op = UnaryOp::Sqrt; break;
+ case llvm::Intrinsic::trunc: op = UnaryOp::Trunc; break;
default: UNREACHABLE();
}
RETURN_IDENTIFIER(make_unique<UnaryOp>(*ty, value_name(i), *val, op,

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -967,6 +967,31 @@ expr expr::fma(const expr &a, const expr &b, const expr &c) {
return Z3_mk_fpa_fma(ctx(), rm, a(), b(), c());
}
+expr expr::ceil() const {
+ C();
+ return Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rtp(ctx()), ast());
+}
+
+expr expr::floor() const {
+ C();
+ return Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rtn(ctx()), ast());
+}
+
+expr expr::roundna() const {
+ C();
+ return Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rna(ctx()), ast());
+}
+
+expr expr::roundne() const {
+ C();
+ return Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rne(ctx()), ast());
+}
+
+expr expr::roundtz() const {
+ C();
+ return Z3_mk_fpa_round_to_integral(ctx(), Z3_mk_fpa_rtz(ctx()), ast());
+}
+
expr expr::foeq(const expr &rhs) const {
return binop_commutative(rhs, Z3_mk_fpa_eq);
}

MODIFY
smt/expr.h
smt/expr.h
@@ -218,6 +218,12 @@ public:
static expr fma(const expr &a, const expr &b, const expr &c);
+ expr ceil() const;
+ expr floor() const;
+ expr roundna() const;
+ expr roundne() const;
+ expr roundtz() const;
+
expr foeq(const expr &rhs) const;
expr fogt(const expr &rhs) const;
expr foge(const expr &rhs) const;

ADD
tests/alive-tv/fpround.srctgt.ll
+define void @src() {
+ %a = call float @llvm.ceil.f32(float 0.5)
+ %b = call float @llvm.ceil.f32(float -0.5)
+ %c = call float @llvm.floor.f32(float 0.5)
+ %d = call float @llvm.floor.f32(float -0.5)
+ %e = call float @llvm.round.f32(float 0.5)
+ %f = call float @llvm.round.f32(float -0.5)
+ %g = call float @llvm.trunc.f32(float 0.5)
+ %h = call float @llvm.trunc.f32(float -0.5)
+ %i = call float @llvm.roundeven.f32(float 0.5)
+ %j = call float @llvm.roundeven.f32(float -0.5)
+ call void (...) @test(float %a, float %b, float %c, float %d, float %e,
+ float %f, float %g, float %h, float %i, float %j)
+ ret void
+}
+
+declare float @llvm.ceil.f32(float) nounwind readnone
+declare float @llvm.floor.f32(float) nounwind readnone
+declare float @llvm.round.f32(float) nounwind readnone
+declare float @llvm.roundeven.f32(float) nounwind readnone
+declare float @llvm.trunc.f32(float) nounwind readnone
+
+declare void @test(...)

add support for ceil, floor, round, roundeven, trunc