From 49481e272718ee34d4580d0ed55de969a0b5e50a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 19 Feb 2021 23:06:05 +0000
Subject: [PATCH] Pointer arithmetic check: do not use pointer-to-int
 conversion

We do not currently have a sound pointer-to-int conversion, and thus
arithmetic involving pointers and integers does not translate to
arithmetic over the integer representation of a pointer.

With the recently added bounds checks on pointers involved in arithmetic
we have a more reliable way of testing for overflow in pointer
arithmetic.
---
 regression/cbmc-library/getenv-01/test.desc |  2 +-
 regression/cbmc/pointer-overflow1/test.desc | 10 ++++++----
 regression/cbmc/pointer-overflow2/test.desc |  8 ++++----
 src/analyses/goto_check.cpp                 | 16 ----------------
 4 files changed, 11 insertions(+), 25 deletions(-)

diff --git a/regression/cbmc-library/getenv-01/test.desc b/regression/cbmc-library/getenv-01/test.desc
index 1e96fe8b0db..babdd9fd78e 100644
--- a/regression/cbmc-library/getenv-01/test.desc
+++ b/regression/cbmc-library/getenv-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---signed-overflow-check --unsigned-overflow-check
+--signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --pointer-check --bounds-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc
index fedee95fa1a..f075fb98df5 100644
--- a/regression/cbmc/pointer-overflow1/test.desc
+++ b/regression/cbmc/pointer-overflow1/test.desc
@@ -3,12 +3,14 @@ main.c
 --pointer-overflow-check --unsigned-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.overflow\.\d+\] line 8 (pointer )?arithmetic overflow on .*: FAILURE
-^\[main\.overflow\.\d+\] line 9 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 8 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 9 pointer arithmetic: pointer outside dynamic object bounds in .*: 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
+^\[main\.pointer_arithmetic\.\d+\] line 10 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 11 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 12 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
 ^VERIFICATION FAILED$
 --
 ^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
+^\[main\.overflow\.\d+\] line 1[45] pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
 ^warning: ignoring
diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc
index 090e350f3cd..29f2ee235f8 100644
--- a/regression/cbmc/pointer-overflow2/test.desc
+++ b/regression/cbmc/pointer-overflow2/test.desc
@@ -3,9 +3,9 @@ main.c
 --pointer-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.overflow.1\] line \d+ pointer arithmetic overflow on - in p - \(signed long (long )?int\)1: SUCCESS
-\[main.overflow.2\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long (long )?int\)1: SUCCESS
-\[main.overflow.3\] line \d+ pointer arithmetic overflow on \+ in p \+ \(signed long (long )?int\)-1: SUCCESS
-\[main.overflow.4\] line \d+ pointer arithmetic overflow on - in p - \(signed long (long )?int\)-1: SUCCESS
+\[main.pointer_arithmetic.1\] line \d+ pointer arithmetic: invalid integer address in p - \(signed long (long )?int\)1: SUCCESS
+\[main.pointer_arithmetic.2\] line \d+ pointer arithmetic: invalid integer address in p \+ \(signed long (long )?int\)1: SUCCESS
+\[main.pointer_arithmetic.3\] line \d+ pointer arithmetic: invalid integer address in p \+ \(signed long (long )?int\)-1: SUCCESS
+\[main.pointer_arithmetic.4\] line \d+ pointer arithmetic: invalid integer address in p - \(signed long (long )?int\)-1: SUCCESS
 --
 ^warning: ignoring
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 55169428900..1d97aaee439 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1177,22 +1177,6 @@ void goto_checkt::pointer_overflow_check(
     expr.operands().size() == 2,
     "pointer arithmetic expected to have exactly 2 operands");
 
-  // check for address space overflow by checking for overflow on integers
-  exprt overflow("overflow-" + expr.id_string(), bool_typet());
-  for(const auto &op : expr.operands())
-  {
-    overflow.add_to_operands(
-      typecast_exprt::conditional_cast(op, pointer_diff_type()));
-  }
-
-  add_guarded_property(
-    not_exprt(overflow),
-    "pointer arithmetic overflow on " + expr.id_string(),
-    "overflow",
-    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);