Skip to content

Commit 71da49a

Browse files
kroeningkroening
authored
Merge pull request #6199 from diffblue/floatbv_mod
floating-point mod and remainder
2 parents 43c7f71 + 5f7eedc commit 71da49a

17 files changed

+186
-26
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1558,8 +1558,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
15581558
else if(bytecode == patternt("?rem"))
15591559
{
15601560
PRECONDITION(op.size() == 2 && results.size() == 1);
1561+
// This is _not_ the remainder operation defined by IEEE 754,
1562+
// but similar to the fmod C library function.
15611563
if(bytecode == BC_frem || bytecode == BC_drem)
1562-
results[0]=rem_exprt(op[0], op[1]);
1564+
results[0] = binary_exprt(op[0], ID_floatbv_mod, op[1]);
15631565
else
15641566
results[0]=mod_exprt(op[0], op[1]);
15651567
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2567,6 +2567,54 @@ exprt c_typecheck_baset::do_special_functions(
25672567

25682568
return std::move(abs_expr);
25692569
}
2570+
else if(
2571+
identifier == CPROVER_PREFIX "fmod" ||
2572+
identifier == CPROVER_PREFIX "fmodf" ||
2573+
identifier == CPROVER_PREFIX "fmodl")
2574+
{
2575+
if(expr.arguments().size() != 2)
2576+
{
2577+
error().source_location = f_op.source_location();
2578+
error() << "fmod-functions expect two operands" << eom;
2579+
throw 0;
2580+
}
2581+
2582+
typecheck_function_call_arguments(expr);
2583+
2584+
// Note that the semantics differ from the
2585+
// "floating point remainder" operation as defined by IEEE.
2586+
// Note that these do not take a rounding mode.
2587+
binary_exprt fmod_expr(
2588+
expr.arguments()[0], ID_floatbv_mod, expr.arguments()[1]);
2589+
2590+
fmod_expr.add_source_location() = source_location;
2591+
2592+
return std::move(fmod_expr);
2593+
}
2594+
else if(
2595+
identifier == CPROVER_PREFIX "remainder" ||
2596+
identifier == CPROVER_PREFIX "remainderf" ||
2597+
identifier == CPROVER_PREFIX "remainderl")
2598+
{
2599+
if(expr.arguments().size() != 2)
2600+
{
2601+
error().source_location = f_op.source_location();
2602+
error() << "remainder-functions expect two operands" << eom;
2603+
throw 0;
2604+
}
2605+
2606+
typecheck_function_call_arguments(expr);
2607+
2608+
// The semantics of these functions is meant to match the
2609+
// "floating point remainder" operation as defined by IEEE.
2610+
// Note that these do not take a rounding mode.
2611+
binary_exprt floatbv_rem_expr(
2612+
expr.arguments()[0], ID_floatbv_rem, expr.arguments()[1]);
2613+
2614+
floatbv_rem_expr.add_source_location() = source_location;
2615+
2616+
return std::move(floatbv_rem_expr);
2617+
}
25702618
else if(identifier==CPROVER_PREFIX "allocate")
25712619
{
25722620
if(expr.arguments().size()!=2)

‎src/ansi-c/cprover_builtin_headers.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,14 @@ double __CPROVER_fabs(double x);
8686
long double __CPROVER_fabsl(long double x);
8787
float __CPROVER_fabsf(float x);
8888

89+
// modulo and remainder
90+
double __CPROVER_fmod(double, double);
91+
float __CPROVER_fmodf(float, float);
92+
long double __CPROVER_fmodl(long double, long double);
93+
double __CPROVER_remainder(double, double);
94+
float __CPROVER_remainderf(float, float);
95+
long double __CPROVER_remainderl(long double, long double);
96+
8997
// arrays
9098
__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
9199
// overwrite all of *dest (possibly using nondet values), even

‎src/ansi-c/library/cprover.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,14 @@ double __CPROVER_fabs(double);
117117
long double __CPROVER_fabsl(long double);
118118
float __CPROVER_fabsf(float);
119119

120+
// modulo and remainder
121+
double __CPROVER_fmod(double, double);
122+
float __CPROVER_fmodf(float, float);
123+
long double __CPROVER_fmodl(long double, long double);
124+
double __CPROVER_remainder(double, double);
125+
float __CPROVER_remainderf(float, float);
126+
long double __CPROVER_remainderl(long double, long double);
127+
120128
// arrays
121129
//__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
122130
void __CPROVER_array_copy(const void *dest, const void *src);

‎src/ansi-c/library/math.c

Lines changed: 12 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -2140,10 +2140,10 @@ long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long
21402140
#define __CPROVER_FENV_H_INCLUDED
21412141
#endif
21422142

2143-
double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y);
2144-
2145-
double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZERO, x, y); }
2146-
2143+
double fmod(double x, double y)
2144+
{
2145+
return __CPROVER_fmod(x, y);
2146+
}
21472147

21482148
/* FUNCTION: fmodf */
21492149

@@ -2157,10 +2157,10 @@ double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZE
21572157
#define __CPROVER_FENV_H_INCLUDED
21582158
#endif
21592159

2160-
float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y);
2161-
2162-
float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZERO, x, y); }
2163-
2160+
float fmodf(float x, float y)
2161+
{
2162+
return __CPROVER_fmodf(x, y);
2163+
}
21642164

21652165
/* FUNCTION: fmodl */
21662166

@@ -2174,11 +2174,10 @@ float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZER
21742174
#define __CPROVER_FENV_H_INCLUDED
21752175
#endif
21762176

2177-
long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y);
2178-
2179-
long double fmodl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TOWARDZERO, x, y); }
2180-
2181-
2177+
long double fmodl(long double x, long double y)
2178+
{
2179+
return __CPROVER_fmodl(x, y);
2180+
}
21822181

21832182
/* ISO 9899:2011
21842183
*

‎src/goto-programs/adjust_float_expressions.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -41,9 +41,9 @@ static bool have_to_adjust_float_expressions(const exprt &expr)
4141
type.id() == ID_floatbv ||
4242
(type.id() == ID_complex && type.subtype().id() == ID_floatbv))
4343
{
44-
if(expr.id()==ID_plus || expr.id()==ID_minus ||
45-
expr.id()==ID_mult || expr.id()==ID_div ||
46-
expr.id()==ID_rem)
44+
if(
45+
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
46+
expr.id() == ID_div)
4747
return true;
4848
}
4949

@@ -95,9 +95,9 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
9595
type.id() == ID_floatbv ||
9696
(type.id() == ID_complex && type.subtype().id() == ID_floatbv))
9797
{
98-
if(expr.id()==ID_plus || expr.id()==ID_minus ||
99-
expr.id()==ID_mult || expr.id()==ID_div ||
100-
expr.id()==ID_rem)
98+
if(
99+
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
100+
expr.id() == ID_div)
101101
{
102102
DATA_INVARIANT(
103103
expr.operands().size() >= 2,
@@ -115,7 +115,6 @@ void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
115115
expr.id()==ID_minus?ID_floatbv_minus:
116116
expr.id()==ID_mult?ID_floatbv_mult:
117117
expr.id()==ID_div?ID_floatbv_div:
118-
expr.id()==ID_rem?ID_floatbv_rem:
119118
irep_idt());
120119

121120
expr.operands().resize(3);

‎src/solvers/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,7 @@ SRC = $(BOOLEFORCE_SRC) \
102102
flattening/boolbv_equality.cpp \
103103
flattening/boolbv_extractbit.cpp \
104104
flattening/boolbv_extractbits.cpp \
105+
flattening/boolbv_floatbv_mod_rem.cpp \
105106
flattening/boolbv_floatbv_op.cpp \
106107
flattening/boolbv_get.cpp \
107108
flattening/boolbv_ieee_float_rel.cpp \

‎src/solvers/flattening/boolbv.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -137,12 +137,16 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
137137
else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
138138
expr.id()==ID_rol || expr.id()==ID_ror)
139139
return convert_shift(to_shift_expr(expr));
140-
else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
141-
expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
142-
expr.id()==ID_floatbv_rem)
140+
else if(
141+
expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
142+
expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div)
143143
{
144144
return convert_floatbv_op(to_ieee_float_op_expr(expr));
145145
}
146+
else if(expr.id() == ID_floatbv_mod)
147+
return convert_floatbv_mod_rem(to_binary_expr(expr));
148+
else if(expr.id() == ID_floatbv_rem)
149+
return convert_floatbv_mod_rem(to_binary_expr(expr));
146150
else if(expr.id()==ID_floatbv_typecast)
147151
return convert_floatbv_typecast(to_floatbv_typecast_expr(expr));
148152
else if(expr.id()==ID_concatenation)

‎src/solvers/flattening/boolbv.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -168,6 +168,7 @@ class boolbvt:public arrayst
168168
virtual bvt convert_div(const div_exprt &expr);
169169
virtual bvt convert_mod(const mod_exprt &expr);
170170
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &);
171+
virtual bvt convert_floatbv_mod_rem(const binary_exprt &);
171172
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr);
172173
virtual bvt convert_member(const member_exprt &expr);
173174
virtual bvt convert_with(const with_exprt &expr);

‎src/solvers/flattening/boolbv_floatbv_mod_rem.cpp

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "boolbv.h"
10+
11+
#include <util/bitvector_types.h>
12+
13+
#include <solvers/floatbv/float_utils.h>
14+
15+
bvt boolbvt::convert_floatbv_mod_rem(const binary_exprt &expr)
16+
{
17+
// Note that the expressions do not have rounding modes
18+
// but float_utils requires one.
19+
20+
float_utilst float_utils(prop);
21+
22+
auto rm = bv_utils.build_constant(ieee_floatt::ROUND_TO_EVEN, 32);
23+
float_utils.set_rounding_mode(rm);
24+
25+
float_utils.spec = ieee_float_spect(to_floatbv_type(expr.type()));
26+
27+
bvt lhs_as_bv = convert_bv(expr.lhs());
28+
bvt rhs_as_bv = convert_bv(expr.rhs());
29+
30+
// float_utilst::rem implements lhs-(lhs/rhs)*rhs, which matches
31+
// neither fmod() nor IEEE
32+
return float_utils.rem(lhs_as_bv, rhs_as_bv);
33+
}

‎src/solvers/flattening/boolbv_floatbv_op.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -111,8 +111,6 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
111111
return float_utils.mul(lhs_as_bv, rhs_as_bv);
112112
else if(expr.id()==ID_floatbv_div)
113113
return float_utils.div(lhs_as_bv, rhs_as_bv);
114-
else if(expr.id()==ID_floatbv_rem)
115-
return float_utils.rem(lhs_as_bv, rhs_as_bv);
116114
else
117115
UNREACHABLE;
118116
}

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1370,6 +1370,10 @@ void smt2_convt::convert_expr(const exprt &expr)
13701370
{
13711371
convert_floatbv_mult(to_ieee_float_op_expr(expr));
13721372
}
1373+
else if(expr.id() == ID_floatbv_rem)
1374+
{
1375+
convert_floatbv_rem(to_binary_expr(expr));
1376+
}
13731377
else if(expr.id()==ID_address_of)
13741378
{
13751379
const address_of_exprt &address_of_expr = to_address_of_expr(expr);
@@ -3723,6 +3727,29 @@ void smt2_convt::convert_floatbv_mult(const ieee_float_op_exprt &expr)
37233727
convert_floatbv(expr);
37243728
}
37253729

3730+
void smt2_convt::convert_floatbv_rem(const binary_exprt &expr)
3731+
{
3732+
DATA_INVARIANT(
3733+
expr.type().id() == ID_floatbv,
3734+
"type of ieee floating point expression shall be floatbv");
3735+
3736+
if(use_FPA_theory)
3737+
{
3738+
// Note that these do not have a rounding mode
3739+
out << "(fp.rem ";
3740+
convert_expr(expr.lhs());
3741+
out << " ";
3742+
convert_expr(expr.rhs());
3743+
out << ")";
3744+
}
3745+
else
3746+
{
3747+
SMT2_TODO(
3748+
"smt2_convt::convert_floatbv_rem to be implemented when not using "
3749+
"FPA_theory");
3750+
}
3751+
}
3752+
37263753
void smt2_convt::convert_with(const with_exprt &expr)
37273754
{
37283755
// get rid of "with" that has more than three operands

‎src/solvers/smt2/smt2_conv.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,7 @@ class smt2_convt : public stack_decision_proceduret
130130
void convert_floatbv_minus(const ieee_float_op_exprt &expr);
131131
void convert_floatbv_div(const ieee_float_op_exprt &expr);
132132
void convert_floatbv_mult(const ieee_float_op_exprt &expr);
133+
void convert_floatbv_rem(const binary_exprt &expr);
133134
void convert_mod(const mod_exprt &expr);
134135
void convert_euclidean_mod(const euclidean_mod_exprt &expr);
135136
void convert_index(const index_exprt &expr);

‎src/solvers/smt2/smt2_parser.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1278,6 +1278,27 @@ void smt2_parsert::setup_expressions()
12781278
return function_application_ieee_float_op("fp.div", operands());
12791279
};
12801280

1281+
expressions["fp.rem"] = [this] {
1282+
auto op = operands();
1283+
1284+
// Note that these do not have a rounding mode.
1285+
if(op.size() != 2)
1286+
throw error() << "fp.rem takes three operands";
1287+
1288+
if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
1289+
throw error() << "fp.rem takes FloatingPoint operands";
1290+
1291+
if(op[0].type() != op[1].type())
1292+
{
1293+
throw error()
1294+
<< "fp.rem takes FloatingPoint operands with matching sort, "
1295+
<< "but got " << smt2_format(op[0].type()) << " vs "
1296+
<< smt2_format(op[1].type());
1297+
}
1298+
1299+
return binary_exprt(op[0], ID_floatbv_rem, op[1]);
1300+
};
1301+
12811302
expressions["fp.eq"] = [this] {
12821303
return function_application_ieee_float_eq(operands());
12831304
};

‎src/util/ieee_float.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include "arith_tools.h"
1414
#include "bitvector_types.h"
15+
#include "c_types.h"
1516
#include "invariant.h"
1617
#include "std_expr.h"
1718

@@ -55,6 +56,11 @@ void ieee_float_spect::from_type(const floatbv_typet &type)
5556
e=e-1; // no hidden bit
5657
}
5758

59+
constant_exprt ieee_floatt::rounding_mode_expr(rounding_modet rm)
60+
{
61+
return ::from_integer(static_cast<int>(rm), unsigned_int_type());
62+
}
63+
5864
void ieee_floatt::print(std::ostream &out) const
5965
{
6066
out << to_ansi_c_string();

‎src/util/ieee_float.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,9 @@ class ieee_floatt
128128
UNKNOWN, NONDETERMINISTIC
129129
};
130130

131+
// A helper to turn a rounding mode into a constant bitvector expression
132+
static constant_exprt rounding_mode_expr(rounding_modet);
133+
131134
rounding_modet rounding_mode;
132135

133136
ieee_float_spect spec;

‎src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -546,6 +546,7 @@ IREP_ID_ONE(floatbv_plus)
546546
IREP_ID_ONE(floatbv_minus)
547547
IREP_ID_ONE(floatbv_mult)
548548
IREP_ID_ONE(floatbv_div)
549+
IREP_ID_ONE(floatbv_mod)
549550
IREP_ID_ONE(floatbv_rem)
550551
IREP_ID_ONE(floatbv_typecast)
551552
IREP_ID_ONE(compound_literal)

0 commit comments

Comments
 (0)