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: #5426

Author: tautschnig

regression/cbmc/pointer-overflow1/main.c

@@ -11,8 +11,8 @@ int main()
   p2 = p - other1;
   p2 = p - other2 - other1;
 
-  p2 = p + sizeof(int);
-  p2 = p + sizeof(int) + sizeof(int);
+  p2 = (char *)p + sizeof(int);
+  p2 = (char *)p + sizeof(int) + sizeof(int);
 
   return 0;
 }

regression/cbmc/pointer-overflow1/test.desc

@@ -3,9 +3,12 @@ main.c
 --pointer-overflow-check --unsigned-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS
+^\[main\.overflow\.\d+\] line 8 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 9 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 10 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 11 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 12 (pointer )?arithmetic overflow on .*: FAILURE
 ^VERIFICATION FAILED$
-^\*\* 8 of 13 failed
 --
-^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
+^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring

regression/cbmc/pointer-overflow2/main.c

@@ -2,9 +2,10 @@
 
 void main()
 {
+  __CPROVER_allocated_memory(9, sizeof(char));
   char *p = (char *)10;
   p -= 1;
   p += 1;
-  p += -1; // spurious pointer overflow report
-  p -= -1; // spurious pointer overflow report
+  p += -1; // previously: spurious pointer overflow report
+  p -= -1; // previously: spurious pointer overflow report
 }

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 broken-smt-backend
+main.c
+--pointer-overflow-check --no-simplify
+^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[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 10 pointer arithmetic: pointer outside object bounds in arr \+ \(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
+^\*\* 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

@@ -286,8 +286,12 @@ class goto_checkt
 void goto_checkt::collect_allocations(
   const goto_functionst &goto_functions)
 {
-  if(!enable_pointer_check && !enable_bounds_check)
+  if(
+    !enable_pointer_check && !enable_bounds_check &&
+    !enable_pointer_overflow_check)
+  {
     return;
+  }
 
   for(const auto &gf_entry : goto_functions.function_map)
   {
@@ -1172,6 +1176,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)