diff --git a/regression/cbmc-library/cos-01/main.c b/regression/cbmc-library/cos-01/main.c index 498163411c3..1412cca8db2 100644 --- a/regression/cbmc-library/cos-01/main.c +++ b/regression/cbmc-library/cos-01/main.c @@ -1,9 +1,89 @@ +#define _USE_MATH_DEFINES #include #include int main() { - cos(); - assert(0); + // Test special values - these should be precise + double c; + + // cos(0) should be exactly 1 + c = cos(0.0); + assert(c >= 0.999999999 && c <= 1.0); + + // cos(π/2) should be approximately 0 + c = cos(M_PI / 2.0); + assert(c >= -1e-10 && c <= 1e-10); + + // cos(-π/2) should be approximately 0 + c = cos(-M_PI / 2.0); + assert(c >= -1e-10 && c <= 1e-10); + + // cos(π) should be approximately -1 + c = cos(M_PI); + assert(c >= -1.0 && c <= -0.999999999); + + // cos(-π) should be approximately -1 (cos is even) + c = cos(-M_PI); + assert(c >= -1.0 && c <= -0.999999999); + + // cos(2π) should be approximately 1 + c = cos(2.0 * M_PI); + assert(c >= 0.999999999 && c <= 1.0); + + // Test range narrowing for [-π/2, π/2] + c = cos(M_PI / 4.0); // 45 degrees + assert(c >= 0.0 && c <= 1.0); // Should be in [0, 1] + + // Test range narrowing for [π/2, 3π/2] + c = cos(M_PI); // 180 degrees + assert(c >= -1.0 && c <= 0.0); // Should be in [-1, 0] + + // Test range narrowing for [3π/2, 2π] + c = cos(7.0 * M_PI / 4.0); // 315 degrees + assert(c >= 0.0 && c <= 1.0); // Should be in [0, 1] + + // ========== COSINE TESTS ========== + + // Test 7: cos(0) ≈ 1 + { + double c = cos(0.0); + assert(c >= 0.99 && c <= 1.0); + } + + // Test 8: cos(π/2) ≈ 0 + { + double c = cos(M_PI / 2.0); + assert(c >= -1e-9 && c <= 1e-9); + } + + // Test 9: cos(π) ≈ -1 + { + double c = cos(M_PI); + assert(c >= -1.0 && c <= -0.99); + } + + // Test 10: cos(2π) ≈ 1 + { + double c = cos(2.0 * M_PI); + assert(c >= 0.99 && c <= 1.0); + } + + // Test 11: Range narrowing - cos(x) ≥ 0 for x in [-π/2, π/2] + { + double x; + __CPROVER_assume(x >= -M_PI / 2.0 + 0.1 && x <= M_PI / 2.0 - 0.1); + double c = cos(x); + assert(c >= 0.0 && c <= 1.0); + } + + // Test 12: Range narrowing - cos(x) ≤ 0 for x in [π/2, 3π/2] + { + double x; + __CPROVER_assume(x >= M_PI / 2.0 + 0.1 && x <= 3.0 * M_PI / 2.0 - 0.1); + double c = cos(x); + assert(c >= -1.0 && c <= 0.0); + } + return 0; } diff --git a/regression/cbmc-library/cos-01/test.desc b/regression/cbmc-library/cos-01/test.desc index 9542d988e8d..cacf38ed78a 100644 --- a/regression/cbmc-library/cos-01/test.desc +++ b/regression/cbmc-library/cos-01/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--floatbv ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-library/cos-02/main.c b/regression/cbmc-library/cos-02/main.c new file mode 100644 index 00000000000..f0395b2de02 --- /dev/null +++ b/regression/cbmc-library/cos-02/main.c @@ -0,0 +1,25 @@ +#define _USE_MATH_DEFINES +#include +#include + +int main() +{ + // ========== COMBINED TESTS ========== + + // Test 15: Pythagorean identity approximation for x = π/4 + { + double x = M_PI / 4.0; + double s = sin(x); + double c = cos(x); + + // Both should be positive for this quadrant + assert(s >= 0.0 && s <= 1.0); + assert(c >= 0.0 && c <= 1.0); + + // And both should be close to √2/2 ≈ 0.707 + assert(s >= 0.6 && s <= 0.8); + assert(c >= 0.6 && c <= 0.8); + } + + return 0; +} diff --git a/regression/cbmc-library/cos-02/test.desc b/regression/cbmc-library/cos-02/test.desc new file mode 100644 index 00000000000..cacf38ed78a --- /dev/null +++ b/regression/cbmc-library/cos-02/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--floatbv +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-library/cosf-01/main.c b/regression/cbmc-library/cosf-01/main.c index 7a6fec665fe..6fd7af11a0c 100644 --- a/regression/cbmc-library/cosf-01/main.c +++ b/regression/cbmc-library/cosf-01/main.c @@ -1,9 +1,26 @@ +#define _USE_MATH_DEFINES #include #include int main() { - cosf(); - assert(0); - return 0; + // ========== FLOAT TESTS ========== + + // Test 13: sinf with special values + { + float s0 = sinf(0.0f); + float s_pi_half = sinf(3.14159265f / 2.0f); + + assert(s0 >= -1e-4f && s0 <= 1e-4f); + assert(s_pi_half >= 0.999f && s_pi_half <= 1.0f); + } + + // Test 14: cosf with special values + { + float c0 = cosf(0.0f); + float c_pi = cosf(3.14159265f); + + assert(c0 >= 0.999f && c0 <= 1.0f); + assert(c_pi >= -1.0f && c_pi <= -0.999f); + } } diff --git a/regression/cbmc-library/cosf-01/test.desc b/regression/cbmc-library/cosf-01/test.desc index 9542d988e8d..cacf38ed78a 100644 --- a/regression/cbmc-library/cosf-01/test.desc +++ b/regression/cbmc-library/cosf-01/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--floatbv ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring +^warning: ignoring \ No newline at end of file diff --git a/regression/cbmc-library/sin-01/main.c b/regression/cbmc-library/sin-01/main.c index ba1f5290d61..235973809cb 100644 --- a/regression/cbmc-library/sin-01/main.c +++ b/regression/cbmc-library/sin-01/main.c @@ -1,17 +1,93 @@ #define _USE_MATH_DEFINES +#include #include int main() { - double s, f = 0.0, fStep = 0.1 * M_PI; - int n = 0; + // Test special values - these should be precise + double s; - do + // sin(0) should be exactly 0 + s = sin(0.0); + assert(s >= -1e-10 && s <= 1e-10); + + // sin(π/2) should be approximately 1 + s = sin(M_PI / 2.0); + assert(s >= 0.999999999 && s <= 1.0); + + // sin(-π/2) should be approximately -1 + s = sin(-M_PI / 2.0); + assert(s >= -1.0 && s <= -0.999999999); + + // sin(π) should be approximately 0 + s = sin(M_PI); + assert(s >= -1e-10 && s <= 1e-10); + + // sin(-π) should be approximately 0 + s = sin(-M_PI); + assert(s >= -1e-10 && s <= 1e-10); + + // sin(2π) should be approximately 0 + s = sin(2.0 * M_PI); + assert(s >= -1e-10 && s <= 1e-10); + + // Test range narrowing for first quadrant [0, π/2] + s = sin(M_PI / 4.0); // 45 degrees + assert(s >= 0.0 && s <= 1.0); // Should be in [0, 1] + + // Test range narrowing for second quadrant [π/2, π] + s = sin(3.0 * M_PI / 4.0); // 135 degrees + assert(s >= 0.0 && s <= 1.0); // Should be in [0, 1] + + // Test range narrowing for third quadrant [π, 3π/2] + s = sin(5.0 * M_PI / 4.0); // 225 degrees + assert(s >= -1.0 && s <= 0.0); // Should be in [-1, 0] + + // Test range narrowing for fourth quadrant [3π/2, 2π] + s = sin(7.0 * M_PI / 4.0); // 315 degrees + assert(s >= -1.0 && s <= 0.0); // Should be in [-1, 0] + + // ========== SINE TESTS ========== + + // Test 1: sin(0) ≈ 0 + { + double s = sin(0.0); + assert(s >= -1e-9 && s <= 1e-9); + } + + // Test 2: sin(π/2) ≈ 1 + { + double s = sin(M_PI / 2.0); + assert(s >= 0.99 && s <= 1.0); + } + + // Test 3: sin(-π/2) ≈ -1 + { + double s = sin(-M_PI / 2.0); + assert(s >= -1.0 && s <= -0.99); + } + + // Test 4: sin(π) ≈ 0 + { + double s = sin(M_PI); + assert(s >= -1e-9 && s <= 1e-9); + } + + // Test 5: Range narrowing - sin(x) ≥ 0 for x in [0, π] + { + double x; + __CPROVER_assume(x >= 0.1 && x <= M_PI - 0.1); + double s = sin(x); + assert(s >= 0.0 && s <= 1.0); + } + + // Test 6: Range narrowing - sin(x) ≤ 0 for x in [π, 2π] { - s = sin(f); - f += fStep; - n++; - } while(f < M_PI); + double x; + __CPROVER_assume(x >= M_PI + 0.1 && x <= 2.0 * M_PI - 0.1); + double s = sin(x); + assert(s >= -1.0 && s <= 0.0); + } - assert(n < 11); + return 0; } diff --git a/regression/cbmc-library/sinf-01/main.c b/regression/cbmc-library/sinf-01/main.c index 164508966e6..b01071add18 100644 --- a/regression/cbmc-library/sinf-01/main.c +++ b/regression/cbmc-library/sinf-01/main.c @@ -1,9 +1,36 @@ +#define _USE_MATH_DEFINES #include #include int main() { - sinf(); - assert(0); + // Test special values with float precision + float s; + const float pi = 3.14159265f; + + // sin(0) should be exactly 0 + s = sinf(0.0f); + assert(s >= -1e-5f && s <= 1e-5f); + + // sin(π/2) should be approximately 1 + s = sinf(pi / 2.0f); + assert(s >= 0.99999f && s <= 1.0f); + + // sin(-π/2) should be approximately -1 + s = sinf(-pi / 2.0f); + assert(s >= -1.0f && s <= -0.99999f); + + // sin(π) should be approximately 0 + s = sinf(pi); + assert(s >= -1e-5f && s <= 1e-5f); + + // Test range narrowing for [0, π] + s = sinf(pi / 4.0f); + assert(s >= 0.0f && s <= 1.0f); + + // Test range narrowing for [π, 2π] + s = sinf(5.0f * pi / 4.0f); + assert(s >= -1.0f && s <= 0.0f); + return 0; -} +} \ No newline at end of file diff --git a/regression/cbmc-library/sinf-01/test.desc b/regression/cbmc-library/sinf-01/test.desc index 9542d988e8d..cacf38ed78a 100644 --- a/regression/cbmc-library/sinf-01/test.desc +++ b/regression/cbmc-library/sinf-01/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--floatbv ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -^warning: ignoring +^warning: ignoring \ No newline at end of file diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index ac594c0e590..a1f49ffd895 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -489,20 +489,130 @@ int __fpclassify(double d) /* FUNCTION: sin */ +#ifndef __CPROVER_MATH_H_INCLUDED +# include +# define __CPROVER_MATH_H_INCLUDED +#endif + double __VERIFIER_nondet_double(void); double sin(double x) { - // gross over-approximation +__CPROVER_hide:; double ret=__VERIFIER_nondet_double(); + // Handle special cases: NaN and Inf if(__CPROVER_isinfd(x) || __CPROVER_isnand(x)) + { __CPROVER_assume(__CPROVER_isnand(ret)); + return ret; + } + + // Define pi with sufficient precision for double + const double pi = 3.14159265358979323846; + const double pi_half = 1.57079632679489661923; + const double pi_3half = 4.71238898038468985769; + const double two_pi = 6.28318530717958647692; + + // For small epsilon for floating-point comparisons + const double epsilon = 1e-10; + + // Handle exact special values + // sin(0) = 0 + if(x >= -epsilon && x <= epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // sin(π/2) ≈ 1 + if(x >= pi_half - epsilon && x <= pi_half + epsilon) + { + __CPROVER_assume(ret >= 1.0 - epsilon && ret <= 1.0); + return ret; + } + + // sin(-π/2) ≈ -1 + if(x >= -pi_half - epsilon && x <= -pi_half + epsilon) + { + __CPROVER_assume(ret >= -1.0 && ret <= -1.0 + epsilon); + return ret; + } + + // sin(π) ≈ 0 + if( + (x >= pi - epsilon && x <= pi + epsilon) || + (x >= -pi - epsilon && x <= -pi + epsilon)) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // sin(3π/2) ≈ -1 + if(x >= pi_3half - epsilon && x <= pi_3half + epsilon) + { + __CPROVER_assume(ret >= -1.0 && ret <= -1.0 + epsilon); + return ret; + } + + // sin(-3π/2) ≈ 1 + if(x >= -pi_3half - epsilon && x <= -pi_3half + epsilon) + { + __CPROVER_assume(ret >= 1.0 - epsilon && ret <= 1.0); + return ret; + } + + // sin(2π) ≈ 0 + if( + (x >= two_pi - epsilon && x <= two_pi + epsilon) || + (x >= -two_pi - epsilon && x <= -two_pi + epsilon)) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // Range narrowing based on quadrants + // Normalize x to [-π, π] for range analysis + double x_normalized = x; + if(x > two_pi) + { + // For large positive values, we can't narrow the range precisely + // due to floating-point errors in modulo operations + __CPROVER_assume(ret <= 1.0 && ret >= -1.0); + return ret; + } + else if(x < -two_pi) + { + // For large negative values, same reasoning + __CPROVER_assume(ret <= 1.0 && ret >= -1.0); + return ret; + } + + // For values in [-2π, 2π], apply range narrowing + // sin is in [0, 1] for x in [0, π] + if(x >= 0 && x <= pi) + { + __CPROVER_assume(ret >= 0.0 && ret <= 1.0); + } + // sin is in [-1, 0] for x in [π, 2π] + else if(x >= pi && x <= two_pi) + { + __CPROVER_assume(ret >= -1.0 && ret <= 0.0); + } + // sin is in [-1, 0] for x in [-π, 0] + else if(x >= -pi && x < 0) + { + __CPROVER_assume(ret >= -1.0 && ret <= 0.0); + } + // sin is in [0, 1] for x in [-2π, -π] + else if(x >= -two_pi && x < -pi) + { + __CPROVER_assume(ret >= 0.0 && ret <= 1.0); + } else { - __CPROVER_assume(ret<=1); - __CPROVER_assume(ret>=-1); - __CPROVER_assume(x!=0 || ret==0); + // General case + __CPROVER_assume(ret <= 1.0 && ret >= -1.0); } return ret; @@ -510,20 +620,114 @@ double sin(double x) /* FUNCTION: sinl */ +#ifndef __CPROVER_MATH_H_INCLUDED +# include +# define __CPROVER_MATH_H_INCLUDED +#endif + long double __VERIFIER_nondet_long_double(void); long double sinl(long double x) { - // gross over-approximation +__CPROVER_hide:; long double ret=__VERIFIER_nondet_long_double(); + // Handle special cases: NaN and Inf if(__CPROVER_isinfld(x) || __CPROVER_isnanld(x)) + { __CPROVER_assume(__CPROVER_isnanld(ret)); + return ret; + } + + // Define pi with sufficient precision for long double + const long double pi = 3.14159265358979323846L; + const long double pi_half = 1.57079632679489661923L; + const long double pi_3half = 4.71238898038468985769L; + const long double two_pi = 6.28318530717958647692L; + + // For small epsilon for floating-point comparisons + const long double epsilon = 1e-12L; + + // Handle exact special values + // sin(0) = 0 + if(x >= -epsilon && x <= epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // sin(π/2) ≈ 1 + if(x >= pi_half - epsilon && x <= pi_half + epsilon) + { + __CPROVER_assume(ret >= 1.0L - epsilon && ret <= 1.0L); + return ret; + } + + // sin(-π/2) ≈ -1 + if(x >= -pi_half - epsilon && x <= -pi_half + epsilon) + { + __CPROVER_assume(ret >= -1.0L && ret <= -1.0L + epsilon); + return ret; + } + + // sin(π) ≈ 0 + if( + (x >= pi - epsilon && x <= pi + epsilon) || + (x >= -pi - epsilon && x <= -pi + epsilon)) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // sin(3π/2) ≈ -1 + if(x >= pi_3half - epsilon && x <= pi_3half + epsilon) + { + __CPROVER_assume(ret >= -1.0L && ret <= -1.0L + epsilon); + return ret; + } + + // sin(-3π/2) ≈ 1 + if(x >= -pi_3half - epsilon && x <= -pi_3half + epsilon) + { + __CPROVER_assume(ret >= 1.0L - epsilon && ret <= 1.0L); + return ret; + } + + // sin(2π) ≈ 0 + if( + (x >= two_pi - epsilon && x <= two_pi + epsilon) || + (x >= -two_pi - epsilon && x <= -two_pi + epsilon)) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // Range narrowing based on quadrants + // For values in [-2π, 2π], apply range narrowing + // sin is in [0, 1] for x in [0, π] + if(x >= 0 && x <= pi) + { + __CPROVER_assume(ret >= 0.0L && ret <= 1.0L); + } + // sin is in [-1, 0] for x in [π, 2π] + else if(x >= pi && x <= two_pi) + { + __CPROVER_assume(ret >= -1.0L && ret <= 0.0L); + } + // sin is in [-1, 0] for x in [-π, 0] + else if(x >= -pi && x < 0) + { + __CPROVER_assume(ret >= -1.0L && ret <= 0.0L); + } + // sin is in [0, 1] for x in [-2π, -π] + else if(x >= -two_pi && x < -pi) + { + __CPROVER_assume(ret >= 0.0L && ret <= 1.0L); + } else { - __CPROVER_assume(ret<=1); - __CPROVER_assume(ret>=-1); - __CPROVER_assume(x!=0 || ret==0); + // General case for values outside [-2π, 2π] + __CPROVER_assume(ret <= 1.0L && ret >= -1.0L); } return ret; @@ -531,20 +735,114 @@ long double sinl(long double x) /* FUNCTION: sinf */ +#ifndef __CPROVER_MATH_H_INCLUDED +# include +# define __CPROVER_MATH_H_INCLUDED +#endif + float __VERIFIER_nondet_float(void); float sinf(float x) { - // gross over-approximation +__CPROVER_hide:; float ret=__VERIFIER_nondet_float(); + // Handle special cases: NaN and Inf if(__CPROVER_isinff(x) || __CPROVER_isnanf(x)) + { __CPROVER_assume(__CPROVER_isnanf(ret)); + return ret; + } + + // Define pi with sufficient precision for float + const float pi = 3.14159265f; + const float pi_half = 1.57079633f; + const float pi_3half = 4.71238898f; + const float two_pi = 6.28318531f; + + // For small epsilon for floating-point comparisons (float has less precision) + const float epsilon = 1e-5f; + + // Handle exact special values + // sin(0) = 0 + if(x >= -epsilon && x <= epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // sin(π/2) ≈ 1 + if(x >= pi_half - epsilon && x <= pi_half + epsilon) + { + __CPROVER_assume(ret >= 1.0f - epsilon && ret <= 1.0f); + return ret; + } + + // sin(-π/2) ≈ -1 + if(x >= -pi_half - epsilon && x <= -pi_half + epsilon) + { + __CPROVER_assume(ret >= -1.0f && ret <= -1.0f + epsilon); + return ret; + } + + // sin(π) ≈ 0 + if( + (x >= pi - epsilon && x <= pi + epsilon) || + (x >= -pi - epsilon && x <= -pi + epsilon)) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // sin(3π/2) ≈ -1 + if(x >= pi_3half - epsilon && x <= pi_3half + epsilon) + { + __CPROVER_assume(ret >= -1.0f && ret <= -1.0f + epsilon); + return ret; + } + + // sin(-3π/2) ≈ 1 + if(x >= -pi_3half - epsilon && x <= -pi_3half + epsilon) + { + __CPROVER_assume(ret >= 1.0f - epsilon && ret <= 1.0f); + return ret; + } + + // sin(2π) ≈ 0 + if( + (x >= two_pi - epsilon && x <= two_pi + epsilon) || + (x >= -two_pi - epsilon && x <= -two_pi + epsilon)) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // Range narrowing based on quadrants + // For values in [-2π, 2π], apply range narrowing + // sin is in [0, 1] for x in [0, π] + if(x >= 0 && x <= pi) + { + __CPROVER_assume(ret >= 0.0f && ret <= 1.0f); + } + // sin is in [-1, 0] for x in [π, 2π] + else if(x >= pi && x <= two_pi) + { + __CPROVER_assume(ret >= -1.0f && ret <= 0.0f); + } + // sin is in [-1, 0] for x in [-π, 0] + else if(x >= -pi && x < 0) + { + __CPROVER_assume(ret >= -1.0f && ret <= 0.0f); + } + // sin is in [0, 1] for x in [-2π, -π] + else if(x >= -two_pi && x < -pi) + { + __CPROVER_assume(ret >= 0.0f && ret <= 1.0f); + } else { - __CPROVER_assume(ret<=1); - __CPROVER_assume(ret>=-1); - __CPROVER_assume(x!=0 || ret==0); + // General case for values outside [-2π, 2π] + __CPROVER_assume(ret <= 1.0f && ret >= -1.0f); } return ret; @@ -552,20 +850,114 @@ float sinf(float x) /* FUNCTION: cos */ +#ifndef __CPROVER_MATH_H_INCLUDED +# include +# define __CPROVER_MATH_H_INCLUDED +#endif + double __VERIFIER_nondet_double(void); double cos(double x) { - // gross over-approximation +__CPROVER_hide:; double ret=__VERIFIER_nondet_double(); + // Handle special cases: NaN and Inf if(__CPROVER_isinfd(x) || __CPROVER_isnand(x)) + { __CPROVER_assume(__CPROVER_isnand(ret)); + return ret; + } + + // Define pi with sufficient precision for double + const double pi = 3.14159265358979323846; + const double pi_half = 1.57079632679489661923; + const double pi_3half = 4.71238898038468985769; + const double two_pi = 6.28318530717958647692; + + // For small epsilon for floating-point comparisons + const double epsilon = 1e-10; + + // Handle exact special values + // cos(0) = 1 + if(x >= -epsilon && x <= epsilon) + { + __CPROVER_assume(ret >= 1.0 - epsilon && ret <= 1.0); + return ret; + } + + // cos(π/2) ≈ 0 + if(x >= pi_half - epsilon && x <= pi_half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(-π/2) ≈ 0 + if(x >= -pi_half - epsilon && x <= -pi_half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(π) ≈ -1 + if( + (x >= pi - epsilon && x <= pi + epsilon) || + (x >= -pi - epsilon && x <= -pi + epsilon)) + { + __CPROVER_assume(ret >= -1.0 && ret <= -1.0 + epsilon); + return ret; + } + + // cos(3π/2) ≈ 0 + if(x >= pi_3half - epsilon && x <= pi_3half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(-3π/2) ≈ 0 + if(x >= -pi_3half - epsilon && x <= -pi_3half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(2π) ≈ 1 + if( + (x >= two_pi - epsilon && x <= two_pi + epsilon) || + (x >= -two_pi - epsilon && x <= -two_pi + epsilon)) + { + __CPROVER_assume(ret >= 1.0 - epsilon && ret <= 1.0); + return ret; + } + + // Range narrowing based on quadrants + // For values in [-2π, 2π], apply range narrowing + // cos is in [0, 1] for x in [-π/2, π/2] + if(x >= -pi_half && x <= pi_half) + { + __CPROVER_assume(ret >= 0.0 && ret <= 1.0); + } + // cos is in [-1, 0] for x in [π/2, 3π/2] + else if(x >= pi_half && x <= pi_3half) + { + __CPROVER_assume(ret >= -1.0 && ret <= 0.0); + } + // cos is in [0, 1] for x in [3π/2, 2π] or x in [-2π, -3π/2] + else if((x >= pi_3half && x <= two_pi) || (x >= -two_pi && x <= -pi_3half)) + { + __CPROVER_assume(ret >= 0.0 && ret <= 1.0); + } + // cos is in [-1, 0] for x in [-3π/2, -π/2] + else if(x >= -pi_3half && x <= -pi_half) + { + __CPROVER_assume(ret >= -1.0 && ret <= 0.0); + } else { - __CPROVER_assume(ret<=1); - __CPROVER_assume(ret>=-1); - __CPROVER_assume(x!=0 || ret==1); + // General case for values outside [-2π, 2π] + __CPROVER_assume(ret <= 1.0 && ret >= -1.0); } return ret; @@ -573,20 +965,114 @@ double cos(double x) /* FUNCTION: cosl */ +#ifndef __CPROVER_MATH_H_INCLUDED +# include +# define __CPROVER_MATH_H_INCLUDED +#endif + long double __VERIFIER_nondet_long_double(void); long double cosl(long double x) { - // gross over-approximation +__CPROVER_hide:; long double ret=__VERIFIER_nondet_long_double(); + // Handle special cases: NaN and Inf if(__CPROVER_isinfld(x) || __CPROVER_isnanld(x)) + { __CPROVER_assume(__CPROVER_isnanld(ret)); + return ret; + } + + // Define pi with sufficient precision for long double + const long double pi = 3.14159265358979323846L; + const long double pi_half = 1.57079632679489661923L; + const long double pi_3half = 4.71238898038468985769L; + const long double two_pi = 6.28318530717958647692L; + + // For small epsilon for floating-point comparisons + const long double epsilon = 1e-12L; + + // Handle exact special values + // cos(0) = 1 + if(x >= -epsilon && x <= epsilon) + { + __CPROVER_assume(ret >= 1.0L - epsilon && ret <= 1.0L); + return ret; + } + + // cos(π/2) ≈ 0 + if(x >= pi_half - epsilon && x <= pi_half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(-π/2) ≈ 0 + if(x >= -pi_half - epsilon && x <= -pi_half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(π) ≈ -1 + if( + (x >= pi - epsilon && x <= pi + epsilon) || + (x >= -pi - epsilon && x <= -pi + epsilon)) + { + __CPROVER_assume(ret >= -1.0L && ret <= -1.0L + epsilon); + return ret; + } + + // cos(3π/2) ≈ 0 + if(x >= pi_3half - epsilon && x <= pi_3half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(-3π/2) ≈ 0 + if(x >= -pi_3half - epsilon && x <= -pi_3half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(2π) ≈ 1 + if( + (x >= two_pi - epsilon && x <= two_pi + epsilon) || + (x >= -two_pi - epsilon && x <= -two_pi + epsilon)) + { + __CPROVER_assume(ret >= 1.0L - epsilon && ret <= 1.0L); + return ret; + } + + // Range narrowing based on quadrants + // For values in [-2π, 2π], apply range narrowing + // cos is in [0, 1] for x in [-π/2, π/2] + if(x >= -pi_half && x <= pi_half) + { + __CPROVER_assume(ret >= 0.0L && ret <= 1.0L); + } + // cos is in [-1, 0] for x in [π/2, 3π/2] + else if(x >= pi_half && x <= pi_3half) + { + __CPROVER_assume(ret >= -1.0L && ret <= 0.0L); + } + // cos is in [0, 1] for x in [3π/2, 2π] or x in [-2π, -3π/2] + else if((x >= pi_3half && x <= two_pi) || (x >= -two_pi && x <= -pi_3half)) + { + __CPROVER_assume(ret >= 0.0L && ret <= 1.0L); + } + // cos is in [-1, 0] for x in [-3π/2, -π/2] + else if(x >= -pi_3half && x <= -pi_half) + { + __CPROVER_assume(ret >= -1.0L && ret <= 0.0L); + } else { - __CPROVER_assume(ret<=1); - __CPROVER_assume(ret>=-1); - __CPROVER_assume(x!=0 || ret==1); + // General case for values outside [-2π, 2π] + __CPROVER_assume(ret <= 1.0L && ret >= -1.0L); } return ret; @@ -594,21 +1080,114 @@ long double cosl(long double x) /* FUNCTION: cosf */ +#ifndef __CPROVER_MATH_H_INCLUDED +# include +# define __CPROVER_MATH_H_INCLUDED +#endif + float __VERIFIER_nondet_float(void); float cosf(float x) { __CPROVER_hide:; - // gross over-approximation float ret=__VERIFIER_nondet_float(); + // Handle special cases: NaN and Inf if(__CPROVER_isinff(x) || __CPROVER_isnanf(x)) + { __CPROVER_assume(__CPROVER_isnanf(ret)); + return ret; + } + + // Define pi with sufficient precision for float + const float pi = 3.14159265f; + const float pi_half = 1.57079633f; + const float pi_3half = 4.71238898f; + const float two_pi = 6.28318531f; + + // For small epsilon for floating-point comparisons (float has less precision) + const float epsilon = 1e-5f; + + // Handle exact special values + // cos(0) = 1 + if(x >= -epsilon && x <= epsilon) + { + __CPROVER_assume(ret >= 1.0f - epsilon && ret <= 1.0f); + return ret; + } + + // cos(π/2) ≈ 0 + if(x >= pi_half - epsilon && x <= pi_half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(-π/2) ≈ 0 + if(x >= -pi_half - epsilon && x <= -pi_half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(π) ≈ -1 + if( + (x >= pi - epsilon && x <= pi + epsilon) || + (x >= -pi - epsilon && x <= -pi + epsilon)) + { + __CPROVER_assume(ret >= -1.0f && ret <= -1.0f + epsilon); + return ret; + } + + // cos(3π/2) ≈ 0 + if(x >= pi_3half - epsilon && x <= pi_3half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(-3π/2) ≈ 0 + if(x >= -pi_3half - epsilon && x <= -pi_3half + epsilon) + { + __CPROVER_assume(ret >= -epsilon && ret <= epsilon); + return ret; + } + + // cos(2π) ≈ 1 + if( + (x >= two_pi - epsilon && x <= two_pi + epsilon) || + (x >= -two_pi - epsilon && x <= -two_pi + epsilon)) + { + __CPROVER_assume(ret >= 1.0f - epsilon && ret <= 1.0f); + return ret; + } + + // Range narrowing based on quadrants + // For values in [-2π, 2π], apply range narrowing + // cos is in [0, 1] for x in [-π/2, π/2] + if(x >= -pi_half && x <= pi_half) + { + __CPROVER_assume(ret >= 0.0f && ret <= 1.0f); + } + // cos is in [-1, 0] for x in [π/2, 3π/2] + else if(x >= pi_half && x <= pi_3half) + { + __CPROVER_assume(ret >= -1.0f && ret <= 0.0f); + } + // cos is in [0, 1] for x in [3π/2, 2π] or x in [-2π, -3π/2] + else if((x >= pi_3half && x <= two_pi) || (x >= -two_pi && x <= -pi_3half)) + { + __CPROVER_assume(ret >= 0.0f && ret <= 1.0f); + } + // cos is in [-1, 0] for x in [-3π/2, -π/2] + else if(x >= -pi_3half && x <= -pi_half) + { + __CPROVER_assume(ret >= -1.0f && ret <= 0.0f); + } else { - __CPROVER_assume(ret<=1); - __CPROVER_assume(ret>=-1); - __CPROVER_assume(x!=0 || ret==1); + // General case for values outside [-2π, 2π] + __CPROVER_assume(ret <= 1.0f && ret >= -1.0f); } return ret;