[analyzer] Fix cast evaluation on scoped enums in ExprEngine

[steakhal]

Summary

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 (aka. fixes #43375)

[vsavchenko]

Good catch!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

98–104

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

101

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

103–105

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

[steakhal]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

98–104

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?

101

You are right, I will add such cases as well.

103–105

Yes, I will move it closer.

[whisperity]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

98–104

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

98–104

Edit: should not be
It does not have to go into Type.h.

[steakhal]

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

[NoQ]

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?

[steakhal]

• Using dumps instead of reaching in tests.
• Not requiring complete enums anymore (unlike we did before the patch).

[steakhal]

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.

[xazax.hun]

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<ScopedPrimitive>();
if (sym == ScopedPrimitive::Max)
  return;
int sym2 = static_cast<unsigned char>(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?

[steakhal]

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<ScopedPrimitive>();
if (sym == ScopedPrimitive::Max)
  return;
int sym2 = static_cast<unsigned char>(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<ScopedPrimitive>();
  if (sym == ScopedPrimitive::Max)
    return;

  int sym2 = static_cast<unsigned char>(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.

[steakhal]

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.

[NoQ]

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.

[whisperity]

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

6

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

[xazax.hun]

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.

[steakhal]

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

[steakhal]

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

[xazax.hun]

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.

[steakhal]

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:

experiment.sh826 BDownload

[steakhal]

ping

[NoQ]

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

[steakhal]

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.

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

25

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

[NoQ]

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

[steakhal]

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&sort-by=name&sort-desc=false

[steakhal]

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?

[steakhal]

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

[martong]

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.

[steakhal]

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.

[steakhal]

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

[martong]

LGTM! Thanks!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

public:
 
   virtual ~SValBuilder() = default;
 
   bool haveSameType(const SymExpr *Sym1, const SymExpr *Sym2) {
     return haveSameType(Sym1->getType(), Sym2->getType());
   }
 
   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);
 
   // Handles casts of type CK_IntegralCast.
   SVal evalIntegralCast(ProgramStateRef state, SVal val, QualType castTy,
                         QualType originalType);
 

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

+// 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 <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{{((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_}}
+  }
+}