Skip to content

Commit

Permalink
[analyzer] Fix crash exposed by D140059
Browse files Browse the repository at this point in the history
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
  • Loading branch information
einvbri committed Jan 26, 2023
1 parent 7dbeb12 commit f027dd5
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 1 deletion.
12 changes: 12 additions & 0 deletions clang/test/Analysis/z3-crosscheck.c
Original file line number Diff line number Diff line change
Expand Up @@ -77,3 +77,15 @@ void floatUnaryLNotInEq(int h, int l) {
// expected-warning@-1{{garbage}}
}
}

// don't crash, and also produce a core.CallAndMessage finding
void a(int);
typedef struct {
int b;
} c;
c *d;
void e() {
(void)d->b;
int f;
a(f); // expected-warning {{1st function call argument is an uninitialized value [core.CallAndMessage]}}
}
2 changes: 1 addition & 1 deletion llvm/lib/Support/Z3Solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -729,7 +729,7 @@ class Z3Solver : public SMTSolver {
const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;

// Slow path, when 64 bits are not enough.
if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
if (LLVM_UNLIKELY(!Int.isRepresentableByInt64())) {
SmallString<40> Buffer;
Int.toString(Buffer, 10);
return newExprRef(Z3Expr(
Expand Down

0 comments on commit f027dd5

Please sign in to comment.