Add FloatType::toInt

AliveToolkit · Jan 5, 2025 · be245a9 · be245a9
1 parent b7cf1ae
commit be245a9
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git 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
@@ -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;