Merge pull request #8552 from diffblue/ieee_floatt_one

`ieee_floatt::one`(...)

src/goto-programs/interpreter_evaluate.cpp

@@ -709,9 +709,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      ieee_floatt f(to_floatbv_type(expr.type()));
-      f.from_integer(1);
-      result=f.pack();
+      result = ieee_floatt::one(to_floatbv_type(expr.type())).pack();
     }
     else
       result=1;

src/solvers/flattening/boolbv_typecast.cpp

@@ -204,10 +204,8 @@ bool boolbvt::type_conversion(
         // bool to float
 
         // build a one
-        ieee_floatt f(to_floatbv_type(dest_type));
-        f.from_integer(1);
-
-        dest = convert_bv(f.to_expr());
+        auto one = ieee_floatt::one(to_floatbv_type(dest_type));
+        dest = convert_bv(one.to_expr());
 
         INVARIANT(
           src_width == 1, "bitvector of type boolean shall have width one");

src/solvers/smt2/smt2_conv.cpp

@@ -3064,32 +3064,13 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
 
     if(src_type.id()==ID_bool)
     {
-      constant_exprt val(irep_idt(), dest_type);
-
-      ieee_floatt a(dest_floatbv_type);
-
-      mp_integer significand;
-      mp_integer exponent;
-
       out << "(ite ";
       convert_expr(src);
-      out << " ";
-
-      significand = 1;
-      exponent = 0;
-      a.build(significand, exponent);
-      val.set_value(integer2bvrep(a.pack(), a.spec.width()));
-
-      convert_constant(val);
-      out << " ";
-
-      significand = 0;
-      exponent = 0;
-      a.build(significand, exponent);
-      val.set_value(integer2bvrep(a.pack(), a.spec.width()));
-
-      convert_constant(val);
-      out << ")";
+      out << ' ';
+      convert_constant(ieee_floatt::one(dest_floatbv_type).to_expr());
+      out << ' ';
+      convert_constant(ieee_floatt::zero(dest_floatbv_type).to_expr());
+      out << ')';
     }
     else if(src_type.id()==ID_c_bool)
     {

src/util/ieee_float.cpp

@@ -470,6 +470,19 @@ void ieee_floatt::extract_base10(
   }
 }
 
+ieee_floatt ieee_floatt::one(const ieee_float_spect &spec)
+{
+  ieee_floatt result{spec};
+  result.exponent = 0;
+  result.fraction = power(2, result.spec.f);
+  return result;
+}
+
+ieee_floatt ieee_floatt::one(const floatbv_typet &type)
+{
+  return one(ieee_float_spect{type});
+}
+
 void ieee_floatt::build(
   const mp_integer &_fraction,
   const mp_integer &_exponent)

src/util/ieee_float.h

@@ -220,6 +220,16 @@ class ieee_floatt
     return result;
   }
 
+  static ieee_floatt zero(const ieee_float_spect &spec)
+  {
+    ieee_floatt result(spec);
+    result.make_zero();
+    return result;
+  }
+
+  static ieee_floatt one(const floatbv_typet &);
+  static ieee_floatt one(const ieee_float_spect &);
+
   void make_NaN();
   void make_plus_infinity();
   void make_minus_infinity();

unit/Makefile

@@ -150,6 +150,7 @@ SRC += analyses/ai/ai.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \
        util/help_formatter.cpp \
+       util/ieee_float.cpp \
        util/interval/add.cpp \
        util/interval/bitwise.cpp \
        util/interval/comparisons.cpp \

unit/util/ieee_float.cpp

@@ -0,0 +1,17 @@
+/*******************************************************************\
+
+Module: Unit tests for ieee_floatt
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/ieee_float.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Make an IEEE 754 one", "[core][util][ieee_float]")
+{
+  auto spec = ieee_float_spect::single_precision();
+  REQUIRE(ieee_floatt::one(spec) == 1);
+}