Merge pull request #3662 from diffblue/shl-overflow

shift left overflow check now done in goto_check

Author: kroening

regression/cbmc/Overflow_Leftshift1/main.c

@@ -1,11 +1,24 @@
 int main()
 {
   unsigned char x;
+
+  // signed, owing to promotion, and may overflow
   unsigned r=x << ((sizeof(unsigned)-1)*8);
+
+  // signed, owing to promotion, and cannot overflow
   r=x << ((sizeof(unsigned)-1)*8-1);
+
+  // unsigned
   r=(unsigned)x << ((sizeof(unsigned)-1)*8);
 
-  int s=-1 << ((sizeof(int)-1)*8);
-  s=-256 << ((sizeof(int)-1)*8);
+  // negative value or zero, not an overflow
+  int s = -x << ((sizeof(int) - 1) * 8);
+
+  // overflow
+  s = 1 << x;
+
+  // distance too far, not an overflow
+  s = s << 100;
+
   return 0;
 }

regression/cbmc/Overflow_Leftshift1/test.desc

@@ -3,8 +3,13 @@ main.c
 --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*\] .* arithmetic overflow on signed shl in .*: FAILURE$
-^\*\* 2 of 4 failed
+^\[.*\] 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
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+^\[.*\] line 12 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 21 arithmetic overflow on signed shl in .*: .*

scripts/delete_failing_smt2_solver_tests

@@ -37,8 +37,6 @@ rm Linking7/test.desc
 rm Linking7/member-name-mismatch.desc
 rm Malloc23/test.desc
 rm Multi_Dimensional_Array2/test.desc
-rm Overflow_Leftshift1/test.desc
-rm Overflow_Subtraction1/test.desc
 rm Pointer_Arithmetic11/test.desc
 rm Pointer_byte_extract2/test.desc
 rm Pointer_byte_extract5/no-simplify.desc

src/analyses/goto_check.cpp

@@ -589,6 +589,81 @@ void goto_checkt::integer_overflow_check(
 
     return;
   }
+  else if(expr.id() == ID_shl)
+  {
+    if(type.id() == ID_signedbv)
+    {
+      const auto &shl_expr = to_shl_expr(expr);
+      const auto &op = shl_expr.op();
+      const auto &op_type = to_signedbv_type(type);
+      const auto op_width = op_type.get_width();
+      const auto &distance = shl_expr.distance();
+      const auto &distance_type = distance.type();
+
+      // a left shift of a negative value is undefined;
+      // yet this isn't an overflow
+      exprt neg_value_shift;
+
+      if(op_type.id() == ID_unsignedbv)
+        neg_value_shift = false_exprt();
+      else
+        neg_value_shift =
+          binary_relation_exprt(op, ID_lt, from_integer(0, op_type));
+
+      // a shift with negative distance is undefined;
+      // yet this isn't an overflow
+      exprt neg_dist_shift;
+
+      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));
+
+      // shifting a non-zero value by more than its width is undefined;
+      // yet this isn't an overflow
+      const exprt dist_too_large = binary_predicate_exprt(
+        distance, ID_gt, from_integer(op_width, distance_type));
+
+      const exprt op_zero = equal_exprt(op, from_integer(0, op_type));
+
+      auto new_type = to_bitvector_type(op_type);
+      new_type.set_width(op_width * 2);
+
+      const exprt op_ext = typecast_exprt(op, new_type);
+
+      const exprt op_ext_shifted = shl_exprt(op_ext, distance);
+
+      // get top bits of the shifted operand
+      const exprt top_bits = extractbits_exprt(
+        op_ext_shifted,
+        new_type.get_width() - 1,
+        op_width - 1,
+        unsignedbv_typet(op_width + 1));
+
+      const exprt top_bits_zero =
+        equal_exprt(top_bits, from_integer(0, top_bits.type()));
+
+      // a negative distance shift isn't an overflow;
+      // a negative value shift isn't an overflow;
+      // a shift that's too far isn't an overflow;
+      // a shift of zero isn't overflow;
+      // else check the top bits
+      add_guarded_claim(
+        disjunction({neg_value_shift,
+                     neg_dist_shift,
+                     dist_too_large,
+                     op_zero,
+                     top_bits_zero}),
+        "arithmetic overflow on signed shl",
+        "overflow",
+        expr.find_source_location(),
+        expr,
+        guard);
+    }
+
+    return;
+  }
 
   exprt overflow("overflow-"+expr.id_string(), bool_typet());
   overflow.operands()=expr.operands();

src/util/std_expr.h

@@ -2959,6 +2959,29 @@ class shl_exprt:public shift_exprt
   }
 };
 
+/// \brief Cast an exprt to a \ref shl_exprt
+///
+/// \a expr must be known to be \ref shl_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref shl_exprt
+inline const shl_exprt &to_shl_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_shl);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "Bit-wise shl must have two operands");
+  return static_cast<const shl_exprt &>(expr);
+}
+
+/// \copydoc to_shl_expr(const exprt &)
+inline shl_exprt &to_shl_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_shl);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "Bit-wise shl must have two operands");
+  return static_cast<shl_exprt &>(expr);
+}
+
 /// \brief Arithmetic right shift
 class ashr_exprt:public shift_exprt
 {