ansi-c: tighten null-pointer-constant check in conditional operator

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 <linux/bits.h>).  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;
+}

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.

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