Pointer overflow checks should detect overflow in offset multiplication

Pointer arithmetic requires multiplication of the offset by the size of
the base type (for any base type larger than 1 byte). Such a
multiplication isn't introduced until the back-end, where no opportunity
for adding properties exists anymore. Therefore, synthesize the
multiplication to generate arithmetic overflow checks at the GOTO level.

Fixes: #6631

Author: tautschnig

regression/cbmc/pointer-overflow4/main.c

@@ -0,0 +1,12 @@
+#include <limits.h>
+#include <stdint.h>
+
+int main()
+{
+	int32_t i[5];
+  // Offset 1 resulted in spuriously failing to detect an overflow in pointer
+  // arithmetic in the next line for SSIZE_MAX * 4 + 4 = 0 in wrap-around
+  // semantics. Any other offset would yield the expected failure.
+	int32_t *p = &i[1];
+	int32_t*q = p + SSIZE_MAX;
+}

regression/cbmc/pointer-overflow4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-overflow-check
+^\[main.pointer_arithmetic.2\] line 11 pointer arithmetic: pointer outside object bounds in p + 0x7FFFFFFFFFFFFFFFl: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check_c.cpp

@@ -1270,6 +1270,27 @@ void goto_check_ct::pointer_overflow_check(
     expr.operands().size() == 2,
     "pointer arithmetic expected to have exactly 2 operands");
 
+  // multiplying the offset by the object size must not result in arithmetic
+  // overflow
+  const typet &object_type = to_pointer_type(expr.type()).base_type();
+  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.source_location() = offset_operand.source_location();
+
+  flag_resett resetter(i);
+  resetter.set_flag(enable_signed_overflow_check, true, "no_enum_check");
+  resetter.set_flag(enable_unsigned_overflow_check, true, "no_enum_check");
+    integer_overflow_check(mul, guard);
+  }
+
   // the result must be within object bounds or one past the end
   const auto size = from_integer(0, size_type());
   auto conditions = get_pointer_dereferenceable_conditions(expr, size);