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

File tree

17 files changed

+186
-26
lines changed

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, kroening@kroening.com
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+
}

0 commit comments

Comments
 (0)