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."

Author: tautschnig

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);
   }
 }