From a7d2d63caf61468cf946a7e97ba10c32a6d6bf31 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Sep 2023 12:26:07 +0000 Subject: [PATCH] Cleanup fmod vs IEEE remainder 1. Add tests for both the C and Java front-end. 2. Make sure we support both variants of the modulus operator on floating-point values in the back-ends: the SMT back-end only supported remainder (and only for FPA mode), the propositional back-end did not distinguish between fmod and IEEE remainder. --- jbmc/regression/jbmc/farith2/farith2.class | Bin 0 -> 884 bytes jbmc/regression/jbmc/farith2/farith2.java | 17 ++++ .../regression/jbmc/farith2}/test.desc | 6 +- .../__sort_of_CPROVER_remainder-01/main.c | 9 -- .../__sort_of_CPROVER_remainderf-01/main.c | 9 -- .../__sort_of_CPROVER_remainderf-01/test.desc | 8 -- .../__sort_of_CPROVER_remainderl-01/main.c | 9 -- .../__sort_of_CPROVER_remainderl-01/test.desc | 8 -- regression/cbmc-library/fmod-01/main.c | 14 ++- regression/cbmc-library/fmod-01/test.desc | 4 +- regression/cbmc-library/fmodf-01/main.c | 14 ++- regression/cbmc-library/fmodf-01/test.desc | 4 +- regression/cbmc-library/fmodl-01/main.c | 14 ++- regression/cbmc-library/fmodl-01/test.desc | 4 +- regression/cbmc-library/remainder-01/main.c | 8 +- .../cbmc-library/remainder-01/test.desc | 4 +- regression/cbmc-library/remainderf-01/main.c | 8 +- .../cbmc-library/remainderf-01/test.desc | 4 +- regression/cbmc-library/remainderl-01/main.c | 8 +- .../cbmc-library/remainderl-01/test.desc | 4 +- src/ansi-c/expr2c.cpp | 1 + src/ansi-c/library/math.c | 95 +++--------------- .../adjust_float_expressions.cpp | 12 +-- .../flattening/boolbv_floatbv_mod_rem.cpp | 5 +- src/solvers/floatbv/float_bv.cpp | 36 +++++++ src/solvers/floatbv/float_bv.h | 4 + src/solvers/smt2/smt2_conv.cpp | 39 ++++++- src/solvers/smt2/smt2_conv.h | 1 + .../smt2_incremental/convert_expr_to_smt.cpp | 4 +- src/util/format_expr.cpp | 3 +- 30 files changed, 181 insertions(+), 175 deletions(-) create mode 100644 jbmc/regression/jbmc/farith2/farith2.class create mode 100644 jbmc/regression/jbmc/farith2/farith2.java rename {regression/cbmc-library/__sort_of_CPROVER_remainder-01 => jbmc/regression/jbmc/farith2}/test.desc (59%) delete mode 100644 regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c delete mode 100644 regression/cbmc-library/__sort_of_CPROVER_remainderf-01/main.c delete mode 100644 regression/cbmc-library/__sort_of_CPROVER_remainderf-01/test.desc delete mode 100644 regression/cbmc-library/__sort_of_CPROVER_remainderl-01/main.c delete mode 100644 regression/cbmc-library/__sort_of_CPROVER_remainderl-01/test.desc diff --git a/jbmc/regression/jbmc/farith2/farith2.class b/jbmc/regression/jbmc/farith2/farith2.class new file mode 100644 index 0000000000000000000000000000000000000000..119c806b1cdfdf7102feec0eb27a1395db6bfb74 GIT binary patch literal 884 zcmZvZ%}*0S7{;IJezDs{K3cJ$pdd;?p^6yOfCU2>Vu~IxBp{b;$?jtCukeUq z;>Ck!HIYOUNxW(F>>on75#lpTr7=3m>^$?%`@ZwrXTBeQ`U2n%Zd*v;nm+z*M~+<+ zEx2xA(1OP3el4m`bTOGjpTG|}e(K`~*4>RazbuNS^x@YRO9qB4WN^d4O@TzO69ldw zdeurWPAIoHc)_k?-l;<7a zllxjw4OhKDz|1c*9TeH>Df>=tMyhC}7~1*Oqo6_5QCerp zOrml7HEb!GUcRcgl5|Q$*Mo+LM1@7dIC*T0pbkJUVi3Jl8f(+ILS?W+H?C5d=wnq2)FX5#M`%}$kyaGN;N|I4|3)HnnAY0z d5v{v0)VENT4^aR0Qg+i2vnQnE{oKSb@EfPxt~dYy literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/farith2/farith2.java b/jbmc/regression/jbmc/farith2/farith2.java new file mode 100644 index 000000000000..bed6761c5839 --- /dev/null +++ b/jbmc/regression/jbmc/farith2/farith2.java @@ -0,0 +1,17 @@ +class farith2 +{ + public static void main(String[] args) + { + // examples from + // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double + // and + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + double d1 = 0.5 % 0.3; + assert d1 == 0.2; + double d2 = (-0.5) % 0.3; + assert d2 == -0.2; + double x = 7.5, y = 2.1; + double xModY = x % y; + assert xModY > 1.19 && xModY < 1.21; + } +} diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc b/jbmc/regression/jbmc/farith2/test.desc similarity index 59% rename from regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc rename to jbmc/regression/jbmc/farith2/test.desc index 9542d988e8d5..915684ced8db 100644 --- a/regression/cbmc-library/__sort_of_CPROVER_remainder-01/test.desc +++ b/jbmc/regression/jbmc/farith2/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check +CORE +farith2 + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c deleted file mode 100644 index 97bed88803b1..000000000000 --- a/regression/cbmc-library/__sort_of_CPROVER_remainder-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - __sort_of_CPROVER_remainder(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/main.c deleted file mode 100644 index cb5060b1ad3c..000000000000 --- a/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - __sort_of_CPROVER_remainderf(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/test.desc deleted file mode 100644 index 9542d988e8d5..000000000000 --- a/regression/cbmc-library/__sort_of_CPROVER_remainderf-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/main.c b/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/main.c deleted file mode 100644 index 24c42bbe2a32..000000000000 --- a/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/main.c +++ /dev/null @@ -1,9 +0,0 @@ -#include -#include - -int main() -{ - __sort_of_CPROVER_remainderl(); - assert(0); - return 0; -} diff --git a/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/test.desc b/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/test.desc deleted file mode 100644 index 9542d988e8d5..000000000000 --- a/regression/cbmc-library/__sort_of_CPROVER_remainderl-01/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -main.c ---pointer-check --bounds-check -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/cbmc-library/fmod-01/main.c b/regression/cbmc-library/fmod-01/main.c index 775d5b7d64a6..a7ae621eec59 100644 --- a/regression/cbmc-library/fmod-01/main.c +++ b/regression/cbmc-library/fmod-01/main.c @@ -3,7 +3,15 @@ int main() { - fmod(); - assert(0); - return 0; + // examples from + // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double + // and + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + double d1 = fmod(0.5, 0.3); + assert(d1 == 0.2); + double d2 = fmod(-0.5, 0.3); + assert(d2 == -0.2); + double x = 7.5, y = 2.1; + double xModY = fmod(x, y); + assert(xModY > 1.19 && xModY < 1.21); } diff --git a/regression/cbmc-library/fmod-01/test.desc b/regression/cbmc-library/fmod-01/test.desc index 9542d988e8d5..3510d48c5c66 100644 --- a/regression/cbmc-library/fmod-01/test.desc +++ b/regression/cbmc-library/fmod-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--float-overflow-check --nan-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/fmodf-01/main.c b/regression/cbmc-library/fmodf-01/main.c index 0e14f93f46cb..ec3eefe90ef2 100644 --- a/regression/cbmc-library/fmodf-01/main.c +++ b/regression/cbmc-library/fmodf-01/main.c @@ -3,7 +3,15 @@ int main() { - fmodf(); - assert(0); - return 0; + // examples from + // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double + // and + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + float d1 = fmodf(0.5f, 0.3f); + assert(d1 > 0.19f && d1 < 0.21f); + float d2 = fmodf(-0.5f, 0.3f); + assert(d2 > -0.21f && d2 < -0.19f); + float x = 7.5f, y = 2.1f; + float xModY = fmodf(x, y); + assert(xModY > 1.19f && xModY < 1.21f); } diff --git a/regression/cbmc-library/fmodf-01/test.desc b/regression/cbmc-library/fmodf-01/test.desc index 9542d988e8d5..3510d48c5c66 100644 --- a/regression/cbmc-library/fmodf-01/test.desc +++ b/regression/cbmc-library/fmodf-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--float-overflow-check --nan-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/fmodl-01/main.c b/regression/cbmc-library/fmodl-01/main.c index b24c534c69ae..c5ccd85c4bc8 100644 --- a/regression/cbmc-library/fmodl-01/main.c +++ b/regression/cbmc-library/fmodl-01/main.c @@ -3,7 +3,15 @@ int main() { - fmodl(); - assert(0); - return 0; + // examples from + // https://stackoverflow.com/questions/2947044/how-do-i-use-modulus-for-float-double + // and + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + long double d1 = fmodl(0.5l, 0.3l); + assert(d1 == 0.2l); + long double d2 = fmodl(-0.5l, 0.3l); + assert(d2 == -0.2l); + long double x = 7.5l, y = 2.1l; + long double xModY = fmodl(x, y); + assert(xModY > 1.19l && xModY < 1.21l); } diff --git a/regression/cbmc-library/fmodl-01/test.desc b/regression/cbmc-library/fmodl-01/test.desc index 9542d988e8d5..3510d48c5c66 100644 --- a/regression/cbmc-library/fmodl-01/test.desc +++ b/regression/cbmc-library/fmodl-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--float-overflow-check --nan-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/remainder-01/main.c b/regression/cbmc-library/remainder-01/main.c index dba529354de9..4cd13925eb49 100644 --- a/regression/cbmc-library/remainder-01/main.c +++ b/regression/cbmc-library/remainder-01/main.c @@ -3,7 +3,9 @@ int main() { - remainder(); - assert(0); - return 0; + // example from + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + double x = 7.5, y = 2.1; + double xModY = remainder(x, y); + assert(xModY > -0.91 && xModY < -0.89); } diff --git a/regression/cbmc-library/remainder-01/test.desc b/regression/cbmc-library/remainder-01/test.desc index 9542d988e8d5..3510d48c5c66 100644 --- a/regression/cbmc-library/remainder-01/test.desc +++ b/regression/cbmc-library/remainder-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--float-overflow-check --nan-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/remainderf-01/main.c b/regression/cbmc-library/remainderf-01/main.c index edf674f5d559..d9ed13d54768 100644 --- a/regression/cbmc-library/remainderf-01/main.c +++ b/regression/cbmc-library/remainderf-01/main.c @@ -3,7 +3,9 @@ int main() { - remainderf(); - assert(0); - return 0; + // example from + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + float x = 7.5f, y = 2.1f; + float xModY = remainderf(x, y); + assert(xModY > -0.91f && xModY < -0.89f); } diff --git a/regression/cbmc-library/remainderf-01/test.desc b/regression/cbmc-library/remainderf-01/test.desc index 9542d988e8d5..3510d48c5c66 100644 --- a/regression/cbmc-library/remainderf-01/test.desc +++ b/regression/cbmc-library/remainderf-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--float-overflow-check --nan-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/remainderl-01/main.c b/regression/cbmc-library/remainderl-01/main.c index 5a84b872d646..ba2203e6dffb 100644 --- a/regression/cbmc-library/remainderl-01/main.c +++ b/regression/cbmc-library/remainderl-01/main.c @@ -3,7 +3,9 @@ int main() { - remainderl(); - assert(0); - return 0; + // example from + // https://stackoverflow.com/questions/25734144/difference-between-c-functions-remainder-and-fmod + long double x = 7.5l, y = 2.1l; + long double xModY = remainderl(x, y); + assert(xModY > -0.91l && xModY < -0.89l); } diff --git a/regression/cbmc-library/remainderl-01/test.desc b/regression/cbmc-library/remainderl-01/test.desc index 9542d988e8d5..3510d48c5c66 100644 --- a/regression/cbmc-library/remainderl-01/test.desc +++ b/regression/cbmc-library/remainderl-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--float-overflow-check --nan-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 9578d6d7376d..4f08e7c9614e 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -4038,6 +4038,7 @@ optionalt expr2ct::convert_function(const exprt &src) {ID_separate, "SEPARATE"}, {ID_floatbv_div, "FLOAT/"}, {ID_floatbv_minus, "FLOAT-"}, + {ID_floatbv_mod, "fmod"}, {ID_floatbv_mult, "FLOAT*"}, {ID_floatbv_plus, "FLOAT+"}, {ID_floatbv_rem, "FLOAT%"}, diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 17e7dc3e9bba..05c5315b94da 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -2186,60 +2186,6 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double return (x - *iptr); } - - -/* FUNCTION: __sort_of_CPROVER_remainder */ -// TODO : Should be a real __CPROVER function to convert to SMT-LIB -double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); - -double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y) -{ - if (x == 0.0 || __CPROVER_isinfd(y)) - return x; - - // Extended precision helps... a bit... - long double div = x/y; - long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div); - long double res = (-y * n) + x; // TODO : FMA would be an improvement - return res; -} - -/* FUNCTION: __sort_of_CPROVER_remainderf */ -// TODO : Should be a real __CPROVER function to convert to SMT-LIB - -float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); - -float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y) -{ - if (x == 0.0f || __CPROVER_isinff(y)) - return x; - - // Extended precision helps... a bit... - long double div = x/y; - long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div); - long double res = (-y * n) + x; // TODO : FMA would be an improvement - return res; -} - -/* FUNCTION: __sort_of_CPROVER_remainderl */ -// TODO : Should be a real __CPROVER function to convert to SMT-LIB - -long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); - -long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y) -{ - if (x == 0.0 || __CPROVER_isinfld(y)) - return x; - - // Extended precision helps... a bit... - long double div = x/y; - long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div); - long double res = (-y * n) + x; // TODO : FMA would be an improvement - return res; -} - - - /* ISO 9899:2011 * * The fmod functions return the value x - ny, for some @@ -2320,15 +2266,10 @@ long double fmodl(long double x, long double y) #define __CPROVER_MATH_H_INCLUDED #endif -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - -double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y); - -double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TONEAREST, x, y); } - +double remainder(double x, double y) +{ + return __CPROVER_remainder(x, y); +} /* FUNCTION: remainderf */ @@ -2337,15 +2278,10 @@ double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TON #define __CPROVER_MATH_H_INCLUDED #endif -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - -float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y); - -float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONEAREST, x, y); } - +float remainderf(float x, float y) +{ + return __CPROVER_remainderf(x, y); +} /* FUNCTION: remainderl */ @@ -2354,17 +2290,10 @@ float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONE #define __CPROVER_MATH_H_INCLUDED #endif -#ifndef __CPROVER_FENV_H_INCLUDED -#include -#define __CPROVER_FENV_H_INCLUDED -#endif - -long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y); - -long double remainderl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TONEAREST, x, y); } - - - +long double remainderl(long double x, long double y) +{ + return __CPROVER_remainderl(x, y); +} /* ISO 9899:2011 * The copysign functions produce a value with the magnitude of x and diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp index 9b44d90f1fe2..a5182669e1b4 100644 --- a/src/goto-programs/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -31,13 +31,11 @@ irep_idt rounding_mode_identifier() /// yet. static bool have_to_adjust_float_expressions(const exprt &expr) { - if(expr.id()==ID_floatbv_plus || - expr.id()==ID_floatbv_minus || - expr.id()==ID_floatbv_mult || - expr.id()==ID_floatbv_div || - expr.id()==ID_floatbv_div || - expr.id()==ID_floatbv_rem || - expr.id()==ID_floatbv_typecast) + if( + expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus || + expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div || + expr.id() == ID_floatbv_mod || expr.id() == ID_floatbv_rem || + expr.id() == ID_floatbv_typecast) return false; const typet &type = expr.type(); diff --git a/src/solvers/flattening/boolbv_floatbv_mod_rem.cpp b/src/solvers/flattening/boolbv_floatbv_mod_rem.cpp index 3a91c5adac65..217e6089a59e 100644 --- a/src/solvers/flattening/boolbv_floatbv_mod_rem.cpp +++ b/src/solvers/flattening/boolbv_floatbv_mod_rem.cpp @@ -19,7 +19,10 @@ bvt boolbvt::convert_floatbv_mod_rem(const binary_exprt &expr) float_utilst float_utils(prop); - auto rm = bv_utils.build_constant(ieee_floatt::ROUND_TO_EVEN, 32); + auto rm = bv_utils.build_constant( + expr.id() == ID_floatbv_rem ? ieee_floatt::ROUND_TO_EVEN + : ieee_floatt::ROUND_TO_ZERO, + 32); float_utils.set_rounding_mode(rm); float_utils.spec = ieee_float_spect(to_floatbv_type(expr.type())); diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 3611abd36328..c989c57f0ffd 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -133,6 +133,16 @@ exprt float_bvt::convert(const exprt &expr) const float_expr.rounding_mode(), get_spec(expr)); } + else if(expr.id() == ID_floatbv_mod) + { + const auto &float_expr = to_binary_expr(expr); + return mod(float_expr.lhs(), float_expr.rhs()); + } + else if(expr.id() == ID_floatbv_rem) + { + const auto &float_expr = to_binary_expr(expr); + return rem(float_expr.lhs(), float_expr.rhs()); + } else if(expr.id()==ID_isnan) { const auto &op = to_unary_expr(expr).op(); @@ -820,6 +830,32 @@ exprt float_bvt::div( return rounder(result, rm, spec); } +exprt float_bvt::mod(const exprt &x, const exprt &y) const +{ + // x - round-to-zero(x / y) * y + const constant_exprt round_to_zero = + from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet{2}); + + exprt div = convert(ieee_float_op_exprt{x, ID_floatbv_div, y, round_to_zero}); + exprt mul = convert( + ieee_float_op_exprt{std::move(div), ID_floatbv_mult, y, round_to_zero}); + return convert( + ieee_float_op_exprt{x, ID_floatbv_minus, std::move(mul), round_to_zero}); +} + +exprt float_bvt::rem(const exprt &x, const exprt &y) const +{ + // x - round-to-even(x / y) * y + const constant_exprt round_to_even = + from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet{2}); + + exprt div = convert(ieee_float_op_exprt{x, ID_floatbv_div, y, round_to_even}); + exprt mul = convert( + ieee_float_op_exprt{std::move(div), ID_floatbv_mult, y, round_to_even}); + return convert( + ieee_float_op_exprt{x, ID_floatbv_minus, std::move(mul), round_to_even}); +} + exprt float_bvt::relation( const exprt &src1, relt rel, diff --git a/src/solvers/floatbv/float_bv.h b/src/solvers/floatbv/float_bv.h index 7c4ff63b84da..26d598f912bf 100644 --- a/src/solvers/floatbv/float_bv.h +++ b/src/solvers/floatbv/float_bv.h @@ -48,6 +48,10 @@ class float_bvt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const; + // fmod and remainder + exprt mod(const exprt &, const exprt &) const; + exprt rem(const exprt &, const exprt &) const; + // conversion exprt from_unsigned_integer( const exprt &, diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2cb65bcff1ea..956c895c67a2 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1483,6 +1483,10 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_floatbv_mult(to_ieee_float_op_expr(expr)); } + else if(expr.id() == ID_floatbv_mod) + { + convert_floatbv_mod(to_binary_expr(expr)); + } else if(expr.id() == ID_floatbv_rem) { convert_floatbv_rem(to_binary_expr(expr)); @@ -4061,6 +4065,33 @@ void smt2_convt::convert_floatbv_mult(const ieee_float_op_exprt &expr) convert_floatbv(expr); } +void smt2_convt::convert_floatbv_mod(const binary_exprt &expr) +{ + DATA_INVARIANT( + expr.type().id() == ID_floatbv, + "type of ieee floating point expression shall be floatbv"); + + if(use_FPA_theory) + { + // x - round-to-zero(x / y) * y + out << "(fp.sub roundTowardZero "; + convert_expr(expr.lhs()); + out << " "; + out << "(fp.mul roundTowardZero "; + out << "(fp.roundToIntegral roundTowardZero "; + out << "(fp.div roundTowardZero "; + convert_expr(expr.lhs()); + out << " "; + convert_expr(expr.rhs()); + out << "))"; // div, roundToIntegral + out << " "; + convert_expr(expr.rhs()); + out << "))"; // mul, sub + } + else + convert_floatbv(expr); +} + void smt2_convt::convert_floatbv_rem(const binary_exprt &expr) { DATA_INVARIANT( @@ -4077,11 +4108,7 @@ void smt2_convt::convert_floatbv_rem(const binary_exprt &expr) out << ")"; } else - { - SMT2_TODO( - "smt2_convt::convert_floatbv_rem to be implemented when not using " - "FPA_theory"); - } + convert_floatbv(expr); } void smt2_convt::convert_with(const with_exprt &expr) @@ -5126,6 +5153,8 @@ void smt2_convt::find_symbols(const exprt &expr) expr.id() == ID_floatbv_minus || expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div || + expr.id() == ID_floatbv_mod || + expr.id() == ID_floatbv_rem || expr.id() == ID_floatbv_typecast || expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal || diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 2a2e1f3b0980..65d027e8c094 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -141,6 +141,7 @@ class smt2_convt : public stack_decision_proceduret void convert_floatbv_minus(const ieee_float_op_exprt &expr); void convert_floatbv_div(const ieee_float_op_exprt &expr); void convert_floatbv_mult(const ieee_float_op_exprt &expr); + void convert_floatbv_mod(const binary_exprt &expr); void convert_floatbv_rem(const binary_exprt &expr); void convert_mod(const mod_exprt &expr); void convert_euclidean_mod(const euclidean_mod_exprt &expr); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 5f0a97ad98ed..f67f68babc07 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1616,9 +1616,9 @@ static smt_termt dispatch_expr_to_smt_conversion( return convert_expr_to_smt(*multiply, converted); } #if 0 - else if(expr.id() == ID_floatbv_rem) + else if(expr.id() == ID_floatbv_mod || expr.id() == ID_floatbv_rem) { - convert_floatbv_rem(to_binary_expr(expr)); + convert_floatbv_mod_rem(to_binary_expr(expr)); } #endif if(const auto address_of = expr_try_dynamic_cast(expr)) diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 9821af008dd7..9ae8761674c6 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -340,7 +340,8 @@ void format_expr_configt::setup() expr_map[ID_floatbv_minus] = ternary_expr; expr_map[ID_floatbv_mult] = ternary_expr; expr_map[ID_floatbv_div] = ternary_expr; - expr_map[ID_floatbv_mod] = ternary_expr; + expr_map[ID_floatbv_mod] = binary_infix_expr; + expr_map[ID_floatbv_rem] = binary_infix_expr; expr_map[ID_constant] = [](std::ostream &os, const exprt &expr) -> std::ostream & {