clang/test/Analysis/z3-refute-enum-crash.cpp

   1 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
   2 // RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
   3 //
   4 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
   5 // RUN:   -verify %s
   6 //
   7 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
   8 // RUN:   -analyzer-config support-symbolic-integer-casts=true -verify=symbolic %s
   9 //
  10 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
  11 // RUN:   -analyzer-config support-symbolic-integer-casts=false -verify %s
  12 //
  13 // REQUIRES: asserts, z3
  14 //
  15 // Requires z3 only for refutation. Works with both constraint managers.
  16
  17 void clang_analyzer_dump(int);
  18
  19 using sugar_t = unsigned char;
  20
  21 // Enum types
  22 enum class ScopedSugared : sugar_t {};
  23 enum class ScopedPrimitive : unsigned char {};
  24 enum UnscopedSugared : sugar_t {};
  25 enum UnscopedPrimitive : unsigned char {};
  26
  27 template <typename T>
  28 T conjure();
  29
  30 void test_enum_types() {
  31   // Let's construct a 'binop(sym, int)', where the binop will trigger an
  32   // integral promotion to int. Note that we need to first explicit cast
  33   // the scoped-enum to an integral, to make it compile. We could have choosen
  34   // any other binary operator.
  35   int sym1 = static_cast<unsigned char>(conjure<ScopedSugared>()) & 0x0F;
  36   int sym2 = static_cast<unsigned char>(conjure<ScopedPrimitive>()) & 0x0F;
  37   int sym3 = static_cast<unsigned char>(conjure<UnscopedSugared>()) & 0x0F;
  38   int sym4 = static_cast<unsigned char>(conjure<UnscopedPrimitive>()) & 0x0F;
  39
  40   // We need to introduce a constraint referring to the binop, to get it
  41   // serialized during the z3-refutation.
  42   if (sym1 && sym2 && sym3 && sym4) {
  43     // no-crash on these dumps
  44     //
  45     // The 'clang_analyzer_dump' will construct a bugreport, which in turn will
  46     // trigger a z3-refutation. Refutation will walk the bugpath, collect and
  47     // serialize the path-constraints into z3 expressions. The binop will
  48     // operate over 'int' type, but the symbolic operand might have a different
  49     // type - surprisingly.
  50     // Historically, the static analyzer did not emit symbolic casts in a lot
  51     // of cases, not even when the c++ standard mandated it, like for casting
  52     // a scoped enum to its underlying type. Hence, during the z3 constraint
  53     // serialization, it made up these 'missing' integral casts - for the
  54     // implicit cases at least.
  55     // However, it would still not emit the cast for missing explicit casts,
  56     // hence 8-bit wide symbol would be bitwise 'and'-ed with a 32-bit wide
  57     // int, violating an assertion stating that the operands should have the
  58     // same bitwidths.
  59
  60     clang_analyzer_dump(sym1);
  61     // expected-warning-re@-1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
  62     // symbolic-warning-re@-2           {{((int) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
  63
  64     clang_analyzer_dump(sym2);
  65     // expected-warning-re@-1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
  66     // symbolic-warning-re@-2           {{((int) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
  67
  68     clang_analyzer_dump(sym3);
  69     // expected-warning-re@-1        {{(conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}
  70     // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
  71
  72     clang_analyzer_dump(sym4);
  73     // expected-warning-re@-1        {{(conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}
  74     // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
  75   }
  76 }
  77