ansi-c: tighten null-pointer-constant check in conditional operator#9052
Open
tautschnig wants to merge 1 commit into
Open
ansi-c: tighten null-pointer-constant check in conditional operator#9052tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
tautschnig
requested review from
kroening,
peterschrammel and
remi-delmas-3000
as code owners
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Tightens CBMC’s conditional-operator (?:) null-pointer-constant handling to match the C-standard distinction between “simplifies to 0” and “integer constant expression (ICE) equal to 0”, restoring correct behavior for Linux kernel __is_constexpr-based idioms.
Changes:
- Adds a pre-simplification scan to reject null-pointer-constant classification when the original operand contains non-constant leaves.
- Updates ternary pointer-operand coercion logic to use the new “ICE-zero” predicate.
- Adds a regression test that distinguishes
__is_constexpr(5)(true) from__is_constexpr(argc)(false).
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| src/ansi-c/c_typecheck_expr.cpp | Adds a pre-simplification “non-constant leaf” scan and uses it to refine null-pointer-constant detection in typecheck_expr_trinary. |
| regression/cbmc/is_constexpr_null_ptr/test.desc | Registers a new CORE regression describing and checking the fixed behavior. |
| regression/cbmc/is_constexpr_null_ptr/main.c | Implements the regression using the kernel-style __is_constexpr macro and assertions for constant vs runtime cases. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+1714
to
+1728
| const auto contains_non_constant_leaf = [](const exprt &e) | ||
| { | ||
| bool found = false; | ||
| e.visit_pre( | ||
| [&found](const exprt &sub) | ||
| { | ||
| if( | ||
| sub.id() == ID_symbol || sub.id() == ID_side_effect || | ||
| sub.id() == ID_function_application || sub.id() == ID_dereference) | ||
| { | ||
| found = true; | ||
| } | ||
| }); | ||
| return found; | ||
| }; |
Comment on lines
+1717
to
+1726
| e.visit_pre( | ||
| [&found](const exprt &sub) | ||
| { | ||
| if( | ||
| sub.id() == ID_symbol || sub.id() == ID_side_effect || | ||
| sub.id() == ID_function_application || sub.id() == ID_dereference) | ||
| { | ||
| found = true; | ||
| } | ||
| }); |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9052 +/- ##
========================================
Coverage 80.68% 80.68%
========================================
Files 1714 1714
Lines 189501 189514 +13
Branches 73 73
========================================
+ Hits 152902 152915 +13
Misses 36599 36599 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
extract/ansi-c-null-ptr-constant-cond
branch
from
a01b7a2 to
9b5857f
Compare
`typecheck_expr_trinary` decides whether each pointer operand of a
ternary is a null pointer constant by (a) simplifying the operand and
(b) calling is_null_pointer() on the result. That misses the C-standard
distinction between an integer constant expression with value 0 and a
runtime expression that merely simplifies to 0: pre-fix, an operand like
`(long)(argc) * 0L` simplified to 0 and CBMC treated the whole
expression as a null pointer constant, even though argc is runtime.
Consequence: the kernel's `__is_constexpr` macro
(sizeof(int) == sizeof(*(8 ? ((void *)((long)(x) * 0l))
: (int *)8)))
— which exploits exactly this distinction to select between compile-time
and runtime branches of header-level static checks — returned 1 for
every x on CBMC. Linux 6.x GENMASK_INPUT_CHECK and related idioms
depend on it and broke kernel-TU compiles.
Fix: before treating the simplified operand as a null pointer constant,
walk the PRE-simplification operand and confirm it contains no
non-constant leaves. Any symbol read, side effect, function call, or
dereference in the original expression disqualifies it from being an
integer constant expression regardless of what it simplifies to. This
is a sound proxy here because sizeof/_Alignof are already folded and
enumeration constants resolved by this point, so the only remaining
leaves are genuinely non-ICE constructs.
Regression test: regression/cbmc/is_constexpr_null_ptr/ exercises
__is_constexpr(5) (constant, expected 1) and the non-ICE leaf kinds
__is_constexpr(argc) (symbol), __is_constexpr(*p) (dereference), and
__is_constexpr(nondet_int()) (call), all expected 0. All pass post-fix;
pre-fix the runtime assertion failed.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
extract/ansi-c-null-ptr-constant-cond
branch
from
9b5857f to
52988d1
Compare
Collaborator
Author
|
We need to consider to what extent this is trying to solve the same problem as #7959. |
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.
typecheck_expr_trinarydecides whether each pointer operand of a ternary is a null pointer constant by (a) simplifying the operand and (b) calling is_null_pointer() on the result. That misses the C-standard distinction between an integer constant expression with value 0 and a runtime expression that merely simplifies to 0: pre-fix, an operand like(long)(argc) * 0Lsimplified to 0 and CBMC treated the whole expression as a null pointer constant, even though argc is runtime.Consequence: the kernel's
__is_constexprmacro(sizeof(int) == sizeof(*(8 ? ((void *)((long)(x) * 0l))
: (int *)8)))
— which exploits exactly this distinction to select between compile-time and runtime branches of header-level static checks — returned 1 for every x on CBMC. Linux 6.x GENMASK_INPUT_CHECK and related idioms depend on it and broke kernel-TU compiles.
Fix: before treating the simplified operand as a null pointer constant, walk the PRE-simplification operand and confirm it contains no non-constant leaves. Any symbol read, side effect, function call, or dereference in the original expression disqualifies it from being an integer constant expression regardless of what it simplifies to. The check composes both directions: simplify-to-null + no-non-constant- leaves implies genuine null pointer constant.
Regression test: regression/cbmc/is_constexpr_null_ptr/ exercises __is_constexpr(5) (constant, expected 1) and __is_constexpr(argc) (runtime, expected 0). Both pass post-fix; pre-fix the runtime assertion failed.
Validated: all 98 CORE ctest entries pass (cbmc-CORE, ansi-c-gcc-CORE, ansi-c-clang-CORE, contracts-*, etc., including the ~2000 cbmc-CORE regression suites).
Also removes the now-redundant
__is_constexproverride from integration/linux/scan/fragments/scan-compat.h. Linux 6.12 crypto/algif_aead.c compiles end-to-end without the scan-compat workaround. The other scan-compat overrides (GENMASK_INPUT_CHECK, __cacheline_group_begin_aligned, __must_be_cstr) stay in place; they address separate kernel idioms.