|
| 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 | + |
0 commit comments