Merge pull request #9461 from tautschnig/pr/void-pointer-arithmetic-type

C front end: arithmetic on void * yields a void *

Author: kroening

regression/cbmc/ptr_arithmetic_on_null/test.desc

@@ -1,9 +1,9 @@
 CORE gcc-only
 main.c
 
-^\[main.assertion.1\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ (\(.*\))?1: SUCCESS$
-^\[main.assertion.2\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 - (\(.*\))?1: SUCCESS$
-^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)offset: SUCCESS$
+^\[main.assertion.1\] line .* assertion \(void \*\)0 != \(void \*\)\(\(char \*\)\(void \*\)0 \+ (\(.*\))?1\): SUCCESS$
+^\[main.assertion.2\] line .* assertion \(void \*\)0 != \(void \*\)\(\(char \*\)\(void \*\)0 - (\(.*\))?1\): SUCCESS$
+^\[main.assertion.3\] line .* assertion \(void \*\)0 != \(void \*\)\(\(char \*\)\(void \*\)0 \+ \(.*\)offset\): SUCCESS$
 ^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == (\(.*\))?0: UNKNOWN$
 ^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == (\(.*\))?0: FAILURE$
 ^\[main.assertion.6\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): UNKNOWN$

regression/cbmc/void_pointer_arithmetic_type/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+// GCC computes arithmetic on void * with a size of 1, and the result is a
+// void * (GCC manual, "Arithmetic on void- and Function-Pointers").  Linux
+// 5.10's ethtool_get_any_eeprom subtracts `useraddr + sizeof(eeprom)' from a
+// void *, which goto-cc rejected ("pointer subtraction over different
+// types"): void * + integer was typed char *.
+int main()
+{
+  char buf[16];
+  void *a = buf + 12, *b = buf;
+  assert(a - (b + 8) == 4);
+  assert((b + 8) - a == -4);
+  assert(a - (8 + b) == 4);
+  void *c = b;
+  c += 4;
+  assert(c == buf + 4);
+  c -= 2;
+  assert(c == buf + 2);
+  assert(sizeof(b + 1) == sizeof(void *));
+  assert(a - (b + 8) == 5);
+  return 0;
+}

regression/cbmc/void_pointer_arithmetic_type/test.desc

@@ -0,0 +1,12 @@
+CORE gcc-only
+main.c
+
+^\[main\.assertion\.7\] line \d+ assertion a - \(b \+ 8\) == 5: FAILURE$
+^\*\* 1 of \d+ failed
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+pointer subtraction over different types
+--
+The other assertions hold.

src/ansi-c/c_typecheck_expr.cpp

@@ -4398,6 +4398,25 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(exprt &expr)
   }
 }
 
+/// GCC's arithmetic on `void *' (an extension, "Pointer Arith" in the GCC
+/// manual) computes with a size of 1, and the result has the pointer's type:
+/// `p + 8' for a `void *' p is a `void *'.  typecheck_arithmetic_pointer
+/// computes it on `char *'; cast the result \p expr of the pointer
+/// arithmetic back to \p pointer_type, the type of the pointer operand.  A
+/// compound assignment (`p += 8') is cast by the assignment itself.
+static void keep_void_pointer_type(exprt &expr, const typet &pointer_type)
+{
+  if(
+    expr.id() == ID_side_effect ||
+    to_pointer_type(pointer_type).base_type().id() != ID_empty ||
+    expr.type() == pointer_type)
+  {
+    return;
+  }
+  typecast_exprt result{expr, pointer_type};
+  expr.swap(result);
+}
+
 void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
 {
   auto &binary_expr = to_binary_expr(expr);
@@ -4432,9 +4451,11 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
         type1.id()==ID_c_bit_field ||
         type1.id()==ID_c_enum_tag))
     {
+      const typet pointer_type = type0;
       typecheck_arithmetic_pointer(op0);
       make_index_type(op1);
       expr.type() = op0.type();
+      keep_void_pointer_type(expr, pointer_type);
       return;
     }
   }
@@ -4468,9 +4489,11 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
        int_op_type.id()==ID_c_bit_field ||
        int_op_type.id()==ID_c_enum_tag)
     {
+      const typet pointer_type = p_op->type();
       typecheck_arithmetic_pointer(*p_op);
       make_index_type(*int_op);
       expr.type()=p_op->type();
+      keep_void_pointer_type(expr, pointer_type);
       return;
     }
   }