From 52988d14a81eaebb42869faec305fa281f0fb509 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 May 2026 23:40:33 +0000 Subject: [PATCH] ansi-c: tighten null-pointer-constant check in conditional operator MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 --- regression/cbmc/is_constexpr_null_ptr/main.c | 45 ++++++++++++++ .../cbmc/is_constexpr_null_ptr/test.desc | 16 +++++ src/ansi-c/c_typecheck_expr.cpp | 61 ++++++++++++++++++- 3 files changed, 120 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/is_constexpr_null_ptr/main.c create mode 100644 regression/cbmc/is_constexpr_null_ptr/test.desc diff --git a/regression/cbmc/is_constexpr_null_ptr/main.c b/regression/cbmc/is_constexpr_null_ptr/main.c new file mode 100644 index 00000000000..6f5753718e6 --- /dev/null +++ b/regression/cbmc/is_constexpr_null_ptr/main.c @@ -0,0 +1,45 @@ +// Regression test for the conditional-operator null-pointer- +// constant check (see src/ansi-c/c_typecheck_expr.cpp: +// typecheck_expr_trinary). Before the fix, the type checker +// simplified each operand before calling is_null_pointer(), +// which treated `(void *)((long)argc * 0L)` as a null pointer +// constant — even though the ORIGINAL expression is not an +// integer constant expression (argc is runtime). +// +// The Linux kernel's `__is_constexpr` macro exploits exactly +// this distinction to select between compile-time and runtime +// branches in header-level static checks (e.g. GENMASK_INPUT_ +// CHECK in ). Pre-fix, CBMC reported +// __is_constexpr(x) == 1 for every x and broke 6.x kernel +// TU compiles. See LIM-014 in integration/linux/CBMC_ +// LIMITATIONS.md. + +#define __is_constexpr(x) \ + (sizeof(int) == sizeof(*(8 ? ((void *)((long)(x)*0l)) : (int *)8))) + +int nondet_int(void); + +int main(int argc, char **argv) +{ + // Compile-time constant: the conditional's first branch IS a + // null pointer constant, so the type is `int *`; dereferenced + // is int; sizeof(int) == sizeof(int) is true. + __CPROVER_assert(__is_constexpr(5) == 1, "constant is ICE"); + + // Runtime value: the conditional's first branch is NOT an + // integer constant expression, so the type degenerates to + // `void *`; dereferenced is `void`; sizeof(void) != sizeof(int) + // so the macro returns 0. + __CPROVER_assert(__is_constexpr(argc) == 0, "runtime is not ICE"); + + // A dereference is likewise not an ICE leaf (the operand lives + // inside sizeof, so *p is never evaluated): macro yields 0. + int *p = &argc; + __CPROVER_assert(__is_constexpr(*p) == 0, "dereference is not ICE"); + + // A function call is not an ICE leaf either (also unevaluated + // inside sizeof): macro yields 0. + __CPROVER_assert(__is_constexpr(nondet_int()) == 0, "call is not ICE"); + + return 0; +} diff --git a/regression/cbmc/is_constexpr_null_ptr/test.desc b/regression/cbmc/is_constexpr_null_ptr/test.desc new file mode 100644 index 00000000000..30c3b12668e --- /dev/null +++ b/regression/cbmc/is_constexpr_null_ptr/test.desc @@ -0,0 +1,16 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +LIM-014 regression: the conditional-operator typechecker +distinguishes an ORIGINAL integer constant expression with +value 0 from a runtime expression that merely simplifies to 0. +The Linux kernel's __is_constexpr macro depends on this +distinction. Pre-fix, CBMC reported __is_constexpr(x) == 1 +for both x=5 and x=argc; this test requires 1 and 0 +respectively. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index afc0f3ca884..d71b96a4109 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1688,17 +1688,74 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr) exprt tmp1=simplify_expr(operands[1], *this); exprt tmp2=simplify_expr(operands[2], *this); + // C standard: a "null pointer constant" is an integer + // constant expression (ICE) with value 0, or such an + // expression cast to `void *`. An ICE does not contain + // any non-constant leaves (variable reads, function calls, + // …), so `(long)argc * 0L`, while it simplifies to 0, is + // NOT a null pointer constant even though simplification + // masks that. The __is_constexpr kernel macro exploits + // this exact distinction: + // + // sizeof(int) == sizeof(*(8 ? ((void *)((long)(x) * 0l)) + // : (int *)8)) + // + // and relies on the compiler treating the first branch as + // `void *` (non-null-ptr-const) when x is runtime, making + // the conditional's type `void *` and the sizeof of its + // dereference differ from sizeof(int). Previously CBMC + // simplified before checking, losing the distinction and + // misreporting runtime `x` as constant. The helper below + // walks the PRE-simplification operand looking for any + // symbol read; we only recognise the operand as a null + // pointer constant if it is both (a) a constant after + // simplification and (b) free of non-constant leaves + // originally. + // + // The leaf-scan is a sound proxy for "not an ICE" here only + // because by this point sizeof/_Alignof have been folded to + // constants and enumeration constants resolved via + // follow_macros; the only remaining leaves are genuinely + // non-ICE constructs (variable reads, dereferences, calls, + // side effects). A const-qualified local is also correctly + // rejected, as it is not an ICE in C. + const auto contains_non_constant_leaf = [](const exprt &e) + { + return has_subexpr( + e, + [](const exprt &sub) + { + return sub.id() == ID_symbol || sub.id() == ID_side_effect || + sub.id() == ID_function_application || + sub.id() == ID_dereference; + }); + }; + + // an operand is a null pointer constant if it is null after + // simplification AND was an integer constant expression originally (i.e. + // free of non-constant leaves) + const auto is_null_pointer_constant = + [&](const exprt &original, const exprt &simplified) + { + return simplified.is_constant() && + to_constant_expr(simplified).is_null_pointer() && + !contains_non_constant_leaf(original); + }; + + const bool op1_ice_zero = is_null_pointer_constant(operands[1], tmp1); + const bool op2_ice_zero = is_null_pointer_constant(operands[2], tmp2); + // is one of them void * AND null? Convert that to the other. // (at least that's how GCC behaves) if( to_pointer_type(operands[1].type()).base_type().id() == ID_empty && - tmp1.is_constant() && to_constant_expr(tmp1).is_null_pointer()) + op1_ice_zero) { implicit_typecast(operands[1], operands[2].type()); } else if( to_pointer_type(operands[2].type()).base_type().id() == ID_empty && - tmp2.is_constant() && to_constant_expr(tmp2).is_null_pointer()) + op2_ice_zero) { implicit_typecast(operands[2], operands[1].type()); }