Simplification of nested pointer arithmetic: do not assume same type

Pointer arithmetic is permitted with both signed and unsigned numeric
operands. Nested expressions could possibly mix this when the front-end
does not strictly use the same type for pointer arithmetic as for index
types. Observed in model-checking/kani#708.

Introducing type casts (as needed) exposed a further issue in this code:
it previously did not make sure that it was really the numeric operands
that ended up being grouped together. This became apparent on test
Pointer_Arithmetic15, which specifically constructs such expressions.

Author: tautschnig

regression/cbmc/Pointer_Arithmetic15/main.c

@@ -15,5 +15,9 @@ int main()
 
   a = p - q;
 
+  // mixing types: the C front-end will insert casts
+  unsigned long long u;
+  p = (p + a) + u;
+
   assert(0);
 }

src/util/simplify_expr_int.cpp

@@ -440,17 +440,21 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr)
       expr.op0().operands().size() == 2)
     {
       plus_exprt result = to_plus_expr(expr.op0());
+      if(as_const(result).op0().type().id() != ID_pointer)
+        result.op0().swap(result.op1());
       const exprt &op1 = as_const(result).op1();
 
       if(op1.id() == ID_plus)
       {
         plus_exprt new_op1 = to_plus_expr(op1);
-        new_op1.add_to_operands(expr.op1());
+        new_op1.add_to_operands(
+          typecast_exprt::conditional_cast(expr.op1(), new_op1.op0().type()));
         result.op1() = simplify_plus(new_op1);
       }
       else
       {
-        plus_exprt new_op1{op1, expr.op1()};
+        plus_exprt new_op1{
+          op1, typecast_exprt::conditional_cast(expr.op1(), op1.type())};
         result.op1() = simplify_plus(new_op1);
       }