C++: Round towards +/- Inf in range analysis#374
Merged
Conversation
Contributor
Author
|
This test case is an example of the good results that go away with this change: Notice that the 32-bit case is wrong independently of this PR, so this PR just changes the 64-bit case to be as wrong as the 32-bit case. |
| bindingset[x] | ||
| private float normalizeFloatUp(float x) { | ||
| result = x + 0.0 | ||
| } |
Contributor
There was a problem hiding this comment.
It would be better if we added IEEE comparison as a method of float, but this looks like it will work for now.
kevinbackhouse
approved these changes
Oct 29, 2018
aibaars
added a commit
that referenced
this pull request
Oct 21, 2021
Sync with `github/codeql:main`
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR attempts to fix a long-standing problem with the range analysis. It doesn't handle 64-bit numbers correctly because we’re using double-precision floats for the arithmetic internally, and when we add 0xffff_ffff_ffff_ffff + 1 as doubles we get 0xffff_ffff_ffff_ffff. This makes the analysis believe the numbers can’t wrap around.
The problem is tracked in ODASA-7205 and was most recently reported on the lgtm.com forum by @pm215. The last attempt to fix this was the internal PR 26489 by @kevinbackhouse, which was abandoned due to a lack of time to investigate (1) performance implications and (2) a test failure caused by how the new rounding interacts with negative zero.
The first two commits are ports of PR 26489 to the open QL repository. Commit 3 factors out similar code, and commit 4 fixes the treatment of negative zero. I've tested the changes for performance on LibreOffice, ChakraCore, Blender and p3/regal, and I've found any slowdown to be within the noise level of our performance measurements. I've tested for correctness on LibreOffice, ChakraCore and Blender, and I found two FPs removed and two TPs removed. The removed TPs are of the following form, where we can't establish that
my64bitnumberis small enough.