Fix C++ ternary operator type checking for bitfield operands#8792
Open
tautschnig wants to merge 2 commits into
Open
Fix C++ ternary operator type checking for bitfield operands#8792tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8792 +/- ##
===========================================
+ Coverage 80.55% 80.58% +0.02%
===========================================
Files 1707 1707
Lines 189051 189055 +4
Branches 73 73
===========================================
+ Hits 152299 152349 +50
+ Misses 36752 36706 -46 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
cpp_typecheckt::typecheck_expr_trinary uses implicit_conversion_sequence to compute the common type of the second and third operands of a C++ ternary expression, then sets the expression's type to the result and swaps the converted operand back in. The post-condition was implicitly assumed to be that all three of expr.type(), expr.op1().type() and expr.op2().type() agree, but that breaks when bit-fields are involved: implicit_conversion_sequence strips the c_bit_field wrapper from the requested type during standard conversion (cpp_typecheck_conversions.cpp:690-692), so the operand that did not undergo the conversion is left wearing the original c_bit_field<T,N> type label while the result type is the underlying T. Downstream code (e.g. simplification of nested expressions) then trips on the type mismatch. Fix: after the implicit conversion succeeds, re-align the other operand to the result type with a typecast_exprt. The outer implicit_conversion_sequence call has already proved the conversion is legal, so an unconditional typecast is sufficient and avoids the silent-failure surface a second implicit_conversion_sequence call would introduce. Apply this fix-up symmetrically to both branches (op1 -> op2.type() and op2 -> op1.type()). Add an INVARIANT at the end of the else block stating that the post- condition (all three types match) holds, so a future branch added without the alignment step trips at typecheck time rather than producing a malformed expression tree that surfaces much later. Tests: Bitfields_Ternary1 covers the first branch of typecheck_expr_trinary (op1 is a bool function-call result, op2 is a c_bit_field<uint8_t,1> bit-field access -- the original diffblue#933 reproducer). Bitfields_Ternary2 covers the symmetric branch via two cases: * Case 1: op1 is a bool literal, op2 is a class with a one-way user-defined conversion 'operator bool() const'. The first branch's implicit_conversion_sequence(bool -> class) fails; the symmetric branch then succeeds via the conversion operator. Result types align, so the inner typecast fix-up is a no-op here; this case exercises the outer symmetric branch. * Case 2: op1 is a c_bit_field<uint8_t,1> bit-field access, op2 is a class with 'operator uint8_t() const'. The first branch's conversion fails; the symmetric branch converts op2 to op1's bit-field type, which strips the wrapper, leaving op1 in the bit-field type and the result in the underlying type. The symmetric inner typecast fix-up is required to align them. Fixes: diffblue#933 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-933-ternary-cpp
branch
from
1b4ef10 to
375a747
Compare
There was a problem hiding this comment.
Pull request overview
Fixes C++ conditional (?:) expression typechecking in the C++ frontend to avoid malformed expression trees when operands involve bit-fields, and corrects a typo that prevented the dedicated void/throw-operand handling from triggering.
Changes:
- Fix void-operand guard in
cpp_typecheckt::typecheck_expr_trinaryto correctly check both operands (op1andop2). - After successful
implicit_conversion_sequence, explicitly typecast the other operand when the computed common type differs (notably whenc_bit_fieldwrappers are stripped), and add an invariant to enforce the post-condition that operand/result types match. - Add regression tests covering bitfield ternary conversions and
cond ? x : throw ...ternary acceptance.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
src/cpp/cpp_typecheck_expr.cpp |
Ensures ternary operand/result type consistency (bitfield wrapper stripping) and fixes void/throw operand guard. |
regression/cbmc-cpp/Bitfields_Ternary1/main.cpp |
Regression test for ternary with bitfield operand requiring implicit conversion to bool. |
regression/cbmc-cpp/Bitfields_Ternary1/test.desc |
Test expectations for Bitfields_Ternary1. |
regression/cbmc-cpp/Bitfields_Ternary2/main.cpp |
Regression test for the symmetric implicit-conversion branch, including a bitfield-triggered alignment case. |
regression/cbmc-cpp/Bitfields_Ternary2/test.desc |
Test expectations for Bitfields_Ternary2. |
regression/cbmc-cpp/Ternary_Throw1/main.cpp |
Regression test ensuring cond ? x : throw 1 typechecks and verifies successfully. |
regression/cbmc-cpp/Ternary_Throw1/test.desc |
Test expectations, including disallowed prior failure messages. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
cpp_typecheckt::typecheck_expr_trinary opens its second operand
handling with a void-operand fast path:
if(expr.op1().type().id() == ID_empty ||
expr.op1().type().id() == ID_empty) // <-- typo: both reference op1
The intent is to enter the block whenever EITHER operand is void
(typically because that operand is a 'throw' expression, which has
type void by [expr.cond] in the C++ standard, or because it is a
call to a function returning void). The disjunction was meant to
catch op1 being void OR op2 being void, but both clauses reference
op1, so a ternary whose third operand is void but whose second
operand is not is silently routed to the regular type-matching paths
and fails with
"types are incompatible. I got 'signed int' and 'void'."
instead of being typechecked under the throw/void rules. GCC and
Clang accept the construct without warnings.
Fix the second disjunct to read op2(), as originally intended.
clang-format collapses the two-line condition onto one line because
it now fits.
Add a regression test, regression/cbmc-cpp/Ternary_Throw1, that
takes the form 'static_cast<void>(cond ? x : throw 1)' with cond
fixed to true so the throw branch is never executed. The discarded
form (static_cast<void>) avoids generating a goto-program assignment
of the if_exprt, which would otherwise expose a separate
pre-existing issue under the regression suite's
--validate-goto-model profile (the if_exprt's op2 retains its void
type even though expr.type() is set to op1's type, so an assignment
that wraps the ternary fails the lhs-rhs type-equality validation).
That latter issue exists independently on origin/develop for the
mirror case 'cond ? throw : x' and is out of scope for this PR.
The test asserts both that cbmc accepts the construct (^EXIT=0$,
^VERIFICATION SUCCESSFUL$) and that the prior failure modes do not
appear in the output (negative patterns ^CONVERSION ERROR$ and
^.*types are incompatible.*$). Verified by re-introducing the typo
locally that the test fails on all four patterns when the typo is
present.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-933-ternary-cpp
branch
from
375a747 to
d223a89
Compare
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
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.
implicit_conversion_sequencedoes not guarantee to produce the exact type requested as bitfields promote to the underlying type. Therefore, add typecasts as needed to ensure type consistency.Fixes: #933