[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
This commit is contained in:
Balazs Benics 2022-05-02 10:54:26 +02:00
parent aae5f8115a
commit fd7efe33f1
2 changed files with 79 additions and 2 deletions

View File

@ -983,8 +983,8 @@ SVal SValBuilder::evalCastSubKind(nonloc::SymbolVal V, QualType CastTy,
// 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.

View File

@ -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}}
}
}