aboutsummaryrefslogtreecommitdiff
path: root/clang/test/Analysis/z3-refute-enum-crash.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'clang/test/Analysis/z3-refute-enum-crash.cpp')
-rw-r--r--clang/test/Analysis/z3-refute-enum-crash.cpp77
1 files changed, 77 insertions, 0 deletions
diff --git a/clang/test/Analysis/z3-refute-enum-crash.cpp b/clang/test/Analysis/z3-refute-enum-crash.cpp
new file mode 100644
index 0000000..355c10f
--- /dev/null
+++ b/clang/test/Analysis/z3-refute-enum-crash.cpp
@@ -0,0 +1,77 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-config crosscheck-with-z3=true -verify %s
+//
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN: -verify %s
+//
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-config support-symbolic-integer-casts=true -verify=symbolic %s
+//
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-config support-symbolic-integer-casts=false -verify %s
+//
+// REQUIRES: asserts, z3
+//
+// Requires z3 only for refutation. Works with both constraint managers.
+
+void clang_analyzer_dump(int);
+
+using sugar_t = unsigned char;
+
+// Enum types
+enum class ScopedSugared : sugar_t {};
+enum class ScopedPrimitive : unsigned char {};
+enum UnscopedSugared : sugar_t {};
+enum UnscopedPrimitive : unsigned char {};
+
+template <typename T>
+T conjure();
+
+void test_enum_types() {
+ // Let's construct a 'binop(sym, int)', where the binop will trigger an
+ // integral promotion to int. Note that we need to first explicit cast
+ // the scoped-enum to an integral, to make it compile. We could have choosen
+ // any other binary operator.
+ int sym1 = static_cast<unsigned char>(conjure<ScopedSugared>()) & 0x0F;
+ int sym2 = static_cast<unsigned char>(conjure<ScopedPrimitive>()) & 0x0F;
+ int sym3 = static_cast<unsigned char>(conjure<UnscopedSugared>()) & 0x0F;
+ int sym4 = static_cast<unsigned char>(conjure<UnscopedPrimitive>()) & 0x0F;
+
+ // We need to introduce a constraint referring to the binop, to get it
+ // serialized during the z3-refutation.
+ if (sym1 && sym2 && sym3 && sym4) {
+ // no-crash on these dumps
+ //
+ // The 'clang_analyzer_dump' will construct a bugreport, which in turn will
+ // trigger a z3-refutation. Refutation will walk the bugpath, collect and
+ // serialize the path-constraints into z3 expressions. The binop will
+ // operate over 'int' type, but the symbolic operand might have a different
+ // type - surprisingly.
+ // Historically, the static analyzer did not emit symbolic casts in a lot
+ // of cases, not even when the c++ standard mandated it, like for casting
+ // a scoped enum to its underlying type. Hence, during the z3 constraint
+ // serialization, it made up these 'missing' integral casts - for the
+ // implicit cases at least.
+ // However, it would still not emit the cast for missing explicit casts,
+ // hence 8-bit wide symbol would be bitwise 'and'-ed with a 32-bit wide
+ // int, violating an assertion stating that the operands should have the
+ // same bitwidths.
+
+ clang_analyzer_dump(sym1);
+ // expected-warning-re@-1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+ // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+
+ clang_analyzer_dump(sym2);
+ // expected-warning-re@-1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+ // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+
+ clang_analyzer_dump(sym3);
+ // expected-warning-re@-1 {{(conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}
+ // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+
+ clang_analyzer_dump(sym4);
+ // expected-warning-re@-1 {{(conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}
+ // symbolic-warning-re@-2 {{((int) (conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+ }
+}
+