[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 <https://reviews.llvm.org/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<unsigned char>(conjure<ScopedSugared>()) & 0x0F;
+  int sym2 = static_cast<unsigned char>(conjure<ScopedPrimitive>()) & 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