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,10 @@
+CORE
+main.c
+--pointer-overflow-check
+^\[main.overflow.1\] line 11 arithmetic overflow on signed \* in 0x7F+l* \* \(signed (long (long )?)?int\)4ul*: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/contracts/no_redudant_checks/test.desc

@@ -6,6 +6,7 @@ main.c
 ^\[malloc.assertion.1\].*: SUCCESS
 ^\[malloc.assertion.2\].*: SUCCESS
 ^\[main.overflow.1\].*: SUCCESS
+^\[main.overflow.2\].*: SUCCESS
 ^\[main.pointer_arithmetic.1\].*: SUCCESS
 ^\[main.pointer_arithmetic.2\].*: SUCCESS
 ^\[main.pointer_arithmetic.3\].*: SUCCESS
@@ -17,13 +18,14 @@ main.c
 ^\[main.pointer_arithmetic.9\].*: SUCCESS
 ^\[main.pointer_arithmetic.10\].*: SUCCESS
 ^\[main.pointer_arithmetic.11\].*: SUCCESS
+^\[main.overflow.3\].*: SUCCESS
 ^\[main.pointer_arithmetic.12\].*: SUCCESS
 ^\[main.pointer_arithmetic.13\].*: SUCCESS
 ^\[main.pointer_arithmetic.14\].*: SUCCESS
 ^\[main.pointer_arithmetic.15\].*: SUCCESS
 ^\[main.pointer_arithmetic.16\].*: SUCCESS
 ^\[main.pointer_arithmetic.17\].*: SUCCESS
-^\*\* 0 of 20 failed \(1 iterations\)
+^\*\* 0 of 22 failed \(1 iterations\)
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.overflow.\d+\].*: FAILURE

src/analyses/goto_check_c.cpp

@@ -1346,6 +1346,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_resett resetter(offset_operand.source_location());
+    resetter.set_flag(
+      enable_signed_overflow_check, true, "signed_overflow_check");
+    resetter.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);