Merge pull request #6324 from diffblue/overflow_unsigned_unary_minus

Check overflow on unsigned unary minus

Author: kroening

regression/cbmc/Overflow_Multiplication1/falsealarm.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+leftshift_overflow.c
 --signed-overflow-check --c89
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Leftshift1/test-c89.desc renamed to regression/cbmc/overflow/leftshift_overflow-c89.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+leftshift_overflow.c
 --signed-overflow-check --c99
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Leftshift1/test-c99.desc renamed to regression/cbmc/overflow/leftshift_overflow-c99.desc

@@ -8,10 +8,10 @@ int main()
   unsigned r = x << ((sizeof(unsigned) - 1) * 8 + 1);
 
   // signed, owing to promotion, and cannot overflow
-  r=x << ((sizeof(unsigned)-1)*8-1);
+  r = x << ((sizeof(unsigned) - 1) * 8 - 1);
 
   // unsigned
-  r=(unsigned)x << ((sizeof(unsigned)-1)*8);
+  r = (unsigned)x << ((sizeof(unsigned) - 1) * 8);
 
   // negative value or zero, not an overflow
   int s = -x << ((sizeof(int) - 1) * 8);

regression/cbmc/Overflow_Leftshift1/main.c renamed to regression/cbmc/overflow/leftshift_overflow.c

@@ -1,7 +1,8 @@
-int main() {
+int main()
+{
   signed int i, j;
 
-  i=j;
+  i = j;
 
   i++;
 }

regression/cbmc/Overflow_Addition1/main.c renamed to regression/cbmc/overflow/signed_addition_overflow1.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow1.c
 --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition1/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow1.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow2.c
 --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition2/main.c renamed to regression/cbmc/overflow/signed_addition_overflow2.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow3.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition2/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow2.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow4.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition3/main.c renamed to regression/cbmc/overflow/signed_addition_overflow3.c

@@ -0,0 +1,16 @@
+// From Cousot's FMSD paper
+
+void main()
+{
+  int x, y, _x, _y;
+
+  x = _x;
+  y = _y;
+
+  if(
+    (-4681 < y) && (y < 4681) && (x < 32767) && (-32767 < x) &&
+    ((7 * y * y - 1) == x * x))
+  {
+    y = 1 / x;
+  }
+}

regression/cbmc/Overflow_Addition3/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow3.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_multiplication1.c
 --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition4/main.c renamed to regression/cbmc/overflow/signed_addition_overflow4.c

@@ -1,19 +1,19 @@
-#define INT_MIN (-1<<(sizeof(int)*8-1))
+#define INT_MIN (-1 << (sizeof(int) * 8 - 1))
 
 int main()
 {
   int a, b, neg;
 
   // this should not overflow, even not for a=INT_MIN
-  b=a-a;
+  b = a - a;
 
   // this should also not overflow as long as pos<0
-  if(neg<0)
-    b=neg-INT_MIN;
+  if(neg < 0)
+    b = neg - INT_MIN;
 
   int x, y, z;
 
-  x = INT_MIN+1;
+  x = INT_MIN + 1;
   y = INT_MIN;
-  z = x-y; // neither
+  z = x - y; // neither
 }

regression/cbmc/Overflow_Addition4/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow4.desc

@@ -1,5 +1,5 @@
 CORE
-falsealarm.c
+signed_subtraction1.c
 --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/overflow/signed_multiplication1.c

@@ -0,0 +1,22 @@
+#include <limits.h>
+
+int main()
+{
+  signed int x, y;
+
+  x = INT_MIN;
+
+  // this is an overflow
+  y = -x;
+
+  // ok
+  x = -(x + 1);
+
+  unsigned a, b;
+
+  a = 1;
+  a = -a; // overflow, -1 is not representable
+
+  b = 0;
+  b = -b; // ok
+}

regression/cbmc/Overflow_Subtraction1/test.desc renamed to regression/cbmc/overflow/signed_multiplication1.desc

@@ -0,0 +1,10 @@
+CORE
+unary_minus_overflow.c
+--signed-overflow-check --unsigned-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] line .* arithmetic overflow on signed unary minus in -x: FAILURE$
+^\[.*\] line .* arithmetic overflow on signed unary minus in -\(x \+ 1\): SUCCESS$
+^\[.*\] line .* arithmetic overflow on unsigned unary minus in -a: SUCCESS$
+^\[.*\] line .* arithmetic overflow on unsigned unary minus in -b: FAILURE$
+--

regression/cbmc/Overflow_Subtraction1/main.c renamed to regression/cbmc/overflow/signed_subtraction1.c

@@ -734,8 +734,8 @@ void goto_checkt::integer_overflow_check(
   {
     if(type.id()==ID_signedbv)
     {
-      // overflow on unary- can only happen with the smallest
-      // representable number 100....0
+      // overflow on unary- on signed integers can only happen with the
+      // smallest representable number 100....0
 
       equal_exprt int_min_eq(
         to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
@@ -748,6 +748,22 @@ void goto_checkt::integer_overflow_check(
         expr,
         guard);
     }
+    else if(type.id() == ID_unsignedbv)
+    {
+      // Overflow on unary- on unsigned integers happens for all operands
+      // that are not zero.
+
+      notequal_exprt not_eq_zero(
+        to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
+
+      add_guarded_property(
+        not_eq_zero,
+        "arithmetic overflow on unsigned unary minus",
+        "overflow",
+        expr.find_source_location(),
+        expr,
+        guard);
+    }
 
     return;
   }