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

[Balázs Benics via Phabricator via cfe-commits]

steakhal updated this revision to Diff 424470.
steakhal added a comment.

Added two new RUN lines, demonstrating the behavior of `support-symbolic-integer-casts={true,false}`.
Also refined the match string to be less fuzzy. It helps to grasp the difference between the expectations.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D85528/new/

https://reviews.llvm.org/D85528

Files:
  clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
  clang/test/Analysis/z3-refute-enum-crash.cpp


Index: clang/test/Analysis/z3-refute-enum-crash.cpp
===================================================================
--- /dev/null
+++ clang/test/Analysis/z3-refute-enum-crash.cpp
@@ -0,0 +1,55 @@
+// 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 %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() {
+  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;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+    // no-crash on these dumps
+    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}}
+  }
+}
+
Index: clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -983,8 +983,8 @@
 
     // Produce SymbolCast if CastTy and T are different 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.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D85528.424470.patch
Type: text/x-patch
Size: 3532 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220422/87039944/attachment-0001.bin>