From 0003223346272cc026ea08630d774f0e1e0c5ead Mon Sep 17 00:00:00 2001 From: Norbert Manthey Date: Fri, 11 Nov 2016 11:57:16 +0100 Subject: [PATCH] Bitand/bitor promotion with ~ may have unexpected results The combination of bitand and bitnot on variables/expressions with different bit width might lead to unexpected computations. Hence, goto-cc produces a warning when the combination is spotted. The check also works for the &= operator. When constants are used, no warning is produced. --- regression/ansi-c/implicit_promotion1/main.c | 63 +++++++++++++++++++ .../ansi-c/implicit_promotion1/test.desc | 9 +++ regression/ansi-c/implicit_promotion2/main.c | 55 ++++++++++++++++ .../ansi-c/implicit_promotion2/test.desc | 30 +++++++++ regression/ansi-c/implicit_promotion3/main.c | 32 ++++++++++ .../ansi-c/implicit_promotion3/test.desc | 11 ++++ src/ansi-c/c_typecheck_expr.cpp | 48 ++++++++++++++ 7 files changed, 248 insertions(+) create mode 100644 regression/ansi-c/implicit_promotion1/main.c create mode 100644 regression/ansi-c/implicit_promotion1/test.desc create mode 100644 regression/ansi-c/implicit_promotion2/main.c create mode 100644 regression/ansi-c/implicit_promotion2/test.desc create mode 100644 regression/ansi-c/implicit_promotion3/main.c create mode 100644 regression/ansi-c/implicit_promotion3/test.desc diff --git a/regression/ansi-c/implicit_promotion1/main.c b/regression/ansi-c/implicit_promotion1/main.c new file mode 100644 index 00000000000..10ab94e3198 --- /dev/null +++ b/regression/ansi-c/implicit_promotion1/main.c @@ -0,0 +1,63 @@ +#include +#include + +#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; +} diff --git a/regression/ansi-c/implicit_promotion1/test.desc b/regression/ansi-c/implicit_promotion1/test.desc new file mode 100644 index 00000000000..b39e70e96ae --- /dev/null +++ b/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$ diff --git a/regression/ansi-c/implicit_promotion2/main.c b/regression/ansi-c/implicit_promotion2/main.c new file mode 100644 index 00000000000..274f0348501 --- /dev/null +++ b/regression/ansi-c/implicit_promotion2/main.c @@ -0,0 +1,55 @@ +#include +#include + +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, u1 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 u, and negation on higher bit width + + return 0; +} diff --git a/regression/ansi-c/implicit_promotion2/test.desc b/regression/ansi-c/implicit_promotion2/test.desc new file mode 100644 index 00000000000..773605266a1 --- /dev/null +++ b/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$ diff --git a/regression/ansi-c/implicit_promotion3/main.c b/regression/ansi-c/implicit_promotion3/main.c new file mode 100644 index 00000000000..c45a2fcb29b --- /dev/null +++ b/regression/ansi-c/implicit_promotion3/main.c @@ -0,0 +1,32 @@ +#include + +#include + + +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; +} diff --git a/regression/ansi-c/implicit_promotion3/test.desc b/regression/ansi-c/implicit_promotion3/test.desc new file mode 100644 index 00000000000..a4a9e8a24d8 --- /dev/null +++ b/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$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index c41a2240309..05c105ad064 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -16,11 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include #include #include +#include #include #include #include @@ -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=(width0width1 && 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; }