Add floating-point type cast safety handling #7443
Conversation
📝 WalkthroughWalkthroughAdds floating-point cast-safety handling to type-cast logic: when both cast and expression types are floating-point, casts are treated as safe if primary annotations match. If each side has a single annotation and both denote DOUBLEVAL, value-based checks are applied for float↔double casts (exact rounded-equality for float→double; matching rounded float values for double→float). Other cases defer to existing safety logic. Also updates docs/manual/contributors.tex to adjust punctuation and add two contributor lines. 🚥 Pre-merge checks | ✅ 1✅ Passed checks (1 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Fix all issues with AI agents
In `@framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java`:
- Around line 421-441: The Float-to-Double comparison block calls
atypeFactory.getDoubleValues(castAnno)/getDoubleValues(exprAnno) without
verifying the annotation types; add checks like the integer branch does by using
atypeFactory.areSameByClass(castAnno, DoubleVal.class) and
atypeFactory.areSameByClass(exprAnno, DoubleVal.class) (similar to the IntVal
checks) before calling getDoubleValues so you only extract double values when
both annotations are DoubleVal; update the condition guarding the block that
currently tests castTypeKind/exprTypeKind and castAnnos/exprAnnos to also
require both annotations are DoubleVal (use the same pattern as the IntVal
verification).
- Around line 408-411: The comment in ValueVisitor about handling floating-point
type casts only mentions double → float but the surrounding code also handles
float → double; update the comment above the floating-point cast handling to
mention both directions (double → float and float → double), describing that
double→float may lose precision while float→double promotes without precision
loss but both follow IEEE 754 semantics and should not be flagged when correctly
rounded or representable; keep the note brief and place it with the existing
floating-point cast handling block in ValueVisitor so the comment accurately
describes both cases.
| // Handle floating-point type casts (double -> float). | ||
| // When a double is cast to float, precision loss may occur, but this is expected | ||
| // IEEE 754 behavior and should not be flagged as an unsafe cast if the result | ||
| // is the correctly-rounded representation. |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Comment is incomplete — also handles float → double.
The comment only describes the double → float case, but lines 442-444 also handle float → double. Consider updating the comment to reflect both directions.
- // Handle floating-point type casts (double -> float).
- // When a double is cast to float, precision loss may occur, but this is expected
- // IEEE 754 behavior and should not be flagged as an unsafe cast if the result
- // is the correctly-rounded representation.
+ // Handle floating-point type casts (double <-> float).
+ // When a double is cast to float, precision loss may occur, but this is expected
+ // IEEE 754 behavior and should not be flagged as an unsafe cast if the result
+ // is the correctly-rounded representation.
+ // When a float is cast to double, no precision is lost, so it is always safe.📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| // Handle floating-point type casts (double -> float). | |
| // When a double is cast to float, precision loss may occur, but this is expected | |
| // IEEE 754 behavior and should not be flagged as an unsafe cast if the result | |
| // is the correctly-rounded representation. | |
| // Handle floating-point type casts (double <-> float). | |
| // When a double is cast to float, precision loss may occur, but this is expected | |
| // IEEE 754 behavior and should not be flagged as an unsafe cast if the result | |
| // is the correctly-rounded representation. | |
| // When a float is cast to double, no precision is lost, so it is always safe. |
🤖 Prompt for AI Agents
In `@framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java`
around lines 408 - 411, The comment in ValueVisitor about handling
floating-point type casts only mentions double → float but the surrounding code
also handles float → double; update the comment above the floating-point cast
handling to mention both directions (double → float and float → double),
describing that double→float may lose precision while float→double promotes
without precision loss but both follow IEEE 754 semantics and should not be
flagged when correctly rounded or representable; keep the note brief and place
it with the existing floating-point cast handling block in ValueVisitor so the
comment accurately describes both cases.
framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java
Show resolved
Hide resolved
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Fix all issues with AI agents
In `@docs/manual/contributors.tex`:
- Line 155: Update the contributor entry string "shubham kapoor." to title case
and match the other entries by changing it to "Shubham Kapoor." — locate the
literal text "shubham kapoor." in the contributors list in contributors.tex (the
contributor line), replace it with "Shubham Kapoor." preserving the trailing
period and surrounding formatting so the list remains consistent.
In `@framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java`:
- Around line 435-448: The current index-based loop in ValueVisitor compares
castValues and exprValues by position, which is order-dependent and can fail if
the lists are differently ordered; change this to an order-independent
containment check by converting both lists into sets of the same element type
(e.g., HashSet<Double> or a TreeSet with a consistent comparator) after applying
the cast logic ((double)(float)exprVal) to exprValues, then use the existing
sortedSetContainsAll (or an equivalent set-contains-all) to check membership
between the set made from castValues and the set made from exprValues; update
the block that references castValues and exprValues to build these sets and
replace the index loop with the set-based comparison so the result is
order-independent.
- Around line 450-452: In ValueVisitor (the cast-handling block using
castTypeKind and exprTypeKind) the branch for float→double currently returns
true unconditionally; change it to mirror the double→float branch by verifying
both the cast target and the expression are annotated with `@DoubleVal` before
returning true (i.e., check the same annotation presence used in the
double→float check), so the float→double case only succeeds when both sides
carry the `@DoubleVal` annotation.
docs/manual/contributors.tex
Outdated
| Werner Dietl, | ||
| Zhiping Cai. | ||
| Zhiping Cai, | ||
| shubham kapoor. |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Capitalize name to match contributor list format.
All other contributor names use title case. For consistency, this should be "Shubham Kapoor."
📝 Suggested fix
-shubham kapoor.
+Shubham Kapoor.📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| shubham kapoor. | |
| Shubham Kapoor. |
🤖 Prompt for AI Agents
In `@docs/manual/contributors.tex` at line 155, Update the contributor entry
string "shubham kapoor." to title case and match the other entries by changing
it to "Shubham Kapoor." — locate the literal text "shubham kapoor." in the
contributors list in contributors.tex (the contributor line), replace it with
"Shubham Kapoor." preserving the trailing period and surrounding formatting so
the list remains consistent.
| if (castValues != null && exprValues != null && castValues.size() == exprValues.size()) { | ||
| boolean allMatch = true; | ||
| for (int i = 0; i < exprValues.size(); i++) { | ||
| double exprVal = exprValues.get(i); | ||
| double castVal = castValues.get(i); | ||
| if (Double.compare(castVal, (double) (float) exprVal) != 0) { | ||
| allMatch = false; | ||
| break; | ||
| } | ||
| } | ||
| if (allMatch) { | ||
| return true; | ||
| } | ||
| } |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Index-based comparison assumes value ordering — consider set-based containment.
The integer cast handling (lines 371-402) uses TreeSet and sortedSetContainsAll for order-independent comparison. The floating-point handling assumes castValues and exprValues are in the same order by index. If the annotation value lists are derived or stored differently, this could incorrectly fail.
Consider using set-based comparison for robustness:
♻️ Suggested approach
if (castValues != null && exprValues != null && castValues.size() == exprValues.size()) {
- boolean allMatch = true;
- for (int i = 0; i < exprValues.size(); i++) {
- double exprVal = exprValues.get(i);
- double castVal = castValues.get(i);
- if (Double.compare(castVal, (double) (float) exprVal) != 0) {
- allMatch = false;
- break;
- }
- }
- if (allMatch) {
- return true;
+ // Compute expected cast values (double→float→double round-trip)
+ TreeSet<Double> expectedCastValues = new TreeSet<>();
+ for (Double exprVal : exprValues) {
+ expectedCastValues.add((double) (float) exprVal.doubleValue());
}
+ TreeSet<Double> actualCastValues = new TreeSet<>(castValues);
+ if (actualCastValues.equals(expectedCastValues)) {
+ return true;
+ }
}🤖 Prompt for AI Agents
In `@framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java`
around lines 435 - 448, The current index-based loop in ValueVisitor compares
castValues and exprValues by position, which is order-dependent and can fail if
the lists are differently ordered; change this to an order-independent
containment check by converting both lists into sets of the same element type
(e.g., HashSet<Double> or a TreeSet with a consistent comparator) after applying
the cast logic ((double)(float)exprVal) to exprValues, then use the existing
sortedSetContainsAll (or an equivalent set-contains-all) to check membership
between the set made from castValues and the set made from exprValues; update
the block that references castValues and exprValues to build these sets and
replace the index loop with the set-based comparison so the result is
order-independent.
framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java
Outdated
Show resolved
Hide resolved
shubhamk0205
force-pushed
the
fix/floating-point-cast-safety
branch
from
bef74a1 to
762d67d
Compare
shubhamk0205
force-pushed
the
fix/floating-point-cast-safety
branch
from
762d67d to
3213a02
Compare
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@docs/manual/contributors.tex`:
- Around line 155-156: Remove the redundant contributor entry by keeping only
the proper name "Shubham Kapoor" and deleting the duplicate username
"shubhamk0205." Locate the two lines containing "shubham kapoor," and
"shubhamk0205." in the contributors list and remove the username entry (or vice
versa if you prefer the username), ensuring formatting and punctuation match the
surrounding entries.
♻️ Duplicate comments (2)
docs/manual/contributors.tex (1)
155-155: Capitalize name to match contributor list format.All other contributor names use title case (e.g., "Abhijit Kulkarni", "Abraham Lin"). This should be "Shubham Kapoor," for consistency.
📝 Suggested fix
-shubham kapoor, +Shubham Kapoor,framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java (1)
437-444: Consider set-based comparison for robustness.The index-based comparison assumes
castValuesandexprValuesare in the same order. The integer handling (lines 372-402) usesTreeSetandsortedSetContainsAllfor order-independent comparison. Consider the same approach here for consistency.♻️ Suggested approach using set-based comparison
if (castValues != null && exprValues != null && castValues.size() == exprValues.size()) { - boolean allMatch = true; - for (int i = 0; i < exprValues.size(); i++) { - double exprVal = exprValues.get(i); - double castVal = castValues.get(i); - if (Double.compare(castVal, (double) (float) exprVal) != 0) { - allMatch = false; - break; - } - } - if (allMatch) { - return true; - } + TreeSet<Double> expectedCastValues = new TreeSet<>(); + for (Double exprVal : exprValues) { + expectedCastValues.add((double) (float) exprVal.doubleValue()); + } + TreeSet<Double> actualCastValues = new TreeSet<>(castValues); + if (actualCastValues.equals(expectedCastValues)) { + return true; + } }
| shubham kapoor, | ||
| shubhamk0205. |
There was a problem hiding this comment.
🧹 Nitpick | 🔵 Trivial
Redundant contributor entries.
Both entries appear to refer to the same contributor (name and GitHub username). Consider keeping only one entry — either the proper name "Shubham Kapoor" or the username "shubhamk0205", but not both.
📝 Suggested fix (keep only proper name)
Zhiping Cai,
-shubham kapoor,
-shubhamk0205.
+Shubham Kapoor.📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| shubham kapoor, | |
| shubhamk0205. | |
| Zhiping Cai, | |
| Shubham Kapoor. |
🤖 Prompt for AI Agents
In `@docs/manual/contributors.tex` around lines 155 - 156, Remove the redundant
contributor entry by keeping only the proper name "Shubham Kapoor" and deleting
the duplicate username "shubhamk0205." Locate the two lines containing "shubham
kapoor," and "shubhamk0205." in the contributors list and remove the username
entry (or vice versa if you prefer the username), ensuring formatting and
punctuation match the surrounding entries.
|
@mernst all checks are passing please review this pr when u get time |
1 participant
solves #6141
This PR updates the isTypeCastSafe method in ValueVisitor to better handle type casts between double and float. Previously, the method only handled integer casts, which could cause valid floating-point casts to be incorrectly flagged as unsafe.
For double to float casts, the code now checks whether the value after casting behaves the same way Java would normally handle the conversion. If the values match, the cast is treated as safe.
For float to double casts, the method always considers the cast safe since this conversion does not lose information.