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,11 @@
+#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 PTRDIFF_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 + PTRDIFF_MAX;
+}

regression/cbmc/pointer-overflow4/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-overflow-check
+^\[main.overflow.1\] line 10 arithmetic overflow on signed \* in (0x)?[0-9a-fA-F]+l* \* \(signed (long (long )?)?int\)4ul*: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_check_c.cpp

@@ -1343,6 +1343,32 @@ 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.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);
+  }
+
   // 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);