-
Notifications
You must be signed in to change notification settings - Fork 13.5k
z3 sort equality assertion failed on scoped enum cast to integer. #47570
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Comments
assigned to @devincoughlin |
A workaround is to not use an underlying type (if that's possible). Looks like SMTConv.h does not handle extraction of the underlying type for scoped enums. Looking at ASTContext.cpp, there is a comment added from commit e65ab9e ... +static const Type *getIntegerTypeForEnum(const EnumType *ET) {
and SMTConv.h specifically only looks for Integral Or Enumeration types that are also Arithmetic - and a scoped enum is excluded as Arithmetic in Type.cpp, see ... bool Type::isArithmeticType() const { One approach in SMTConv.h is to check the LTy and RTy and "promote" the scoped enum to the LTy or RTy type. This seems to work. But I don't feel comfortable making this change at this time without first correcting the test infra to support non Z3 and Z3 usage when running LITs (per Balazs comments). |
I think https://reviews.llvm.org/D85528 should resolve this. Most of the projects we are testing on lack this property. Cheers. |
changed the description |
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 llvm#47570 llvm#43375 Reviewed By: martong Differential Revision: https://reviews.llvm.org/D85528 (cherry picked from commit fd7efe3)
Extended Description
Test case:
(excerpted from llvm/include/llvm/Analysis/AliasAnalysis.h)
///////////////////////////////////////////////////////////////////////////////
(llvm commit: 37c74df)
Invocation:
Stack Dump:
The text was updated successfully, but these errors were encountered: