Detect dangerous implicit integer promotions during compilation

regression/ansi-c/implicit_promotion1/main.c

@@ -0,0 +1,63 @@
+#include <inttypes.h>
+#include <stdio.h>
+
+#define G (1024L*1024L*1024L*1024L)
+
+void broken(unsigned int a, unsigned long b, unsigned long c ) {
+	if( a != 2 && a != 4 && a != 8 ) return;
+	if ( a == 2 )
+		b = (int16_t)b;
+	else if ( a == 4 )
+		b = (int32_t)b;
+	if( (long)b < 0 ) {
+		unsigned long d;
+		// here, we would like to have some warning like
+		// increasing bit width automatically before applying "~" operator
+		d = a + (((-b-1) >> 3) & ~(a-1));
+		c -= d;
+		b = (d << 3) + b;
+	} else {
+		// increasing bit width automatically before applying "~" operator
+		c += (b >> 3) & ~(a - 1);
+		b &= (a << 3) - 1;
+	}
+	printf("b: %ld c: %ld\n", b, c);
+}
+
+void fixed(unsigned int a, unsigned long b, unsigned long c ) {
+	if( a != 2 && a != 4 && a != 8 ) return;
+	if ( a == 2 )
+		b = (int16_t)b;
+	else if ( a == 4 )
+		b = (int32_t)b;
+	if( (long)b < 0 ) {
+		unsigned long d;
+		// the problem is that the 1 (i.e. not 1L) turned the later operand
+		// into a 32bit value first, and then the ~ operator turns this
+		// back into 64, with many leading 0bits, which are then flipped
+		// to 1, and successfully pass the & operator.
+		// combinations we might want to look for are hence:
+		// (bigger_t) & ~(bigger_t vs smaller_t)
+		// but basically, any ~ together with a silent cast looks weird
+		d = a + (((-b-1) >> 3) & ~(a-1L));
+		c -= d;
+		b = (d << 3) + b;
+	} else {
+		c += (b >> 3) & ~(a - 1L);
+		b &= (a << 3) - 1;
+	}
+	printf("b: %ld c: %ld\n", b, c);
+}
+
+void test(unsigned int a, unsigned long b, unsigned long c) {
+	printf("broken for %u,%lu,%lu\n",a,b,c);
+	broken(a, b, c);
+	printf("  and fixed:\n");
+	fixed(a,b,c);
+}
+
+int main() {
+	test(8, G+1023L, 0);
+	test(8, -G-1023L, 0);
+	return 0;
+}

regression/ansi-c/implicit_promotion1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+-Wall
+^EXIT=0$
+^SIGNAL=0$
+Implicit zero extension of bitwise operand in combination with bitwise negation may cause unexpected results$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/implicit_promotion2/main.c

@@ -0,0 +1,55 @@
+#include <inttypes.h>
+#include <stdio.h>
+
+int main() {
+	unsigned int u=1023;
+	unsigned char c=3;
+	unsigned long l=1024L*1024L*1024L*1024L*1024L - 1L;
+	unsigned long d=l;
+
+	d&=u; // fine, no negation
+
+	d&=c; // fine, no negation
+
+	d&=~u; // dangerous, u<d, negation
+
+	d&=~c; // dangerous, c<d, negation
+
+	u&=d; // fine, u<d
+
+	c&=d; // fine, c<d
+
+	c&=1024L*1024L*1024L*1024L*1024L - 1L; // fine, c < constant
+
+	c&=~d; // fine, c < d
+
+	c&=~1024L*1024L*1024L*1024L*1024L - 1L; // fine, c < constant
+
+	d&=1; // fine, constant
+
+	d=l & 1; // fine, no negation
+
+	d=l & c; // fine, no negation
+
+	d=d & ~1; // dangerous, d>1 and negation
+
+	d=~d & 1; // fine, d>1, but negation on greater bit width
+
+	d=(l&=~u); // dangerous, l>u and negation
+
+	d=(u&=~l); // fine, u < l
+
+	d=(l & ~u); // dangerous, l>u and negation
+
+	d=(u & ~l); // fine, u < l, i.e. ~ on greater bit width
+
+	d=(l&=u); // fine, no negation
+
+	d=(u&=l); // fine, no negation
+
+	d=(~5 & l); // dangerous, negation and 5<l
+
+	d=(~5L & u); // fine, negation on constant, 5L > u, and negation on higher bit width
+
+	return 0;
+}

regression/ansi-c/implicit_promotion2/test.desc

@@ -0,0 +1,30 @@
+CORE
+main.c
+-Wall
+^EXIT=0$
+^SIGNAL=0$
+main.c:14:
+main.c:16:
+main.c:34:
+main.c:38:
+main.c:42:
+main.c:50:
+--
+main.c:10:
+main.c:12:
+main.c:18:
+main.c:20:
+main.c:22:
+main.c:24:
+main.c:26:
+main.c:28:
+main.c:30:
+main.c:32:
+main.c:36:
+main.c:40:
+main.c:44:
+main.c:46:
+main.c:48:
+main.c:52:
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/implicit_promotion3/main.c

@@ -0,0 +1,32 @@
+#include <stdio.h>
+
+#include <inttypes.h>
+
+
+int main() {
+
+	uint32_t a=0;
+	uint64_t b=1024L;
+	b=b * b * b * b + 1023;
+
+	printf("a=%u b=%lu\n", a, b);
+	b=b & ~a;
+	printf("a=%u b=%lu\n", a, b);
+
+	uint16_t c=0;
+	uint32_t d=256 * 256 + 127;
+
+	printf("c=%u d=%u\n", c, d);
+	d=d & ~c;
+	printf("c=%u d=%u\n", c, d);
+
+	uint64_t e=3;
+	unsigned __int128 f=1024;
+	f=f * f * f * f; // >32bit
+	f=f * f;         // >64bit
+
+	printf("e=%lu f=hi:%lu lo:%lu\n", e, (uint64_t)(f >> 64), (uint64_t)f);
+	f=f & ~e;
+	printf("e=%lu f=hi:%lu lo:%lu\n", e, (uint64_t)(f >> 64), (uint64_t)f);
+	return 0;
+}

regression/ansi-c/implicit_promotion3/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+-Wall
+^EXIT=0$
+^SIGNAL=0$
+main.c:13:
+main.c:29:
+--
+main.c:20:
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_expr.cpp

@@ -16,11 +16,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_util.h>
 #include <util/std_types.h>
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
+#include <util/file_util.h>
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -2813,6 +2815,36 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
 
   // promote!
 
+  // warn about an implicit 0-extension of bitand operands
+  // expect an explicit cast to avoid this warning
+  if((expr.id()==ID_bitand) &&
+     (op0.type().id()==ID_signedbv || op0.type().id()==ID_unsignedbv) &&
+     (op1.type().id()==ID_signedbv || op1.type().id()==ID_unsignedbv))
+  {
+    bool unintentional=false;
+    // do not apply, if we are working with constants and the & operator
+    if(op0.id()!=ID_constant && op1.id()!=ID_constant)
+    {
+      // mismatch occurs only, if we have "&" with two different width,
+      // where the side with the smaller width has to use the "~" operator
+      const size_t width0=to_bitvector_type(op0.type()).get_width();
+      const size_t width1=to_bitvector_type(op1.type()).get_width();
+      unintentional=(width0<width1 && has_subexpr(op0, ID_bitnot)) ||
+                    (width0>width1 && has_subexpr(op1, ID_bitnot));
+    }
+
+    // is all conditions are met for an unintended combination
+    // of the operators ~ and &, print a warning
+    if(unintentional)
+    {
+      warning().source_location=expr.find_source_location();
+      warning() << "Implicit zero extension of bitwise operand"
+                << " in combination with bitwise negation may"
+                << " cause unexpected results"
+                << eom;
+    }
+  }
+
   implicit_typecast_arithmetic(op0, op1);
 
   const typet &type0=follow(op0.type());
@@ -3205,6 +3237,22 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
             o_type0.id()==ID_signedbv ||
             o_type0.id()==ID_c_bit_field)
     {
+      // check whether an implicit cast might be dangerous,
+      // i.e. it involves the & and ~ operator
+      if((o_type0.id()==ID_unsignedbv || o_type0.id()==ID_signedbv) &&
+         (o_type1.id()==ID_unsignedbv || o_type1.id()==ID_signedbv) &&
+         op1.id()!=ID_constant &&
+         (to_bitvector_type(o_type0).get_width()>
+           to_bitvector_type(o_type1).get_width()) &&
+         has_subexpr(op1, ID_bitnot))
+      {
+        warning().source_location=expr.find_source_location();
+        warning() << "Implicit zero extension of bitwise operand"
+                  << " in combination with bitwise negation may"
+                  << " cause unexpected results"
+                  << eom;
+      }
+      // perform the cast
       implicit_typecast(op1, o_type0);
       return;
     }