Skip to content

Commit 1ba3c55

Browse files
tautschnigtautschnig
committed
Transform float_utils unit test to use CATCH and enable it
It now tests both the approximating and non-approximating version of float_utilst.
1 parent cee5157 commit 1ba3c55

File tree

5 files changed

+201
-135
lines changed

5 files changed

+201
-135
lines changed

‎unit/CMakeLists.txt

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ list(REMOVE_ITEM sources
77
${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
88

99
# Don't build
10-
${CMAKE_CURRENT_SOURCE_DIR}/sharing_map.cpp
1110
${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
1211
${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
1312
${CMAKE_CURRENT_SOURCE_DIR}/json.cpp
@@ -16,7 +15,6 @@ list(REMOVE_ITEM sources
1615
${CMAKE_CURRENT_SOURCE_DIR}/unicode.cpp
1716
${CMAKE_CURRENT_SOURCE_DIR}/wp.cpp
1817
${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
19-
${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
2018
${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
2119

2220
# Will be built into a separate library and linked

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ SRC += unit_tests.cpp \
1616
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
1717
goto-programs/goto_trace_output.cpp \
1818
path_strategies.cpp \
19+
solvers/floatbv/float_utils.cpp \
1920
solvers/refinement/array_pool/array_pool.cpp \
2021
solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
2122
solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \

‎unit/float_utils.cpp

Lines changed: 0 additions & 133 deletions
This file was deleted.

‎unit/solvers/floatbv/float_utils.cpp

Lines changed: 196 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,196 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for float utils and approximation
4+
5+
Author: Daniel Kroening
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/catch.hpp>
10+
11+
// for debug output in case of failure
12+
#include <iostream>
13+
14+
#include <solvers/floatbv/float_approximation.h>
15+
#include <solvers/floatbv/float_utils.h>
16+
#include <solvers/sat/satcheck.h>
17+
18+
float random_float()
19+
{
20+
unsigned u=random();
21+
u=(u<<16)^random();
22+
return *reinterpret_cast<float *>(&u);
23+
}
24+
25+
bool eq(const ieee_floatt &a, const ieee_floatt &b)
26+
{
27+
return (a.is_NaN() && b.is_NaN()) ||
28+
(a.is_infinity() && b.is_infinity() && a.get_sign() == b.get_sign()) ||
29+
a == b;
30+
}
31+
32+
std::string to_str(const bvt &bv)
33+
{
34+
std::string result;
35+
for(unsigned i=0; i<bv.size(); i++)
36+
{
37+
char ch;
38+
if(bv[i]==const_literal(true))
39+
ch='1';
40+
else if(bv[i]==const_literal(false))
41+
ch='0';
42+
else
43+
ch='?';
44+
result=ch+result;
45+
}
46+
return result;
47+
}
48+
49+
typedef enum { PLUS=0, MINUS=1, MULT=2, DIV=3 } binopt;
50+
const char *binopsyms[]={ " + ", " - ", " * ", " / " };
51+
52+
float set_values(
53+
float_utilst &float_utils,
54+
float &f1,
55+
float &f2,
56+
ieee_floatt &i1,
57+
ieee_floatt &i2)
58+
{
59+
f1 = random_float();
60+
f2 = random_float();
61+
i1.from_float(f1);
62+
i2.from_float(f2);
63+
float_utils.spec = i1.spec;
64+
65+
return f1;
66+
}
67+
68+
bvt compute(
69+
unsigned i,
70+
float_utilst &float_utils,
71+
const float &f2,
72+
float &f3,
73+
const ieee_floatt &i1,
74+
const ieee_floatt &i2)
75+
{
76+
const bvt b1 = float_utils.build_constant(i1);
77+
const bvt b2 = float_utils.build_constant(i2);
78+
79+
const binopt op = reinterpret_cast<binopt>(i % 3);
80+
81+
switch(op)
82+
{
83+
case PLUS:
84+
f3 += f2;
85+
return float_utils.add(b1, b2);
86+
87+
case MINUS:
88+
f3 -= f2;
89+
return float_utils.sub(b1, b2);
90+
91+
case MULT:
92+
f3 *= f2;
93+
return float_utils.mul(b1, b2);
94+
95+
case DIV:
96+
f3 /= f2;
97+
return float_utils.div(b1, b2);
98+
}
99+
100+
return bvt();
101+
}
102+
103+
void print(
104+
unsigned i,
105+
const ieee_floatt &i1,
106+
const ieee_floatt &i2,
107+
const ieee_floatt &i3,
108+
const ieee_floatt &fres,
109+
const float &f1,
110+
const float &f2,
111+
const float &f3)
112+
{
113+
const unsigned op = i % 3;
114+
const char *opsym = binopsyms[op];
115+
116+
std::cout << i1 << opsym << i2 << " != " << fres << '\n';
117+
std::cout << f1 << opsym << f2 << " == " << f3 << '\n';
118+
std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " "
119+
<< integer2binary(i1.get_fraction(), i1.spec.f + 1) << opsym
120+
<< integer2binary(i2.get_exponent(), i1.spec.e) << " "
121+
<< integer2binary(i2.get_fraction(), i1.spec.f + 1) << " != "
122+
<< integer2binary(fres.get_exponent(), i1.spec.e) << " "
123+
<< integer2binary(fres.get_fraction(), i1.spec.f + 1) << '\n';
124+
std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " "
125+
<< integer2binary(i1.get_fraction(), i1.spec.f + 1) << opsym
126+
<< integer2binary(i2.get_exponent(), i1.spec.e) << " "
127+
<< integer2binary(i2.get_fraction(), i1.spec.f + 1) << " == "
128+
<< integer2binary(i3.get_exponent(), i1.spec.e) << " "
129+
<< integer2binary(i3.get_fraction(), i1.spec.f + 1) << '\n';
130+
}
131+
132+
SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
133+
{
134+
ieee_floatt i1, i2, i3;
135+
float f1, f2, f3;
136+
137+
for(unsigned i = 0; i < 200; i++)
138+
{
139+
satcheckt satcheck;
140+
float_utilst float_utils(satcheck);
141+
142+
GIVEN("Two random floating point numbers")
143+
{
144+
f3 = set_values(float_utils, f1, f2, i1, i2);
145+
bvt res = compute(i, float_utils, f2, f3, i1, i2);
146+
147+
THEN("Machine execution yields the same result as symbolic computation")
148+
{
149+
i3.from_float(f3);
150+
151+
const satcheckt::resultt result = satcheck.prop_solve();
152+
REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
153+
154+
const ieee_floatt fres = float_utils.get(res);
155+
156+
if(!eq(fres, i3))
157+
print(i, i1, i2, i3, fres, f1, f2, f3);
158+
159+
REQUIRE(eq(fres, i3));
160+
}
161+
}
162+
}
163+
}
164+
165+
SCENARIO("float_approximation", "[core][solvers][floatbv][float_approximation]")
166+
{
167+
ieee_floatt i1, i2, i3;
168+
float f1, f2, f3;
169+
170+
for(unsigned i = 0; i < 200; i++)
171+
{
172+
satcheckt satcheck;
173+
float_approximationt float_utils(satcheck);
174+
175+
GIVEN("Two random floating point numbers")
176+
{
177+
f3 = set_values(float_utils, f1, f2, i1, i2);
178+
bvt res = compute(i, float_utils, f2, f3, i1, i2);
179+
180+
THEN("Machine execution yields the same result as symbolic computation")
181+
{
182+
i3.from_float(f3);
183+
184+
const satcheckt::resultt result = satcheck.prop_solve();
185+
REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
186+
187+
const ieee_floatt fres = float_utils.get(res);
188+
189+
if(!eq(fres, i3))
190+
print(i, i1, i2, i3, fres, f1, f2, f3);
191+
192+
REQUIRE(eq(fres, i3));
193+
}
194+
}
195+
}
196+
}

‎unit/solvers/floatbv/module_dependencies.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
solvers/floatbv
2+
solvers/sat
3+
testing-utils
4+
util

0 commit comments

Comments
 (0)