From 206cf2a3f2fc2bf4a3070ac0234a70047ee9b021 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 14 Dec 2022 22:13:38 +0000
Subject: [PATCH] C front-end: reject pointer subtraction over distinct types

This is rejected by GCC, and we should equally refuse to process this.
---
 .../pointer_subtraction_diff_types.c                   | 10 ----------
 .../pointer_subtraction_diff_types.desc                | 10 ----------
 regression/cbmc/ptr_arithmetic_on_null/main.c          |  4 ++++
 regression/cbmc/ptr_arithmetic_on_null/test.desc       |  2 +-
 .../cbmc/ptr_arithmetic_on_null/type_conflict.desc     |  9 +++++++++
 src/ansi-c/c_typecheck_expr.cpp                        |  7 +++++--
 6 files changed, 19 insertions(+), 23 deletions(-)
 delete mode 100644 regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c
 delete mode 100644 regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc
 create mode 100644 regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc

diff --git a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c b/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c
deleted file mode 100644
index 1796cfd240b..00000000000
--- a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c
+++ /dev/null
@@ -1,10 +0,0 @@
-#include <stdlib.h>
-int main()
-{
-  int *x = malloc(sizeof(int));
-  float *y = x + 3;
-  int z = y - x;
-  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
-  __CPROVER_assert(z == 3, "expected successful after pointer manipulation");
-  __CPROVER_assert(z != 3, "expected failure after pointer manipulation");
-}
diff --git a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc b/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc
deleted file mode 100644
index 57cba47089b..00000000000
--- a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc
+++ /dev/null
@@ -1,10 +0,0 @@
-CORE
-pointer_subtraction_diff_types.c
---trace
-^Reason: only pointers of the same object type can be subtracted.
-^EXIT=(134|127)$
-^SIGNAL=0$
---
---
-This test is for making sure that we only subtract pointers with the
-same underlying (base) type.
diff --git a/regression/cbmc/ptr_arithmetic_on_null/main.c b/regression/cbmc/ptr_arithmetic_on_null/main.c
index 344c66b81a3..bbb7082c70c 100644
--- a/regression/cbmc/ptr_arithmetic_on_null/main.c
+++ b/regression/cbmc/ptr_arithmetic_on_null/main.c
@@ -12,7 +12,11 @@ void main()
   assert(NULL - NULL == 0);
 
   int *ptr;
+#ifdef MISSING_CAST
   assert(ptr - NULL == 0);
+#else
+  assert(ptr - (int *)NULL == 0);
+#endif
   ptr = NULL;
   assert((ptr - 1) + 1 == NULL);
 
diff --git a/regression/cbmc/ptr_arithmetic_on_null/test.desc b/regression/cbmc/ptr_arithmetic_on_null/test.desc
index b60f5bb3539..1e948bacd4a 100644
--- a/regression/cbmc/ptr_arithmetic_on_null/test.desc
+++ b/regression/cbmc/ptr_arithmetic_on_null/test.desc
@@ -5,7 +5,7 @@ main.c
 ^\[main.assertion.2\] line .* assertion \(void \*\)0 != \(void \*\)0 - \(.*\)1: SUCCESS$
 ^\[main.assertion.3\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)offset: SUCCESS$
 ^\[main.assertion.4\] line .* assertion \(void \*\)0 - \(void \*\)0 == \(.*\)0: SUCCESS$
-^\[main.assertion.5\] line .* assertion ptr - \(void \*\)0 == \(.*\)0: FAILURE$
+^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == \(.*\)0: FAILURE$
 ^\[main.assertion.6\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): SUCCESS$
 ^\[main.assertion.7\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): FAILURE$
 ^EXIT=10$
diff --git a/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc
new file mode 100644
index 00000000000..0f5cbf5fcea
--- /dev/null
+++ b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc
@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+-DMISSING_CAST
+pointer subtraction over different types
+CONVERSION ERROR
+^EXIT=6$
+^SIGNAL=0$
+--
+--
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 647b6817f58..b6fcddeaf1d 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -4171,8 +4171,11 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
     if(type0.id()==ID_pointer &&
        type1.id()==ID_pointer)
     {
-      // We should check the subtypes, and complain if
-      // they are really different.
+      if(type0 != type1)
+      {
+        throw invalid_source_file_exceptiont{
+          "pointer subtraction over different types", expr.source_location()};
+      }
       expr.type()=pointer_diff_type();
       typecheck_arithmetic_pointer(op0);
       typecheck_arithmetic_pointer(op1);