Merge pull request #1528 from tautschnig/shl-overflow

Check for overflow on left shift of signed ints

Author: Daniel Kroening

regression/cbmc/Overflow_Leftshift1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  unsigned char x;
+  unsigned r=x << ((sizeof(unsigned)-1)*8);
+  r=x << ((sizeof(unsigned)-1)*8-1);
+  r=(unsigned)x << ((sizeof(unsigned)-1)*8);
+
+  int s=-1 << ((sizeof(int)-1)*8);
+  s=-256 << ((sizeof(int)-1)*8);
+  return 0;
+}

regression/cbmc/Overflow_Leftshift1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--signed-overflow-check
+^SIGNAL=0$
+^\[.*\] arithmetic overflow on signed shl in .*: FAILURE$
+^\*\* 2 of 4 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/Undefined_Shift1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  unsigned char x;
+  unsigned r=x << ((sizeof(unsigned)-1)*8);
+  r=x << ((sizeof(unsigned)-1)*8-1);
+  r=(unsigned)x << ((sizeof(unsigned)-1)*8);
+
+  int s=-1 << ((sizeof(int)-1)*8);
+  s=-256 << ((sizeof(int)-1)*8);
+  return 0;
+}

regression/cbmc/Undefined_Shift1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--undefined-shift-check
+^SIGNAL=0$
+^\[.*\] shift operand is negative in .*: FAILURE$
+^\*\* 1 of 2 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -286,6 +286,30 @@ void goto_checkt::undefined_shift_check(
       expr.find_source_location(),
       expr,
       guard);
+
+    if(op_type.id()==ID_signedbv && expr.id()==ID_shl)
+    {
+      binary_relation_exprt inequality(
+        expr.op(), ID_ge, from_integer(0, op_type));
+
+      add_guarded_claim(
+        inequality,
+        "shift operand is negative",
+        "undefined-shift",
+        expr.find_source_location(),
+        expr,
+        guard);
+    }
+  }
+  else
+  {
+    add_guarded_claim(
+      false_exprt(),
+      "shift of non-integer type",
+      "undefined-shift",
+      expr.find_source_location(),
+      expr,
+      guard);
   }
 }
 
@@ -1418,6 +1442,9 @@ void goto_checkt::check_rec(
   else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
   {
     undefined_shift_check(to_shift_expr(expr), guard);
+
+    if(expr.id()==ID_shl && expr.type().id()==ID_signedbv)
+      integer_overflow_check(expr, guard);
   }
   else if(expr.id()==ID_mod)
   {

src/solvers/flattening/boolbv_overflow.cpp

@@ -8,8 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <cassert>
-
+#include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/string2int.h>
 
@@ -59,7 +58,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     if(operands[0].type()!=operands[1].type())
       throw "operand type mismatch on overflow-*";
 
-    assert(bv0.size()==bv1.size());
+    DATA_INVARIANT(bv0.size()==bv1.size(), "operands size mismatch");
     std::size_t old_size=bv0.size();
     std::size_t new_size=old_size*2;
 
@@ -86,7 +85,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)
       bv_overflow.reserve(old_size);
 
       // get top result bits, plus one more
-      assert(old_size!=0);
+      DATA_INVARIANT(old_size!=0, "zero-size operand");
       for(std::size_t i=old_size-1; i<result.size(); i++)
         bv_overflow.push_back(result[i]);
 
@@ -96,6 +95,72 @@ literalt boolbvt::convert_overflow(const exprt &expr)
       return !prop.lor(all_one, all_zero);
     }
   }
+  else if(expr.id() == ID_overflow_shl)
+  {
+    if(operands.size() != 2)
+      throw "operator " + expr.id_string() + " takes two operands";
+
+    const bvt &bv0=convert_bv(operands[0]);
+    const bvt &bv1=convert_bv(operands[1]);
+
+    std::size_t old_size = bv0.size();
+    std::size_t new_size = old_size * 2;
+
+    bv_utilst::representationt rep=
+      operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
+                                           bv_utilst::representationt::UNSIGNED;
+
+    bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
+
+    bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::LEFT, bv1);
+
+    // a negative shift is undefined; yet this isn't an overflow
+    literalt neg_shift =
+      operands[1].type().id() == ID_unsignedbv ?
+        const_literal(false) :
+        bv1.back(); // sign bit
+
+    // an undefined shift of a non-zero value always results in overflow; the
+    // use of unsigned comparision is safe here as we cover the signed negative
+    // case via neg_shift
+    literalt undef =
+      bv_utils.rel(
+        bv1,
+        ID_gt,
+        bv_utils.build_constant(old_size, bv1.size()),
+        bv_utilst::representationt::UNSIGNED);
+
+    literalt overflow;
+
+    if(rep == bv_utilst::representationt::UNSIGNED)
+    {
+      // get top result bits
+      result.erase(result.begin(), result.begin() + old_size);
+
+      // one of the top bits is non-zero
+      overflow=prop.lor(result);
+    }
+    else
+    {
+      // get top result bits plus sign bit
+      DATA_INVARIANT(old_size != 0, "zero-size operand");
+      result.erase(result.begin(), result.begin() + old_size - 1);
+
+      // the sign bit has changed
+      literalt sign_change=!prop.lequal(bv0.back(), result.front());
+
+      // these need to be either all 1's or all 0's
+      literalt all_one=prop.land(result);
+      literalt all_zero=!prop.lor(result);
+
+      overflow=prop.lor(sign_change, !prop.lor(all_one, all_zero));
+    }
+
+    // a negative shift isn't an overflow; else check the conditions built
+    // above
+    return
+      prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
+  }
   else if(expr.id()==ID_overflow_unary_minus)
   {
     if(operands.size()!=1)

src/util/irep_ids.def

@@ -830,6 +830,7 @@ IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
 IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
 IREP_ID_ONE(havoc_object)
+IREP_ID_TWO(overflow_shl, overflow-shl)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO