Skip to content

Commit f027dd5

Browse files
author
einvbri
committed
[analyzer] Fix crash exposed by D140059
Change https://reviews.llvm.org/D140059 exposed the following crash in Z3Solver, where bit widths were not checked consistently with that change. This change makes the check consistent, and fixes the crash. ``` clang: <root>/llvm/include/llvm/ADT/APSInt.h:99: int64_t llvm::APSInt::getExtValue() const: Assertion `isRepresentableByInt64() && "Too many bits for int64_t"' failed. ... Stack dump: 0. Program arguments: clang -cc1 -internal-isystem <root>/lib/clang/16/include -nostdsysteminc -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify reproducer.c #0 0x00000000045b3476 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) <root>/llvm/lib/Support/Unix/Signals.inc:567:22 #1 0x00000000045b3862 PrintStackTraceSignalHandler(void*) <root>/llvm/lib/Support/Unix/Signals.inc:641:1 #2 0x00000000045b14a5 llvm::sys::RunSignalHandlers() <root>/llvm/lib/Support/Signals.cpp:104:20 #3 0x00000000045b2eb4 SignalHandler(int) <root>/llvm/lib/Support/Unix/Signals.inc:412:1 ... #9 0x0000000004be2eb3 llvm::APSInt::getExtValue() const <root>/llvm/include/llvm/ADT/APSInt.h:99:5 <root>/llvm/lib/Support/Z3Solver.cpp:740:53 clang::ASTContext&, clang::ento::SymExpr const*, llvm::APSInt const&, llvm::APSInt const&, bool) <root>/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:552:61 ``` Reviewed By: steakhal Differential Revision: https://reviews.llvm.org/D142627
1 parent 7dbeb12 commit f027dd5

File tree

2 files changed

+13
-1
lines changed

2 files changed

+13
-1
lines changed

clang/test/Analysis/z3-crosscheck.c

+12
Original file line numberDiff line numberDiff line change
@@ -77,3 +77,15 @@ void floatUnaryLNotInEq(int h, int l) {
7777
// expected-warning@-1{{garbage}}
7878
}
7979
}
80+
81+
// don't crash, and also produce a core.CallAndMessage finding
82+
void a(int);
83+
typedef struct {
84+
int b;
85+
} c;
86+
c *d;
87+
void e() {
88+
(void)d->b;
89+
int f;
90+
a(f); // expected-warning {{1st function call argument is an uninitialized value [core.CallAndMessage]}}
91+
}

llvm/lib/Support/Z3Solver.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -729,7 +729,7 @@ class Z3Solver : public SMTSolver {
729729
const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;
730730

731731
// Slow path, when 64 bits are not enough.
732-
if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
732+
if (LLVM_UNLIKELY(!Int.isRepresentableByInt64())) {
733733
SmallString<40> Buffer;
734734
Int.toString(Buffer, 10);
735735
return newExprRef(Z3Expr(

0 commit comments

Comments
 (0)