[llvm] c71bbd5 - [analyzer] Correct Z3 test cases, fix exposed crashes (#146597)

[via llvm-commits]

Author: vabridgers
Date: 2025-07-03T09:08:00-05:00
New Revision: c71bbd50a10d733dc066db8f83638f9454c9705d

URL: https://github.com/llvm/llvm-project/commit/c71bbd50a10d733dc066db8f83638f9454c9705d
DIFF: https://github.com/llvm/llvm-project/commit/c71bbd50a10d733dc066db8f83638f9454c9705d.diff

LOG: [analyzer] Correct Z3 test cases, fix exposed crashes (#146597)

PR145731 corrected the analyzer test runner to consider use of z3 when
used by testcases, which exposed problems in test cases PR37855.c and
crashes in z3-crosscheck.c This change fixes those crashes and
re-enables the test cases that were "XFAIL"'d out.

Co-authored-by: einvbri <vince.a.bridgers at ericsson.com>

Added: 
    

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    clang/test/Analysis/PR37855.c
    clang/test/Analysis/z3-crosscheck.c
    llvm/lib/Support/Z3Solver.cpp

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 70a7953918ace..a6cb6c0f12a8c 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -598,6 +598,9 @@ class SMTConv {
     if (APSIntBitwidth == 1 && Ty.isNull())
       return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
               getAPSIntType(Ctx, NewInt)};
+    else if (APSIntBitwidth == 1 && !Ty.isNull())
+      return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
+              getAPSIntType(Ctx, NewInt)};
     if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
       return {Int, Ty};
     return {Int.extend(Ctx.getTypeSize(Ty)), Ty};

diff  --git a/clang/test/Analysis/PR37855.c b/clang/test/Analysis/PR37855.c
index 434df576e8ece..92ed9ffe69a7d 100644
--- a/clang/test/Analysis/PR37855.c
+++ b/clang/test/Analysis/PR37855.c
@@ -2,23 +2,21 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
-// XFAIL: *
-
 typedef struct o p;
 struct o {
   struct {
   } s;
 };
 
-void q(*r, p2) { r < p2; }
+void q(int *r, int p2) { r < p2; }
 
-void k(l, node) {
+void k(int l, int node) {
   struct {
     p *node;
   } * n, *nodep, path[sizeof(void)];
-  path->node = l;
+  path->node = (p*) l;
   for (n = path; node != l;) {
-    q(node, n->node);
+    q((int *)&node, (int)n->node);
     nodep = n;
   }
   if (nodep) // expected-warning {{Branch condition evaluates to a garbage value}}

diff  --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c
index ca20cd6a879f1..8cbe7dd2975d0 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/clang/test/Analysis/z3-crosscheck.c
@@ -2,8 +2,6 @@
 // RUN: %clang_analyze_cc1 -triple x86_64-pc-linux-gnu -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
-// XFAIL: *
-
 void clang_analyzer_dump(float);
 
 int foo(int x) 

diff  --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index 27027093a0c6f..056a17ad80123 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -932,7 +932,8 @@ class Z3Statistics final : public SMTSolverStatistics {
   };
   unsigned getUnsigned(StringRef Key) const override {
     auto It = UnsignedValues.find(Key.str());
-    assert(It != UnsignedValues.end());
+    if (It == UnsignedValues.end())
+      return 0;
     return It->second;
   };