From e9d3ac047a30256673f81f36b9970b52eacecf89 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 15:39:09 +0100 Subject: [PATCH] Fix pointer validity instrumentation for incomplete array types Use the same fall-back as is done for void pointers. Fixes: #8700 --- .../pointer-check-incomplete-array/main.c | 31 ++++++++++ .../pointer-check-incomplete-array/test.desc | 15 +++++ src/ansi-c/goto-conversion/goto_check_c.cpp | 58 ++++++++++++------- src/goto-instrument/contracts/utils.cpp | 16 ++++- 4 files changed, 98 insertions(+), 22 deletions(-) create mode 100644 regression/cbmc/pointer-check-incomplete-array/main.c create mode 100644 regression/cbmc/pointer-check-incomplete-array/test.desc diff --git a/regression/cbmc/pointer-check-incomplete-array/main.c b/regression/cbmc/pointer-check-incomplete-array/main.c new file mode 100644 index 00000000000..99d712c7f99 --- /dev/null +++ b/regression/cbmc/pointer-check-incomplete-array/main.c @@ -0,0 +1,31 @@ +// This test checks that dereferencing a pointer to an incomplete array type +// does not trigger an invariant violation. +// Related to issues #5293 and #4930 + +int (*a)[]; + +void b() +{ + *a; // This should not cause an invariant violation +} + +void c() +{ + int(*p)[]; + *p; // Another case with a local variable +} + +void test_pointer_arithmetic() +{ + int(*p)[] = a; + int(*q)[] = p + 1; // Pointer arithmetic on incomplete array type + int(*r)[] = q - 1; // Subtraction +} + +int main() +{ + b(); + c(); + test_pointer_arithmetic(); + return 0; +} diff --git a/regression/cbmc/pointer-check-incomplete-array/test.desc b/regression/cbmc/pointer-check-incomplete-array/test.desc new file mode 100644 index 00000000000..4b0b38747b2 --- /dev/null +++ b/regression/cbmc/pointer-check-incomplete-array/test.desc @@ -0,0 +1,15 @@ +CORE no-new-smt +main.c + +^\[b.pointer_dereference.1\] line 9 dereference failure: pointer NULL in \*a: FAILURE$ +^\[c.pointer_dereference.1\] line 15 dereference failure: pointer NULL in \*p: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +^Invariant check failed +-- +Test that dereferencing pointers to incomplete array types does not cause +invariant violations. diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 68c04604a94..06a8d58a3f7 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -1407,24 +1407,31 @@ void goto_check_ct::pointer_overflow_check( if(object_type.id() != ID_empty) { auto size_of_expr_opt = size_of_expr(object_type, ns); - CHECK_RETURN(size_of_expr_opt.has_value()); - exprt object_size = size_of_expr_opt.value(); - - const binary_exprt &binary_expr = to_binary_expr(expr); - exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer - ? binary_expr.rhs() - : binary_expr.lhs(); - mult_exprt mul{ - offset_operand, - typecast_exprt::conditional_cast(object_size, offset_operand.type())}; - mul.add_source_location() = offset_operand.source_location(); - - flag_overridet override_overflow(offset_operand.source_location()); - override_overflow.set_flag( - enable_signed_overflow_check, true, "signed_overflow_check"); - override_overflow.set_flag( - enable_unsigned_overflow_check, true, "unsigned_overflow_check"); - integer_overflow_check(mul, guard); + + // For incomplete types (e.g., incomplete arrays), we cannot perform + // overflow checking since the size is unknown. We skip the overflow check + // for such types. + if(size_of_expr_opt.has_value()) + { + exprt object_size = size_of_expr_opt.value(); + + const binary_exprt &binary_expr = to_binary_expr(expr); + exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer + ? binary_expr.rhs() + : binary_expr.lhs(); + mult_exprt mul{ + offset_operand, + typecast_exprt::conditional_cast(object_size, offset_operand.type())}; + mul.add_source_location() = offset_operand.source_location(); + + flag_overridet override_overflow(offset_operand.source_location()); + override_overflow.set_flag( + enable_signed_overflow_check, true, "signed_overflow_check"); + override_overflow.set_flag( + enable_unsigned_overflow_check, true, "unsigned_overflow_check"); + integer_overflow_check(mul, guard); + } + // else: incomplete type - cannot check overflow } // the result must be within object bounds or one past the end @@ -1467,8 +1474,19 @@ void goto_check_ct::pointer_validity_check( else { auto size_of_expr_opt = size_of_expr(expr.type(), ns); - CHECK_RETURN(size_of_expr_opt.has_value()); - size = size_of_expr_opt.value(); + + // For incomplete array types (e.g., when dereferencing int (*p)[]), + // size_of_expr returns an empty optional since the size is not known. In + // this case, we perform a minimal validity check similar to void pointers. + if(!size_of_expr_opt.has_value()) + { + // Cannot determine size for incomplete types; use minimal check + size = from_integer(1, size_type()); + } + else + { + size = size_of_expr_opt.value(); + } } auto conditions = get_pointer_dereferenceable_conditions(pointer, size); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index ecd6e779b72..c3666704cee 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -10,6 +10,7 @@ Date: September 2021 #include "utils.h" +#include #include #include #include @@ -179,9 +180,20 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns) if(auto deref = expr_try_dynamic_cast(expr)) { const auto size_of_expr_opt = size_of_expr(expr.type(), ns); - CHECK_RETURN(size_of_expr_opt.has_value()); - validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt}); + // For incomplete types (e.g., incomplete arrays), size_of_expr returns + // an empty optional. In such cases, we use a minimal size check. + if(size_of_expr_opt.has_value()) + { + validity_checks.push_back( + r_ok_exprt{deref->pointer(), *size_of_expr_opt}); + } + else + { + // Cannot determine size for incomplete types; use minimal size + validity_checks.push_back( + r_ok_exprt{deref->pointer(), from_integer(1, size_type())}); + } } for(const auto &op : expr.operands())