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