[clang] [analyzer] Correct crash in Z3 wrapper (PR #158276)

[via cfe-commits]

https://github.com/vabridgers updated https://github.com/llvm/llvm-project/pull/158276

>From a02784c3fb5bd1c4b4110e05a6de3869a4f8887c Mon Sep 17 00:00:00 2001
From: Vince Bridgers <vince.a.bridgers at ericsson.com>
Date: Fri, 12 Sep 2025 13:19:40 +0200
Subject: [PATCH] [analyzer] Correct crash in Z3 wrapper

If a UnarySymExpr with an arithmetic negation of a logical operation
to obtain a SMTRefExpr, the Z3 engine will crash. Since an arithmetic
negation of a logical operation makes no sense and has no effect, the
arithmetic negation is detected and removed to avoid the crash in Z3.

This shows up following this C snippet

  1: void bb(int a) {
  2:  if (-(&c && a)) {
  3:     int *d;
  4:   *d; // expected-warning{{Dereference of undefined pointer value}}
  5:  }
  6: }

Line 2 is expressed as SymExpr -((reg_$1<int a>) != 0) , which is then
attempted to be converted to SMTRefExpr (not (= reg_$1 #x00000000)). This
does not make sense to Z3 since a logical expression cannot be
arithmetically negated.

A solution is to detect that the result of a comparison is attempted to
be arithmetically negated and remove that arithmetic negation since
the negation of a bool is the same as the positive of a bool. Bool's
have no sign, they are only True or False.
---
 .../Core/PathSensitive/SMTConv.h              |  8 +++++
 clang/test/Analysis/z3-unarysymexpr.c         | 36 ++++++++++++++++++-
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index a6cb6c0f12a8c..faac8b9ae3559 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -455,6 +455,14 @@ class SMTConv {
       QualType OperandTy;
       llvm::SMTExprRef OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
+
+      if (const BinarySymExpr *BSE =
+              dyn_cast<BinarySymExpr>(USE->getOperand())) {
+        if (USE->getOpcode() == UO_Minus &&
+            BinaryOperator::isComparisonOp(BSE->getOpcode()))
+          return getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
+      }
+
       llvm::SMTExprRef UnaryExp =
           OperandTy->isRealFloatingType()
               ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c
index ed9ba72468422..e5b35a80f258b 100644
--- a/clang/test/Analysis/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3-unarysymexpr.c
@@ -1,5 +1,8 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
 // RUN:  -analyzer-constraints=z3 
+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN:  -analyzer-checker=core,debug.ExprInspection \
+// RUN:  -analyzer-config crosscheck-with-z3=true
 
 // REQUIRES: Z3
 //
@@ -7,9 +10,40 @@
 // that this no longer happens.
 //
 
-// expected-no-diagnostics
 int negate(int x, int y) {
   if ( ~(x && y))
     return 0;
   return 1;
 }
+
+// Z3 is presented with a SymExpr like this : -((reg_$0<int a>) != 0) :
+// from the Z3 refutation wrapper, that it attempts to convert to a
+// SMTRefExpr, then crashes inside of Z3. The "not zero" portion
+// of that expression is converted to the SMTRefExpr
+// "(not (= reg_$1 #x00000000))", which is a boolean result then the
+// "negative" operator is attempted to be applied which then causes
+// Z3 to crash. The accompanying patch just strips the negative operator
+// before submitting to Z3 to avoid the crash.
+//
+// TODO: Find the root cause of this and fix it in symbol manager
+//
+void c();
+
+int z3crash(int a, int b) {
+  b = a || b;
+  return (-b == a) / a; // expected-warning{{Division by zero [core.DivideZero]}}
+}
+
+// Floats are handled specifically, and differently in the Z3 refutation layer
+// Just cover that code path
+int z3_nocrash(float a, float b) {
+  b = a || b;
+  return (-b == a) / a;
+}
+
+int z3_crash2(int a) {
+  int *d;
+  if (-(&c && a))
+    return *d; // expected-warning{{Dereference of undefined pointer value}}
+  return 0;
+}