Perform pointer validity checks when doing pointer arithmetic

Arithmetic over pointers requires that they point to valid objects (or
one past the end of an object).

The test uncovered two further problems: 1) there was a typo in
subtraction handling in bv_pointerst; 2) redundant assertions are
removed, even when they refer to different expressions.

Fixes: diffblue#5426

Author: tautschnig

regression/cbmc/pointer-overflow3/main.c

@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int) * 5);
+  int *p2 = p + 10; // undefined behavior for indexing out of bounds
+  int *p3 = p - 10; // undefined behavior for indexing out of bounds
+
+  int arr[5];
+  int *p4 = arr + 10; // undefined behavior for indexing out of bounds
+  int *p5 = arr - 10; // undefined behavior for indexing out of bounds
+  return 0;
+}

regression/cbmc/pointer-overflow3/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--pointer-overflow-check --no-simplify
+^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p + \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 8 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr + \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 12 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed
+--
+Uses --no-simplify to avoid removing repeated ASSERT FALSE statements.

src/analyses/goto_check.cpp

@@ -1172,6 +1172,21 @@ void goto_checkt::pointer_overflow_check(
     expr.find_source_location(),
     expr,
     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);
+
+  for(const auto &c : conditions)
+  {
+    add_guarded_property(
+      c.assertion,
+      "pointer arithmetic: " + c.description,
+      "pointer arithmetic",
+      expr.find_source_location(),
+      expr,
+      guard);
+  }
 }
 
 void goto_checkt::pointer_validity_check(

src/solvers/flattening/bv_pointers.cpp

@@ -506,7 +506,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     const bvt &bv = convert_bv(minus_expr.lhs());
 
-    typet pointer_sub_type = minus_expr.rhs().type().subtype();
+    typet pointer_sub_type = minus_expr.lhs().type().subtype();
     mp_integer element_size;
 
     if(pointer_sub_type.id()==ID_empty)