[PATCH] D142627: [analyzer] Fix crash exposed by D140059

[Vince Bridgers via Phabricator via llvm-commits]

vabridgers created this revision.
Herald added subscribers: manas, steakhal, ASDenysPetrov, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, hiraditya, xazax.hun.
Herald added a project: All.
vabridgers requested review of this revision.
Herald added projects: clang, LLVM.
Herald added subscribers: llvm-commits, cfe-commits.

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


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D142627

Files:
  clang/test/Analysis/z3-crosscheck.c
  llvm/lib/Support/Z3Solver.cpp


Index: llvm/lib/Support/Z3Solver.cpp
===================================================================
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -729,7 +729,7 @@
     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(
Index: clang/test/Analysis/z3-crosscheck.c
===================================================================
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -55,3 +55,15 @@
     h(2);
   }
 }
+
+// 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]}}
+}


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D142627.492432.patch
Type: text/x-patch
Size: 1018 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20230126/21233027/attachment.bin>