Convert to signed type to make negation meaningful

src/solvers/floatbv/float_approximation.cpp

@@ -48,7 +48,8 @@ void float_approximationt::normalization_shift(bvt &fraction, bvt &exponent)
     bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
 
     // build new exponent
-    bvt adjustment=bv_utils.build_constant(-i, exponent.size());
+    bvt adjustment =
+      bv_utils.build_constant(-static_cast<int>(i), exponent.size());
     bvt added_exponent=bv_utils.add(exponent, adjustment);
     bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
   }

unit/CMakeLists.txt

@@ -7,15 +7,13 @@ list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
 
     # Don't build
-    ${CMAKE_CURRENT_SOURCE_DIR}/sharing_map.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/json.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/cpp_parser.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/osx_fat_reader.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/wp.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
 
     # Will be built into a separate library and linked

unit/Makefile

@@ -17,6 +17,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
        path_strategies.cpp \
+       solvers/floatbv/float_utils.cpp \
        solvers/refinement/array_pool/array_pool.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \

unit/solvers/floatbv/float_utils.cpp

@@ -0,0 +1,219 @@
+/*******************************************************************\
+
+ Module: Unit tests for float utils and approximation
+
+ Author: Daniel Kroening
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+// for debug output in case of failure
+#include <iostream>
+#include <limits>
+#include <random>
+
+#include <solvers/floatbv/float_approximation.h>
+#include <solvers/floatbv/float_utils.h>
+#include <solvers/sat/satcheck.h>
+
+typedef std::uniform_int_distribution<unsigned> distt;
+
+static float random_float(distt &dist, std::mt19937 &gen)
+{
+  union
+  {
+    float f;
+    unsigned int i;
+  } u;
+
+  u.i = dist(gen);
+  u.i = (u.i << 16) ^ dist(gen);
+
+  return u.f;
+}
+
+static bool eq(const ieee_floatt &a, const ieee_floatt &b)
+{
+  return (a.is_NaN() && b.is_NaN()) ||
+         (a.is_infinity() && b.is_infinity() && a.get_sign() == b.get_sign()) ||
+         a == b;
+}
+
+#if 0
+static std::string to_str(const bvt &bv)
+{
+  std::string result;
+  for(unsigned i=0; i<bv.size(); i++)
+  {
+    char ch;
+    if(bv[i]==const_literal(true))
+      ch='1';
+    else if(bv[i]==const_literal(false))
+      ch='0';
+    else
+      ch='?';
+    result=ch+result;
+  }
+  return result;
+}
+#endif
+
+typedef enum { PLUS=0, MINUS=1, MULT=2, DIV=3 } binopt;
+const char *binopsyms[]={ " + ", " - ", " * ", " / " };
+
+static float set_values(
+  distt &dist,
+  std::mt19937 &gen,
+  float_utilst &float_utils,
+  float &f1,
+  float &f2,
+  ieee_floatt &i1,
+  ieee_floatt &i2)
+{
+  f1 = random_float(dist, gen);
+  f2 = random_float(dist, gen);
+  i1.from_float(f1);
+  i2.from_float(f2);
+  float_utils.spec = i1.spec;
+
+  return f1;
+}
+
+static bvt compute(
+  unsigned i,
+  float_utilst &float_utils,
+  const float &f2,
+  float &f3,
+  const ieee_floatt &i1,
+  const ieee_floatt &i2)
+{
+  const bvt b1 = float_utils.build_constant(i1);
+  const bvt b2 = float_utils.build_constant(i2);
+
+  const auto op = i % 3;
+
+  switch(op)
+  {
+  case PLUS:
+    f3 += f2;
+    return float_utils.add(b1, b2);
+
+  case MINUS:
+    f3 -= f2;
+    return float_utils.sub(b1, b2);
+
+  case MULT:
+    f3 *= f2;
+    return float_utils.mul(b1, b2);
+
+  case DIV:
+    f3 /= f2;
+    return float_utils.div(b1, b2);
+  }
+
+  return bvt();
+}
+
+static void print(
+  unsigned i,
+  const ieee_floatt &i1,
+  const ieee_floatt &i2,
+  const ieee_floatt &i3,
+  const ieee_floatt &fres,
+  const float &f1,
+  const float &f2,
+  const float &f3)
+{
+  const unsigned op = i % 3;
+  const char *opsym = binopsyms[op];
+
+  std::cout << i1 << opsym << i2 << " != " << fres << '\n';
+  std::cout << f1 << opsym << f2 << " == " << f3 << '\n';
+  std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i1.get_fraction(), i1.spec.f + 1) << opsym
+            << integer2binary(i2.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i2.get_fraction(), i1.spec.f + 1) << " != "
+            << integer2binary(fres.get_exponent(), i1.spec.e) << " "
+            << integer2binary(fres.get_fraction(), i1.spec.f + 1) << '\n';
+  std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i1.get_fraction(), i1.spec.f + 1) << opsym
+            << integer2binary(i2.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i2.get_fraction(), i1.spec.f + 1) << " == "
+            << integer2binary(i3.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i3.get_fraction(), i1.spec.f + 1) << '\n';
+}
+
+SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
+{
+  ieee_floatt i1, i2, i3;
+  float f1, f2, f3;
+
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  distt dist(0, std::numeric_limits<unsigned>::max());
+
+  for(unsigned i = 0; i < 200; i++)
+  {
+    satcheckt satcheck;
+    float_utilst float_utils(satcheck);
+
+    GIVEN("Two random floating point numbers")
+    {
+      f3 = set_values(dist, gen, float_utils, f1, f2, i1, i2);
+      bvt res = compute(i, float_utils, f2, f3, i1, i2);
+
+      THEN("Machine execution yields the same result as symbolic computation")
+      {
+        i3.from_float(f3);
+
+        const satcheckt::resultt result = satcheck.prop_solve();
+        REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
+
+        const ieee_floatt fres = float_utils.get(res);
+
+        if(!eq(fres, i3))
+          print(i, i1, i2, i3, fres, f1, f2, f3);
+
+        REQUIRE(eq(fres, i3));
+      }
+    }
+  }
+}
+
+SCENARIO("float_approximation", "[core][solvers][floatbv][float_approximation]")
+{
+  ieee_floatt i1, i2, i3;
+  float f1, f2, f3;
+
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  distt dist(0, std::numeric_limits<unsigned>::max());
+
+  for(unsigned i = 0; i < 200; i++)
+  {
+    satcheckt satcheck;
+    float_approximationt float_utils(satcheck);
+
+    GIVEN("Two random floating point numbers")
+    {
+      f3 = set_values(dist, gen, float_utils, f1, f2, i1, i2);
+      bvt res = compute(i, float_utils, f2, f3, i1, i2);
+
+      THEN("Machine execution yields the same result as symbolic computation")
+      {
+        i3.from_float(f3);
+
+        const satcheckt::resultt result = satcheck.prop_solve();
+        REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
+
+        const ieee_floatt fres = float_utils.get(res);
+
+        if(!eq(fres, i3))
+          print(i, i1, i2, i3, fres, f1, f2, f3);
+
+        REQUIRE(eq(fres, i3));
+      }
+    }
+  }
+}

unit/solvers/floatbv/module_dependencies.txt

@@ -0,0 +1,4 @@
+solvers/floatbv
+solvers/sat
+testing-utils
+util