From 8b2bd7b849c9d7beeb0c10c4f080507668aab396 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 22 Jun 2018 13:15:44 +0100 Subject: [PATCH 1/2] Convert to signed type to make negation meaningful --- src/solvers/floatbv/float_approximation.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/solvers/floatbv/float_approximation.cpp b/src/solvers/floatbv/float_approximation.cpp index 63d2e372813..16384fdb435 100644 --- a/src/solvers/floatbv/float_approximation.cpp +++ b/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(i), exponent.size()); bvt added_exponent=bv_utils.add(exponent, adjustment); bv_utils.cond_implies_equal(shift, added_exponent, new_exponent); } From e90b61bab3e0b14ea55d5b0708cc36d9b85b2e29 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Jul 2018 19:17:08 +0100 Subject: [PATCH 2/2] Transform float_utils unit test to use CATCH and enable it It now tests both the approximating and non-approximating version of float_utilst. --- unit/CMakeLists.txt | 2 - unit/Makefile | 1 + unit/float_utils.cpp | 133 ----------- unit/solvers/floatbv/float_utils.cpp | 219 +++++++++++++++++++ unit/solvers/floatbv/module_dependencies.txt | 4 + 5 files changed, 224 insertions(+), 135 deletions(-) delete mode 100644 unit/float_utils.cpp create mode 100644 unit/solvers/floatbv/float_utils.cpp create mode 100644 unit/solvers/floatbv/module_dependencies.txt diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 6def86d4887..036cc3ce4c4 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -7,7 +7,6 @@ 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 @@ -15,7 +14,6 @@ list(REMOVE_ITEM sources ${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 diff --git a/unit/Makefile b/unit/Makefile index a52eafa79b8..1e4dc900bdd 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/float_utils.cpp b/unit/float_utils.cpp deleted file mode 100644 index d9280280c41..00000000000 --- a/unit/float_utils.cpp +++ /dev/null @@ -1,133 +0,0 @@ -#include - -#include -#include - -float random_float() -{ - unsigned u=random(); - u=(u<<16)^random(); - return *(float *)&u; -} - -bool eq(const ieee_floatt &a, const ieee_floatt &b) -{ - if(a.is_NaN() && b.is_NaN()) return true; - if(a.is_infinity() && b.is_infinity() && - a.get_sign()==b.get_sign()) return true; - return a==b; -} - -std::string to_str(const bvt &bv) -{ - std::string result; - for(unsigned i=0; i + +// for debug output in case of failure +#include +#include +#include + +#include +#include +#include + +typedef std::uniform_int_distribution 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::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::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)); + } + } + } +} diff --git a/unit/solvers/floatbv/module_dependencies.txt b/unit/solvers/floatbv/module_dependencies.txt new file mode 100644 index 00000000000..1a7bba2910a --- /dev/null +++ b/unit/solvers/floatbv/module_dependencies.txt @@ -0,0 +1,4 @@ +solvers/floatbv +solvers/sat +testing-utils +util