diff --git a/ir/type.cpp b/ir/type.cpp index f67e69d31..2cc64a823 100644 --- a/ir/type.cpp +++ b/ir/type.cpp @@ -525,6 +525,22 @@ expr FloatType::isNaN(const expr &v, bool signalling) const { } } +smt::expr FloatType::toInt(State &s, smt::expr v) const { + expr isnan = v.BV2float(getDummyFloat()).isNaN(); + + if (isnan.isFalse()) + return v; + + expr sign = s.getFreshNondetVar("#sign", expr::mkUInt(0, 1)); + expr nan = sign.concat(v.trunc(bits() - 1)); + + return expr::mkIf(isnan, nan, v); +} + +IR::StateValue FloatType::toInt(State &s, IR::StateValue v) const { + return Type::toInt(s, std::move(v)); +} + unsigned FloatType::bits() const { assert(fpType != Unknown); return float_sizes[fpType].first; diff --git a/ir/type.h b/ir/type.h index b2b02c9e7..11bcabcba 100644 --- a/ir/type.h +++ b/ir/type.h @@ -207,6 +207,8 @@ class FloatType final : public Type { unsigned nary, const smt::expr &a, const smt::expr &b = {}, const smt::expr &c = {}) const; smt::expr isNaN(const smt::expr &v, bool signalling) const; + smt::expr toInt(State &s, smt::expr v) const override; + IR::StateValue toInt(State &s, IR::StateValue v) const override; IR::StateValue getDummyValue(bool non_poison) const override; smt::expr getTypeConstraints() const override;