From 59a3c2a24eb539cb6378c89eb34a68f2dcdca396 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 17 Jan 2021 00:19:06 +0000
Subject: [PATCH] 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
---
 regression/ansi-c/int128_and_bool1/main.c    |  6 +++++
 regression/ansi-c/int128_and_bool1/test.desc |  7 ++++++
 regression/cbmc/enum9/main.c                 | 25 ++++++++++++++++++++
 regression/cbmc/enum9/test.desc              |  9 +++++++
 src/ansi-c/c_typecast.cpp                    | 18 +-------------
 5 files changed, 48 insertions(+), 17 deletions(-)
 create mode 100644 regression/ansi-c/int128_and_bool1/main.c
 create mode 100644 regression/ansi-c/int128_and_bool1/test.desc
 create mode 100644 regression/cbmc/enum9/main.c
 create mode 100644 regression/cbmc/enum9/test.desc

diff --git a/regression/ansi-c/int128_and_bool1/main.c b/regression/ansi-c/int128_and_bool1/main.c
new file mode 100644
index 00000000000..f050c46c24f
--- /dev/null
+++ b/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);
+}
diff --git a/regression/ansi-c/int128_and_bool1/test.desc b/regression/ansi-c/int128_and_bool1/test.desc
new file mode 100644
index 00000000000..d9d5bdfa642
--- /dev/null
+++ b/regression/ansi-c/int128_and_bool1/test.desc
@@ -0,0 +1,7 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
diff --git a/regression/cbmc/enum9/main.c b/regression/cbmc/enum9/main.c
new file mode 100644
index 00000000000..2b9a61c3698
--- /dev/null
+++ b/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");
+}
diff --git a/regression/cbmc/enum9/test.desc b/regression/cbmc/enum9/test.desc
new file mode 100644
index 00000000000..245d2eacb1b
--- /dev/null
+++ b/regression/cbmc/enum9/test.desc
@@ -0,0 +1,9 @@
+CORE gcc-only
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$
+^warning: ignoring
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 8092ac457c5..d6899f9261a 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/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);