From 6bb387237bf239ca7c5ed1f409f9004eed2b18db Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 26 Oct 2017 12:21:12 +0100
Subject: [PATCH 1/2] Check for overflow on left shift of signed ints

This is undefined behaviour according to 6.5.7 paragraph 4 in C11.
---
 regression/cbmc/Overflow_Leftshift1/main.c    | 11 +++
 regression/cbmc/Overflow_Leftshift1/test.desc |  9 +++
 src/analyses/goto_check.cpp                   |  3 +
 src/solvers/flattening/boolbv_overflow.cpp    | 73 ++++++++++++++++++-
 src/util/irep_ids.def                         |  1 +
 5 files changed, 93 insertions(+), 4 deletions(-)
 create mode 100644 regression/cbmc/Overflow_Leftshift1/main.c
 create mode 100644 regression/cbmc/Overflow_Leftshift1/test.desc

diff --git a/regression/cbmc/Overflow_Leftshift1/main.c b/regression/cbmc/Overflow_Leftshift1/main.c
new file mode 100644
index 00000000000..70dd6e5c478
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/Overflow_Leftshift1/test.desc b/regression/cbmc/Overflow_Leftshift1/test.desc
new file mode 100644
index 00000000000..04360e32357
--- /dev/null
+++ b/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
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 95345814426..ffb8cd255b1 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1418,6 +1418,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)
   {
diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index 33dd61bca33..ceef7d19f0d 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/src/solvers/flattening/boolbv_overflow.cpp
@@ -8,8 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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)
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index e5e998633c0..18ba6509988 100644
--- a/src/util/irep_ids.def
+++ b/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

From 1e3712c33b0946beb0b6e59f5a5435d906c745bc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 26 Oct 2017 17:05:45 +0100
Subject: [PATCH 2/2] Shifts of non-integers and left shifts of negative
 integers are undefined

6.5.7 of C11: "Each of the operands shall have integer type."

Paragraph 4: "If E1 has a signed type and nonnegative value, and E1 x 2^E2 is
representable in the result type, then that is the resulting value; otherwise,
the behavior is undefined."
---
 regression/cbmc/Undefined_Shift1/main.c    | 11 ++++++++++
 regression/cbmc/Undefined_Shift1/test.desc |  9 ++++++++
 src/analyses/goto_check.cpp                | 24 ++++++++++++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 regression/cbmc/Undefined_Shift1/main.c
 create mode 100644 regression/cbmc/Undefined_Shift1/test.desc

diff --git a/regression/cbmc/Undefined_Shift1/main.c b/regression/cbmc/Undefined_Shift1/main.c
new file mode 100644
index 00000000000..70dd6e5c478
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc
new file mode 100644
index 00000000000..e82c3b92690
--- /dev/null
+++ b/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
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index ffb8cd255b1..c36c8b189dc 100644
--- a/src/analyses/goto_check.cpp
+++ b/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);
   }
 }