Skip to content

Commit 4112d43

Browse files
kroeningkroening
committed
Split ieee_floatt into ieee_float_valuet and ieee_floatt
This splits ieee_floatt into two parts: 1) ieee_float_valuet stores an IEEE 754 floating-point value. It offers no operations that require rounding, and hence, does not require a rounding mode. 2) ieee_floatt extends ieee_float_valuet with a rounding mode, and hence, offers operators that require rounding.
1 parent 36b2335 commit 4112d43

33 files changed

+527
-477
lines changed

Diff for: ‎jbmc/src/java_bytecode/assignments_from_json.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -358,13 +358,13 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)
358358
}
359359
else if(expr.type() == java_double_type())
360360
{
361-
ieee_floatt ieee_float(to_floatbv_type(expr.type()));
361+
ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
362362
ieee_float.from_double(std::stod(json.value));
363363
result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
364364
}
365365
else if(expr.type() == java_float_type())
366366
{
367-
ieee_floatt ieee_float(to_floatbv_type(expr.type()));
367+
ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
368368
ieee_float.from_float(std::stof(json.value));
369369
result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
370370
}

Diff for: ‎jbmc/src/java_bytecode/expr2java.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -230,7 +230,7 @@ std::string expr2javat::convert_constant(
230230
(src.type()==java_double_type()))
231231
{
232232
// This converts NaNs to the canonical NaN
233-
const ieee_floatt ieee_repr(to_constant_expr(src));
233+
const ieee_float_valuet ieee_repr(to_constant_expr(src));
234234
if(ieee_repr.is_double())
235235
return floating_point_to_java_string(ieee_repr.to_double());
236236
return floating_point_to_java_string(ieee_repr.to_float());

Diff for: ‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -2181,16 +2181,19 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
21812181
is_float ? ieee_float_spect::single_precision()
21822182
: ieee_float_spect::double_precision());
21832183

2184-
ieee_floatt value(spec);
21852184
if(arg0.type().id() != ID_floatbv)
21862185
{
2186+
// conversion from integer to float may need rounding
2187+
auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
21872188
const mp_integer number = numeric_cast_v<mp_integer>(arg0);
2189+
ieee_floatt value(spec, rm);
21882190
value.from_integer(number);
2191+
results[0] = value.to_expr();
21892192
}
21902193
else
2191-
value.from_expr(arg0);
2192-
2193-
results[0] = value.to_expr();
2194+
{
2195+
results[0] = ieee_float_valuet{arg0}.to_expr();
2196+
}
21942197
}
21952198
else
21962199
{

Diff for: ‎jbmc/src/java_bytecode/java_bytecode_parser.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -782,7 +782,7 @@ void java_bytecode_parsert::rconstant_pool()
782782

783783
case CONSTANT_Float:
784784
{
785-
ieee_floatt value(ieee_float_spect::single_precision());
785+
ieee_float_valuet value(ieee_float_spect::single_precision());
786786
value.unpack(entry.number);
787787
entry.expr = value.to_expr();
788788
}
@@ -794,7 +794,7 @@ void java_bytecode_parsert::rconstant_pool()
794794

795795
case CONSTANT_Double:
796796
{
797-
ieee_floatt value(ieee_float_spect::double_precision());
797+
ieee_float_valuet value(ieee_float_spect::double_precision());
798798
value.unpack(entry.number);
799799
entry.expr = value.to_expr();
800800
}

Diff for: ‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

+5-4
Original file line numberDiff line numberDiff line change
@@ -938,7 +938,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
938938

939939
// Expression representing 0.0
940940
const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
941-
ieee_floatt zero_float(float_spec);
941+
ieee_float_valuet zero_float(float_spec);
942942
zero_float.from_float(0.0);
943943
const constant_exprt zero = zero_float.to_expr();
944944

@@ -996,16 +996,17 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
996996
string_expr_list.push_back(zero_string);
997997

998998
// Case of -0.0
999-
ieee_floatt minus_zero_float(float_spec);
999+
ieee_float_valuet minus_zero_float(float_spec);
10001000
minus_zero_float.from_float(-0.0f);
10011001
condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
10021002
const refined_string_exprt minus_zero_string =
10031003
string_literal_to_string_expr("-0.0", loc, symbol_table, code);
10041004
string_expr_list.push_back(minus_zero_string);
10051005

10061006
// Case of simple notation
1007-
ieee_floatt bound_inf_float(float_spec);
1008-
ieee_floatt bound_sup_float(float_spec);
1007+
auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
1008+
ieee_floatt bound_inf_float(float_spec, rm);
1009+
ieee_floatt bound_sup_float(float_spec, rm);
10091010
bound_inf_float.from_float(1e-3f);
10101011
bound_sup_float.from_float(1e7f);
10111012
bound_inf_float.change_spec(float_spec);

Diff for: ‎src/analyses/interval_domain.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -288,7 +288,7 @@ void interval_domaint::assume_rec(
288288
}
289289
else if(is_float(lhs.type()) && is_float(rhs.type()))
290290
{
291-
ieee_floatt tmp(to_constant_expr(rhs));
291+
ieee_float_valuet tmp(to_constant_expr(rhs));
292292
if(id==ID_lt)
293293
tmp.decrement();
294294
ieee_float_intervalt &fi=float_map[lhs_identifier];
@@ -313,7 +313,7 @@ void interval_domaint::assume_rec(
313313
}
314314
else if(is_float(lhs.type()) && is_float(rhs.type()))
315315
{
316-
ieee_floatt tmp(to_constant_expr(lhs));
316+
ieee_float_valuet tmp(to_constant_expr(lhs));
317317
if(id==ID_lt)
318318
tmp.increment();
319319
ieee_float_intervalt &fi=float_map[rhs_identifier];

Diff for: ‎src/analyses/interval_domain.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include "ai_domain.h"
2020

21-
typedef interval_templatet<ieee_floatt> ieee_float_intervalt;
21+
typedef interval_templatet<ieee_float_valuet> ieee_float_intervalt;
2222

2323
class interval_domaint:public ai_domain_baset
2424
{

Diff for: ‎src/ansi-c/expr2c.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1912,7 +1912,7 @@ std::string expr2ct::convert_constant(
19121912
}
19131913
else if(type.id()==ID_floatbv)
19141914
{
1915-
dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();
1915+
dest = ieee_float_valuet(to_constant_expr(src)).to_ansi_c_string();
19161916

19171917
if(!dest.empty() && isdigit(dest[dest.size() - 1]))
19181918
{

Diff for: ‎src/ansi-c/goto-conversion/goto_check_c.cpp

+10-8
Original file line numberDiff line numberDiff line change
@@ -761,12 +761,13 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
761761
else if(old_type.id() == ID_floatbv) // float -> signed
762762
{
763763
// Note that the fractional part is truncated!
764-
ieee_floatt upper(to_floatbv_type(old_type));
764+
auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
765+
ieee_floatt upper(to_floatbv_type(old_type), rm);
765766
upper.from_integer(power(2, new_width - 1));
766767
const binary_relation_exprt no_overflow_upper(
767768
op, ID_lt, upper.to_expr());
768769

769-
ieee_floatt lower(to_floatbv_type(old_type));
770+
ieee_floatt lower(to_floatbv_type(old_type), rm);
770771
lower.from_integer(-power(2, new_width - 1) - 1);
771772
const binary_relation_exprt no_overflow_lower(
772773
op, ID_gt, lower.to_expr());
@@ -844,12 +845,13 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
844845
else if(old_type.id() == ID_floatbv) // float -> unsigned
845846
{
846847
// Note that the fractional part is truncated!
847-
ieee_floatt upper(to_floatbv_type(old_type));
848+
auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
849+
ieee_floatt upper(to_floatbv_type(old_type), rm);
848850
upper.from_integer(power(2, new_width));
849851
const binary_relation_exprt no_overflow_upper(
850852
op, ID_lt, upper.to_expr());
851853

852-
ieee_floatt lower(to_floatbv_type(old_type));
854+
ieee_floatt lower(to_floatbv_type(old_type), rm);
853855
lower.from_integer(-1);
854856
const binary_relation_exprt no_overflow_lower(
855857
op, ID_gt, lower.to_expr());
@@ -1295,8 +1297,8 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
12951297
// -inf + +inf = NaN and +inf + -inf = NaN,
12961298
// i.e., signs differ
12971299
ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
1298-
exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1299-
exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1300+
exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
1301+
exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
13001302

13011303
isnan = or_exprt(
13021304
and_exprt(
@@ -1315,8 +1317,8 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
13151317

13161318
ieee_float_spect spec =
13171319
ieee_float_spect(to_floatbv_type(minus_expr.type()));
1318-
exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
1319-
exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
1320+
exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
1321+
exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
13201322

13211323
isnan = or_exprt(
13221324
and_exprt(

Diff for: ‎src/ansi-c/literals/convert_float_literal.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,9 @@ exprt convert_float_literal(const std::string &src)
7171
// but these aren't handled anywhere
7272
}
7373

74-
ieee_floatt a(type);
74+
// This may require rounding.
75+
auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
76+
ieee_floatt a(type, rm);
7577

7678
if(parsed_float.exponent_base==10)
7779
a.from_base10(parsed_float.significand, parsed_float.exponent);

Diff for: ‎src/goto-instrument/goto_program2code.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1923,7 +1923,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
19231923
{
19241924
if(expr.type().id()==ID_floatbv)
19251925
{
1926-
const ieee_floatt f(to_constant_expr(expr));
1926+
const ieee_float_valuet f(to_constant_expr(expr));
19271927
if(f.is_NaN() || f.is_infinity())
19281928
system_headers.insert("math.h");
19291929
}

Diff for: ‎src/goto-programs/interpreter.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -576,7 +576,7 @@ exprt interpretert::get_value(
576576
}
577577
else if(type.id() == ID_floatbv)
578578
{
579-
ieee_floatt f(to_floatbv_type(type));
579+
ieee_float_valuet f(to_floatbv_type(type));
580580
f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
581581
return f.to_expr();
582582
}

Diff for: ‎src/goto-programs/interpreter_evaluate.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
364364
}
365365
else if(expr.type().id()==ID_floatbv)
366366
{
367-
ieee_floatt f;
367+
ieee_float_valuet f;
368368
f.from_expr(to_constant_expr(expr));
369369
return {f.pack()};
370370
}
@@ -731,8 +731,9 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
731731
}
732732
else if(expr.type().id()==ID_floatbv)
733733
{
734-
ieee_floatt f1(to_floatbv_type(expr.type()));
735-
ieee_floatt f2(to_floatbv_type(op.type()));
734+
auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
735+
ieee_floatt f1(to_floatbv_type(expr.type()), rm);
736+
ieee_floatt f2(to_floatbv_type(op.type()), rm);
736737
f1.unpack(result);
737738
f2.unpack(tmp.front());
738739
f1*=f2;

Diff for: ‎src/goto-programs/json_expr.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -276,7 +276,7 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
276276
json_numbert(std::to_string(to_bitvector_type(type).get_width()));
277277
result["binary"] = json_stringt(binary(constant_expr));
278278
result["data"] =
279-
json_stringt(ieee_floatt(constant_expr).to_ansi_c_string());
279+
json_stringt(ieee_float_valuet(constant_expr).to_ansi_c_string());
280280
}
281281
else if(type.id() == ID_pointer)
282282
{

Diff for: ‎src/goto-programs/xml_expr.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
212212
result.set_attribute("width", width);
213213
result.set_attribute(
214214
"binary", integer2binary(bvrep2integer(value, width, false), width));
215-
result.data = ieee_floatt(constant_expr).to_ansi_c_string();
215+
result.data = ieee_float_valuet(constant_expr).to_ansi_c_string();
216216
}
217217
else if(type.id() == ID_pointer)
218218
{

Diff for: ‎src/solvers/floatbv/float_bv.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -240,7 +240,7 @@ exprt float_bvt::is_zero(const exprt &src)
240240

241241
constant_exprt mask(integer2bvrep(v, width), src.type());
242242

243-
ieee_floatt z(type);
243+
ieee_float_valuet z(type);
244244
z.make_zero();
245245

246246
return equal_exprt(bitand_exprt(src, mask), z.to_expr());

Diff for: ‎src/solvers/floatbv/float_utils.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ bvt float_utilst::to_integer(
136136
return result;
137137
}
138138

139-
bvt float_utilst::build_constant(const ieee_floatt &src)
139+
bvt float_utilst::build_constant(const ieee_float_valuet &src)
140140
{
141141
unbiased_floatt result;
142142

@@ -1268,14 +1268,14 @@ bvt float_utilst::pack(const biased_floatt &src)
12681268
return result;
12691269
}
12701270

1271-
ieee_floatt float_utilst::get(const bvt &src) const
1271+
ieee_float_valuet float_utilst::get(const bvt &src) const
12721272
{
12731273
mp_integer int_value=0;
12741274

12751275
for(std::size_t i=0; i<src.size(); i++)
12761276
int_value+=power(2, i)*prop.l_get(src[i]).is_true();
12771277

1278-
ieee_floatt result;
1278+
ieee_float_valuet result;
12791279
result.spec=spec;
12801280
result.unpack(int_value);
12811281

Diff for: ‎src/solvers/floatbv/float_utils.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ class float_utilst
8787

8888
ieee_float_spect spec;
8989

90-
bvt build_constant(const ieee_floatt &);
90+
bvt build_constant(const ieee_float_valuet &);
9191

9292
static inline literalt sign_bit(const bvt &src)
9393
{
@@ -139,7 +139,7 @@ class float_utilst
139139
literalt relation(const bvt &src1, relt rel, const bvt &src2);
140140

141141
// constants
142-
ieee_floatt get(const bvt &) const;
142+
ieee_float_valuet get(const bvt &) const;
143143

144144
// helpers
145145
literalt exponent_all_ones(const bvt &);

Diff for: ‎src/solvers/smt2/smt2_conv.cpp

+6-4
Original file line numberDiff line numberDiff line change
@@ -476,23 +476,25 @@ constant_exprt smt2_convt::parse_literal(
476476
{
477477
std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
478478
std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
479-
return ieee_floatt::plus_infinity(ieee_float_spect(s - 1, e)).to_expr();
479+
return ieee_float_valuet::plus_infinity(ieee_float_spect(s - 1, e))
480+
.to_expr();
480481
}
481482
else if(src.get_sub().size()==4 &&
482483
src.get_sub()[0].id()=="_" &&
483484
src.get_sub()[1].id()=="-oo") // (_ -oo e s)
484485
{
485486
std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
486487
std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
487-
return ieee_floatt::minus_infinity(ieee_float_spect(s - 1, e)).to_expr();
488+
return ieee_float_valuet::minus_infinity(ieee_float_spect(s - 1, e))
489+
.to_expr();
488490
}
489491
else if(src.get_sub().size()==4 &&
490492
src.get_sub()[0].id()=="_" &&
491493
src.get_sub()[1].id()=="NaN") // (_ NaN e s)
492494
{
493495
std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
494496
std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
495-
return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
497+
return ieee_float_valuet::NaN(ieee_float_spect(s - 1, e)).to_expr();
496498
}
497499

498500
if(type.id()==ID_signedbv ||
@@ -3445,7 +3447,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
34453447
significands including the hidden bit. Thus some encoding
34463448
is needed to get to IEEE-754 style representations. */
34473449

3448-
ieee_floatt v=ieee_floatt(expr);
3450+
ieee_float_valuet v = ieee_float_valuet(expr);
34493451
size_t e=floatbv_type.get_e();
34503452
size_t f=floatbv_type.get_f()+1;
34513453

Diff for: ‎src/solvers/smt2/smt2_format.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
9393
}
9494
else if(expr_type.id() == ID_floatbv)
9595
{
96-
const ieee_floatt v = ieee_floatt(constant_expr);
96+
const ieee_float_valuet v = ieee_float_valuet(constant_expr);
9797
const size_t e = v.spec.e;
9898
const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit
9999

Diff for: ‎src/solvers/strings/string_constraint_generator_float.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ exprt get_significand(
7777
/// \return an expression representing this floating point
7878
exprt constant_float(const double f, const ieee_float_spect &float_spec)
7979
{
80-
ieee_floatt fl(float_spec);
80+
ieee_float_valuet fl(float_spec);
8181
if(float_spec == ieee_float_spect::single_precision())
8282
fl.from_float(f);
8383
else if(float_spec == ieee_float_spect::double_precision())

Diff for: ‎src/statement-list/converters/convert_real_literal.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Author: Matthias Weiss, [email protected]
1818

1919
constant_exprt convert_real_literal(const std::string &src)
2020
{
21-
ieee_floatt real{get_real_type()};
21+
ieee_float_valuet real{get_real_type()};
2222
real.from_float(std::stof(src));
2323
return real.to_expr();
2424
}

Diff for: ‎src/statement-list/statement_list_parse_tree_io.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ static void output_constant(std::ostream &os, const constant_exprt &constant)
3131
os << ivalue;
3232
else if(can_cast_type<floatbv_typet>(constant.type()))
3333
{
34-
ieee_floatt real{get_real_type()};
34+
ieee_float_valuet real{get_real_type()};
3535
real.from_expr(constant);
3636
os << real.to_float();
3737
}

Diff for: ‎src/util/arith_tools.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,9 @@ constant_exprt from_integer(
171171
}
172172
else if(type_id==ID_floatbv)
173173
{
174-
ieee_floatt ieee_float(to_floatbv_type(type));
174+
ieee_floatt ieee_float(
175+
to_floatbv_type(type), ieee_floatt::rounding_modet::ROUND_TO_EVEN);
176+
// always rounds to zero
175177
ieee_float.from_integer(int_value);
176178
return ieee_float.to_expr();
177179
}

0 commit comments

Comments
 (0)