add more constrained FP ops
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -704,13 +704,19 @@ static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
return fn(rm);
auto &var = s.getFpRoundingMode();
- DisjointExpr<StateValue> vals;
- for (auto rm : { FpRoundingMode::RNE, FpRoundingMode::RNA,
- FpRoundingMode::RTP, FpRoundingMode::RTN,
- FpRoundingMode::RTZ }) {
- vals.add(fn(rm), var == rm);
+ return StateValue::mkIf(var == FpRoundingMode::RNE, fn(FpRoundingMode::RNE),
+ StateValue::mkIf(var == FpRoundingMode::RNA, fn(FpRoundingMode::RNA),
+ StateValue::mkIf(var == FpRoundingMode::RTP, fn(FpRoundingMode::RTP),
+ StateValue::mkIf(var == FpRoundingMode::RTN, fn(FpRoundingMode::RTN),
+ fn(FpRoundingMode::RTZ)))));
}
- return *vals();
+
+static expr get_fp_rounding(const State &s) {
+ auto &var = s.getFpRoundingMode();
+ return expr::mkIf(var == FpRoundingMode::RNE, expr::rne(),
+ expr::mkIf(var == FpRoundingMode::RNA, expr::rna(),
+ expr::mkIf(var == FpRoundingMode::RTP, expr::rtp(),
+ expr::mkIf(var == FpRoundingMode::RTN, expr::rtn(), expr::rtz()))));
}
StateValue FpBinOp::toSMT(State &s) const {
@@ -965,6 +971,8 @@ void FpUnaryOp::print(ostream &os) const {
case FNeg: str = "fneg "; break;
case Ceil: str = "ceil "; break;
case Floor: str = "floor "; break;
+ case RInt: str = "rint "; break;
+ case NearbyInt: str = "nearbyint "; break;
case Round: str = "round "; break;
case RoundEven: str = "roundeven "; break;
case Trunc: str = "trunc "; break;
@@ -999,6 +1007,15 @@ StateValue FpUnaryOp::toSMT(State &s) const {
true);
};
break;
+ case RInt:
+ case NearbyInt:
+ // TODO: they differ in exception behavior
+ fn = [&](auto &v, auto &np, auto rm) -> StateValue {
+ return fm_poison(s, v, np,
+ [&](expr &v) { return v.round(get_fp_rounding(s)); },
+ fmath, true);
+ };
+ break;
case Round:
fn = [&](auto &v, auto &np, auto rm) -> StateValue {
return fm_poison(s, v, np, [](expr &v) { return v.round(expr::rna()); },
@@ -1462,6 +1479,10 @@ void FpConversionOp::print(ostream &os) const {
case FPToUInt: str = "fptoui "; break;
case FPExt: str = "fpext "; break;
case FPTrunc: str = "fptrunc "; break;
+ case LRInt: str = "lrint "; break;
+ case LLRInt: str = "llrint "; break;
+ case LRound: str = "lround "; break;
+ case LLRound: str = "llround "; break;
}
os << getName() << " = " << str << *val << print_type(getType(), " to ", "")
@@ -1486,21 +1507,41 @@ StateValue FpConversionOp::toSMT(State &s) const {
};
break;
case FPToSInt:
- fn = [](auto &val, auto &to_type, auto rm) -> StateValue {
- expr bv = val.fp2sint(to_type.bits());
- expr fp2 = bv.sint2fp(val, expr::rtz());
+ case LRInt:
+ case LLRInt:
+ case LRound:
+ case LLRound:
+ fn = [&](auto &val, auto &to_type, auto rm_) -> StateValue {
+ expr rm;
+ switch (op) {
+ case FPToSInt:
+ rm = expr::rtz();
+ break;
+ case LRInt:
+ case LLRInt:
+ rm = get_fp_rounding(s);
+ break;
+ case LRound:
+ case LLRound:
+ rm = expr::rna();
+ break;
+ default: UNREACHABLE();
+ }
+ expr bv = val.fp2sint(to_type.bits(), rm);
+ expr fp2 = bv.sint2fp(val, rm);
// -0.xx is converted to 0 and then to 0.0, though -0.xx is ok to convert
- expr valrtz = val.round(expr::rtz());
- return { move(bv), valrtz.isFPZero() || fp2 == valrtz };
+ expr val_rounded = val.round(rm);
+ return { move(bv), val_rounded.isFPZero() || fp2 == val_rounded };
};
break;
case FPToUInt:
- fn = [](auto &val, auto &to_type, auto rm) -> StateValue {
- expr bv = val.fp2uint(to_type.bits());
- expr fp2 = bv.uint2fp(val, expr::rtz());
+ fn = [](auto &val, auto &to_type, auto rm_) -> StateValue {
+ expr rm = expr::rtz();
+ expr bv = val.fp2uint(to_type.bits(), rm);
+ expr fp2 = bv.uint2fp(val, rm);
// -0.xx must be converted to 0, not poison.
- expr valrtz = val.round(expr::rtz());
- return { move(bv), valrtz.isFPZero() || fp2 == valrtz };
+ expr val_rounded = val.round(rm);
+ return { move(bv), val_rounded.isFPZero() || fp2 == val_rounded };
};
break;
case FPExt:
@@ -1540,6 +1581,10 @@ expr FpConversionOp::getTypeConstraints(const Function &f) const {
break;
case FPToSInt:
case FPToUInt:
+ case LRInt:
+ case LLRInt:
+ case LRound:
+ case LLRound:
c = getType().enforceIntOrVectorType() &&
val->getType().enforceFloatOrVectorType();
break;

MODIFY
ir/instr.h
ir/instr.h
@@ -111,7 +111,7 @@ public:
class FpUnaryOp final : public Instr {
public:
enum Op {
- FAbs, FNeg, Ceil, Floor, Round, RoundEven, Trunc, Sqrt
+ FAbs, FNeg, Ceil, Floor, RInt, NearbyInt, Round, RoundEven, Trunc, Sqrt
};
private:
@@ -235,7 +235,8 @@ public:
class FpConversionOp final : public Instr {
public:
- enum Op { SIntToFP, UIntToFP, FPToSInt, FPToUInt, FPExt, FPTrunc };
+ enum Op { SIntToFP, UIntToFP, FPToSInt, FPToUInt, FPExt, FPTrunc, LRInt,
+ LLRInt, LRound, LLRound };
private:
Value *val;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -863,27 +863,6 @@ public:
}
RETURN_IDENTIFIER(make_unique<UnaryOp>(*ty, value_name(i), *val, op));
}
- case llvm::Intrinsic::fabs:
- case llvm::Intrinsic::floor:
- case llvm::Intrinsic::round:
- case llvm::Intrinsic::roundeven:
- case llvm::Intrinsic::sqrt:
- case llvm::Intrinsic::trunc: {
- PARSE_UNOP();
- FpUnaryOp::Op op;
- switch (i.getIntrinsicID()) {
- case llvm::Intrinsic::ceil: op = FpUnaryOp::Ceil; break;
- case llvm::Intrinsic::fabs: op = FpUnaryOp::FAbs; break;
- case llvm::Intrinsic::floor: op = FpUnaryOp::Floor; break;
- case llvm::Intrinsic::round: op = FpUnaryOp::Round; break;
- case llvm::Intrinsic::roundeven: op = FpUnaryOp::RoundEven; break;
- case llvm::Intrinsic::sqrt: op = FpUnaryOp::Sqrt; break;
- case llvm::Intrinsic::trunc: op = FpUnaryOp::Trunc; break;
- default: UNREACHABLE();
- }
- RETURN_IDENTIFIER(make_unique<FpUnaryOp>(*ty, value_name(i), *val, op,
- parse_fmath(i)));
- }
case llvm::Intrinsic::vector_reduce_add:
case llvm::Intrinsic::vector_reduce_mul:
case llvm::Intrinsic::vector_reduce_and:
@@ -976,21 +955,41 @@ public:
make_unique<FpBinOp>(*ty, value_name(i), *a, *b, op, parse_fmath(i),
parse_rounding(i)));
}
+ case llvm::Intrinsic::ceil:
case llvm::Intrinsic::experimental_constrained_ceil:
+ case llvm::Intrinsic::floor:
case llvm::Intrinsic::experimental_constrained_floor:
+ case llvm::Intrinsic::rint:
+ case llvm::Intrinsic::experimental_constrained_rint:
+ case llvm::Intrinsic::nearbyint:
+ case llvm::Intrinsic::experimental_constrained_nearbyint:
+ case llvm::Intrinsic::round:
case llvm::Intrinsic::experimental_constrained_round:
+ case llvm::Intrinsic::roundeven:
case llvm::Intrinsic::experimental_constrained_roundeven:
+ case llvm::Intrinsic::sqrt:
case llvm::Intrinsic::experimental_constrained_sqrt:
+ case llvm::Intrinsic::trunc:
case llvm::Intrinsic::experimental_constrained_trunc:
{
PARSE_UNOP();
FpUnaryOp::Op op;
switch (i.getIntrinsicID()) {
+ case llvm::Intrinsic::ceil:
case llvm::Intrinsic::experimental_constrained_ceil: op = FpUnaryOp::Ceil; break;
+ case llvm::Intrinsic::floor:
case llvm::Intrinsic::experimental_constrained_floor: op = FpUnaryOp::Floor; break;
+ case llvm::Intrinsic::rint:
+ case llvm::Intrinsic::experimental_constrained_rint: op = FpUnaryOp::RInt; break;
+ case llvm::Intrinsic::nearbyint:
+ case llvm::Intrinsic::experimental_constrained_nearbyint: op = FpUnaryOp::NearbyInt; break;
+ case llvm::Intrinsic::round:
case llvm::Intrinsic::experimental_constrained_round: op = FpUnaryOp::Round; break;
+ case llvm::Intrinsic::roundeven:
case llvm::Intrinsic::experimental_constrained_roundeven: op = FpUnaryOp::RoundEven; break;
+ case llvm::Intrinsic::sqrt:
case llvm::Intrinsic::experimental_constrained_sqrt: op = FpUnaryOp::Sqrt; break;
+ case llvm::Intrinsic::trunc:
case llvm::Intrinsic::experimental_constrained_trunc: op = FpUnaryOp::Trunc; break;
default: UNREACHABLE();
}
@@ -1005,6 +1004,14 @@ public:
case llvm::Intrinsic::experimental_constrained_fptoui:
case llvm::Intrinsic::experimental_constrained_fpext:
case llvm::Intrinsic::experimental_constrained_fptrunc:
+ case llvm::Intrinsic::lrint:
+ case llvm::Intrinsic::experimental_constrained_lrint:
+ case llvm::Intrinsic::llrint:
+ case llvm::Intrinsic::experimental_constrained_llrint:
+ case llvm::Intrinsic::lround:
+ case llvm::Intrinsic::experimental_constrained_lround:
+ case llvm::Intrinsic::llround:
+ case llvm::Intrinsic::experimental_constrained_llround:
{
PARSE_UNOP();
FpConversionOp::Op op;
@@ -1015,6 +1022,14 @@ public:
case llvm::Intrinsic::experimental_constrained_fptoui: op = FpConversionOp::FPToUInt; break;
case llvm::Intrinsic::experimental_constrained_fpext: op = FpConversionOp::FPExt; break;
case llvm::Intrinsic::experimental_constrained_fptrunc: op = FpConversionOp::FPTrunc; break;
+ case llvm::Intrinsic::lrint:
+ case llvm::Intrinsic::experimental_constrained_lrint: op = FpConversionOp::LRInt; break;
+ case llvm::Intrinsic::llrint:
+ case llvm::Intrinsic::experimental_constrained_llrint: op = FpConversionOp::LLRInt; break;
+ case llvm::Intrinsic::lround:
+ case llvm::Intrinsic::experimental_constrained_lround: op = FpConversionOp::LRound; break;
+ case llvm::Intrinsic::llround:
+ case llvm::Intrinsic::experimental_constrained_llround: op = FpConversionOp::LLRound; break;
default:
return error(i);
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1726,16 +1726,14 @@ expr expr::float2Float(const expr &type, const expr &rm) const {
return Z3_mk_fpa_to_fp_float(ctx(), rm(), ast(), type.sort());
}
-expr expr::fp2sint(unsigned bits) const {
- C();
- auto rm = Z3_mk_fpa_rtz(ctx());
- return simplify_const(Z3_mk_fpa_to_sbv(ctx(), rm, ast(), bits), *this);
+expr expr::fp2sint(unsigned bits, const expr &rm) const {
+ C(rm);
+ return simplify_const(Z3_mk_fpa_to_sbv(ctx(), rm(), ast(), bits), *this);
}
-expr expr::fp2uint(unsigned bits) const {
- C();
- auto rm = Z3_mk_fpa_rtz(ctx());
- return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm, ast(), bits), *this);
+expr expr::fp2uint(unsigned bits, const expr &rm) const {
+ C(rm);
+ return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm(), ast(), bits), *this);
}
expr expr::sint2fp(const expr &type, const expr &rm) const {

MODIFY
smt/expr.h
smt/expr.h
@@ -303,8 +303,8 @@ public:
expr BV2float(const expr &type) const;
expr float2Float(const expr &type, const expr &rm) const;
- expr fp2sint(unsigned bits) const;
- expr fp2uint(unsigned bits) const;
+ expr fp2sint(unsigned bits, const expr &rm) const;
+ expr fp2uint(unsigned bits, const expr &rm) const;
expr sint2fp(const expr &type, const expr &rm) const;
expr uint2fp(const expr &type, const expr &rm) const;

add more constrained FP ops