Merge pull request #6186 from tautschnig/overflow-check

Fix distance check in overflow checking of left shift

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)u32) << 32;
+
   return 0;
 }

regression/cbmc/Overflow_Leftshift1/test-c89.desc

@@ -3,14 +3,15 @@ main.c
 --signed-overflow-check --c89
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$
-^\[.*\] 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 8 arithmetic overflow on signed shl in .*: FAILURE$
+^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$
+^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$
+^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$
+^\[.*\] line 30 arithmetic overflow on signed shl in .*: SUCCESS$
+^\*\* 2 of 6 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
-^\[.*\] line 12 arithmetic overflow on signed shl in .*: .*
-^\[.*\] line 21 arithmetic overflow on signed shl in .*: .*
-^\[.*\] line 24 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 14 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 23 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 26 arithmetic overflow on signed shl in .*: .*

regression/cbmc/Overflow_Leftshift1/test-c99.desc

@@ -3,14 +3,15 @@ main.c
 --signed-overflow-check --c99
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$
-^\[.*\] 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$
-^\[.*\] line 24 arithmetic overflow on signed shl in .*: FAILURE$
-^\*\* 3 of 6 failed
+^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$
+^\[.*\] line 11 arithmetic overflow on signed shl in .*: SUCCESS$
+^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$
+^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$
+^\[.*\] line 26 arithmetic overflow on signed shl in .*: FAILURE$
+^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$
+^\*\* 4 of 7 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
-^\[.*\] line 12 arithmetic overflow on signed shl in .*: .*
-^\[.*\] line 21 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 14 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 23 arithmetic overflow on signed shl in .*: .*

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