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

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

This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rGfd7efe33f1b2: [analyzer] Fix cast evaluation on scoped enums 
in ExprEngine (authored by steakhal).

Repository:
  rG LLVM Github Monorepo

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,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 
+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(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 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}}
+  }
+}
+
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 

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

[Gabor Marton via Phabricator via cfe-commits]

martong accepted this revision.
martong added a comment.
This revision is now accepted and ready to land.

LGTM! Thanks!


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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[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 424497.
steakhal added a comment.

Added the missing `-verify` flag for the new RUN line.
Also, add an elaborate description in the test for explaining the situation.


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,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 
+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(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 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}}
+  }
+}
+
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()) {
   

[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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+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}}
+  }
+}
+
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  =
   StateMgr.getOwningEngine().getAnalysisManager().getAnalyzerOptions();
   // If appropriate option is disabled, ignore the cast.


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 {};
+

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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

I'd like to have a guarantee that if `Opts.ShouldSupportSymbolicIntegerCasts` 
is set to `true` then the `SymboCast` is produced both for the scoped and the 
unscoped enums. Could you please have an additional lit test for that? At some 
point we'd like to make `ShouldSupportSymbolicIntegerCasts` to be `true` by 
default, thus in the existing test it would be better to explicitly have 
`-analyzer-config support-symbolic-integer-casts=false` set.


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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[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 423624.
steakhal edited the summary of this revision.
steakhal added a comment.
Herald added a subscriber: manas.
Herald added a project: All.

rebased; I'm still interested in this. WDYT @martong
BTW we have this downstream for about two years now without any problems.


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,38 @@
+// 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
+//
+// REQUIRES: 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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+clang_analyzer_dump(sym1); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym2); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym3); // expected-warning{{(conj_}}
+clang_analyzer_dump(sym4); // expected-warning{{(conj_}}
+  }
+}
+
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  =
   StateMgr.getOwningEngine().getAnalysisManager().getAnalyzerOptions();
   // If appropriate option is disabled, ignore the cast.


Index: clang/test/Analysis/z3-refute-enum-crash.cpp
===
--- /dev/null
+++ clang/test/Analysis/z3-refute-enum-crash.cpp
@@ -0,0 +1,38 @@
+// 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
+//
+// REQUIRES: 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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+clang_analyzer_dump(sym1); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym2); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym3); // expected-warning{{(conj_}}
+clang_analyzer_dump(sym4); // expected-warning{{(conj_}}
+  }
+}
+
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  =
   StateMgr.getOwningEngine().getAnalysisManager().getAnalyzerOptions();
   // If appropriate option is disabled, ignore the cast.
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

I really want to move this forward so I made a further evaluation on this, on 
the MongoDB project.
The analysis took approx. 22 and half hours on 24 cores for the baseline and 
for this revision as well.

There were 7116 common reports, 5 disappeared and new 34 were introduced.
We internally already landed this change more than half a year ago, and we 
haven't heard any complaints.
new 34:

  alpha.deadcode.UnreachableCode: 9
  alpha.security.ArrayBound: 4
  alpha.security.ReturnPtrRange: 2
  alpha.unix.cstring.OutOfBounds: 1
  deadcdoe.DeadStores: 18

disappeared 5:

  alpha.cplusplus.EnumCastOutOfRange: 1
  alpha.security.ArrayBound: 2
  alpha.security.ArrayBoundV2: 1
  core.NullDereference: 1 (infeasible)

---

In hindsight, I think we could get away with only applying the explicit cast 
**only if** the bitwidth wouldn't match. That way we would solve the crash in 
case of the Z3 crosscheck, and preserve the previous behavior otherwise.
WDYT?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

The patch doesn't seem to affect the reports.
It only introduced 3 new reports during the analysis of clang + clang-tidy.
The analysis times indeed increased slightly, ~~ +3%.

Overall, I think it's a valuable patch, which resolves crashes when the Z3 
refutation enabled.
However, I can evaluate this patch on more C++ projects if you are still not 
convinced.

---

You can inspect my evaluation results at:
https://codechecker-demo.eastus.cloudapp.azure.com/Default/runs?run=D85528-fix-scoped-enum-cast-evaluation=name=false


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

With Z3 //constraint// manager you absolutely want your constraints to be as 
precise as possible. The only reason we don't add these casts is because it 
confuses the constraint manager a lot. With a better constraint manager we 
would have spared ourselves a lot of suffering in this area.

With Z3 //refutation// manager - probably same but not sure, experimental data 
needed. Z3 occasionally refuting correct reports is not that big of a deal; the 
overall picture is still much better than without refutation due to sheer 
numbers of eliminated false positives. Improved cast modeling will also allow 
it to occasionally eliminate more false positives because it's now being fed 
correct formulas. However most of the decisions *during* the path are still 
made with RangeConstraintManager, which includes deciding whether to make a 
state split. RangeConstraintManager fails to solve constraints => double up the 
remaining analysis time. Exponentially with respect to the amount of 
constraints it couldn't solve. We'll have to weigh that performance cost 
against the improved quality.

> We might be able to do that by extending the Equivalence class of the 
> constraint map with the notion of casts of...

In my previous life i once did an experiment with RangeConstraintManager in 
which i added truncating cast symbols but not widening cast symbols. I believe 
it worked fairly well but i'm not sure, i was too young to properly assess the 
situation. So i believe something like this might actually work but there's 
still a high risk of failure (behaving overall worse than before) and it won't 
solve the entirety of the problem anyway (for instance, it won't help us solve 
https://bugs.llvm.org/show_bug.cgi?id=44114 by making our SVals type-correct so 
that extents didn't have to be stored separately - and that's currently one of 
the main sources of false positives we have).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

In D85528#2307785 , @NoQ wrote:

> Aha, ok, thanks, I now understand what the problem is because I was able to 
> run the test before the patch and see how the patch changes the behavior.
>
> What do you think about flattening the enum type out entirely? I.e., instead 
> of `(unsigned char) conj_$2{enum ScopedSugared}` have `conj_$2{unsigned 
> char}` from the start. Possibly same for unscoped enums. I don't think we 
> actually extract any value from knowing that a symbol is an enum value. We 
> also don't track enum types for concrete values (i.e., `nonloc::ConcreteInt` 
> doesn't know whether it belongs to an enum).

That's a great idea. It should work. I will investigate this direction.

---

By the same token - being cheap on modeling explicit casts - I have seen other 
cases where we do not represent casts explicitly. Just like in this example, at 
the inner-most if branch we will simply assume that `a == b` instead of 
`(uchar)a == b`.

  void should_warn_twice(int a, unsigned char b) {
// Consider this interpretation: {a: -250, b: 6}
// It should satisfy both branches since (unsigned char)-250 == 6.
if (a < -200) {
  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
  if ((unsigned char)a == b) {
clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}, no 
report shown WITH refutation
  }
}
  }

Refutation does not cooperate well with our constraint manager if we don't emit 
the symbolic casts in the Z3 model. And we won't since we store constraints 
without casts.
Without this cast, Z3 will find the constraints of the second bugreport to be 
//unsatisfiable//, thus invalidating a true-positive bugreport.

To come around this problem, I would suggest to evaluate any casts as-is in the 
analyzed source code and make sure that we can recognize and reuse the 
constraints on any form of a symbol.
We might be able to do that by extending the Equivalence class of the 
constraint map with the notion of casts of:

- which do **not change** the castee's value range (eg. `int -> long`, 
`unsigned char -> unsigned long`)
- which do **change** the value range (eg. `int -> signed char`, `int -> 
unsigned int`)

I might will raise this on cfe-dev - that's probably a better place to discuss 
such ideas.




Comment at: clang/test/Analysis/z3-refute-enum-crash.cpp:25
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;

I will document the step-by-step reasoning in the test code to make sure why 
the crash happened.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Aha, ok, thanks, I now understand what the problem is because I was able to run 
the test before the patch and see how the patch changes the behavior.

What do you think about flattening the enum type out entirely? I.e., instead of 
`(unsigned char) conj_$2{enum ScopedSugared}` have `conj_$2{unsigned char}` 
from the start. Possibly same for unscoped enums. I don't think we actually 
extract any value from knowing that a symbol is an enum value. We also don't 
track enum types for concrete values (i.e., `nonloc::ConcreteInt` doesn't know 
whether it belongs to an enum).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

ping


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

In D85528#2232074 , @xazax.hun wrote:

> I'm not opposed to landing this to master, as we will have more time there to 
> see whether there are any unwanted side effects in practice.

I made some experiments on the following projects:
symengine,oatpp,zstd,simbody,duckdb,drogon,fmt,cppcheck,capnproto

Only these projects were C++ projects using `enum class` constructs under the 
`clang/utils/analyzer/projects/projects.json` enumeration.
According to the results, no reports changed using the `SATest.py` tool for the 
measurement.
I was using this script to collect the log: F12840610: experiment.sh 



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In D85528#2229309 , @steakhal wrote:

> It would be nice to have this fix in clang11.
> Do you think it's qualified for it?

Unfortunately, this is not a fix only change. This is a fix for refutation, but 
also a behavioral change for the default settings (so for most users). With 
this little time left until release, I would be uncomfortable landing a 
behavioral change. I'm not opposed to landing this to master, as we will have 
more time there to see whether there are any unwanted side effects in practice.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

It would be nice to have this fix in clang11.
Do you think it's qualified for it?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[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 286209.
steakhal marked an inline comment as done.
steakhal added a comment.

Add an extra `RUN` line without //refutation//.
The expected result is the same as with refutation.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  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,37 @@
+// 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
+//
+// REQUIRES: 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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+clang_analyzer_dump(sym1); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym2); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym3); // expected-warning{{(conj_}}
+clang_analyzer_dump(sym4); // expected-warning{{(conj_}}
+  }
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -95,11 +95,15 @@
   }
 
   bool haveSameType(QualType Ty1, QualType Ty2) {
+const bool BothHaveSameCanonicalTypes =
+Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2);
+const bool BothHaveIntegralOrUnscopedEnumerationType =
+Ty1->isIntegralOrUnscopedEnumerationType() &&
+Ty2->isIntegralOrUnscopedEnumerationType();
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
-return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
-(Ty1->isIntegralOrEnumerationType() &&
- Ty2->isIntegralOrEnumerationType()));
+return BothHaveSameCanonicalTypes ||
+   BothHaveIntegralOrUnscopedEnumerationType;
   }
 
   SVal evalCast(SVal val, QualType castTy, QualType originalType);


Index: clang/test/Analysis/z3-refute-enum-crash.cpp
===
--- /dev/null
+++ clang/test/Analysis/z3-refute-enum-crash.cpp
@@ -0,0 +1,37 @@
+// 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
+//
+// REQUIRES: 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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+clang_analyzer_dump(sym1); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym2); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym3); // expected-warning{{(conj_}}
+clang_analyzer_dump(sym4); // expected-warning{{(conj_}}
+  }
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -95,11 +95,15 @@
   }
 
   bool haveSameType(QualType Ty1, QualType Ty2) {
+const bool BothHaveSameCanonicalTypes =
+Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2);
+const bool BothHaveIntegralOrUnscopedEnumerationType =
+Ty1->isIntegralOrUnscopedEnumerationType() &&
+

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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In D85528#2205799 , @NoQ wrote:

> I expect at least one LIT test //without// `-analyzer-config 
> crosscheck-with-z3=true`

Agreed. I think the code snippet I proposed would be a great test to include 
with this revision.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Whisperity via Phabricator via cfe-commits]

whisperity added inline comments.



Comment at: clang/test/Analysis/z3-refute-enum-crash.cpp:5
+//
+// Requires z3 only for refutation. Works with both constraint managers.
+

You can have multiple `RUN` lines in the same test file, which will result in 
the tests potentially executed with multiple configuration.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In D85528#2204664 , @steakhal wrote:

> In D85528#2203325 , @NoQ wrote:
>
>> Because this patch changes the behavior of regular analysis (without Z3), i 
>> expect tests to reflect that.
>
> What do you expect exactly?
>
> `REQUIRES: z3` is necessary for the refutation.
> However, adding this requirement would not mean that this test will run if 
> you have Z3 installed though.
> You should add the extra `llvm-lit` param to enable such tests.
> I don't want to repeat myself too much but D83677 
>  describes all the details of this test 
> infra fiasco.
> I would appreciate some feedback there.

I expect at least one LIT test //without// `-analyzer-config 
crosscheck-with-z3=true` (i.e., tests the default behavior, not the Z3 
behavior) and works differently before and after the patch. Because you are 
introducing a change in the default behavior: an unknown value is now denoted 
by a different symbolic value. And the default behavior is much more important 
to cover with tests than the non-default behavior - simply because it's the 
default behavior, which means the vast majority of our users will notice the 
change.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

I mean, this shouldn't be an issue. Since we already omitted the 'unnecessary' 
cast expressions... That decision is the root cause of this, we should have 
expected that.

IMO we do the right thing here. If we want to treat sym and sym2 to refer to 
the same symbol, we should patch the CM to canonize, and remove such casts 
before storing the constraint.
But the cast symbols should exist for casting scoped enums.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

In D85528#2205094 , @xazax.hun wrote:

> Looks reasonable to me, but I am not very familiar with the impacts of the 
> additional casts. Do we lose some modeling power when we are using the 
> regular constraint solver?
>
> For example, when we have constraints both on the original and the cased 
> symbol can the analyzer "merge" them?
>
> Something like:
>
>   ScopedPrimitive sym = conjure();
>   if (sym == ScopedPrimitive::Max)
> return;
>   int sym2 = static_cast(sym);
>   if (sym2 == 0)
> return;
>   // Do we know here that both sym and sym2 has the same range?
>   // Is there a change in the behavior compared to before the patch?

Huh, it's a really interesting question.
Here is the result:

---

Here is the test code:

  enum class ScopedPrimitive : unsigned char { Min = 2, Max = 8 };
  void foo() {
auto sym = conjure();
if (sym == ScopedPrimitive::Max)
  return;
  
int sym2 = static_cast(sym);
if (sym2 == 0)
  return;
  
// Do we know here that both sym and sym2 has the same range?
// Is there a change in the behavior compared to before the patch?
clang_analyzer_printState();
(void)sym;
(void)sym2;
  }

Before the patch:

  "constraints": [
  { "symbol": "conj_$2{enum ScopedPrimitive, LC1, S1083, #1}", "range": "{ 
[1, 7], [9, 255] }" }
]

After the patch:

  "constraints": [
  { "symbol": "conj_$2{enum ScopedPrimitive, LC1, S1881, #1}", "range": "{ 
[0, 7], [9, 255] }" },
  { "symbol": "(unsigned char) (conj_$2{enum ScopedPrimitive, LC1, S1881, 
#1})", "range": "{ [1, 255] }" }
]



---

> For example, when we have constraints both on the original and the cased 
> symbol can the analyzer "merge" them?

Apparently, not xD.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

Looks reasonable to me, but I am not very familiar with the impacts of the 
additional casts. Do we lose some modeling power when we are using the regular 
constraint solver?

For example, when we have constraints both on the original and the cased symbol 
can the analyzer "merge" them?

Something like:

  ScopedPrimitive sym = conjure();
  if (sym == ScopedPrimitive::Max)
return;
  int sym2 = static_cast(sym);
  if (sym2 == 0)
return;
  // Do we know here that both sym and sym2 has the same range?
  // Is there a change in the behavior compared to before the patch?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal added a comment.

In D85528#2203325 , @NoQ wrote:

> Aha, ok, sounds like the right thing to do. Like, for Z3 it's actually the 
> wrong thing to do (you'd prefer to evaluate the cast perfectly by adding 
> `SymbolCast`) but for pure RangeConstraintManager this is the lesser of two 
> evils.

My primary objective is to fix all the crashes related to //Range CM + Z3 
refutation//.

> Because this patch changes the behavior of regular analysis (without Z3), i 
> expect tests to reflect that.

What do you expect exactly?

`REQUIRES: z3` is necessary for the refutation.
However, adding this requirement would not mean that this test will run if you 
have Z3 installed though.
You should add the extra `llvm-lit` param to enable such tests.
I don't want to repeat myself too much but D83677 
 describes all the details of this test infra 
fiasco.
I would appreciate some feedback there.

> Please add `ExprInspection`-based tests to test values produced by casts.

Ok, I fixed that - thanks.

> I don't understand why should the behavior be different for incomplete types. 
> Can you explain?

You should be right. Fixed that.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[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 284126.
steakhal marked 3 inline comments as done.
steakhal edited the summary of this revision.
steakhal added a comment.

- Using `dump`s instead of `reaching` in tests.
- Not requiring complete enums anymore //(unlike we did before the patch)//.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  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,33 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: 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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+clang_analyzer_dump(sym1); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym2); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym3); // expected-warning{{(conj_}}
+clang_analyzer_dump(sym4); // expected-warning{{(conj_}}
+  }
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -95,11 +95,15 @@
   }
 
   bool haveSameType(QualType Ty1, QualType Ty2) {
+const bool BothHaveSameCanonicalTypes =
+Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2);
+const bool BothHaveIntegralOrUnscopedEnumerationType =
+Ty1->isIntegralOrUnscopedEnumerationType() &&
+Ty2->isIntegralOrUnscopedEnumerationType();
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
-return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
-(Ty1->isIntegralOrEnumerationType() &&
- Ty2->isIntegralOrEnumerationType()));
+return BothHaveSameCanonicalTypes ||
+   BothHaveIntegralOrUnscopedEnumerationType;
   }
 
   SVal evalCast(SVal val, QualType castTy, QualType originalType);


Index: clang/test/Analysis/z3-refute-enum-crash.cpp
===
--- /dev/null
+++ clang/test/Analysis/z3-refute-enum-crash.cpp
@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: 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 
+T conjure();
+
+void test_enum_types() {
+  int sym1 = static_cast(conjure()) & 0x0F;
+  int sym2 = static_cast(conjure()) & 0x0F;
+  int sym3 = static_cast(conjure()) & 0x0F;
+  int sym4 = static_cast(conjure()) & 0x0F;
+
+  if (sym1 && sym2 && sym3 && sym4) {
+// no-crash on these dumps
+clang_analyzer_dump(sym1); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym2); // expected-warning{{((unsigned char) (conj_}}
+clang_analyzer_dump(sym3); // expected-warning{{(conj_}}
+clang_analyzer_dump(sym4); // expected-warning{{(conj_}}
+  }
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -95,11 +95,15 @@
   }
 
   bool haveSameType(QualType Ty1, QualType Ty2) {
+const bool BothHaveSameCanonicalTypes =
+Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2);
+const bool BothHaveIntegralOrUnscopedEnumerationType =
+Ty1->isIntegralOrUnscopedEnumerationType() &&
+Ty2->isIntegralOrUnscopedEnumerationType();
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
-return 

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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

Aha, ok, sounds like the right thing to do. Like, for Z3 it's actually the 
wrong thing to do (you'd prefer to evaluate the cast perfectly by adding 
`SymbolCast`) but for pure RangeConstraintManager this is the lesser of two 
evils.

Because this patch changes the behavior of regular analysis (without Z3), i 
expect tests to reflect that. Please add `ExprInspection`-based tests to test 
values produced by casts.

I don't understand why should the behavior be different for incomplete types. 
Can you explain?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[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 283936.
steakhal added a comment.

- Moved the FIXME closer to the subject.
- Added tests for covering incomplete enums as well.
- Added `REQUIRES: z3`. This will mark the test case `unsupported` on every 
buildbots. See my notes about this behavior at D83677 
.
- Refined test file.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  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,70 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+//
+// Requires z3 only for refutation. Works with both constraint managers.
+
+void clang_analyzer_warnIfReached();
+
+using sugar_t = unsigned char;
+
+// Complete enum types
+enum class ScopedSugaredComplete : sugar_t {};
+enum class ScopedPrimitiveComplete : unsigned char {};
+enum UnscopedSugaredComplete : sugar_t {};
+enum UnscopedPrimitiveComplete : unsigned char {};
+
+// Incomplete enum types
+enum class ScopedSugaredIncomplete : sugar_t;
+enum class ScopedPrimitiveIncomplete : unsigned char;
+enum UnscopedSugaredIncomplete : sugar_t;
+enum UnscopedPrimitiveIncomplete : unsigned char;
+
+template 
+T conjure();
+
+void test_complete_enum_types() {
+  auto var1 = conjure();
+  auto var2 = conjure();
+  auto var3 = conjure();
+  auto var4 = conjure();
+
+  int sym1 = static_cast(var1) & 0x0F;
+  if (sym1)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym2 = static_cast(var2) & 0x0F;
+  if (sym2)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym3 = static_cast(var3) & 0x0F;
+  if (sym3)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym4 = static_cast(var4) & 0x0F;
+  if (sym4)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+}
+
+void test_incomplete_enum_types() {
+  auto var1 = conjure();
+  auto var2 = conjure();
+  auto var3 = conjure();
+  auto var4 = conjure();
+
+  int sym1 = static_cast(var1) & 0x0F;
+  if (sym1)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym2 = static_cast(var2) & 0x0F;
+  if (sym2)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym3 = static_cast(var3) & 0x0F;
+  if (sym3)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym4 = static_cast(var4) & 0x0F;
+  if (sym4)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -95,11 +95,22 @@
   }
 
   bool haveSameType(QualType Ty1, QualType Ty2) {
+const auto IsIntegralOrUnscopedCompleteEnumerationType = [](QualType Ty) {
+  const Type *CanonicalType = Ty.getCanonicalType().getTypePtr();
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+  return Ty->isIntegralOrEnumerationType();
+};
+
+const bool BothHaveSameCanonicalTypes =
+Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2);
+const bool BothHaveIntegralLikeTypes =
+IsIntegralOrUnscopedCompleteEnumerationType(Ty1) &&
+IsIntegralOrUnscopedCompleteEnumerationType(Ty2);
+
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
-return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
-(Ty1->isIntegralOrEnumerationType() &&
- Ty2->isIntegralOrEnumerationType()));
+return BothHaveSameCanonicalTypes || BothHaveIntegralLikeTypes;
   }
 
   SVal evalCast(SVal val, QualType castTy, QualType originalType);
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Whisperity via Phabricator via cfe-commits]

whisperity added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:98-104
+const auto IsIntegralOrUnscopedCompleteEnumerationType = [](QualType Ty) {
+  const Type *CanonicalType = Ty.getCanonicalType().getTypePtr();
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+
+  return Ty->isIntegralOrEnumerationType();
+};

whisperity wrote:
> steakhal wrote:
> > vsavchenko wrote:
> > > I don't really see any reasons why is this a lambda and not a free 
> > > function
> > It's somewhat domain-specific that we require:
> >  - `bool-uint128` builtin types
> >  - complete, scoped `enum` types ((I think we need completeness for the 
> > analysis))
> > 
> > ---
> > The one that comes quite close to these requirements was the 
> > `isIntegralOrEnumerationType`, but that does not check if the enum is 
> > //unscoped//.
> > 
> > We can extend the `Type` header with this.
> > Should we go on that route?
> I think they meant that this function should be a lambda, but a function 
> inside the current translation unit (either in namespace anonymous, or a 
> member function of SValBuilder).
Edit: should //not// be
It does not have to go into `Type.h`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Whisperity via Phabricator via cfe-commits]

whisperity added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:98-104
+const auto IsIntegralOrUnscopedCompleteEnumerationType = [](QualType Ty) {
+  const Type *CanonicalType = Ty.getCanonicalType().getTypePtr();
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+
+  return Ty->isIntegralOrEnumerationType();
+};

steakhal wrote:
> vsavchenko wrote:
> > I don't really see any reasons why is this a lambda and not a free function
> It's somewhat domain-specific that we require:
>  - `bool-uint128` builtin types
>  - complete, scoped `enum` types ((I think we need completeness for the 
> analysis))
> 
> ---
> The one that comes quite close to these requirements was the 
> `isIntegralOrEnumerationType`, but that does not check if the enum is 
> //unscoped//.
> 
> We can extend the `Type` header with this.
> Should we go on that route?
I think they meant that this function should be a lambda, but a function inside 
the current translation unit (either in namespace anonymous, or a member 
function of SValBuilder).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal planned changes to this revision.
steakhal added inline comments.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:98-104
+const auto IsIntegralOrUnscopedCompleteEnumerationType = [](QualType Ty) {
+  const Type *CanonicalType = Ty.getCanonicalType().getTypePtr();
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+
+  return Ty->isIntegralOrEnumerationType();
+};

vsavchenko wrote:
> I don't really see any reasons why is this a lambda and not a free function
It's somewhat domain-specific that we require:
 - `bool-uint128` builtin types
 - complete, scoped `enum` types ((I think we need completeness for the 
analysis))

---
The one that comes quite close to these requirements was the 
`isIntegralOrEnumerationType`, but that does not check if the enum is 
//unscoped//.

We can extend the `Type` header with this.
Should we go on that route?



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:101
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+

vsavchenko wrote:
> I think it's better to add tests for this condition.
You are right, I will add such cases as well.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:106-107
+
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
+const bool BothHaveSameCanonicalTypes =

vsavchenko wrote:
> Maybe this comment should be moved closer to the `return` statement?
Yes, I will move it closer.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Good catch!




Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:98-104
+const auto IsIntegralOrUnscopedCompleteEnumerationType = [](QualType Ty) {
+  const Type *CanonicalType = Ty.getCanonicalType().getTypePtr();
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+
+  return Ty->isIntegralOrEnumerationType();
+};

I don't really see any reasons why is this a lambda and not a free function



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:101
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+

I think it's better to add tests for this condition.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:106-107
+
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
+const bool BothHaveSameCanonicalTypes =

Maybe this comment should be moved closer to the `return` statement?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85528

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

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

steakhal created this revision.
steakhal added reviewers: NoQ, Szelethus, baloghadamsoftware, vsavchenko, 
xazax.hun, martong, ASDenysPetrov.
Herald added subscribers: cfe-commits, Charusso, dkrupp, donat.nagy, 
mikhail.ramalho, a.sidorin, rnkovacs, szepet, whisperity.
Herald added a project: clang.
steakhal requested review of this revision.

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**.

This materialized in crashes on analyzing the LLVM itself using the Z3 
refutation.
Refutation synthesized the given Z3 expression with the wrong bitwidth in the 
end.

Now, we evaluate the cast according to the standard.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D85528

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  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,38 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+
+void clang_analyzer_warnIfReached();
+
+using sugar_t = unsigned char;
+enum class ScopedSugared : sugar_t {};
+enum class ScopedPrimitive : unsigned char {};
+enum UnscopedSugared : sugar_t {};
+enum UnscopedPrimitive : unsigned char {};
+
+ScopedSugared conjure_scoped_enum_with_sugar_type();
+ScopedPrimitive conjure_scoped_enum_with_primitive_type();
+UnscopedSugared conjure_unscoped_enum_with_sugar_type();
+UnscopedPrimitive conjure_unscoped_enum_with_primitive_type();
+
+void test() {
+  auto var1 = conjure_scoped_enum_with_sugar_type();
+  auto var2 = conjure_scoped_enum_with_primitive_type();
+  auto var3 = conjure_unscoped_enum_with_sugar_type();
+  auto var4 = conjure_unscoped_enum_with_primitive_type();
+
+  int sym1 = static_cast(var1) & 0x0F;
+  if (sym1)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym2 = static_cast(var2) & 0x0F;
+  if (sym2)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym3 = static_cast(var3) & 0x0F;
+  if (sym3)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+
+  int sym4 = static_cast(var4) & 0x0F;
+  if (sym4)
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} no-crash
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -95,11 +95,22 @@
   }
 
   bool haveSameType(QualType Ty1, QualType Ty2) {
+const auto IsIntegralOrUnscopedCompleteEnumerationType = [](QualType Ty) {
+  const Type *CanonicalType = Ty.getCanonicalType().getTypePtr();
+  if (const auto *ET = dyn_cast(CanonicalType))
+return ET->getDecl()->isComplete() && !ET->getDecl()->isScoped();
+
+  return Ty->isIntegralOrEnumerationType();
+};
+
 // FIXME: Remove the second disjunct when we support symbolic
 // truncation/extension.
-return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
-(Ty1->isIntegralOrEnumerationType() &&
- Ty2->isIntegralOrEnumerationType()));
+const bool BothHaveSameCanonicalTypes =
+Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2);
+const bool BothHaveIntegralLikeTypes =
+IsIntegralOrUnscopedCompleteEnumerationType(Ty1) &&
+IsIntegralOrUnscopedCompleteEnumerationType(Ty2);
+return BothHaveSameCanonicalTypes || BothHaveIntegralLikeTypes;
   }
 
   SVal evalCast(SVal val, QualType castTy, QualType originalType);


Index: clang/test/Analysis/z3-refute-enum-crash.cpp
===
--- /dev/null
+++ clang/test/Analysis/z3-refute-enum-crash.cpp
@@ -0,0 +1,38 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+
+void clang_analyzer_warnIfReached();
+
+using sugar_t = unsigned char;
+enum class ScopedSugared : sugar_t {};
+enum class ScopedPrimitive : unsigned char {};
+enum UnscopedSugared : sugar_t {};
+enum UnscopedPrimitive : unsigned char {};
+
+ScopedSugared conjure_scoped_enum_with_sugar_type();
+ScopedPrimitive conjure_scoped_enum_with_primitive_type();
+UnscopedSugared conjure_unscoped_enum_with_sugar_type();
+UnscopedPrimitive conjure_unscoped_enum_with_primitive_type();
+
+void test() {
+  auto var1 = conjure_scoped_enum_with_sugar_type();
+  auto var2 = conjure_scoped_enum_with_primitive_type();
+  auto var3 = conjure_unscoped_enum_with_sugar_type();
+  auto var4 =