[analyzer] Fix crash in Z3 SMTConv when negating a boolean expression (#165779)#168034
Merged
vabridgers merged 1 commit intollvm:mainfrom Nov 15, 2025
Merged
[analyzer] Fix crash in Z3 SMTConv when negating a boolean expression (#165779)#168034vabridgers merged 1 commit intollvm:mainfrom
vabridgers merged 1 commit intollvm:mainfrom
Conversation
…llvm#165779) Refer to llvm#158276 for previous hotfix. In Z3, boolean expressions are incompatible with bitvec operators. However, C expressions like `-(5 && a)` will generate such symbolic expressions, which will be further used as an integer. To be compatible with such usages, this fix converts such expressions to integer using the existing `fromCast`.
Member
|
@llvm/pr-subscribers-clang Author: Ella Ma (Snape3058) ChangesRefer to #158276 for previous hotfix. In Z3, boolean expressions are incompatible with bitvec operators. However, C expressions like Full diff: https://github.com/llvm/llvm-project/pull/168034.diff 2 Files Affected:
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 7f25223d232cf..b0673b62efffe 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -456,17 +456,15 @@ class SMTConv {
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;
+ // When the operand is a bool expr, but the operator is an integeral
+ // operator, casting the bool expr to the integer before creating the
+ // unary operator.
+ // E.g. -(5 && a)
+ if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy &&
+ (*RetTy)->isIntegerType()) {
+ OperandExp = fromCast(Solver, OperandExp, (*RetTy),
+ Ctx.getTypeSize(*RetTy), OperandTy, 1);
+ OperandTy = (*RetTy);
}
llvm::SMTExprRef UnaryExp =
diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c
index 89c043e5befab..82b0fc988a383 100644
--- a/clang/test/Analysis/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3-unarysymexpr.c
@@ -47,3 +47,11 @@ int z3_crash2(int a) {
return *d; // expected-warning{{Dereference of undefined pointer value}}
return 0;
}
+
+// Refer to issue 165779
+void z3_crash3(long a) {
+ if (~-(5 && a)) {
+ long *c;
+ *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}}
+ }
+}
|
Member
|
@llvm/pr-subscribers-clang-static-analyzer-1 Author: Ella Ma (Snape3058) ChangesRefer to #158276 for previous hotfix. In Z3, boolean expressions are incompatible with bitvec operators. However, C expressions like Full diff: https://github.com/llvm/llvm-project/pull/168034.diff 2 Files Affected:
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 7f25223d232cf..b0673b62efffe 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -456,17 +456,15 @@ class SMTConv {
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;
+ // When the operand is a bool expr, but the operator is an integeral
+ // operator, casting the bool expr to the integer before creating the
+ // unary operator.
+ // E.g. -(5 && a)
+ if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy &&
+ (*RetTy)->isIntegerType()) {
+ OperandExp = fromCast(Solver, OperandExp, (*RetTy),
+ Ctx.getTypeSize(*RetTy), OperandTy, 1);
+ OperandTy = (*RetTy);
}
llvm::SMTExprRef UnaryExp =
diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c
index 89c043e5befab..82b0fc988a383 100644
--- a/clang/test/Analysis/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3-unarysymexpr.c
@@ -47,3 +47,11 @@ int z3_crash2(int a) {
return *d; // expected-warning{{Dereference of undefined pointer value}}
return 0;
}
+
+// Refer to issue 165779
+void z3_crash3(long a) {
+ if (~-(5 && a)) {
+ long *c;
+ *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}}
+ }
+}
|
Member
Author
|
This patch cannot fix the conditional expression In the original |
Contributor
|
Thanks for fixing this! LGTM, but I think @steakhal should comment. |
steakhal
approved these changes
Nov 15, 2025
Contributor
steakhal
left a comment
There was a problem hiding this comment.
Thank you Snape for the fix! It looks much better than the previous. However, I expect more similar issues to come without a generalized fix.
Member
Author
|
I will further dig into why the symbolic expression If nothing needs to be adjusted in this patch, please merge it when suitable. Thank you. |
shafik
reviewed
Feb 10, 2026
| // operator, casting the bool expr to the integer before creating the | ||
| // unary operator. | ||
| // E.g. -(5 && a) | ||
| if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy && |
Collaborator
There was a problem hiding this comment.
These unconditional dereferences of RetTy look wrong considering these is a nullptr check right above. Either the check is wrong or these derferences need to be guarded.
CC @steakhal
Contributor
There was a problem hiding this comment.
Turns out it's never null and the code is overly generic. I'll come back and simplify this.
Thanks for calling this out!
steakhal
added a commit
to steakhal/llvm-project
that referenced
this pull request
Feb 10, 2026
…ference Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses llvm#168034 (comment)
steakhal
added a commit
that referenced
this pull request
Feb 16, 2026
…ference (#180801) Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses #168034 (comment)
llvm-sync bot
pushed a commit
to arm/arm-toolchain
that referenced
this pull request
Feb 16, 2026
… a RetTy reference (#180801) Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses llvm/llvm-project#168034 (comment)
manasij7479
pushed a commit
to manasij7479/llvm-project
that referenced
this pull request
Feb 18, 2026
…ference (llvm#180801) Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses llvm#168034 (comment)
Snape3058
added a commit
to Snape3058/llvm-patch-revision
that referenced
this pull request
Feb 24, 2026
… boolean expression to integer * Fixing llvm#108900 for incorrect "REQUIRES" condition for Z3 * Fixing llvm#168034 for the test failure * Adding more comments about the fixes in llvm#168034 for the tests introduced in llvm#158276
KornevNikita
pushed a commit
to intel/llvm
that referenced
this pull request
Mar 10, 2026
…ference (#180801) Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses llvm/llvm-project#168034 (comment)
HendrikHuebner
pushed a commit
to HendrikHuebner/llvm-project
that referenced
this pull request
Mar 10, 2026
…ference (llvm#180801) Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses llvm#168034 (comment)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Refer to #158276 for previous hotfix.
In Z3, boolean expressions are incompatible with bitvec operators. However, C expressions like
-(5 && a)will generate such symbolic expressions, which will be further used as an integer. To be compatible with such usages, this fix converts such expressions to integer using the existingfromCast.