[clang] fd7efe3 - [analyzer] Fix cast evaluation on scoped enums in ExprEngine

[Balazs Benics via cfe-commits]

Author: Balazs Benics
Date: 2022-05-02T10:54:26+02:00
New Revision: fd7efe33f1b2d0dc3bce940154dba27413b72e7a

URL: https://github.com/llvm/llvm-project/commit/fd7efe33f1b2d0dc3bce940154dba27413b72e7a
DIFF: https://github.com/llvm/llvm-project/commit/fd7efe33f1b2d0dc3bce940154dba27413b72e7a.diff

LOG: [analyzer] Fix cast evaluation on scoped enums in ExprEngine

We ignored the cast if the enum was scoped.
This is bad since there is no implicit conversion from the scoped enum to the corresponding underlying type.

The fix is basically: isIntegralOrEnumerationType() -> isIntegralOr**Unscoped**EnumerationType()

This materialized in crashes on analyzing the LLVM itself using the Z3 refutation.
Refutation synthesized the given Z3 Binary expression (`BO_And` of `unsigned char` aka. 8 bits
and an `int` 32 bits) with the wrong bitwidth in the end, which triggered an assert.

Now, we evaluate the cast according to the standard.

This bug could have been triggered using the Z3 CM according to
https://bugs.llvm.org/show_bug.cgi?id=44030

Fixes #47570 #43375

Reviewed By: martong

Differential Revision: https://reviews.llvm.org/D85528

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

Modified: 
    clang/lib/StaticAnalyzer/Core/SValBuilder.cpp

Removed: 
    


################################################################################
diff  --git a/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp b/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
index e045c9a91e60c..12b46426c027d 100644
--- a/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -983,8 +983,8 @@ SVal SValBuilder::evalCastSubKind(nonloc::SymbolVal V, QualType CastTy,
 
     // Produce SymbolCast if CastTy and T are 
diff erent integers.
     // NOTE: In the end the type of SymbolCast shall be equal to CastTy.
-    if (T->isIntegralOrEnumerationType() &&
-        CastTy->isIntegralOrEnumerationType()) {
+    if (T->isIntegralOrUnscopedEnumerationType() &&
+        CastTy->isIntegralOrUnscopedEnumerationType()) {
       AnalyzerOptions &Opts =
           StateMgr.getOwningEngine().getAnalysisManager().getAnalyzerOptions();
       // If appropriate option is disabled, ignore the cast.

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 0000000000000..355c10f4e284e
--- /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 
diff erent
+    // 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 at -1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+    // symbolic-warning-re at -2           {{((int) (conj_${{[0-9]+}}{enum ScopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+
+    clang_analyzer_dump(sym2);
+    // expected-warning-re at -1 {{((unsigned char) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+    // symbolic-warning-re at -2           {{((int) (conj_${{[0-9]+}}{enum ScopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+
+    clang_analyzer_dump(sym3);
+    // expected-warning-re at -1        {{(conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}
+    // symbolic-warning-re at -2 {{((int) (conj_${{[0-9]+}}{enum UnscopedSugared, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+
+    clang_analyzer_dump(sym4);
+    // expected-warning-re at -1        {{(conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}}) & 15}}
+    // symbolic-warning-re at -2 {{((int) (conj_${{[0-9]+}}{enum UnscopedPrimitive, LC{{[0-9]+}}, S{{[0-9]+}}, #{{[0-9]+}}})) & 15}}
+  }
+}
+