diff --git a/trunk/examples/programs/FloatingPoint/todo/cbmc_float-flags-simp1_PART1.i b/trunk/examples/programs/FloatingPoint/regression/c/all/cbmc_float-flags-simp1_PART1.i similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/cbmc_float-flags-simp1_PART1.i rename to trunk/examples/programs/FloatingPoint/regression/c/all/cbmc_float-flags-simp1_PART1.i diff --git a/trunk/examples/programs/FloatingPoint/todo/cbmc_float-flags-simp1_PART3.i b/trunk/examples/programs/FloatingPoint/regression/c/all/cbmc_float-flags-simp1_PART3.i similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/cbmc_float-flags-simp1_PART3.i rename to trunk/examples/programs/FloatingPoint/regression/c/all/cbmc_float-flags-simp1_PART3.i diff --git a/trunk/examples/programs/FloatingPoint/regression/c/all/cos.c b/trunk/examples/programs/FloatingPoint/regression/c/all/cos.c new file mode 100644 index 00000000000..9f196aa4140 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/cos.c @@ -0,0 +1,14 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = cosf(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (isinf(x) && !isnan(y)) reach_error(); + if (x == 0 && y != 1) reach_error(); + if (y > 1 || y < -1) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-2.c b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-2.c similarity index 81% rename from trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-2.c rename to trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-2.c index 98ad89ad5dc..56b7434f1ef 100644 --- a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-2.c +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-2.c @@ -20,5 +20,6 @@ int main(void) x = copysign(NAN, -2.0); __VERIFIER_assert(isnan(x)); - __VERIFIER_assert(signbit(x)); + // Due to our overapproximation of signbit for NaN, we currently cannot prove this assertion. + // __VERIFIER_assert(signbit(x)); } \ No newline at end of file diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-NAN-2.c b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-NAN-2.c similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-NAN-2.c rename to trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-NAN-2.c diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-NAN.c b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-NAN.c similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign-NAN.c rename to trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-NAN.c diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign.c b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign.c similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/ctrans-float-copysign.c rename to trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign.c diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-signbit.c b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-signbit.c similarity index 79% rename from trunk/examples/programs/FloatingPoint/todo/ctrans-float-signbit.c rename to trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-signbit.c index 25a55e888a8..29e85e23442 100644 --- a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-signbit.c +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-signbit.c @@ -32,11 +32,12 @@ int main(void) x = -0.0; rtr = signbit(x); __VERIFIER_assert(rtr != 0); - x = NAN; - rtr = signbit(x); - __VERIFIER_assert(rtr == 0); - x = 0.0 / 0.0; - rtr = signbit(x); - __VERIFIER_assert(rtr != 0); + // Due to our overapproximation of signbit for NaN, we currently cannot prove these assertions. + // x = NAN; + // rtr = signbit(x); + // __VERIFIER_assert(rtr == 0); + // x = 0.0 / 0.0; + // rtr = signbit(x); + // __VERIFIER_assert(rtr != 0); return 0; } \ No newline at end of file diff --git a/trunk/examples/programs/FloatingPoint/regression/c/all/exp.c b/trunk/examples/programs/FloatingPoint/regression/c/all/exp.c new file mode 100644 index 00000000000..9d2cd28ef32 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/exp.c @@ -0,0 +1,13 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = expf(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (x == 0 && y != 1) reach_error(); + if (y < 0) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/all/isinf_sign.c b/trunk/examples/programs/FloatingPoint/regression/c/all/isinf_sign.c new file mode 100644 index 00000000000..1263b05af47 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/isinf_sign.c @@ -0,0 +1,14 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + int x = __builtin_isinf_sign(5.7); + int y = __builtin_isinf_sign(INFINITY); + int z = __builtin_isinf_sign(-INFINITY); + //@ assert x == 0; + //@ assert y > 0; + //@ assert z < 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/all/log.c b/trunk/examples/programs/FloatingPoint/regression/c/all/log.c new file mode 100644 index 00000000000..d2c969234c7 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/log.c @@ -0,0 +1,15 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = logf(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (x == 0 && !isinf(y)) reach_error(); + if (x == 1 && y != 0) reach_error(); + if (x > 1 && y <= 0) reach_error(); + if (x >= 0 && y > x-1) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/todo/signbit.c b/trunk/examples/programs/FloatingPoint/regression/c/all/signbit.c similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/signbit.c rename to trunk/examples/programs/FloatingPoint/regression/c/all/signbit.c diff --git a/trunk/examples/programs/FloatingPoint/regression/c/all/sin.c b/trunk/examples/programs/FloatingPoint/regression/c/all/sin.c new file mode 100644 index 00000000000..442dbd32cb7 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/sin.c @@ -0,0 +1,14 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = sinf(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (isinf(x) && !isnan(y)) reach_error(); + if (x == 0 && y != 0) reach_error(); + if (y > 1 || y < -1) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore index 98f261bbceb..d31f8ac4a5f 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore @@ -5,3 +5,18 @@ TIMEOUT: - task: ctrans-float-rounding.c settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf toolchain: AutomizerC.xml +- task: ctrans-float-fmod-1.c + settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf + toolchain: AutomizerC.xml +- task: ctrans-float-fmod-2.c + settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf + toolchain: AutomizerC.xml +- task: ctrans-float-fmod-3.c + settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf + toolchain: AutomizerC.xml +- task: ctrans-float-fmod-4.c + settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf + toolchain: AutomizerC.xml +- task: ctrans-float-fmod-inf.c + settings: AutomizerC-Reach-32bit-WOLF-Float.epf + toolchain: AutomizerC.xml diff --git a/trunk/examples/programs/FloatingPoint/todo/cbmc_float-no-simp8.i b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/cbmc_float-no-simp8.i similarity index 100% rename from trunk/examples/programs/FloatingPoint/todo/cbmc_float-no-simp8.i rename to trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/cbmc_float-no-simp8.i diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-1.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-1.c new file mode 100644 index 00000000000..ec356ff03d5 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-1.c @@ -0,0 +1,16 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/fmod +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(fmodf(5.1f, 3) == 2.1f); + + return 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-2.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-2.c new file mode 100644 index 00000000000..63d0d7b9fc2 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-2.c @@ -0,0 +1,16 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/fmod +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(fmodf(-5.1f, 3) == -2.1f); + + return 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-3.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-3.c new file mode 100644 index 00000000000..c173ed48918 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-3.c @@ -0,0 +1,16 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/fmod +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(fmodf(5.1f, -3) == 2.1f); + + return 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-4.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-4.c new file mode 100644 index 00000000000..9ee12ed70b0 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-4.c @@ -0,0 +1,16 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/fmod +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(fmodf(-5.1f, -3) == -2.1f); + + return 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-inf.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-inf.c new file mode 100644 index 00000000000..f1cce9143f4 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-inf.c @@ -0,0 +1,22 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/fmod +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(fmod(5.1, INFINITY) == 5.1); + __VERIFIER_assert(fmod(5.1, -INFINITY) == 5.1); + + int i = isnan(fmod(INFINITY, 3)); + __VERIFIER_assert(i); + i = isnan(fmod(-INFINITY, 3)); + __VERIFIER_assert(i); + + return 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-nan.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-nan.c new file mode 100644 index 00000000000..47b73fb1df5 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-fmod-nan.c @@ -0,0 +1,24 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/fmod +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + int i = isnan(fmod(5.1,0)); + __VERIFIER_assert(i); + i = isnan(fmod(5.1,-0)); + __VERIFIER_assert(i); + + i = isnan(fmod(NAN,3)); + __VERIFIER_assert(i); + i = isnan(fmod(5.1,NAN)); + __VERIFIER_assert(i); + + return 0; +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-1.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-1.c new file mode 100644 index 00000000000..e68301d8bef --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-1.c @@ -0,0 +1,17 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(remainderf(5.1f, 3) == -0x1.ccccdp-1); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-2.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-2.c new file mode 100644 index 00000000000..62c78e777e9 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-2.c @@ -0,0 +1,17 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(remainderf(5.1f, -3) == -0x1.ccccdp-1); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-3.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-3.c new file mode 100644 index 00000000000..61877d0df19 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-3.c @@ -0,0 +1,17 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(remainderf(-5.1f, -3) == 0x1.ccccdp-1); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-4.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-4.c new file mode 100644 index 00000000000..d21c7d8b843 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-4.c @@ -0,0 +1,17 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(remainderf(-5.1f, 3) == 0x1.ccccdp-1); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-inf.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-inf.c new file mode 100644 index 00000000000..3d1424be01d --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-inf.c @@ -0,0 +1,22 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + __VERIFIER_assert(remainder(5.1, INFINITY) == 5.1); + + int i = isnan(remainder(INFINITY, 3)); + __VERIFIER_assert(i); + i = isnan(remainder(-INFINITY, 3)); + __VERIFIER_assert(i); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-nan.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-nan.c new file mode 100644 index 00000000000..d8a2052bfe1 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-nan.c @@ -0,0 +1,25 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + int i = isnan(remainder(5.1, 0)); + __VERIFIER_assert(i); + i = isnan(remainder(5.1, -0)); + __VERIFIER_assert(i); + + i = isnan(remainder(NAN, 3)); + __VERIFIER_assert(i); + i = isnan(remainder(5.1, NAN)); + __VERIFIER_assert(i); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-zero.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-zero.c new file mode 100644 index 00000000000..bae5929f710 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/ctrans-float-remainder-zero.c @@ -0,0 +1,20 @@ +//#Safe +/* + https://en.cppreference.com/w/c/numeric/math/remainder +*/ + +#include + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } + +int main(void) +{ + double r = remainder(0.0, 1); + __VERIFIER_assert(r == 0 && !signbit(r)); + r = remainder(-0.0, 1); + __VERIFIER_assert(r == 0 && signbit(r)); + + return 0; +} + diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/erf.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/erf.c new file mode 100644 index 00000000000..6a20d4495aa --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/erf.c @@ -0,0 +1,15 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = erff(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (isinf(x) && x > 0 && y != 1) reach_error(); + if (isinf(x) && x < 0 && y != -1) reach_error(); + if (x == 0 && y != 0) reach_error(); + if (y > 1 || y < -1) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/expm1.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/expm1.c new file mode 100644 index 00000000000..f3bfb83e5d3 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/expm1.c @@ -0,0 +1,13 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = expm1f(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (x == 0 && y != 0) reach_error(); + if (y < -1) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/tanh.c b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/tanh.c new file mode 100644 index 00000000000..fe6c0ffdf69 --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/tanh.c @@ -0,0 +1,15 @@ +// #Safe +/* + * Date: 2025-08-11 + * Author: schuessf@informatik.uni-freiburg.de + */ + +int main() { + float x = __VERIFIER_nondet_float(); + float y = tanhf(x); + if (isnan(x) && !isnan(y)) reach_error(); + if (isinf(x) && x > 0 && y != 1) reach_error(); + if (isinf(x) && x < 0 && y != -1) reach_error(); + if (x == 0 && y != 0) reach_error(); + if (y > 1 || y < -1) reach_error(); +} diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-fmod.c b/trunk/examples/programs/FloatingPoint/todo/ctrans-float-fmod.c deleted file mode 100644 index c7b618d28de..00000000000 --- a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-fmod.c +++ /dev/null @@ -1,41 +0,0 @@ -//#Safe -/* - https://en.cppreference.com/w/c/numeric/math/fmod -*/ - -#include - -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); -void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } - -int main(void) -{ - double rtr; - rtr = fmod(5.1, 3.0); - __VERIFIER_assert(rtr == 2.1); - __VERIFIER_assert(fmod(-5.1, 3) == -2.1); - __VERIFIER_assert(fmod(5.1, -3) == 2.1); - __VERIFIER_assert(fmod(-5.1, -3) == -2.1); - __VERIFIER_assert(fmod(0, 1) == 0.0); - __VERIFIER_assert(fmod(-0, 1) == -0.0); - - __VERIFIER_assert(fmod(5.1,INFINITY) == 5.1); - __VERIFIER_assert(fmod(5.1,-INFINITY) == 5.1); - - int i = isnan(fmod(INFINITY, 3)); - __VERIFIER_assert(i); - i = isnan(fmod(-INFINITY, 3)); - __VERIFIER_assert(i); - - i = isnan(fmod(5.1,0)); - __VERIFIER_assert(i); - i = isnan(fmod(5.1,-0)); - __VERIFIER_assert(i); - - i = isnan(fmod(NAN,3)); - __VERIFIER_assert(i); - i = isnan(fmod(5.1,NAN)); - __VERIFIER_assert(i); - - return 0; -} \ No newline at end of file diff --git a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-remainder.c b/trunk/examples/programs/FloatingPoint/todo/ctrans-float-remainder.c deleted file mode 100644 index b4d88bbc052..00000000000 --- a/trunk/examples/programs/FloatingPoint/todo/ctrans-float-remainder.c +++ /dev/null @@ -1,39 +0,0 @@ -//#Safe -/* - https://en.cppreference.com/w/c/numeric/math/remainder -*/ - -#include - -extern void __VERIFIER_error() __attribute__ ((__noreturn__)); -void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } - -int main(void) -{ - __VERIFIER_assert(remainder(5.1, 3) == -0.9); - __VERIFIER_assert(remainder(-5.1, 3) == 0.9); - __VERIFIER_assert(remainder(5.1, -3) == -0.9); - __VERIFIER_assert(remainder(-5.1, -3) == 0.9); - __VERIFIER_assert(remainder(0, 1) == 0.0); - __VERIFIER_assert(remainder(-0, 1) == -0.0); - - __VERIFIER_assert(remainder(5.1,INFINITY) == 5.1); - - int i = isnan(remainder(INFINITY, 3)); - __VERIFIER_assert(i); - i = isnan(remainder(-INFINITY, 3)); - __VERIFIER_assert(i); - - i = isnan(remainder(5.1,0)); - __VERIFIER_assert(i); - i = isnan(remainder(5.1,-0)); - __VERIFIER_assert(i); - - i = isnan(remainder(NAN,3)); - __VERIFIER_assert(i); - i = isnan(remainder(5.1,NAN)); - __VERIFIER_assert(i); - - return 0; -} - diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java index 9332a274018..f1635789de7 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java @@ -621,7 +621,7 @@ private List getLibraryModels() { new LinuxLibraryModel(helper, mAuxVarInfoBuilder, mExprResultTransformer, mTypeSizes, mExpressionTranslation), new MathLibraryModel(helper, mExprResultTransformer, mExpressionTranslation, mCExpressionTranslator, - mNameHandler), + mNameHandler, mAuxVarInfoBuilder), new PthreadLibraryModel(helper, mSymbolTable, mAuxVarInfoBuilder, mExprResultTransformer, mExpressionTranslation, mMemoryHandler, mTypeHandler, mTypeSizes, mProcedureManager), new SetjmpLibraryModel(helper, mExpressionTranslation), new SocketLibraryModel(helper), diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorFloatingPointHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorFloatingPointHandler.java new file mode 100644 index 00000000000..37af66e19f5 --- /dev/null +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorFloatingPointHandler.java @@ -0,0 +1,159 @@ +/* + * Copyright (C) 2025 Frank Schüssele (schuessf@informatik.uni-freiburg.de) + * Copyright (C) 2025 University of Freiburg + * + * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation; + +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; + +/** + * Implementation of {@link IFloatingPointHandler} that constructs calls to SMT-defined Boogie functions, which refer to + * built-in functions in the SMT theory of floating-point bitvectors (and therefore is coupled to + * {@link BitvectorTranslation}). + * + * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de) + */ +public class BitvectorFloatingPointHandler implements IFloatingPointHandler { + private final BitvectorTranslation mTranslation; + + public BitvectorFloatingPointHandler(final BitvectorTranslation translation) { + mTranslation = translation; + } + + @Override + public Expression roundToIntegral(final ILocation loc, final Expression argument, final CPrimitive type, + final Expression roundingMode) { + final String smtFunctionName = "fp.roundToIntegral"; + mTranslation.declareFloatingPointFunction(loc, smtFunctionName, false, true, type, type); + return mTranslation.constructCallToSmtOperation(loc, smtFunctionName, type, + new Expression[] { roundingMode, argument }); + } + + @Override + public Expression sqrt(final ILocation loc, final Expression argument, final CPrimitive type) { + final String smtFunctionName = "fp.sqrt"; + mTranslation.declareFloatingPointFunction(loc, smtFunctionName, false, true, type, type); + return mTranslation.constructCallToSmtOperation(loc, smtFunctionName, type, + new Expression[] { mTranslation.getCurrentRoundingMode(), argument }); + } + + @Override + public Expression abs(final ILocation loc, final Expression argument, final CPrimitive type) { + final String smtFunctionName = "fp.abs"; + mTranslation.declareFloatingPointFunction(loc, smtFunctionName, false, false, type, type); + return mTranslation.constructCallToSmtOperation(loc, smtFunctionName, type, new Expression[] { argument }); + } + + private Expression constructSmtFloatClassificationFunction(final ILocation loc, final String smtFunctionName, + final Expression argument, final CPrimitive argumentCType) { + mTranslation.declareFloatingPointFunction(loc, smtFunctionName, true, false, new CPrimitive(CPrimitives.BOOL), + argumentCType); + return mTranslation.constructCallToSmtPredicate(loc, smtFunctionName, argumentCType, + new Expression[] { argument }); + } + + @Override + public Expression isNan(final ILocation loc, final Expression argument, final CPrimitive type) { + return constructSmtFloatClassificationFunction(loc, "fp.isNaN", argument, type); + } + + @Override + public Expression isInfinite(final ILocation loc, final Expression argument, final CPrimitive type) { + return constructSmtFloatClassificationFunction(loc, "fp.isInfinite", argument, type); + } + + @Override + public Expression isNormal(final ILocation loc, final Expression argument, final CPrimitive type) { + return constructSmtFloatClassificationFunction(loc, "fp.isNormal", argument, type); + } + + @Override + public Expression isZero(final ILocation loc, final Expression argument, final CPrimitive type) { + return constructSmtFloatClassificationFunction(loc, "fp.isZero", argument, type); + } + + @Override + public Expression isSubnormal(final ILocation loc, final Expression argument, final CPrimitive type) { + return constructSmtFloatClassificationFunction(loc, "fp.isSubnormal", argument, type); + } + + @Override + public Expression isPositive(final ILocation loc, final Expression argument, final CPrimitive type) { + return constructSmtFloatClassificationFunction(loc, "fp.isPositive", argument, type); + } + + private Expression delegateBinaryFloatOperationToSmt(final ILocation loc, final Expression first, + final Expression second, final String smtFunctionName, final CPrimitive type) { + mTranslation.declareFloatingPointFunction(loc, smtFunctionName, false, false, type, type, type); + return mTranslation.constructCallToSmtOperation(loc, smtFunctionName, type, new Expression[] { first, second }); + } + + @Override + public Expression min(final ILocation loc, final Expression firstArgument, final Expression secondArgument, + final CPrimitive type) { + return delegateBinaryFloatOperationToSmt(loc, firstArgument, secondArgument, "fp.min", type); + } + + @Override + public Expression max(final ILocation loc, final Expression firstArgument, final Expression secondArgument, + final CPrimitive type) { + return delegateBinaryFloatOperationToSmt(loc, firstArgument, secondArgument, "fp.max", type); + } + + @Override + public Expression remainder(final ILocation loc, final Expression firstArgument, final Expression secondArgument, + final CPrimitive type) { + return delegateBinaryFloatOperationToSmt(loc, firstArgument, secondArgument, "fp.rem", type); + } + + @Override + public Expression createNan(final ILocation loc, final CPrimitive type) { + return createConstant(loc, BitvectorTranslation.SMT_LIB_NAN, type); + } + + @Override + public Expression createInfinity(final ILocation loc, final CPrimitive type) { + return createConstant(loc, BitvectorTranslation.SMT_LIB_PLUS_INF, type); + } + + @Override + public Expression createMinusInfinity(final ILocation loc, final CPrimitive type) { + return createConstant(loc, BitvectorTranslation.SMT_LIB_MINUS_INF, type); + } + + @Override + public Expression createPlusZero(final ILocation loc, final CPrimitive type) { + return createConstant(loc, BitvectorTranslation.SMT_LIB_PLUS_ZERO, type); + } + + private Expression createConstant(final ILocation loc, final String smtFunctionName, final CPrimitive type) { + mTranslation.declareFloatConstant(loc, smtFunctionName, type); + return mTranslation.constructCallToSmtOperation(loc, smtFunctionName, type, new Expression[] {}); + } +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorTranslation.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorTranslation.java index df9509eb32d..f52050a7df9 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorTranslation.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorTranslation.java @@ -45,7 +45,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.ASTType; import de.uni_freiburg.informatik.ultimate.boogie.ast.Attribute; import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; import de.uni_freiburg.informatik.ultimate.boogie.ast.CallStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; @@ -179,6 +178,7 @@ public VarList getBoogieVarlist() { private final Expression mCurrentRoundingModeMacroValue; // holds the current rounding mode ONLY when fesetround is disabled private final IdentifierExpression mCurrentRoundingMode; + private final BitvectorFloatingPointHandler mFloatingPointHandler; public BitvectorTranslation(final TypeSizes typeSizeConstants, final TranslationSettings translationSettings, final FlatSymbolTable symboltable, final ITypeHandler typeHandler) { @@ -201,6 +201,7 @@ public BitvectorTranslation(final TypeSizes typeSizeConstants, final Translation mCurrentRoundingModeMacroValue = mTypeSizes.constructLiteralForIntegerType(loc, intCPrimitive, BigInteger.valueOf(3)); } + mFloatingPointHandler = new BitvectorFloatingPointHandler(this); } private int computeBitsize(final CPrimitive cType) { @@ -236,9 +237,19 @@ public Expression constructLiteralForFloatingType(final ILocation loc, final CPr final Expression realValue = ExpressionFactory.createRealLiteral(loc, value.toString()); arguments = new Expression[] { getCurrentRoundingMode(), realValue }; } - final String functionName = getBoogieFunctionName(smtFunctionName, type); - return ExpressionFactory.constructFunctionApplication(loc, functionName, arguments, - mTypeHandler.getBoogieTypeForCType(type)); + return constructCallToSmtOperation(loc, smtFunctionName, type, arguments); + } + + protected Expression constructCallToSmtOperation(final ILocation loc, final String smtFunctionName, + final CPrimitive type, final Expression[] arguments) { + return ExpressionFactory.constructFunctionApplication(loc, getBoogieFunctionName(smtFunctionName, type), + arguments, mTypeHandler.getBoogieTypeForCType(type)); + } + + protected Expression constructCallToSmtPredicate(final ILocation loc, final String smtFunctionName, + final CPrimitive type, final Expression[] arguments) { + return ExpressionFactory.constructFunctionApplication(loc, getBoogieFunctionName(smtFunctionName, type), + arguments, BoogieType.TYPE_BOOL); } private String getBoogieFunctionName(final String smtFunctionName, final CPrimitive type) { @@ -552,7 +563,7 @@ private static ASTType constructBitvectorAstType(final ILocation loc, final int return new PrimitiveType(loc, "bv" + bitlength); } - private void declareFloatingPointFunction(final ILocation loc, final String smtFunctionName, + protected void declareFloatingPointFunction(final ILocation loc, final String smtFunctionName, final boolean boogieResultTypeBool, final boolean isRounded, final CPrimitive resultCType, final CPrimitive... paramCType) { declareFloatingPointFunction(loc, smtFunctionName, boogieResultTypeBool, isRounded, resultCType, null, @@ -825,9 +836,7 @@ public Expression constructBinaryComparisonFloatingPointExpression(final ILocati } declareFloatingPointFunction(loc, smtFunctionName, true, false, new CPrimitive(CPrimitives.BOOL), type1, type2); - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, type1); - Expression result = ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, - new Expression[] { exp1, exp2 }, BoogieType.TYPE_BOOL); + Expression result = constructCallToSmtPredicate(loc, smtFunctionName, type1, new Expression[] { exp1, exp2 }); if (isNegated) { result = ExpressionFactory.constructUnaryExpression(loc, UnaryExpression.Operator.LOGICNEG, result); @@ -847,9 +856,7 @@ protected Expression constructUnaryFloatingPointExpression(final ILocation loc, throw new UnsupportedSyntaxException(loc, "Unknown or unsupported unary expression"); } declareFloatingPointFunction(loc, smtFunctionName, false, false, type, type); - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, type); - return ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, new Expression[] { exp }, - mTypeHandler.getBoogieTypeForCType(type)); + return constructCallToSmtOperation(loc, smtFunctionName, type, new Expression[] { exp }); } @Override @@ -885,17 +892,10 @@ protected Expression constructArithmeticFloatingPointExpression(final ILocation default: throw new UnsupportedSyntaxException(loc, "Unknown or unsupported arithmetic expression"); } - if (isRounded) { - declareFloatingPointFunction(loc, smtFunctionName, false, isRounded, type1, type1, type2); - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, type1); - return ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, - new Expression[] { getCurrentRoundingMode(), exp1, exp2 }, - mTypeHandler.getBoogieTypeForCType(type1)); - } declareFloatingPointFunction(loc, smtFunctionName, false, isRounded, type1, type1, type2); - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, type1); - return ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, new Expression[] { exp1, exp2 }, - mTypeHandler.getBoogieTypeForCType(type1)); + final Expression[] arguments = + isRounded ? new Expression[] { getCurrentRoundingMode(), exp1, exp2 } : new Expression[] { exp1, exp2 }; + return constructCallToSmtOperation(loc, smtFunctionName, type1, arguments); } @Override @@ -960,57 +960,6 @@ private String declareConversionFunction(final ILocation loc, final CPrimitive o return prefixedFunctionName; } - @Override - public ExpressionResult createNanOrInfinity(final ILocation loc, final String name) { - final String smtFunctionName; - final CPrimitive type; - if (name.equals("INFINITY") || name.equals("inf") || name.equals("inff")) { - smtFunctionName = SMT_LIB_PLUS_INF; - type = new CPrimitive(CPrimitives.DOUBLE); - } else if (name.equals("NAN") || name.equals("nan")) { - smtFunctionName = SMT_LIB_NAN; - type = new CPrimitive(CPrimitives.DOUBLE); - } else if (name.equals("nanl")) { - smtFunctionName = SMT_LIB_NAN; - type = new CPrimitive(CPrimitives.LONGDOUBLE); - } else if (name.equals("nanf")) { - smtFunctionName = SMT_LIB_NAN; - type = new CPrimitive(CPrimitives.FLOAT); - } else { - throw new IllegalArgumentException("not a nan or infinity type"); - } - declareFloatConstant(loc, smtFunctionName, type); - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, type); - final Expression func = ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, - new Expression[] {}, mTypeHandler.getBoogieTypeForCType(type)); - return new ExpressionResult(new RValue(func, type)); - } - - public ExpressionResult createRoundingMode(final ILocation loc, final String name) { - final String smtFunctionName; - final CPrimitive type; - if (name.equals("INFINITY") || name.equals("inf") || name.equals("inff")) { - smtFunctionName = SMT_LIB_PLUS_INF; - type = new CPrimitive(CPrimitives.DOUBLE); - } else if (name.equals("NAN") || name.equals("nan")) { - smtFunctionName = SMT_LIB_NAN; - type = new CPrimitive(CPrimitives.DOUBLE); - } else if (name.equals("nanl")) { - smtFunctionName = SMT_LIB_NAN; - type = new CPrimitive(CPrimitives.LONGDOUBLE); - } else if (name.equals("nanf")) { - smtFunctionName = SMT_LIB_NAN; - type = new CPrimitive(CPrimitives.FLOAT); - } else { - throw new IllegalArgumentException("not a nan or infinity type"); - } - declareFloatConstant(loc, smtFunctionName, type); - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, type); - final Expression func = ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, - new Expression[] {}, mTypeHandler.getBoogieTypeForCType(type)); - return new ExpressionResult(new RValue(func, type)); - } - @Override public void declareFloatConstant(final ILocation loc, final String smtFunctionName, final CPrimitive type) { final FloatingPointSize fps = mTypeSizes.getFloatingPointSize(type.getType()); @@ -1031,340 +980,6 @@ public Expression getCurrentRoundingMode() { return mCurrentRoundingMode; } - @Override - public RValue constructOtherUnaryFloatOperation(final ILocation loc, final FloatFunction floatFunction, - final RValue argument) { - if ("sqrt".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.sqrt"; - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { getCurrentRoundingMode(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } else if ("trunc".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.roundToIntegral"; - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { SmtRoundingMode.RTZ.getBoogieIdentifierExpression(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } else if ("round".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.roundToIntegral"; - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { SmtRoundingMode.RNA.getBoogieIdentifierExpression(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } else if ("lround".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.roundToIntegral"; - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { SmtRoundingMode.RNA.getBoogieIdentifierExpression(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - - final RValue rval = new RValue(expr, resultType); - final ExpressionResult exprResult = new ExpressionResultBuilder().setLrValue(rval).build(); - - return (RValue) convertFloatToIntNonBool(loc, exprResult, new CPrimitive(CPrimitives.LONG)).getLrValue(); - } else if ("llround".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.roundToIntegral"; - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { SmtRoundingMode.RNA.getBoogieIdentifierExpression(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - - final RValue rval = new RValue(expr, resultType); - final ExpressionResult exprResult = new ExpressionResultBuilder().setLrValue(rval).build(); - - return (RValue) convertFloatToIntNonBool(loc, exprResult, new CPrimitive(CPrimitives.LONGLONG)) - .getLrValue(); - } else if ("floor".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.roundToIntegral"; - - // TODO: Its the wrong return type. We need to get the bv type for this float type and pass it to this - // declare function thing. - // We also need to declare the matching - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { SmtRoundingMode.RTN.getBoogieIdentifierExpression(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } else if ("ceil".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.roundToIntegral"; - declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { SmtRoundingMode.RTP.getBoogieIdentifierExpression(), argument.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } else if ("sin".equals(floatFunction.getFunctionName())) { - // TODO Create correct BoogieFunction using SMT functions. See - // http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml - // Check how sin in calculated in c source. I believe it is approximated with a polynomial - // See Taylor's theorem - throw new UnsupportedOperationException( - "not yet supported float operation " + floatFunction.getFunctionName()); - /* - * checkIsFloatPrimitive(argument); final CPrimitive argumentType = (CPrimitive) - * argument.getCType().getUnderlyingType(); final String smtFunctionName = "fp.sin"; - * declareFloatingPointFunction(loc, smtFunctionName, false, true, argumentType, argumentType); final String - * boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); final CPrimitive resultType = - * (CPrimitive) argument.getCType().getUnderlyingType(); final Expression expr = - * ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, new Expression[] { - * getRoundingMode(), argument.getValue() }, mTypeHandler.getBoogieTypeForCType(resultType)); return new - * RValue(expr, resultType); - */ - } else if ("fabs".equals(floatFunction.getFunctionName())) { - checkIsFloatPrimitive(argument); - final CPrimitive argumentType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String smtFunctionName = "fp.abs"; - declareFloatingPointFunction(loc, smtFunctionName, false, false, argumentType, argumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentType); - final CPrimitive resultType = (CPrimitive) argument.getCType().getUnderlyingType(); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { argument.getValue() }, mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } else if ("isnan".equals(floatFunction.getFunctionName())) { - final String smtFunctionName = "fp.isNaN"; - return constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - } else if ("isinf".equals(floatFunction.getFunctionName())) { - final String smtFunctionName = "fp.isInfinite"; - return constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - } else if ("isnormal".equals(floatFunction.getFunctionName())) { - final String smtFunctionName = "fp.isNormal"; - return constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - } else if ("isfinite".equals(floatFunction.getFunctionName()) - || "finite".equals(floatFunction.getFunctionName())) { - final Expression isNormal; - { - final String smtFunctionName = "fp.isNormal"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isNormal = rvalue.getValue(); - } - final Expression isSubnormal; - { - final String smtFunctionName = "fp.isSubnormal"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isSubnormal = rvalue.getValue(); - } - final Expression isZero; - { - final String smtFunctionName = "fp.isZero"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isZero = rvalue.getValue(); - } - final Expression resultExpr = ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, - ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, isNormal, isSubnormal), isZero); - return new RValue(resultExpr, new CPrimitive(CPrimitives.INT), true); - } else if ("fpclassify".equals(floatFunction.getFunctionName())) { - final Expression isInfinite; - { - final String smtFunctionName = "fp.isInfinite"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isInfinite = rvalue.getValue(); - } - final Expression isNan; - { - final String smtFunctionName = "fp.isNaN"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isNan = rvalue.getValue(); - } - final Expression isNormal; - { - final String smtFunctionName = "fp.isNormal"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isNormal = rvalue.getValue(); - } - final Expression isSubnormal; - { - final String smtFunctionName = "fp.isSubnormal"; - final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - isSubnormal = rvalue.getValue(); - } - // final Expression isZero; - // { - // final String smtLibFunctionName = "fp.isZero"; - // final RValue rvalue = constructSmtFloatClassificationFunction(loc, - // smtLibFunctionName, argument); - // isZero = rvalue.getValue(); - // } - final Expression resultExpr = ExpressionFactory.constructIfThenElseExpression(loc, isInfinite, - handleNumberClassificationMacro(loc, "FP_INFINITE").getValue(), - ExpressionFactory.constructIfThenElseExpression(loc, isNan, - handleNumberClassificationMacro(loc, "FP_NAN").getValue(), - ExpressionFactory.constructIfThenElseExpression(loc, isNormal, - handleNumberClassificationMacro(loc, "FP_NORMAL").getValue(), - ExpressionFactory.constructIfThenElseExpression(loc, isSubnormal, - handleNumberClassificationMacro(loc, "FP_SUBNORMAL").getValue(), - handleNumberClassificationMacro(loc, "FP_ZERO").getValue())))); - return new RValue(resultExpr, new CPrimitive(CPrimitives.INT)); - } else if ("signbit".equals(floatFunction.getFunctionName())) { - // TODO: Handle negative NaN correctly - // final Expression isNegative; - // final String smtFunctionName = "fp.isNegative"; - // final RValue rvalue = constructSmtFloatClassificationFunction(loc, smtFunctionName, argument); - // isNegative = rvalue.getValue(); - // - // final CPrimitive cPrimitive = new CPrimitive(CPrimitives.INT); - // final Expression resultExpr = ExpressionFactory.constructIfThenElseExpression(loc, isNegative, - // mTypeSizes.constructLiteralForIntegerType(loc, cPrimitive, BigInteger.ONE), - // mTypeSizes.constructLiteralForIntegerType(loc, cPrimitive, BigInteger.ZERO)); - // return new RValue(resultExpr, cPrimitive); - } - throw new UnsupportedOperationException("not yet supported float operation " + floatFunction.getFunctionName()); - } - - private static void checkIsFloatPrimitive(final RValue argument) { - if (!(argument.getCType().getUnderlyingType() instanceof final CPrimitive cPrimitive) - || !cPrimitive.getType().isFloatingtype()) { - throw new IllegalArgumentException( - "can apply float operation only to floating type, but saw " + argument.getCType()); - } - } - - @Override - public RValue constructOtherBinaryFloatOperation(final ILocation loc, final FloatFunction floatFunction, - final RValue first, final RValue second) { - // TODO Auto-generated method stub - switch (floatFunction.getFunctionName()) { - case "fmin": - return delegateOtherBinaryFloatOperationToSmt(loc, first, second, "fp.min"); - case "fmax": - return delegateOtherBinaryFloatOperationToSmt(loc, first, second, "fp.max"); - case "remainder": - // TODO: Remove until unsoundness can be investigated - break; - // return delegateOtherBinaryFloatOperationToSmt(loc, first, second, "fp.rem"); - case "fmod": - /** - * 7.12.10.1 The fmod functions - * - * The fmod functions compute the floating-point remainder of x/y. - * - * The fmod functions return the value x − ny, for some integer n such that, if y is nonzero, the result has - * the same sign as x and magnitude less than the magnitude of y. If y is zero, whether a domain error - * occurs or the fmod functions return zero is implementation- defined. - */ - // fmod guarantees that the return value is the same sign as the first argument (x) - // copies the sign of firts element to remainder value - final RValue remainderValue = delegateOtherBinaryFloatOperationToSmt(loc, first, second, "fp.rem"); - final FloatFunction copySignFunction = FloatFunction.decode("copysign"); - return constructOtherBinaryFloatOperation(loc, copySignFunction, remainderValue, first); - case "fdim": - final FloatFunction isNaN = FloatFunction.decode("isnan"); - - // if (first || second) is NaN -> NaN - final RValue firstIsNaN = constructOtherUnaryFloatOperation(loc, isNaN, first); - final RValue secondIsNaN = constructOtherUnaryFloatOperation(loc, isNaN, second); - - // if first>second, first - second, else +0 - final CPrimitive typeFirst = (CPrimitive) first.getCType().getUnderlyingType(); - final CPrimitive typeSecond = (CPrimitive) second.getCType().getUnderlyingType(); - - final Expression comparison = constructBinaryComparisonFloatingPointExpression(loc, - IASTBinaryExpression.op_greaterThan, first.getValue(), typeFirst, second.getValue(), typeSecond); - - final Expression subtraction = constructArithmeticFloatingPointExpression(loc, - IASTBinaryExpression.op_minus, first.getValue(), typeFirst, second.getValue(), typeSecond); - - final Expression zero = constructLiteralForFloatingType(loc, typeFirst, BigDecimal.ZERO); - - final Expression resultExprFdim = - ExpressionFactory.constructIfThenElseExpression(loc, comparison, subtraction, zero); - - final Expression secondNaNExpr = ExpressionFactory.constructIfThenElseExpression(loc, - secondIsNaN.getValue(), second.getValue(), resultExprFdim); - - final Expression firstNaNExpr = ExpressionFactory.constructIfThenElseExpression(loc, firstIsNaN.getValue(), - first.getValue(), secondNaNExpr); - - return new RValue(firstNaNExpr, typeFirst); - case "copysign": - // TODO: Handle negative NaN, check unsoundness - // if second is negative, return arithneg of abs(first), else return abs(first) - // final FloatFunction absfloatFunction = FloatFunction.decode("fabs"); - // final RValue absoluteValue = constructOtherUnaryFloatOperation(loc, absfloatFunction, first); - // - // final String smtNegativeFunctionName = "fp.isNegative"; - // final RValue secondNegativeRvalue = - // constructSmtFloatClassificationFunction(loc, smtNegativeFunctionName, second); - // final Expression isNegativeSecond = secondNegativeRvalue.getValue(); - // final CPrimitive resultType = (CPrimitive) first.getCType().getUnderlyingType(); - // final Expression negative = constructUnaryFloatingPointExpression(loc, IASTUnaryExpression.op_minus, - // absoluteValue.getValue(), resultType); - // final Expression resultExpr = ExpressionFactory.constructIfThenElseExpression(loc, isNegativeSecond, - // negative, absoluteValue.getValue()); - // return new RValue(resultExpr, resultType); - break; - default: - break; - } - throw new UnsupportedOperationException("not yet supported float operation " + floatFunction.getFunctionName()); - } - - private RValue delegateOtherBinaryFloatOperationToSmt(final ILocation loc, final RValue first, final RValue second, - final String smtFunctionName) { - checkIsFloatPrimitive(first); - checkIsFloatPrimitive(second); - final CPrimitive firstArgumentType = (CPrimitive) first.getCType().getUnderlyingType(); - - final CPrimitive secondArgumentType = (CPrimitive) first.getCType().getUnderlyingType(); - if (!firstArgumentType.equals(secondArgumentType)) { - throw new IllegalArgumentException("No mixed type arguments allowed"); - } - declareFloatingPointFunction(loc, smtFunctionName, false, false, firstArgumentType, firstArgumentType, - secondArgumentType); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, firstArgumentType); - final CPrimitive resultType = firstArgumentType; - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { first.getValue(), second.getValue() }, - mTypeHandler.getBoogieTypeForCType(resultType)); - return new RValue(expr, resultType); - } - - private RValue constructSmtFloatClassificationFunction(final ILocation loc, final String smtFunctionName, - final RValue argument) { - final CPrimitive argumentCType = (CPrimitive) argument.getCType().getUnderlyingType(); - final String boogieFunctionName = getBoogieFunctionName(smtFunctionName, argumentCType); - final CPrimitive resultCType = new CPrimitive(CPrimitives.INT); - final ASTType resultBoogieType = new PrimitiveType(loc, BoogieType.TYPE_BOOL, SFO.BOOL); - final Attribute[] attributes = - generateAttributes(loc, mSettings.overapproximateFloatingPointOperations(), smtFunctionName, null); - final ASTType paramBoogieType = mTypeHandler.cType2AstType(loc, argumentCType); - getFunctionDeclarations().declareFunction(loc, boogieFunctionName, attributes, resultBoogieType, - paramBoogieType); - final Expression expr = ExpressionFactory.constructFunctionApplication(loc, boogieFunctionName, - new Expression[] { argument.getValue() }, BoogieType.TYPE_BOOL); - return new RValue(expr, resultCType, true); - } - @Override public Expression transformBitvectorToFloat(final ILocation loc, final Expression bitvector, final CPrimitives floatType) { @@ -1376,12 +991,8 @@ public Expression transformBitvectorToFloat(final ILocation loc, final Expressio final Expression signBit = extractBits(loc, bitvector, floatingPointSize.getSignificant() - 1 + floatingPointSize.getExponent() + 1, floatingPointSize.getSignificant() - 1 + floatingPointSize.getExponent()); - final String smtFunctionName = "fp"; - final String fullFunctionName = getBoogieFunctionName(smtFunctionName, new CPrimitive(floatType)); - return ExpressionFactory.constructFunctionApplication(loc, fullFunctionName, - new Expression[] { signBit, exponentBits, significantBits }, - mTypeHandler.getBoogieTypeForCType(new CPrimitive(floatType))); - + return constructCallToSmtOperation(loc, "fp", new CPrimitive(floatType), + new Expression[] { signBit, exponentBits, significantBits }); } @Override @@ -1633,4 +1244,8 @@ protected Pair constructOverflowCheckForLeftShift(final return new Pair<>(biggerMinInt, smallerMaxInt); } + @Override + public IFloatingPointHandler getFloatingPointHandler() { + return mFloatingPointHandler; + } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java index f7a6523f4ea..6a50a7a3bb4 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java @@ -406,40 +406,8 @@ public abstract Expression eraseBits(final ILocation loc, final Expression value public abstract Expression signExtend(ILocation loc, Expression operand, int bitsBefore, int bitsAfter); - public abstract ExpressionResult createNanOrInfinity(ILocation loc, String name); - - public ExpressionResult createNan(final ILocation loc, final CPrimitive cPrimitive) { - if (!cPrimitive.isFloatingType()) { - throw new IllegalArgumentException("can only create NaN for floating types"); - } - final String s; - switch (cPrimitive.getType()) { - case FLOAT: { - s = "nanf"; - break; - } - case DOUBLE: { - s = "nan"; - break; - } - case LONGDOUBLE: { - s = "nanl"; - break; - } - default: - throw new IllegalArgumentException("can only create NaN for floating types"); - } - return createNanOrInfinity(loc, s); - } - public abstract Expression getCurrentRoundingMode(); - public abstract RValue constructOtherUnaryFloatOperation(ILocation loc, FloatFunction floatFunction, - RValue argument); - - public abstract RValue constructOtherBinaryFloatOperation(ILocation loc, FloatFunction floatFunction, RValue first, - RValue second); - public abstract void declareFloatConstant(final ILocation loc, final String smtFunctionName, final CPrimitive type); public abstract void declareBinaryBitvectorFunctionsForAllIntegerDatatypes(final ILocation loc, @@ -472,36 +440,6 @@ private static String makeBoogieIdentifierSuffix(final String val) { return val; } - /** - * Translate number classification macros according to 7.12.6 of C11. Although the standard allows any distinct - * integers, we take 0,1,2,3,4 because gcc on Matthias' Linux system uses these numbers. - */ - public RValue handleNumberClassificationMacro(final ILocation loc, final String cId) { - final int number; - switch (cId) { - case "FP_NAN": - number = 0; - break; - case "FP_INFINITE": - number = 1; - break; - case "FP_ZERO": - number = 2; - break; - case "FP_SUBNORMAL": - number = 3; - break; - case "FP_NORMAL": - number = 4; - break; - default: - throw new IllegalArgumentException("no number classification macro " + cId); - } - final CPrimitive type = new CPrimitive(CPrimitives.INT); - final Expression expr = mTypeSizes.constructLiteralForIntegerType(loc, type, BigInteger.valueOf(number)); - return new RValue(expr, type); - } - /** * Generate the attributes for the Boogie code that make sure that we either - translate to the desired SMT * functions, or - let Ultimate overapproximate @@ -612,4 +550,6 @@ public static Statement modelUnsupportedFeature(final ILocation loc, final Strin return new WhileStatement(loc, ExpressionFactory.createBooleanLiteral(loc, true), new LoopInvariantSpecification[0], new Statement[] { assertFalse }); } + + public abstract IFloatingPointHandler getFloatingPointHandler(); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java deleted file mode 100644 index b0724aa8fa7..00000000000 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java +++ /dev/null @@ -1,140 +0,0 @@ -/* - * Copyright (C) 2016 Matthias Heizmann (heizmann@informatik.uni-freiburg.de) - * Copyright (C) 2016 University of Freiburg - * - * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * - * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as published - * by the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public License - * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * - * Additional permission under GNU GPL version 3 section 7: - * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission - * to convey the resulting work. - */ -package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation; - -import java.util.Arrays; - -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; - -/** - * Auxiliary class for decomposing and representing C float functions. - * - * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de) - * - */ -public class FloatFunction { - - /** - * Prefix that floating point functions get after preprocessing with gcc. - */ - private static final String GCC_PREFIX = "__"; - - private static final String[] FLOAT_FUNCTIONS = { "fpclassify", // see 7.12.3.1 - "isfinite", "finite", // see 7.12.3.2 - "isinf", // see 7.12.3.3 - "isnan", // see 7.12.3.4 - "isnormal", // see 7.12.3.5 - "signbit", // see 7.12.3.6 - "sqrt", "fabs", // see 7.12.7.2 - "fmin", "fmax", // - "trunc", // see 7.12.9.8 - "round", "lround", "llround", // see 7.12.9.6 and 7.12.9.7 - "floor", // see 7.12.9.2 - "ceil", // see 7.12.9.1 - "sin", // see 7.12.4.6 - "remainder", // see 7.12.10.2 - "copysign", // see 7.12.11.1 - "fmod", // see 7.12.10.1 - "fdim" // see 7.12.12.1 - }; - - private static final String[] TYPE_SUFFIXES = { "f", "d", "l" }; - - private final String mPrefix; - private final String mFunction; - private final String mTypeSuffix; - - public FloatFunction(final String prefix, final String function, final String typeSuffix) { - mPrefix = prefix; - mFunction = function; - mTypeSuffix = typeSuffix; - } - - public String getPrefix() { - return mPrefix; - } - - public String getFunctionName() { - return mFunction; - } - - public String getTypeSuffix() { - return mTypeSuffix; - } - - public CPrimitive getType() { - switch (mTypeSuffix) { - case "f": - return new CPrimitive(CPrimitives.FLOAT); - case "": - case "d": - return new CPrimitive(CPrimitives.DOUBLE); - case "l": - return new CPrimitive(CPrimitives.LONGDOUBLE); - default: - throw new AssertionError("unknown type suffix " + mTypeSuffix); - } - } - - public static FloatFunction decode(final String fullFunctionName) { - final String withoutPrefix; - final String prefix; - if (fullFunctionName.startsWith(GCC_PREFIX)) { - withoutPrefix = fullFunctionName.substring(2); - prefix = GCC_PREFIX; - } else { - withoutPrefix = fullFunctionName; - prefix = ""; - } - final String function = returnFirstMatching(withoutPrefix); - if (function == null) { - return null; - } - final String typeSuffix; - final String remaining = withoutPrefix.substring(function.length()); - if (remaining.isEmpty()) { - typeSuffix = ""; - } else if (Arrays.asList(TYPE_SUFFIXES).contains(remaining)) { - typeSuffix = remaining; - } else { - // some string remaining that we cannot decode - return null; - } - return new FloatFunction(prefix, function, typeSuffix); - } - - private static String returnFirstMatching(final String withoutPrefix) { - for (final String floatFunction : FLOAT_FUNCTIONS) { - if (withoutPrefix.startsWith(floatFunction)) { - return floatFunction; - } - } - return null; - } - -} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IFloatingPointHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IFloatingPointHandler.java new file mode 100644 index 00000000000..fb46146d8b8 --- /dev/null +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IFloatingPointHandler.java @@ -0,0 +1,127 @@ +/* + * Copyright (C) 2025 Frank Schüssele (schuessf@informatik.uni-freiburg.de) + * Copyright (C) 2025 University of Freiburg + * + * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation; + +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; + +/** + * Handles expressions representing floating point operations according to the IEEE standard 754-2008. + * + * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de) + */ +public interface IFloatingPointHandler { + /** + * Returns an expression representing {@code argument} rounded to an integer according to the given + * {@code roundingMode}. + */ + Expression roundToIntegral(ILocation loc, Expression argument, CPrimitive type, Expression roundingMode); + + /** + * Returns an expression representing the square root of {@code argument}. + */ + Expression sqrt(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression representing the absolute value of {@code argument}. + */ + Expression abs(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression that checks if {@code argument} is NaN (not a number). + */ + Expression isNan(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression that checks if {@code argument} is infinite (i.e., either plus or minus infinity). + */ + Expression isInfinite(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression that checks if {@code argument} is a normal number (see IEEE 754-2008 2.1.38: "a finite + * non-zero floating-point number with magnitude greater than or equal to a minimum b^emin value, where b is the + * radix"). + */ + Expression isNormal(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression that checks if {@code argument} is zero (i.e., either plus or minus zero). + */ + Expression isZero(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression that checks if {@code argument} is a subnormal number (see IEEE 754-2008 2.1.51: "a + * non-zero floating-point number with magnitude less than the magnitude of that format's smallest normal number"). + */ + Expression isSubnormal(ILocation loc, Expression argument, CPrimitive type); + + /** + * Returns an expression that checks if {@code argument} is positive (incl. plus zero). + */ + Expression isPositive(ILocation loc, Expression argument, CPrimitive type); + + /** + * Create an expression representing NaN (not a number). + */ + Expression createNan(ILocation loc, CPrimitive type); + + /** + * Create an expression representing plus infinity. + */ + Expression createInfinity(ILocation loc, CPrimitive type); + + /** + * Create an expression representing minus infinity. + */ + Expression createMinusInfinity(ILocation loc, CPrimitive type); + + /** + * Create an expression representing plus zero. + */ + Expression createPlusZero(ILocation loc, CPrimitive type); + + /** + * Returns an expression representing the minimum of {@code firstArgument} and {@code secondArgument}. + */ + Expression min(ILocation loc, Expression firstArgument, Expression secondArgument, CPrimitive type); + + /** + * Returns an expression representing the maximum of {@code firstArgument} and {@code secondArgument}. + */ + Expression max(ILocation loc, Expression firstArgument, Expression secondArgument, CPrimitive type); + + /** + * Returns an expression representing the remainder of {@code firstArgument} divided by {@code secondArgument} (see + * IEEE 754-2008 5.3.1: "When y ≠ 0, the remainder r = remainder(x, y) is defined for finite x and y regardless of + * the rounding-direction attribute by the mathematical relation r = x − y × n, where n is the integer nearest the + * exact number x/y ; whenever | n − x/y | = ½ , then n is even. Thus, the remainder is always exact. If r = 0, its + * sign shall be that of x. remainder(x, ∞) is x for finite x."). + */ + Expression remainder(ILocation loc, Expression firstArgument, Expression secondArgument, CPrimitive type); +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java index 7e07d29a45b..82fa6f2f121 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java @@ -75,6 +75,7 @@ public class IntegerTranslation extends ExpressionTranslation { private static final String NOT_IMPLEMENTED = "Operation is not yet implemented in non-bitprecise translation."; private final BitabsTranslation mBitabsTranslation; + private final IFloatingPointHandler mFloatingPointHandler = new UnsupportedFloatingPointHandler(); public IntegerTranslation(final TypeSizes typeSizeConstants, final TranslationSettings settings, final ITypeHandler typeHandler, final FlatSymbolTable symboltable) { @@ -611,30 +612,11 @@ private static Expression constructEquality(final ILocation loc, final int nodeO throw new IllegalArgumentException("operator is neither equals nor not equals"); } - @Override - public ExpressionResult createNanOrInfinity(final ILocation loc, final String name) { - throw new UnsupportedOperationException("createNanOrInfinity is unsupported in non-bitprecise translation"); - } - @Override public Expression getCurrentRoundingMode() { throw new UnsupportedOperationException("getRoundingMode is unsupported in non-bitprecise translation"); } - @Override - public RValue constructOtherUnaryFloatOperation(final ILocation loc, final FloatFunction floatFunction, - final RValue argument) { - throw new UnsupportedOperationException("floating point operation not supported in non-bitprecise translation: " - + floatFunction.getFunctionName()); - } - - @Override - public RValue constructOtherBinaryFloatOperation(final ILocation loc, final FloatFunction floatFunction, - final RValue first, final RValue second) { - throw new UnsupportedOperationException("floating point operation not supported in non-bitprecise translation: " - + floatFunction.getFunctionName()); - } - @Override public ExpressionResult convertFloatToFloat(final ILocation loc, final ExpressionResult rexp, final CPrimitive newType) { @@ -802,4 +784,9 @@ protected Pair constructOverflowCheckForLeftShift(final final ExpressionResult exprResult) { return constructOverflowCheck(loc, resultType, exprResult.getLrValue().getValue()); } + + @Override + public IFloatingPointHandler getFloatingPointHandler() { + return mFloatingPointHandler; + } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/UnsupportedFloatingPointHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/UnsupportedFloatingPointHandler.java new file mode 100644 index 00000000000..e0ba86c8ec5 --- /dev/null +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/UnsupportedFloatingPointHandler.java @@ -0,0 +1,126 @@ +/* + * Copyright (C) 2025 Frank Schüssele (schuessf@informatik.uni-freiburg.de) + * Copyright (C) 2025 University of Freiburg + * + * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * to convey the resulting work. + */ + +package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation; + +import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; +import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; + +/** + * Implementation of {@link IFloatingPointHandler} that throws {@link UnsupportedOperationException} whenever any method is invoked, which can be used when + * floating-point operations are not supported (e.g., in {@link IntegerTranslation}). + * + * @author Frank Schüssele (schuessf@informatik.uni-freiburg.de) + */ +public class UnsupportedFloatingPointHandler implements IFloatingPointHandler { + private static final String NOT_IMPLEMENTED = "Operation is not yet implemented in non-bitprecise translation."; + + @Override + public Expression roundToIntegral(final ILocation loc, final Expression argument, final CPrimitive type, + final Expression roundingMode) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression sqrt(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression abs(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression isNan(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression isInfinite(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression isNormal(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression isZero(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression isSubnormal(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression isPositive(final ILocation loc, final Expression argument, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression createNan(final ILocation loc, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression createInfinity(final ILocation loc, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression createMinusInfinity(final ILocation loc, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression createPlusZero(final ILocation loc, final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression min(final ILocation loc, final Expression firstArgument, final Expression secondArgument, + final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression max(final ILocation loc, final Expression firstArgument, final Expression secondArgument, + final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } + + @Override + public Expression remainder(final ILocation loc, final Expression firstArgument, final Expression secondArgument, + final CPrimitive type) { + throw new UnsupportedOperationException(NOT_IMPLEMENTED); + } +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/GccBuiltinLibraryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/GccBuiltinLibraryModel.java index aece526b125..f533b425a24 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/GccBuiltinLibraryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/GccBuiltinLibraryModel.java @@ -131,8 +131,6 @@ public Collection getFunctionModels() { result.add(new FunctionModel("__builtin_constant_p", (main, node, loc, name) -> mHelper .handleByOverapproximation(main, node, loc, name, 1, new CPrimitive(CPrimitives.BOOL)))); - result.add(new FunctionModel("__builtin_isinf_sign", (main, node, loc, name) -> mHelper - .handleByOverapproximation(main, node, loc, name, 1, new CPrimitive(CPrimitives.INT)))); /* * 6.56 Built-in Functions to Perform Arithmetic with Overflow Checking diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java index 25bfd86e9bf..7a457baa509 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java @@ -31,6 +31,8 @@ */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.library; +import java.math.BigDecimal; +import java.math.BigInteger; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -39,15 +41,26 @@ import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; import org.eclipse.cdt.core.dom.ast.IASTFunctionCallExpression; import org.eclipse.cdt.core.dom.ast.IASTInitializerClause; +import org.eclipse.cdt.core.dom.ast.IASTUnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; +import de.uni_freiburg.informatik.ultimate.boogie.StatementFactory; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AtomicStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.HavocStatement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CExpressionTranslator; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CTranslationUtil; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.IDispatcher; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.BitvectorTranslation.SmtRoundingMode; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.FloatFunction; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.IFloatingPointHandler; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.AuxVarInfo; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.AuxVarInfoBuilder; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; @@ -56,7 +69,9 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.LRValue; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.Result; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO.AUXVAR; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.INameHandler; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.OverapproxVariable; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; @@ -64,274 +79,329 @@ * Model of functions from math.h (C11 7.12, https://en.cppreference.com/w/c/header/math) */ public class MathLibraryModel implements ILibraryModel { - private final static String[] UNSUPPORTED_FLOAT_OPERATIONS = { "frexp", "ldexp", "pow", "hypot", "cbrt", "drem", - "significand", "j0", "j1", "jn", "y0", "y1", "yn", "erfc", "lgamma", "tgamma", "gamma", "lgamma_r", - "nextafter", "nexttoward", "scalbn", "ilogb", "scalbln", "remquo", "lrint", "llrint", "fma", "scalb", - "frexpf", "ldexpf", "powf", "hypotf", "cbrtf", "dremf", "significandf", "j0f", "j1f", "jnf", "y0f", "y1f", - "ynf", "erfcf", "lgammaf", "tgammaf", "gammaf", "lgammaf_r", "nextafterf", "nexttowardf", "scalbnf", - "ilogbf", "scalblnf", "remquof", "lrintf", "llrintf", "fmaf", "scalbf", "frexpl", "ldexpl", "powl", - "hypotl", "cbrtl", "dreml", "significandl", "j0l", "j1l", "jnl", "y0l", "y1l", "ynl", "erfcl", "lgammal", - "tgammal", "gammal", "lgammal_r", "nextafterl", "nexttowardl", "scalbnl", "ilogbl", "scalblnl", "remquol", - "lrintl", "llrintl", "fmal", "scalbl", "signgam;", "modf", "modff", "modfl" }; - - private static final List UNARY_FUNCTIONS = List.of( - // see 7.12.3.1 or http://en.cppreference.com/w/c/numeric/math/fpclassify - "fpclassify", "__fpclassify", "__fpclassifyf", "__fpclassifyl", - - // see 7.12.3.2 or http://en.cppreference.com/w/c/numeric/math/isfinite - "isfinite", - - // see 7.12.3.3 or http://en.cppreference.com/w/c/numeric/math/isinf - "isinf", "__isinf", - - // see 7.12.3.4 or http://en.cppreference.com/w/c/numeric/math/isnan - "isnan", "__isnan", - - // see https://linux.die.net/man/3/finite (! NOT PART OF ANSI-C) - "finite", "__finite", "finitef", "__finitef", "finitel", "__finitel", "isinff", "__isinff", "isinfl", - "__isinfl", "isnanf", "isnanl", "__isnanf", "__isnanl", - - // see 7.12.3.5 or http://en.cppreference.com/w/c/numeric/math/isnormal - "isnormal", - - // see 7.12.7.5 or http://en.cppreference.com/w/c/numeric/math/sqrt - "sqrt", "sqrtf", "sqrtl", - - // see 7.12.7.2 or http://en.cppreference.com/w/c/numeric/math/fabs - "fabs", "fabsf", "fabsl", + // Number classification macros according to 7.12.6 of C11 + private enum Classification { + NAN("FP_NAN", 0), INFINITE("FP_INFINITE", 1), ZERO("FP_ZERO", 2), SUBNORMAL("FP_SUBNORMAL", 3), + NORMAL("FP_NORMAL", 4); - // see 7.12.9.8 or http://en.cppreference.com/w/c/numeric/math/trunc - "trunc", "truncf", "truncl", + private final String mName; + private final int mValue; - // see 7.12.9.6 or http://en.cppreference.com/w/c/numeric/math/round - "round", "roundf", "roundl", - - // see 7.12.9.7 or http://en.cppreference.com/w/c/numeric/math/round - "lround", "lroundf", "lroundl", "llround", "llroundf", "llroundl", - - // see 7.12.9.2 or http://en.cppreference.com/w/c/numeric/math/floor - "floor", "floorf", "floorl", - - // see 7.12.9.1 or http://en.cppreference.com/w/c/numeric/math/ceil - "ceil", "ceilf", "ceilr"); - - private static final List BINARY_FUNCTIONS = List.of( - // see 7.12.12.2 or http://en.cppreference.com/w/c/numeric/math/fmax - // NaN arguments are treated as missing data: if one argument is a NaN and the - // other numeric, then the - // fmin/fmax functions choose the numeric value. - "fmax", "fmaxf", "fmaxl", + Classification(final String name, final int value) { + mName = name; + mValue = value; + } - // see 7.12.12.3 or http://en.cppreference.com/w/c/numeric/math/fmin - "fmin", "fminf", "fminl", + public String getName() { + return mName; + } - // see 7.12.10.1 or http://en.cppreference.com/w/c/numeric/math/fmod - "fmod", "fmodf", "fmodl", + public Expression asExpression(final ILocation loc, final ExpressionTranslation exprTranslation) { + return exprTranslation.constructLiteralForIntegerType(loc, new CPrimitive(CPrimitives.INT), + BigInteger.valueOf(mValue)); + } + } - // see 7.12.12.1 or https://en.cppreference.com/w/c/numeric/math/fdim - "fdim", "fdimf", "fdiml"); + private final static String[] UNSUPPORTED_FLOAT_OPERATIONS = { "frexp", "ldexp", "pow", "hypot", "cbrt", "drem", + "significand", "j0", "j1", "jn", "y0", "y1", "yn", "erfc", "lgamma", "tgamma", "gamma", "lgamma_r", + "nextafter", "nexttoward", "scalbn", "ilogb", "scalbln", "remquo", "fma", "scalb", "frexpf", "ldexpf", + "powf", "hypotf", "cbrtf", "dremf", "significandf", "j0f", "j1f", "jnf", "y0f", "y1f", "ynf", "erfcf", + "lgammaf", "tgammaf", "gammaf", "lgammaf_r", "nextafterf", "nexttowardf", "scalbnf", "ilogbf", "scalblnf", + "remquof", "fmaf", "scalbf", "frexpl", "ldexpl", "powl", "hypotl", "cbrtl", "dreml", "significandl", "j0l", + "j1l", "jnl", "y0l", "y1l", "ynl", "erfcl", "lgammal", "tgammal", "gammal", "lgammal_r", "nextafterl", + "nexttowardl", "scalbnl", "ilogbl", "scalblnl", "remquol", "fmal", "scalbl", "signgam;", "modf", "modff", + "modfl" }; private final FunctionModelHelper mHelper; private final ExpressionResultTransformer mExprResultTransformer; private final ExpressionTranslation mExpressionTranslation; + private final IFloatingPointHandler mFloatHandler; private final CExpressionTranslator mCEpressionTranslator; private final INameHandler mNameHandler; + private final AuxVarInfoBuilder mAuxVarInfoBuilder; public MathLibraryModel(final FunctionModelHelper helper, final ExpressionResultTransformer exprResultTransformer, final ExpressionTranslation expressionTranslation, final CExpressionTranslator cEpressionTranslator, - final INameHandler nameHandler) { + final INameHandler nameHandler, final AuxVarInfoBuilder auxVarInfoBuilder) { mHelper = helper; mExprResultTransformer = exprResultTransformer; mExpressionTranslation = expressionTranslation; + mFloatHandler = expressionTranslation.getFloatingPointHandler(); mCEpressionTranslator = cEpressionTranslator; mNameHandler = nameHandler; + mAuxVarInfoBuilder = auxVarInfoBuilder; } - private static List> getOverapproximatedUnaryFunctions() { - final List> result = new ArrayList<>(); - - // https://en.cppreference.com/w/c/numeric/math/sin - result.add(new Pair<>("sin", CPrimitives.DOUBLE)); - result.add(new Pair<>("sinf", CPrimitives.FLOAT)); - result.add(new Pair<>("sinl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/exp - result.add(new Pair<>("exp", CPrimitives.DOUBLE)); - result.add(new Pair<>("expf", CPrimitives.FLOAT)); - result.add(new Pair<>("expl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/expm1 - result.add(new Pair<>("expm1", CPrimitives.DOUBLE)); - result.add(new Pair<>("expm1f", CPrimitives.FLOAT)); - result.add(new Pair<>("expm1l", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/tanh - result.add(new Pair<>("tanh", CPrimitives.DOUBLE)); - result.add(new Pair<>("tanhf", CPrimitives.FLOAT)); - result.add(new Pair<>("tanhl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/erf - result.add(new Pair<>("erf", CPrimitives.DOUBLE)); - result.add(new Pair<>("erff", CPrimitives.FLOAT)); - result.add(new Pair<>("erfl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/log - result.add(new Pair<>("log", CPrimitives.DOUBLE)); - result.add(new Pair<>("logf", CPrimitives.FLOAT)); - result.add(new Pair<>("logl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/cos - result.add(new Pair<>("cos", CPrimitives.DOUBLE)); - result.add(new Pair<>("cosf", CPrimitives.FLOAT)); - result.add(new Pair<>("cosl", CPrimitives.LONGDOUBLE)); + @Override + public Collection getFunctionModels() { + final List result = new ArrayList<>(); - // https://en.cppreference.com/w/c/numeric/math/log1p - result.add(new Pair<>("log1p", CPrimitives.DOUBLE)); - result.add(new Pair<>("log1pf", CPrimitives.FLOAT)); - result.add(new Pair<>("log1pl", CPrimitives.LONGDOUBLE)); + // see 7.12.7.5 or http://en.cppreference.com/w/c/numeric/math/sqrt + result.add(new FunctionModel("sqrt", + (main, node, loc, name) -> handleSqrt(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("sqrtf", + (main, node, loc, name) -> handleSqrt(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("sqrtl", + (main, node, loc, name) -> handleSqrt(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + final Expression roundTowardsZero = SmtRoundingMode.RTZ.getBoogieIdentifierExpression(); + final Expression roundTowardsNegative = SmtRoundingMode.RTN.getBoogieIdentifierExpression(); + final Expression roundTowardsPositive = SmtRoundingMode.RTP.getBoogieIdentifierExpression(); + final Expression roundToNearest = SmtRoundingMode.RNA.getBoogieIdentifierExpression(); + + // see 7.12.9.8 or http://en.cppreference.com/w/c/numeric/math/trunc + result.add(new FunctionModel("trunc", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), roundTowardsZero))); + result.add(new FunctionModel("truncf", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), roundTowardsZero))); + result.add(new FunctionModel("truncl", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), roundTowardsZero))); + + // see 7.12.9.2 or http://en.cppreference.com/w/c/numeric/math/floor + result.add(new FunctionModel("floor", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), roundTowardsNegative))); + result.add(new FunctionModel("floorf", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), roundTowardsNegative))); + result.add(new FunctionModel("floorl", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), roundTowardsNegative))); + + // see 7.12.9.1 or http://en.cppreference.com/w/c/numeric/math/ceil + result.add(new FunctionModel("ceil", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), roundTowardsPositive))); + result.add(new FunctionModel("ceilf", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), roundTowardsPositive))); + result.add(new FunctionModel("ceill", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), roundTowardsPositive))); + + // see 7.12.9.6 or http://en.cppreference.com/w/c/numeric/math/round + result.add(new FunctionModel("round", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), roundToNearest))); + result.add(new FunctionModel("roundf", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), roundToNearest))); + result.add(new FunctionModel("roundl", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), roundToNearest))); + + // see 7.12.9.7 or http://en.cppreference.com/w/c/numeric/math/round + result.add(new FunctionModel("lround", (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, + name, new CPrimitive(CPrimitives.DOUBLE), new CPrimitive(CPrimitives.LONG), roundToNearest))); + result.add(new FunctionModel("lroundf", (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, + name, new CPrimitive(CPrimitives.FLOAT), new CPrimitive(CPrimitives.LONG), roundToNearest))); + result.add(new FunctionModel("lroundl", (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, + name, new CPrimitive(CPrimitives.LONGDOUBLE), new CPrimitive(CPrimitives.LONG), roundToNearest))); + result.add(new FunctionModel("llround", (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, + name, new CPrimitive(CPrimitives.DOUBLE), new CPrimitive(CPrimitives.LONGLONG), roundToNearest))); + result.add(new FunctionModel("llroundf", (main, node, loc, name) -> handleRoundWithIntConversion(main, node, + loc, name, new CPrimitive(CPrimitives.FLOAT), new CPrimitive(CPrimitives.LONGLONG), roundToNearest))); + result.add(new FunctionModel("llroundl", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), new CPrimitive(CPrimitives.LONGLONG), roundToNearest))); // https://en.cppreference.com/w/c/numeric/math/rint - result.add(new Pair<>("rint", CPrimitives.DOUBLE)); - result.add(new Pair<>("rintf", CPrimitives.FLOAT)); - result.add(new Pair<>("rintl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/atanh - result.add(new Pair<>("atanh", CPrimitives.DOUBLE)); - result.add(new Pair<>("atanhf", CPrimitives.FLOAT)); - result.add(new Pair<>("atanhl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/asin - result.add(new Pair<>("asin", CPrimitives.DOUBLE)); - result.add(new Pair<>("asinf", CPrimitives.FLOAT)); - result.add(new Pair<>("asinl", CPrimitives.LONGDOUBLE)); - - // https://en.cppreference.com/w/c/numeric/math/acos - result.add(new Pair<>("acos", CPrimitives.DOUBLE)); - result.add(new Pair<>("acosf", CPrimitives.FLOAT)); - result.add(new Pair<>("acosl", CPrimitives.LONGDOUBLE)); + result.add(new FunctionModel("rint", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("rintf", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("rintl", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("lrint", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), new CPrimitive(CPrimitives.LONG), + mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("lrintf", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), new CPrimitive(CPrimitives.LONG), + mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("lrintl", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), new CPrimitive(CPrimitives.LONG), + mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("llrint", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), new CPrimitive(CPrimitives.LONGLONG), + mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("llrintf", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), new CPrimitive(CPrimitives.LONGLONG), + mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("llrintl", + (main, node, loc, name) -> handleRoundWithIntConversion(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), new CPrimitive(CPrimitives.LONGLONG), + mExpressionTranslation.getCurrentRoundingMode()))); // https://en.cppreference.com/w/c/numeric/math/nearbyint - result.add(new Pair<>("nearbyint", CPrimitives.DOUBLE)); - result.add(new Pair<>("nearbyintf", CPrimitives.FLOAT)); - result.add(new Pair<>("nearbyintl", CPrimitives.LONGDOUBLE)); + result.add(new FunctionModel("nearbyint", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.DOUBLE), mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("nearbyintf", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.FLOAT), mExpressionTranslation.getCurrentRoundingMode()))); + result.add(new FunctionModel("nearbyintl", (main, node, loc, name) -> handleRound(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE), mExpressionTranslation.getCurrentRoundingMode()))); + + // see 7.12.7.2 or http://en.cppreference.com/w/c/numeric/math/fabs + result.add(new FunctionModel("fabs", + (main, node, loc, name) -> handleFabs(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("fabsf", + (main, node, loc, name) -> handleFabs(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("fabsl", + (main, node, loc, name) -> handleFabs(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.3.4 or http://en.cppreference.com/w/c/numeric/math/isnan + result.add(new FunctionModel("isnan", this::handleIsNan)); + result.add(new FunctionModel("__isnan", this::handleIsNan)); + + // see https://linux.die.net/man/3/isnanf (! NOT PART OF ANSI-C) + result.add(new FunctionModel("isnanf", this::handleIsNan)); + result.add(new FunctionModel("isnanl", this::handleIsNan)); + result.add(new FunctionModel("__isnanf", this::handleIsNan)); + result.add(new FunctionModel("__isnanl", this::handleIsNan)); + + // see 7.12.3.3 or http://en.cppreference.com/w/c/numeric/math/isinf + result.add(new FunctionModel("isinf", this::handleIsInf)); + result.add(new FunctionModel("__isinf", this::handleIsInf)); + result.add(new FunctionModel("__builtin_isinf_sign", this::handleIsInfSign)); + + // see https://linux.die.net/man/3/isinff (! NOT PART OF ANSI-C) + result.add(new FunctionModel("isinff", this::handleIsInf)); + result.add(new FunctionModel("isinfl", this::handleIsInf)); + result.add(new FunctionModel("__isinff", this::handleIsInf)); + result.add(new FunctionModel("__isinfl", this::handleIsInf)); + + // see 7.12.3.2 or http://en.cppreference.com/w/c/numeric/math/isfinite + result.add(new FunctionModel("isfinite", this::handleIsFinite)); + + // see https://linux.die.net/man/3/finite (! NOT PART OF ANSI-C) + result.add(new FunctionModel("finite", this::handleIsFinite)); + result.add(new FunctionModel("finitel", this::handleIsFinite)); + result.add(new FunctionModel("__finite", this::handleIsFinite)); + result.add(new FunctionModel("__finitef", this::handleIsFinite)); + result.add(new FunctionModel("__finitel", this::handleIsFinite)); + + // see 7.12.3.1 or http://en.cppreference.com/w/c/numeric/math/fpclassify + result.add(new FunctionModel("fpclassify", this::handleFpClassify)); + result.add(new FunctionModel("__fpclassify", this::handleFpClassify)); + result.add(new FunctionModel("__fpclassifyf", this::handleFpClassify)); + result.add(new FunctionModel("__fpclassifyl", this::handleFpClassify)); + + // see 7.12.3.5 or http://en.cppreference.com/w/c/numeric/math/isnormal + result.add(new FunctionModel("isnormal", this::handleIsNormal)); // http://en.cppreference.com/w/c/numeric/math/signbit - result.add(new Pair<>("signbit", CPrimitives.INT)); - result.add(new Pair<>("__signbit", CPrimitives.INT)); - result.add(new Pair<>("__signbitl", CPrimitives.INT)); - result.add(new Pair<>("__signbitf", CPrimitives.INT)); - - // http://en.cppreference.com/w/c/numeric/math/atan - result.add(new Pair<>("atan", CPrimitives.DOUBLE)); - result.add(new Pair<>("atanf", CPrimitives.FLOAT)); - result.add(new Pair<>("atanl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/atan2 - result.add(new Pair<>("atan2", CPrimitives.DOUBLE)); - result.add(new Pair<>("atan2f", CPrimitives.FLOAT)); - result.add(new Pair<>("atan2l", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/tan - result.add(new Pair<>("tan", CPrimitives.DOUBLE)); - result.add(new Pair<>("tanf", CPrimitives.FLOAT)); - result.add(new Pair<>("tanl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/cosh - result.add(new Pair<>("cosh", CPrimitives.DOUBLE)); - result.add(new Pair<>("coshf", CPrimitives.FLOAT)); - result.add(new Pair<>("coshl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/sinh - result.add(new Pair<>("sinh", CPrimitives.DOUBLE)); - result.add(new Pair<>("sinhf", CPrimitives.FLOAT)); - result.add(new Pair<>("sinhl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/acosh - result.add(new Pair<>("acosh", CPrimitives.DOUBLE)); - result.add(new Pair<>("acoshf", CPrimitives.FLOAT)); - result.add(new Pair<>("acoshl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/asinh - result.add(new Pair<>("asinh", CPrimitives.DOUBLE)); - result.add(new Pair<>("asinhf", CPrimitives.FLOAT)); - result.add(new Pair<>("asinhl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/log10 - result.add(new Pair<>("log10", CPrimitives.DOUBLE)); - result.add(new Pair<>("log10f", CPrimitives.FLOAT)); - result.add(new Pair<>("log10l", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/logb - result.add(new Pair<>("logb", CPrimitives.DOUBLE)); - result.add(new Pair<>("logbf", CPrimitives.FLOAT)); - result.add(new Pair<>("logbl", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/exp2 - result.add(new Pair<>("exp2", CPrimitives.DOUBLE)); - result.add(new Pair<>("exp2f", CPrimitives.FLOAT)); - result.add(new Pair<>("exp2l", CPrimitives.LONGDOUBLE)); - - // http://en.cppreference.com/w/c/numeric/math/log2 - result.add(new Pair<>("log2", CPrimitives.DOUBLE)); - result.add(new Pair<>("log2f", CPrimitives.FLOAT)); - result.add(new Pair<>("log2l", CPrimitives.LONGDOUBLE)); - - return result; - } - - private static List> getOverapproximatedBinaryFunctions() { - final List> result = new ArrayList<>(); - - // see 7.12.10.2 or http://en.cppreference.com/w/c/numeric/math/remainder - result.add(new Pair<>("remainder", CPrimitives.DOUBLE)); - result.add(new Pair<>("remainderf", CPrimitives.FLOAT)); - result.add(new Pair<>("remainderl", CPrimitives.LONGDOUBLE)); + result.add(new FunctionModel("signbit", this::handleSignbit)); + result.add(new FunctionModel("__signbit", this::handleSignbit)); + result.add(new FunctionModel("__signbitl", this::handleSignbit)); + result.add(new FunctionModel("__signbitf", this::handleSignbit)); // see 7.12.11.1 or http://en.cppreference.com/w/c/numeric/math/copysign - result.add(new Pair<>("copysign", CPrimitives.DOUBLE)); - result.add(new Pair<>("copysignf", CPrimitives.FLOAT)); - result.add(new Pair<>("copysignl", CPrimitives.LONGDOUBLE)); - - return result; - } - - @Override - public Collection getFunctionModels() { - final List result = new ArrayList<>(); - for (final var overapprox : getOverapproximatedUnaryFunctions()) { - result.add(new FunctionModel(overapprox.getFirst(), (main, node, loc, name) -> mHelper - .handleByOverapproximation(main, node, loc, name, 1, new CPrimitive(overapprox.getSecond())))); - } - for (final var overapprox : getOverapproximatedBinaryFunctions()) { - result.add(new FunctionModel(overapprox.getFirst(), (main, node, loc, name) -> mHelper - .handleByOverapproximation(main, node, loc, name, 2, new CPrimitive(overapprox.getSecond())))); - } - for (final String unary : UNARY_FUNCTIONS) { - result.add(new FunctionModel(unary, this::handleUnaryFloatFunction)); - } - for (final String binary : BINARY_FUNCTIONS) { - result.add(new FunctionModel(binary, this::handleBinaryFloatFunction)); - } + // if second is negative, return -abs(first), else return abs(first) + result.add(new FunctionModel("copysign", + (main, node, loc, name) -> handleCopysign(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("copysignf", + (main, node, loc, name) -> handleCopysign(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("copysignl", (main, node, loc, name) -> handleCopysign(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.4.5 or https://en.cppreference.com/w/c/numeric/math/cos + result.add(new FunctionModel("cos", + (main, node, loc, name) -> handleCos(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("cosf", + (main, node, loc, name) -> handleCos(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("cosl", + (main, node, loc, name) -> handleCos(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.4.6 or https://en.cppreference.com/w/c/numeric/math/sin + result.add(new FunctionModel("sin", + (main, node, loc, name) -> handleSin(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("sinf", + (main, node, loc, name) -> handleSin(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("sinl", + (main, node, loc, name) -> handleSin(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.6.1 or https://en.cppreference.com/w/c/numeric/math/exp + result.add(new FunctionModel("exp", + (main, node, loc, name) -> handleExp(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("expf", + (main, node, loc, name) -> handleExp(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("expl", + (main, node, loc, name) -> handleExp(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.6.3 or https://en.cppreference.com/w/c/numeric/math/expm1 + result.add(new FunctionModel("expm1", + (main, node, loc, name) -> handleExpm1(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("expm1f", + (main, node, loc, name) -> handleExpm1(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("expm1l", + (main, node, loc, name) -> handleExpm1(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.8.1 or https://en.cppreference.com/w/c/numeric/math/erf + result.add(new FunctionModel("erf", + (main, node, loc, name) -> handleErf(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("erff", + (main, node, loc, name) -> handleErf(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("erfl", + (main, node, loc, name) -> handleErf(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.5.6 or https://en.cppreference.com/w/c/numeric/math/tanh + result.add(new FunctionModel("tanh", + (main, node, loc, name) -> handleTanh(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("tanhf", + (main, node, loc, name) -> handleTanh(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("tanhl", + (main, node, loc, name) -> handleTanh(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.6.7 or https://en.cppreference.com/w/c/numeric/math/log + result.add(new FunctionModel("log", + (main, node, loc, name) -> handleLog(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("logf", + (main, node, loc, name) -> handleLog(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("logl", + (main, node, loc, name) -> handleLog(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.12.2 or http://en.cppreference.com/w/c/numeric/math/fmax + result.add(new FunctionModel("fmax", + (main, node, loc, name) -> handleFmax(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("fmaxf", + (main, node, loc, name) -> handleFmax(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("fmaxl", + (main, node, loc, name) -> handleFmax(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.12.3 or http://en.cppreference.com/w/c/numeric/math/fmin + result.add(new FunctionModel("fmin", + (main, node, loc, name) -> handleFmin(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("fminf", + (main, node, loc, name) -> handleFmin(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("fminl", + (main, node, loc, name) -> handleFmin(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + + // see 7.12.12.1 or https://en.cppreference.com/w/c/numeric/math/fdim + result.add(new FunctionModel("fdim", + (main, node, loc, name) -> handleFdim(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("fdimf", + (main, node, loc, name) -> handleFdim(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("fdiml", + (main, node, loc, name) -> handleFdim(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); /** various float builtins **/ - result.add(new FunctionModel("nan", (main, node, loc, name) -> handleNaNOrInfinity(loc, name))); - result.add(new FunctionModel("nanf", (main, node, loc, name) -> handleNaNOrInfinity(loc, name))); - result.add(new FunctionModel("nanl", (main, node, loc, name) -> handleNaNOrInfinity(loc, name))); - result.add(new FunctionModel("__builtin_nan", (main, node, loc, name) -> handleNaNOrInfinity(loc, "nan"))); - result.add(new FunctionModel("__builtin_nanf", (main, node, loc, name) -> handleNaNOrInfinity(loc, "nanf"))); - result.add(new FunctionModel("__builtin_nanl", (main, node, loc, name) -> handleNaNOrInfinity(loc, "nanl"))); - result.add(new FunctionModel("__builtin_inff", (main, node, loc, name) -> handleNaNOrInfinity(loc, "inff"))); - result.add(new FunctionModel("__builtin_huge_val", (main, node, loc, name) -> handleNaNOrInfinity(loc, "inf"))); - result.add( - new FunctionModel("__builtin_huge_valf", (main, node, loc, name) -> handleNaNOrInfinity(loc, "inff"))); + result.add(new FunctionModel("nan", + (main, node, loc, name) -> handleNan(loc, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("nanf", + (main, node, loc, name) -> handleNan(loc, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("nanl", + (main, node, loc, name) -> handleNan(loc, new CPrimitive(CPrimitives.LONGDOUBLE)))); + result.add(new FunctionModel("__builtin_nan", + (main, node, loc, name) -> handleNan(loc, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("__builtin_nanf", + (main, node, loc, name) -> handleNan(loc, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("__builtin_nanl", + (main, node, loc, name) -> handleNan(loc, new CPrimitive(CPrimitives.LONGDOUBLE)))); + result.add(new FunctionModel("__builtin_inff", (main, node, loc, name) -> handleInf(loc))); + result.add(new FunctionModel("__builtin_huge_val", (main, node, loc, name) -> handleInf(loc))); + result.add(new FunctionModel("__builtin_huge_valf", (main, node, loc, name) -> handleInf(loc))); result.add(new FunctionModel("__builtin_isgreater", this::handleIsGreater)); result.add(new FunctionModel("__builtin_isgreaterequal", this::handleIsGreaterEqual)); result.add(new FunctionModel("__builtin_isless", this::handleIsLess)); result.add(new FunctionModel("__builtin_islessequal", this::handleIsLessEqual)); result.add(new FunctionModel("__builtin_isunordered", this::handleIsUnordered)); result.add(new FunctionModel("__builtin_islessgreater", this::handleIsLessGreater)); - result.add(new FunctionModel("__builtin_isnan", - (main, node, loc, name) -> handleUnaryFloatFunction(main, node, loc, "isnan"))); + result.add(new FunctionModel("__builtin_isnan", this::handleIsNan)); result.add(new FunctionModel("isgreater", this::handleIsGreater)); result.add(new FunctionModel("isgreaterequal", this::handleIsGreaterEqual)); @@ -340,6 +410,31 @@ public Collection getFunctionModels() { result.add(new FunctionModel("isunordered", this::handleIsUnordered)); result.add(new FunctionModel("islessgreater", this::handleIsLessGreater)); + // see 7.12.10.2 or http://en.cppreference.com/w/c/numeric/math/remainder + result.add(new FunctionModel("remainder", + (main, node, loc, name) -> handleRemainder(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("remainderf", + (main, node, loc, name) -> handleRemainder(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("remainderl", (main, node, loc, name) -> handleRemainder(main, node, loc, name, + new CPrimitive(CPrimitives.LONGDOUBLE)))); + + /** + * 7.12.10.1 The fmod functions + * + * The fmod functions compute the floating-point remainder of x/y. + * + * The fmod functions return the value x − ny, for some integer n such that, if y is nonzero, the result has the + * same sign as x and magnitude less than the magnitude of y. If y is zero, whether a domain error occurs or the + * fmod functions return zero is implementation- defined. + */ + // fmod guarantees that the return value is the same sign as the first argument (x) + result.add(new FunctionModel("fmod", + (main, node, loc, name) -> handleFmod(main, node, loc, name, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new FunctionModel("fmodf", + (main, node, loc, name) -> handleFmod(main, node, loc, name, new CPrimitive(CPrimitives.FLOAT)))); + result.add(new FunctionModel("fmodl", + (main, node, loc, name) -> handleFmod(main, node, loc, name, new CPrimitive(CPrimitives.LONGDOUBLE)))); + return result; } @@ -348,53 +443,27 @@ public Collection getUnsupportedFunctions() { return Arrays.asList(UNSUPPORTED_FLOAT_OPERATIONS); } - private Result handleNaNOrInfinity(final ILocation loc, final String methodName) { - return mExpressionTranslation.createNanOrInfinity(loc, methodName); + private ExpressionResult handleNan(final ILocation loc, final CPrimitive type) { + return new ExpressionResult(new RValue(mFloatHandler.createNan(loc, type), type)); } - private Result handleUnaryFloatFunction(final IDispatcher main, final IASTFunctionCallExpression node, - final ILocation loc, final String name) { - final FloatFunction floatFunction = FloatFunction.decode(name); - final ExpressionResult arg = handleFloatArguments(main, node, loc, name, 1, floatFunction).get(0); - final RValue rvalue = - mExpressionTranslation.constructOtherUnaryFloatOperation(loc, floatFunction, (RValue) arg.getLrValue()); - return new ExpressionResultBuilder().addAllExceptLrValue(arg).setLrValue(rvalue).build(); - } - - private Result handleBinaryFloatFunction(final IDispatcher main, final IASTFunctionCallExpression node, - final ILocation loc, final String name) { - final FloatFunction floatFunction = FloatFunction.decode(name); - final List args = handleFloatArguments(main, node, loc, name, 2, floatFunction); - final RValue rvalue = mExpressionTranslation.constructOtherBinaryFloatOperation(loc, floatFunction, - (RValue) args.get(0).getLrValue(), (RValue) args.get(1).getLrValue()); - return new ExpressionResultBuilder().addAllExceptLrValue(args).setLrValue(rvalue).build(); + private ExpressionResult handleInf(final ILocation loc) { + final CPrimitive type = new CPrimitive(CPrimitives.DOUBLE); + return new ExpressionResult(new RValue(mFloatHandler.createInfinity(loc, type), type)); } private List handleFloatArguments(final IDispatcher main, final IASTFunctionCallExpression node, - final ILocation loc, final String name, final int numberOfArgs, final FloatFunction floatFunction) { + final ILocation loc, final String name, final int numberOfArgs, final CPrimitive type) { final IASTInitializerClause[] arguments = node.getArguments(); mHelper.checkArguments(loc, numberOfArgs, name, arguments); - if (floatFunction == null) { - throw new IllegalArgumentException( - "Ultimate declared float handling for " + name + ", but is not known float function"); - } final List rtr = new ArrayList<>(); for (final IASTInitializerClause argument : arguments) { final ExpressionResult decayedArgument = mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, argument); final ExpressionResult convertedArgument = - mExprResultTransformer.convertIfNecessary(loc, decayedArgument, floatFunction.getType()); + mExprResultTransformer.convertIfNecessary(loc, decayedArgument, type); rtr.add(convertedArgument); } - - final CPrimitive typeDeterminedByName = floatFunction.getType(); - if (typeDeterminedByName != null) { - final List newRtr = new ArrayList<>(); - for (final ExpressionResult arg : rtr) { - newRtr.add(mExprResultTransformer.convertIfNecessary(loc, arg, typeDeterminedByName)); - } - return newRtr; - } return rtr; } @@ -471,19 +540,14 @@ private Result handleIsUnordered(final IDispatcher main, final IASTFunctionCallE mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); final ExpressionResult rightRvaluedResult = mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[1]); - final ExpressionResult nanLResult = - mExpressionTranslation.createNan(loc, (CPrimitive) leftRvaluedResult.getLrValue().getCType()); - final ExpressionResult nanRResult = - mExpressionTranslation.createNan(loc, (CPrimitive) rightRvaluedResult.getLrValue().getCType()); - final Expression leftExpr = ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, - leftRvaluedResult.getLrValue().getValue(), nanLResult.getLrValue().getValue()); - final Expression rightExpr = ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, - rightRvaluedResult.getLrValue().getValue(), nanRResult.getLrValue().getValue()); + final Expression leftExpr = mFloatHandler.isNan(loc, leftRvaluedResult.getLrValue().getValue(), + (CPrimitive) leftRvaluedResult.getCType()); + final Expression rightExpr = mFloatHandler.isNan(loc, rightRvaluedResult.getLrValue().getValue(), + (CPrimitive) rightRvaluedResult.getCType()); final Expression expr = ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, leftExpr, rightExpr); final LRValue lrVal = new RValue(expr, new CPrimitive(CPrimitives.INT), true); final ExpressionResult rtr = new ExpressionResultBuilder() - .addAllExceptLrValue(leftRvaluedResult, rightRvaluedResult, nanLResult, nanRResult).setLrValue(lrVal) - .build(); + .addAllExceptLrValue(leftRvaluedResult, rightRvaluedResult).setLrValue(lrVal).build(); assert CTranslationUtil.isAuxVarMapComplete(mNameHandler, rtr.getDeclarations(), rtr.getAuxVars()); return rtr; } @@ -532,6 +596,464 @@ private Result handleIsLessGreater(final IDispatcher main, final IASTFunctionCal return rtr; } + private ExpressionResult handleSqrt(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + return new ExpressionResultBuilder() + .addAllExceptLrValue(argumentResult).setLrValue(new RValue(mExpressionTranslation + .getFloatingPointHandler().sqrt(loc, argumentResult.getLrValue().getValue(), type), type)) + .build(); + } + + private ExpressionResult handleRound(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type, final Expression roundingMode) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue( + mFloatHandler.roundToIntegral(loc, argumentResult.getLrValue().getValue(), type, roundingMode), + type)) + .build(); + } + + private ExpressionResult handleRoundWithIntConversion(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type, final CPrimitive resultType, + final Expression roundingMode) { + return mExpressionTranslation.convertFloatToInt(loc, handleRound(main, node, loc, name, type, roundingMode), + resultType); + } + + private ExpressionResult handleFabs(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + return new ExpressionResultBuilder() + .addAllExceptLrValue(argumentResult).setLrValue(new RValue(mExpressionTranslation + .getFloatingPointHandler().abs(loc, argumentResult.getLrValue().getValue(), type), type)) + .build(); + } + + private ExpressionResult handleIsNan(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue(mFloatHandler.isNan(loc, argumentResult.getLrValue().getValue(), + (CPrimitive) argumentResult.getCType()), new CPrimitive(CPrimitives.INT), true)) + .build(); + } + + private ExpressionResult handleIsInf(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue(mFloatHandler.isInfinite(loc, argumentResult.getLrValue().getValue(), + (CPrimitive) argumentResult.getCType()), new CPrimitive(CPrimitives.INT), true)) + .build(); + } + + private ExpressionResult handleIsInfSign(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + final CPrimitive intType = new CPrimitive(CPrimitives.INT); + final Expression argument = argumentResult.getLrValue().getValue(); + final CPrimitive type = (CPrimitive) argumentResult.getCType(); + final Expression isInfinite = mFloatHandler.isInfinite(loc, argument, type); + final Expression isPositive = mFloatHandler.isPositive(loc, argument, type); + final Expression resultExpr = ExpressionFactory.constructIfThenElseExpression(loc, isInfinite, + ExpressionFactory.constructIfThenElseExpression(loc, isPositive, + mExpressionTranslation.constructLiteralForIntegerType(loc, intType, BigInteger.ONE), + mExpressionTranslation.constructLiteralForIntegerType(loc, intType, BigInteger.ONE.negate())), + mExpressionTranslation.constructLiteralForIntegerType(loc, intType, BigInteger.ZERO)); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue(resultExpr, new CPrimitive(CPrimitives.INT))).build(); + } + + private ExpressionResult handleIsFinite(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + final Expression argument = argumentResult.getLrValue().getValue(); + final CPrimitive type = (CPrimitive) argumentResult.getCType(); + final Expression resultExpr = ExpressionFactory.or(loc, mFloatHandler.isNormal(loc, argument, type), + mFloatHandler.isSubnormal(loc, argument, type), mFloatHandler.isZero(loc, argument, type)); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue(resultExpr, new CPrimitive(CPrimitives.INT), true)).build(); + } + + private ExpressionResult handleFpClassify(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + final Expression argument = argumentResult.getLrValue().getValue(); + final CPrimitive type = (CPrimitive) argumentResult.getCType(); + final Expression isInfinite = mFloatHandler.isInfinite(loc, argument, type); + final Expression isNan = mFloatHandler.isNan(loc, argument, type); + final Expression isNormal = mFloatHandler.isNormal(loc, argument, type); + final Expression isSubnormal = mFloatHandler.isSubnormal(loc, argument, type); + // if (isinf(x)) return FP_INFINITE; + // else if (isnan(x)) return FP_NAN; + // else if (isnormal(x)) return FP_NORMAL; + // else if (issubnormal(x)) return FP_SUBNORMAL; + // else return FP_ZERO; + final Expression resultExpr = ExpressionFactory.constructIfThenElseExpression(loc, isInfinite, + Classification.INFINITE.asExpression(loc, mExpressionTranslation), + ExpressionFactory.constructIfThenElseExpression(loc, isNan, + Classification.NAN.asExpression(loc, mExpressionTranslation), + ExpressionFactory.constructIfThenElseExpression(loc, isNormal, + Classification.NORMAL.asExpression(loc, mExpressionTranslation), + ExpressionFactory.constructIfThenElseExpression(loc, isSubnormal, + Classification.SUBNORMAL.asExpression(loc, mExpressionTranslation), + Classification.ZERO.asExpression(loc, mExpressionTranslation))))); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue(resultExpr, new CPrimitive(CPrimitives.INT))).build(); + } + + private ExpressionResult handleIsNormal(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + return new ExpressionResultBuilder().addAllExceptLrValue(argumentResult) + .setLrValue(new RValue(mFloatHandler.isNormal(loc, argumentResult.getLrValue().getValue(), + (CPrimitive) argumentResult.getCType()), new CPrimitive(CPrimitives.INT), true)) + .build(); + } + + private ExpressionResult handleCos(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + final Expression nan = mFloatHandler.createNan(loc, type); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + final Expression one = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE); + final Expression minusOne = + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE.negate()); + final Expression greaterMinusOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_greaterEqual, auxVar.getExp(), type, minusOne, type); + final Expression smallerOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_lessEqual, auxVar.getExp(), type, one, type); + // x = 0 ==> cos(x) = 1 + // x = -oo ==> cos(x) = NaN + // x = oo ==> cos(x) = NaN + // -1 <= cos(x) <= 1 + return overapproximateUnaryFloatFunction(loc, name, argumentResult, auxVar, nan, nan, one, + List.of(greaterMinusOne, smallerOne)); + } + + private ExpressionResult handleSin(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + final Expression nan = mFloatHandler.createNan(loc, type); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + final Expression one = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE); + final Expression minusOne = + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE.negate()); + final Expression greaterMinusOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_greaterEqual, auxVar.getExp(), type, minusOne, type); + final Expression smallerOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_lessEqual, auxVar.getExp(), type, one, type); + // x = 0 ==> sin(x) = 0 + // x = -oo ==> sin(x) = NaN + // x = oo ==> sin(x) = NaN + // -1 <= sin(x) <= 1 + return overapproximateUnaryFloatFunction(loc, name, argumentResult, auxVar, nan, nan, + argumentResult.getLrValue().getValue(), List.of(greaterMinusOne, smallerOne)); + } + + private ExpressionResult handleExp(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + final Expression argument = argumentResult.getLrValue().getValue(); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + final Expression one = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE); + final Expression positive = mFloatHandler.isPositive(loc, auxVar.getExp(), type); + final Expression smallerOneForNegativeValues = ExpressionFactory.or(loc, + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_greaterEqual, + argument, type, + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ZERO), type), + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessThan, + auxVar.getExp(), type, one, type)); + final Expression overLinear = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_greaterEqual, auxVar.getExp(), type, mExpressionTranslation + .constructArithmeticExpression(loc, IASTBinaryExpression.op_plus, argument, type, one, type), + type); + // x = 0 ==> exp(x) = 1 + // x = -oo ==> exp(x) = +0 + // x = oo ==> exp(x) = oo + // exp(x) >= 0 + // x < 0 ==> exp(x) < 1 + // exp(x) >= x+1 + return overapproximateUnaryFloatFunction(loc, name, argumentResult, auxVar, + mFloatHandler.createPlusZero(loc, type), argument, one, + List.of(positive, smallerOneForNegativeValues, overLinear)); + } + + private ExpressionResult handleExpm1(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult expResult = handleExp(main, node, loc, name, type); + // expm1(x) = exp(x) - 1 + final Expression resMinusOne = mExpressionTranslation.constructArithmeticExpression(loc, + IASTBinaryExpression.op_minus, expResult.getLrValue().getValue(), type, + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE), type); + return new ExpressionResultBuilder(expResult).resetLrValue(new RValue(resMinusOne, type)).build(); + } + + private ExpressionResult handleErf(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + final Expression one = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE); + final Expression minusOne = + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE.negate()); + final Expression greaterMinusOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_greaterEqual, auxVar.getExp(), type, minusOne, type); + final Expression smallerOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_lessEqual, auxVar.getExp(), type, one, type); + // x = 0 ==> erf(x) = 0 + // x = -oo ==> erf(x) = -1 + // x = oo ==> erf(x) = 1 + // -1 <= erf(x) <= 1 + return overapproximateUnaryFloatFunction(loc, name, argumentResult, auxVar, minusOne, one, + argumentResult.getLrValue().getValue(), List.of(greaterMinusOne, smallerOne)); + } + + private ExpressionResult handleTanh(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + final Expression one = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE); + final Expression minusOne = + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE.negate()); + final Expression greaterMinusOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_greaterEqual, auxVar.getExp(), type, minusOne, type); + final Expression smallerOne = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_lessEqual, auxVar.getExp(), type, one, type); + // x = 0 ==> tanh(x) = 0 + // x = -oo ==> tanh(x) = -1 + // x = oo ==> tanh(x) = 1 + // -1 <= tanh(x) <= 1 + return overapproximateUnaryFloatFunction(loc, name, argumentResult, auxVar, minusOne, one, + argumentResult.getLrValue().getValue(), List.of(greaterMinusOne, smallerOne)); + } + + private ExpressionResult handleLog(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final ExpressionResult argumentResult = handleFloatArguments(main, node, loc, name, 1, type).getFirst(); + final Expression argument = argumentResult.getLrValue().getValue(); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + final Expression one = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ONE); + final Expression nanForNegative = ExpressionFactory.or(loc, mFloatHandler.isPositive(loc, argument, type), + mFloatHandler.isNan(loc, auxVar.getExp(), type)); + final Expression zeroForOne = ExpressionFactory.or(loc, + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_notequals, + argument, type, one, type), + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_equals, + auxVar.getExp(), type, mFloatHandler.createPlusZero(loc, type), type)); + final Expression positiveForGreaterOne = ExpressionFactory.or(loc, + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessEqual, + argument, type, one, type), + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_greaterThan, + auxVar.getExp(), type, + mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ZERO), type)); + final Expression sublinear = ExpressionFactory.or(loc, + ExpressionFactory.not(loc, mFloatHandler.isPositive(loc, argument, type)), + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessEqual, + auxVar.getExp(), type, mExpressionTranslation.constructArithmeticExpression(loc, + IASTBinaryExpression.op_minus, argument, type, one, type), + type)); + // x = 0 ==> log(x) = -oo + // x = -oo ==> log(x) = NaN + // x = oo ==> log(x) = oo + // x < 0 ==> log(x) = NaN + // x = 1 ==> log(x) = 0 + // x > 1 ==> log(x) > 0 + // x >= 0 ==> log(x) < x-1 + return overapproximateUnaryFloatFunction(loc, name, argumentResult, auxVar, mFloatHandler.createNan(loc, type), + argument, mFloatHandler.createMinusInfinity(loc, type), + List.of(nanForNegative, zeroForOne, positiveForGreaterOne, sublinear)); + } + + private ExpressionResult overapproximateUnaryFloatFunction(final ILocation loc, final String functionName, + final ExpressionResult argumentResult, final AuxVarInfo auxvarinfo, final Expression negInfValue, + final Expression posInfValue, final Expression zeroValue, + final List assumptionsForOverapproximation) { + final ExpressionResultBuilder builder = new ExpressionResultBuilder().addAllExceptLrValue(argumentResult); + builder.addAuxVarWithDeclaration(auxvarinfo); + final IdentifierExpression auxvar = auxvarinfo.getExp(); + final CPrimitive resultType = (CPrimitive) argumentResult.getCType(); + final Expression argument = argumentResult.getLrValue().getValue(); + builder.setLrValue(new RValue(auxvar, resultType)); + final VariableLHS auxvarLhs = auxvarinfo.getLhs(); + final HavocStatement havoc = new HavocStatement(loc, new VariableLHS[] { auxvarLhs }); + final AssumeStatement assume = + new AssumeStatement(loc, ExpressionFactory.and(loc, assumptionsForOverapproximation)); + final Statement overapproxSt = new AtomicStatement(loc, new Statement[] { havoc, assume }); + new OverapproxVariable(functionName, loc).annotate(overapproxSt); + final Expression isZero = mFloatHandler.isZero(loc, argument, resultType); + final Expression isNan = mFloatHandler.isNan(loc, argument, resultType); + final Expression isInfinite = mFloatHandler.isInfinite(loc, argument, resultType); + final Expression isPositive = mFloatHandler.isPositive(loc, argument, resultType); + final Statement resultStatement = + StatementFactory.constructIfStatement(loc, isZero, + List.of(StatementFactory.constructSingleAssignmentStatement(loc, auxvarLhs, zeroValue)), + List.of(StatementFactory.constructIfStatement(loc, isNan, + List.of(StatementFactory.constructSingleAssignmentStatement(loc, auxvarLhs, argument)), + List.of(StatementFactory.constructIfStatement( + loc, isInfinite, List + .of(StatementFactory + .constructSingleAssignmentStatement(loc, auxvarLhs, + ExpressionFactory.constructIfThenElseExpression(loc, + isPositive, posInfValue, negInfValue))), + List.of(overapproxSt)))))); + return builder.addStatement(resultStatement).build(); + } + + // NaN arguments are treated as missing data: if one argument is a NaN and the other numeric, then the numeric value + // is choosen. + private ExpressionResult handleFmin(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final List arguments = handleFloatArguments(main, node, loc, name, 2, type); + return new ExpressionResultBuilder().addAllExceptLrValue(arguments).setLrValue(new RValue(mFloatHandler.min(loc, + arguments.get(0).getLrValue().getValue(), arguments.get(1).getLrValue().getValue(), type), type)) + .build(); + } + + // NaN arguments are treated as missing data: if one argument is a NaN and the other numeric, then the numeric value + // is choosen. + private ExpressionResult handleFmax(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final List arguments = handleFloatArguments(main, node, loc, name, 2, type); + return new ExpressionResultBuilder().addAllExceptLrValue(arguments).setLrValue(new RValue(mFloatHandler.max(loc, + arguments.get(0).getLrValue().getValue(), arguments.get(1).getLrValue().getValue(), type), type)) + .build(); + } + + private ExpressionResult handleFdim(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final List arguments = handleFloatArguments(main, node, loc, name, 2, type); + final Expression first = arguments.get(0).getLrValue().getValue(); + final Expression second = arguments.get(1).getLrValue().getValue(); + final Expression comparison = mExpressionTranslation.constructBinaryComparisonExpression(loc, + IASTBinaryExpression.op_greaterThan, first, type, second, type); + final Expression subtraction = mExpressionTranslation.constructArithmeticExpression(loc, + IASTBinaryExpression.op_minus, first, type, second, type); + final Expression zero = mExpressionTranslation.constructLiteralForFloatingType(loc, type, BigDecimal.ZERO); + final Expression resultExprFdim = + ExpressionFactory.constructIfThenElseExpression(loc, comparison, subtraction, zero); + final Expression secondNaNExpr = ExpressionFactory.constructIfThenElseExpression(loc, + mFloatHandler.isNan(loc, second, type), second, resultExprFdim); + final Expression firstNaNExpr = ExpressionFactory.constructIfThenElseExpression(loc, + mFloatHandler.isNan(loc, first, type), first, secondNaNExpr); + return new ExpressionResultBuilder().addAllExceptLrValue(arguments).setLrValue(new RValue(firstNaNExpr, type)) + .build(); + } + + private ExpressionResult handleSignbit(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name) { + final IASTInitializerClause[] arguments = node.getArguments(); + mHelper.checkArguments(loc, 1, name, arguments); + final ExpressionResult argumentResult = + mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]); + final CPrimitive intType = new CPrimitive(CPrimitives.INT); + final Expression argument = argumentResult.getLrValue().getValue(); + final CPrimitive type = (CPrimitive) argumentResult.getCType(); + final ExpressionResultBuilder builder = new ExpressionResultBuilder().addAllExceptLrValue(argumentResult); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, intType, AUXVAR.RETURNED); + builder.addAuxVarWithDeclaration(auxVar); + final Statement nondet = new HavocStatement(loc, new VariableLHS[] { auxVar.getLhs() }); + // TODO: Handle negative NaN correctly, only overapproximated until then + // signbit(x) := isNegative(x) ? 1 : 0; + new OverapproxVariable("sign of NaN", loc).annotate(nondet); + final Expression zero = mExpressionTranslation.constructLiteralForIntegerType(loc, intType, BigInteger.ZERO); + builder.addStatement(StatementFactory.constructIfStatement(loc, mFloatHandler.isNan(loc, argument, type), + List.of(nondet), + List.of(StatementFactory.constructIfStatement(loc, mFloatHandler.isPositive(loc, argument, type), + List.of(StatementFactory.constructSingleAssignmentStatement(loc, auxVar.getLhs(), zero)), + List.of(new AssumeStatement(loc, ExpressionFactory.newBinaryExpression(loc, Operator.COMPNEQ, + auxVar.getExp(), zero))))))); + return builder.setLrValue(new RValue(auxVar.getExp(), intType)).build(); + } + + private ExpressionResult handleCopysign(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final List arguments = handleFloatArguments(main, node, loc, name, 2, type); + final Expression first = arguments.get(0).getLrValue().getValue(); + final Expression second = arguments.get(1).getLrValue().getValue(); + return new ExpressionResultBuilder().addAllExceptLrValue(arguments) + .addAllIncludingLrValue(handleCopysign(first, second, loc, type)).build(); + } + + private ExpressionResult handleCopysign(final Expression first, final Expression second, final ILocation loc, + final CPrimitive type) { + final ExpressionResultBuilder builder = new ExpressionResultBuilder(); + final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, type, AUXVAR.RETURNED); + builder.addAuxVarWithDeclaration(auxVar); + final Expression abs = mFloatHandler.abs(loc, first, type); + final Statement nondet = new AssumeStatement(loc, + ExpressionFactory.or(loc, + mExpressionTranslation.constructBinaryComparisonExpression(loc, IASTBinaryExpression.op_equals, + auxVar.getExp(), type, first, type), + mExpressionTranslation.constructBinaryComparisonExpression( + loc, IASTBinaryExpression.op_equals, auxVar.getExp(), type, mExpressionTranslation + .constructUnaryExpression(loc, IASTUnaryExpression.op_minus, first, type), + type))); + // TODO: Overapproximate if second is NaN + new OverapproxVariable("sign of NaN", loc).annotate(nondet); + builder.addStatement(StatementFactory.constructIfStatement(loc, mFloatHandler.isNan(loc, first, type), + // If the first argument is NaN, just return it. This works for now, as we cannot handle negative NaN + // anyway. + // TODO: If we can handle negative NaN, this has to be changed! + List.of(StatementFactory.constructSingleAssignmentStatement(loc, auxVar.getLhs(), first)), + List.of(StatementFactory.constructIfStatement(loc, mFloatHandler.isNan(loc, second, type), + List.of(nondet), + List.of(StatementFactory.constructSingleAssignmentStatement(loc, auxVar.getLhs(), + ExpressionFactory.constructIfThenElseExpression(loc, + mFloatHandler.isPositive(loc, second, type), abs, + mExpressionTranslation.constructUnaryExpression(loc, + IASTUnaryExpression.op_minus, abs, type)))))))); + return builder.setLrValue(new RValue(auxVar.getExp(), type)).build(); + } + + private ExpressionResult handleRemainder(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final List arguments = handleFloatArguments(main, node, loc, name, 2, type); + final Expression first = arguments.get(0).getLrValue().getValue(); + final Expression second = arguments.get(1).getLrValue().getValue(); + return new ExpressionResultBuilder().addAllExceptLrValue(arguments) + .setLrValue(new RValue(mFloatHandler.remainder(loc, first, second, type), type)).build(); + } + + private ExpressionResult handleFmod(final IDispatcher main, final IASTFunctionCallExpression node, + final ILocation loc, final String name, final CPrimitive type) { + final List arguments = handleFloatArguments(main, node, loc, name, 2, type); + final Expression first = arguments.get(0).getLrValue().getValue(); + final Expression second = arguments.get(1).getLrValue().getValue(); + // fmod(x, y) { + // r = remainder(fabs(x), fabs(y)); + // pr = isPositive(r) ? r : r + fabs(y); + // return copysign(pr, x) + // } + final Expression remainder = mFloatHandler.remainder(loc, mFloatHandler.abs(loc, first, type), + mFloatHandler.abs(loc, second, type), type); + final Expression positiveRemainder = ExpressionFactory.constructIfThenElseExpression(loc, + mFloatHandler.isPositive(loc, remainder, type), remainder, + mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_plus, remainder, type, + mFloatHandler.abs(loc, second, type), type)); + return new ExpressionResultBuilder().addAllExceptLrValue(arguments) + .addAllIncludingLrValue(handleCopysign(positiveRemainder, first, loc, type)).build(); + } + @Override public Collection getTypeModels() { return List.of( @@ -541,19 +1063,16 @@ public Collection getTypeModels() { new TypeModel("double_t", new CPrimitive(CPrimitives.DOUBLE))); } - private ConstantModel modelNumberClassificationMacro(final String name) { - return new ConstantModel(name, - loc -> new ExpressionResult(mExpressionTranslation.handleNumberClassificationMacro(loc, name))); - } - @Override public Collection getConstantModels() { - return List.of(new ConstantModel("NAN", loc -> mExpressionTranslation.createNanOrInfinity(loc, "NAN")), - new ConstantModel("INFINITY", loc -> mExpressionTranslation.createNanOrInfinity(loc, "INFINITY")), - new ConstantModel("inf", loc -> mExpressionTranslation.createNanOrInfinity(loc, "inf")), - // Check if id is number classification macro according to 7.12.6 of C11. - modelNumberClassificationMacro("FP_NAN"), modelNumberClassificationMacro("FP_INFINITE"), - modelNumberClassificationMacro("FP_ZERO"), modelNumberClassificationMacro("FP_SUBNORMAL"), - modelNumberClassificationMacro("FP_NORMAL")); + final List result = new ArrayList<>(); + result.add(new ConstantModel("NAN", loc -> handleNan(loc, new CPrimitive(CPrimitives.DOUBLE)))); + result.add(new ConstantModel("INFINITY", loc -> handleInf(loc))); + result.add(new ConstantModel("inf", loc -> handleInf(loc))); + for (final Classification c : Classification.values()) { + result.add(new ConstantModel(c.getName(), loc -> new ExpressionResult( + new RValue(c.asExpression(loc, mExpressionTranslation), new CPrimitive(CPrimitives.INT))))); + } + return result; } }