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()); }