Improve precision of sine and cosine library models #8743

tautschnig · 2025-11-27T14:06:40Z

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

Fixes: #6999

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

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

kroening · 2025-11-27T16:58:06Z

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

+
+  // cos(0) should be exactly 1
+  c = cos(0.0);
+  assert(c >= 0.999999999 && c <= 1.0);


Compare with 1, as suggested in the comment.

martin-cs · 2025-11-27T16:58:10Z

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

+
+  // cos(0) should be exactly 1
+  c = cos(0.0);
+  assert(c >= 0.999999999 && c <= 1.0);


0.999999999 == 0x1.fffffff768fa1p-1
so this allows around 22 bits difference so only a bit more accurate than float. I would recommend a tighter bound.

martin-cs · 2025-11-27T16:58:13Z

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

+  c = cos(0.0);
+  assert(c >= 0.999999999 && c <= 1.0);
+
+  // cos(π/2) should be approximately 0


We can work it out exactly. If we use a correctly rounded implementation such as https://core-math.gitlabpages.inria.fr/ then we can compute the double nearest to cos(M_PI / 2.0). Note that it is small but it is not zero. In fact, IIRC, it is a lot further away from zero than you might think because M_PI != \pi.
Personally I would try computing each of these using something like CORE-MATH and then adding an error in the range of a few ULP. Happy to give this a go if useful.

kroening · 2025-11-27T16:59:27Z

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

+
+  // ========== COSINE TESTS ==========
+
+  // Test 7: cos(0) ≈ 1


These just repeat the above.

kroening · 2025-11-27T17:01:11Z

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

+  // Test 13: sinf with special values
+  {
+    float s0 = sinf(0.0f);
+    float s_pi_half = sinf(3.14159265f / 2.0f);


File is called cosf, but tests sinf.

kroening · 2025-11-27T17:01:42Z

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

 ^VERIFICATION SUCCESSFUL$
 --
-^warning: ignoring
+^warning: ignoring


Spurious newline change

martin-cs · 2025-11-27T17:01:42Z

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

+
+  // 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]


Unlike sin, which can produce very small outputs (but only in [-\pi/2, \pi/2], cos has quite a high lower bound on it's outputs. Off the top of my head I think it is something like 0x1.0p-100, very small but a tiny part of the range of double.

kroening · 2025-11-27T17:02:02Z

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

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring


Spurious newline change

kroening · 2025-11-27T17:02:22Z

regression/cbmc-library/cosf-01/test.desc

 ^VERIFICATION SUCCESSFUL$
 --
-^warning: ignoring
+^warning: ignoring


Spurious newline change

kroening · 2025-11-27T17:02:42Z

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

-  do
+  // sin(0) should be exactly 0
+  s = sin(0.0);
+  assert(s >= -1e-10 && s <= 1e-10);


same as above

martin-cs · 2025-11-27T17:03:01Z

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

+
+  // ========== COSINE TESTS ==========
+
+  // Test 7: cos(0) ≈ 1


Is this a duplicate of line 10.

martin-cs · 2025-11-27T17:03:34Z

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

+    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);


Again, these can be tightened quite a bit.

kroening · 2025-11-27T17:04:34Z

src/ansi-c/library/math.c

+
+  // Handle exact special values
+  // sin(0) = 0
+  if(x >= -epsilon && x <= epsilon)


I would handle the special case 0 in addition to that.

martin-cs

Some pedantry. Hope it is helpful.

martin-cs · 2025-11-27T17:06:15Z

src/ansi-c/library/math.c

+  const long double two_pi = 6.28318530717958647692L;
+
+  // For small epsilon for floating-point comparisons
+  const long double epsilon = 1e-12L;


Why this number?

martin-cs · 2025-11-27T17:07:03Z

src/ansi-c/library/math.c

+
+  // For small epsilon for floating-point comparisons
+  const long double epsilon = 1e-12L;
+


Note that it would be possible to do a range reduction here and it might get you more accurate results.

Improve precision of sine and cosine library models

dececea

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

tautschnig requested review from kroening, peterschrammel and remi-delmas-3000 as code owners November 27, 2025 14:06

kroening reviewed Nov 27, 2025

View reviewed changes

martin-cs reviewed Nov 27, 2025

View reviewed changes

kroening reviewed Nov 27, 2025

View reviewed changes

martin-cs reviewed Nov 27, 2025

View reviewed changes

kroening reviewed Nov 27, 2025

View reviewed changes

martin-cs reviewed Nov 27, 2025

View reviewed changes

kroening reviewed Nov 27, 2025

View reviewed changes

martin-cs reviewed Nov 27, 2025

View reviewed changes


		// ========== COSINE TESTS ==========

		// Test 7: cos(0) ≈ 1


		// For small epsilon for floating-point comparisons
		const long double epsilon = 1e-12L;

Improve precision of sine and cosine library models #8743

Are you sure you want to change the base?

Improve precision of sine and cosine library models #8743

Uh oh!

Conversation

tautschnig commented Nov 27, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

martin-cs Nov 27, 2025 •

edited

Loading