Peter added a comment.
In D140059#4081549 <https://reviews.llvm.org/D140059#4081549>, @vabridgers
wrote:
> Hello, it appears this patch causes a crash when I analyze this reproducer,
> with Z3 enabled. In the case shown here, the analyzer finds that 'f' to the
> call a(f) is uninitialized, and then is attempted to be refuted through
> SMTConv, leading to the assertion.
>
> If I modify the below code to not use isRepresentableByIn64(), or use
> 'assert(getMinSignedBits() <= 64 && "Too many bits for int64_t");' instead, I
> do not see the crash.
>
> clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true
> --target=x86_64-redhat-linux case.c
>
> void a(int);
> typedef struct {
> int b;
> } c;
> c *d;
> void e() {
> (void)d->b;
> int f;
> a(f);
> }
>
> The assert ...
>
> clang-16: ../include/llvm/ADT/APSInt.h:99: int64_t
> llvm::APSInt::getExtValue() const: Assertion `isRepresentableByInt64() &&
> "Too many bits for int64_t"' failed.Program received signal SIGABRT, Aborted.
Thanks for helping identifying the bug.
This is not a problem in this patch, the semantics of `getExtValue` changed in
this patch as carefully discussed here
<https://github.com/llvm/llvm-project/issues/59515>.
To summarize, we believe its not reasonable to carry out ext for
`(signed)(int64::Max + 1)`. Although it's still 64 bit, the returned value
would be interpreted as `int64::Min` instead of a large positive integer. This
behavior was allowed before.
To provide a fix for this problem, this patch provides a better way to
determine if the extension is possible `isRepresentableByInt64`, I would
recommend replacing `if (LLVM_UNLIKELY(Int.getBitWidth() > 64u))` in
Z3Solver.cpp:732 with `if (LLVM_UNLIKELY(!Int.isRepresentableByInt64()))`.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D140059/new/
https://reviews.llvm.org/D140059
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
