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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
