implicit_typecast_arithmetic must not assume types are bitvectors

We use Booleans instead of int as type of binary predicates, and enums
don't convert to bitvector types directly either. This must not preclude
mixing binary predicates with bitvector-typed expressions.

Fixes: #5103

Author: tautschnig

regression/ansi-c/int128_and_bool1/main.c

@@ -0,0 +1,6 @@
+int main(int argc, char *argv[])
+{
+  unsigned __int128 z;
+  z = (unsigned __int128)argc;
+  z += (argc < 1);
+}

regression/ansi-c/int128_and_bool1/test.desc

@@ -0,0 +1,7 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$

regression/cbmc/enum9/main.c

@@ -0,0 +1,25 @@
+#include <limits.h>
+
+enum E
+{
+  V1 = 1,
+  V2 = 2
+};
+
+struct B
+{
+  unsigned b : 2;
+};
+
+int main()
+{
+  unsigned __int128 int x;
+  __CPROVER_assume(x < (~(unsigned __int128)0) - 4);
+
+  enum E e;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assert(x + e > x, "long long plus enum");
+
+  struct B b;
+  __CPROVER_assert(x + b.b >= x, "long long plus bitfield");
+}

regression/cbmc/enum9/test.desc

@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
+^warning: ignoring

src/ansi-c/c_typecast.cpp

@@ -650,24 +650,8 @@ void c_typecastt::implicit_typecast_arithmetic(
 
   if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
   {
-    // get the biggest width of both
-    std::size_t width1 = to_bitvector_type(type1).get_width();
-    std::size_t width2 = to_bitvector_type(type2).get_width();
-
     // produce type
-    typet result_type;
-
-    if(width1==width2)
-    {
-      if(max_type==LARGE_SIGNED_INT)
-        result_type=signedbv_typet(width1);
-      else
-        result_type=unsignedbv_typet(width1);
-    }
-    else if(width1>width2)
-      result_type=type1;
-    else // width1<width2
-      result_type=type2;
+    typet result_type = (max_type == c_type1) ? type1 : type2;
 
     do_typecast(expr1, result_type);
     do_typecast(expr2, result_type);