Fix distance check in overflow checking of left shift

The code wrongly compared the shift operand when checking against
negative shifts.

Author: tautschnig

regression/cbmc/Overflow_Leftshift1/main.c

@@ -1,3 +1,5 @@
+#include <inttypes.h>
+
 int main()
 {
   unsigned char x;
@@ -23,5 +25,9 @@ int main()
   // not an overflow in ANSI-C, but undefined in C99
   s = 1 << (sizeof(int) * 8 - 1);
 
+  // overflow in an expression where operand and distance types are different
+  uint32_t u32;
+  int64_t i64 = (int64_t)upper << 32;
+
   return 0;
 }

regression/cbmc/Overflow_Leftshift1/test-c89.desc

@@ -7,7 +7,8 @@ main.c
 ^\[.*\] line 9 arithmetic overflow on signed shl in .*: SUCCESS$
 ^\[.*\] line 15 arithmetic overflow on signed shl in .*: SUCCESS$
 ^\[.*\] line 18 arithmetic overflow on signed shl in .*: FAILURE$
-^\*\* 2 of 5 failed
+^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$
+^\*\* 3 of 6 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Overflow_Leftshift1/test-c99.desc

@@ -8,7 +8,8 @@ main.c
 ^\[.*\] line 15 arithmetic overflow on signed shl in .*: SUCCESS$
 ^\[.*\] line 18 arithmetic overflow on signed shl in .*: FAILURE$
 ^\[.*\] line 24 arithmetic overflow on signed shl in .*: FAILURE$
-^\*\* 3 of 6 failed
+^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$
+^\*\* 4 of 7 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/analyses/goto_check.cpp

@@ -777,8 +777,10 @@ void goto_checkt::integer_overflow_check(
       if(distance_type.id() == ID_unsignedbv)
         neg_dist_shift = false_exprt();
       else
-        neg_dist_shift =
-          binary_relation_exprt(op, ID_lt, from_integer(0, distance_type));
+      {
+        neg_dist_shift = binary_relation_exprt(
+          distance, ID_lt, from_integer(0, distance_type));
+      }
 
       // shifting a non-zero value by more than its width is undefined;
       // yet this isn't an overflow