[analyzer] Fix crash in Z3 SMTConv when negating a boolean expression (#165779) #168034
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`.
llvmbot
added
clang
|
@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')}}
+ }
+}
|
|
@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')}}
+ }
+}
|
|
This patch cannot fix the conditional expression In the original |
|
Thanks for fixing this! LGTM, but I think @steakhal should comment. |
steakhal
left a comment
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.
|
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. |
4 participants
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.