Improve precision of sine and cosine library models

Handle special values (0, ±π/2, ±π, ±3π/2, ±2π) with precise ranges and
and use quadrant-based range narrowing to reduce over-approximation.

Fixes: #6999

Author: tautschnig

regression/cbmc-library/cos-01/main.c

@@ -1,9 +1,89 @@
+#define _USE_MATH_DEFINES
 #include <assert.h>
 #include <math.h>
 
 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;
 }

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

regression/cbmc-library/cos-02/main.c

@@ -0,0 +1,25 @@
+#define _USE_MATH_DEFINES
+#include <assert.h>
+#include <math.h>
+
+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;
+}

regression/cbmc-library/cos-02/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/cosf-01/main.c

@@ -1,9 +1,26 @@
+#define _USE_MATH_DEFINES
 #include <assert.h>
 #include <math.h>
 
 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);
+  }
 }

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

regression/cbmc-library/sin-01/main.c

@@ -1,17 +1,93 @@
 #define _USE_MATH_DEFINES
+#include <assert.h>
 #include <math.h>
 
 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;
 }

regression/cbmc-library/sinf-01/main.c

@@ -1,9 +1,36 @@
+#define _USE_MATH_DEFINES
 #include <assert.h>
 #include <math.h>
 
 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;
-}
+}

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