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.bridg...@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;
+}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
