[clang] 7818089 - [analyzer] Hotfix a boolean conversion crash in the Z3 SMTConv (#158276)

[via cfe-commits]

Author: vabridgers
Date: 2025-09-22T09:38:16-05:00
New Revision: 78180892d5e869d39152c92438571c56d6e0daef

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

LOG: [analyzer] Hotfix a boolean conversion crash in the Z3 SMTConv (#158276)

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

```c++
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.

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

Added: 
    

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    clang/test/Analysis/z3-unarysymexpr.c

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index a6cb6c0f12a8c..7f25223d232cf 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -455,6 +455,20 @@ 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()))
+          // The comparison operator yields a boolean value in the Z3
+          // language and applying the unary minus operator on a boolean
+          // crashes Z3. However, the unary minus does nothing in this
+          // context (a number is truthy if and only if its negative is
+          // truthy), so let's just ignore the unary minus.
+          // TODO: Replace this with a more general solution.
+          return OperandExp;
+      }
+
       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..89c043e5befab 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 (unary '-', UO_Minus) 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 
diff erently 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;
+}