Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

C++: Test and (perhaps) fix an issue with guards on floating point comparisons. #18586

Merged
merged 4 commits into from
Jan 28, 2025

Conversation

geoffw0
Copy link
Contributor

@geoffw0 geoffw0 commented Jan 24, 2025

The issue is with guards library expressions such as guard.comparesEq(e, _, _, _) matching integer comparisons to a constant, but not floating point comparisons to a constant, e.g. in

if (i == 0) && (f == 0) { ...

(where i is int, f is float)

Note that the five argument version guard.comparesEq(e, _, _, _, _) works fine in both cases already.

I've added some more test cases around this (there were a couple already) and put in a naive fix. The fix isn't great, it wouldn't cope with f == 0.5 for example, it's more intended to provoke discussion about what if anything we should be doing with these cases. It may well be the best thing to do is to document this limitation of the four argument version???

@MathiasVP and @jketema I'd love to hear your thoughts on this.

@geoffw0 geoffw0 added the C++ label Jan 24, 2025
@MathiasVP
Copy link
Contributor

MathiasVP commented Jan 24, 2025

When you do something like f == 0 I assume there's an int-to-float conversion on the 0. So that's why the unary one doesn't work (because we're checking if the constant is an integer):

exists(Instruction const | int_value(const) = k |
value.(BooleanValue).getValue() = true and
test.(CompareEQValueNumber).hasOperands(op, const.getAUse())
or
value.(BooleanValue).getValue() = false and
test.(CompareNEValueNumber).hasOperands(op, const.getAUse())
(and as you've noted in your description int_value only holds for integers and pointers).

Note that the five argument version guard.comparesEq(e, _, _, _, _) works fine in both cases already.

The reason the binary (i.e., the five argument) works is because the 0 will be right right-hand side of the equality (as an Expr) and the constant will be the integer 0. So it will hold that guard.comparesEq(e1, e2, 0, _, _) where e1 is f, and e2 is 0.

I don't particularly like this proposed solution since this will work for f == 0, but it won't work for f == 1.2 since 1.2 doesn't have an integer representation.

Instead, I think we should simply make it clear that if people want to do floating point reasoning they need to use the binary version of the predicates. The unary predicates only exist to handle the cases where there's no expression representing the right-hand side in examples such as if(x) (however, it also works for x == k when k is an integer without any int-to-float conversions). And, as far as I'm aware, there is no case where the following two conditions hold:

  • You need floating point reasoning
  • The "right-hand side" doesn't have representation in the database as an Expr.

@geoffw0 geoffw0 marked this pull request as ready for review January 24, 2025 17:54
@Copilot Copilot bot review requested due to automatic review settings January 24, 2025 17:54
@geoffw0 geoffw0 requested a review from a team as a code owner January 24, 2025 17:54

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.

Tip: Copilot code review supports C#, Go, Java, JavaScript, Markdown, Python, Ruby and TypeScript, with more languages coming soon. Learn more

@geoffw0
Copy link
Contributor Author

geoffw0 commented Jan 24, 2025

Thanks for your thoughts - it looks like we're in agreement at this point that this is a documentation issue not a problem with the library. I've changed my PR to leave the QL alone and add to the qldoc comments instead. I've also taken it out of draft.
Further comments / corrections very much welcome.

@geoffw0 geoffw0 added the no-change-note-required This PR does not need a change note label Jan 24, 2025
@MathiasVP
Copy link
Contributor

Thanks for your thoughts - it looks like we're in agreement at this point that this is a documentation issue not a problem with the library. I've changed my PR to leave the QL alone and add to the qldoc comments instead. I've also taken it out of draft. Further comments / corrections very much welcome.

That sounds good, but... you've not actually changed anything compared to the original PR 😂

@geoffw0
Copy link
Contributor Author

geoffw0 commented Jan 25, 2025

Ah, sorry, now pushed.

jketema
jketema previously approved these changes Jan 27, 2025
@geoffw0 geoffw0 merged commit 6337f5a into github:main Jan 28, 2025
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C++ no-change-note-required This PR does not need a change note
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants