[analyzer] Avoid contradicting assumption in tainted div-by-0 error node #144491
Conversation
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
This patch corrects the state of the error node generated by the core.DivideZero checker when it detects potential division by zero involving a tainted denominator. The checker split in llvm@91ac5ed started to introduce a conflicting assumption about the denominator into the error node: Node with the Bug Report "Division by a tainted value, possibly zero" has an assumption "denominator != 0". This has been done as a shortcut to continue analysis with the correct assumption *after* the division - if we proceed, we can only assume the denominator was not zero. However, this assumption is introduced one-node too soon, leading to a self-contradictory error node. In this patch, I make the error node with assumption of zero denominator fatal, but allow analysis to continue on the second half of the state split with the assumption of non-zero denominator. I did not find easy way to demnostrate this internal contradiction in a test case. Downstream, we have a custom bug reporter that is sensitive to it. Theoretically, it should be possible to construct a test case with the wrong assumption in the error node that is not detected by RangeChecker, but would be later on refuted by Z3, but such tests are rarely run anyways. --- CPP-6376
|
I did not find easy way to demnostrate this internal contradiction in a test case. Downstream, we have a custom bug reporter that is sensitive to it. Theoretically, it should be possible to construct a test case with the wrong assumption in the error node that is not detected by RangeChecker, but would be later on refuted by Z3, but such tests are rarely run anyways. Here is the comparison of exploded nodes between current |
|
✅ With the latest revision this PR passed the C/C++ code formatter. |
balazs-benics-sonarsource
approved these changes
Jun 17, 2025
|
Let's wait for a second opinion. |
NagyDonat
approved these changes
Jun 17, 2025
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/88/builds/12926 Here is the relevant piece of the build log for the reference |
|
@llvm/pr-subscribers-clang-static-analyzer-1 Author: Arseniy Zaostrovnykh (necto) ChangesThis patch corrects the state of the error node generated by the core.DivideZero checker when it detects potential division by zero involving a tainted denominator. The checker split in This has been done as a shortcut to continue analysis with the correct assumption after the division - if we proceed, we can only assume the denominator was not zero. However, this assumption is introduced one-node too soon, leading to a self-contradictory error node. In this patch, I make the error node with assumption of zero denominator fatal, but allow analysis to continue on the second half of the state split with the assumption of non-zero denominator. CPP-6376 Full diff: https://github.com/llvm/llvm-project/pull/144491.diff 2 Files Affected:
diff --git a/clang/lib/StaticAnalyzer/Checkers/DivZeroChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/DivZeroChecker.cpp
index 15d73fb9ca39a..ab90615f63182 100644
--- a/clang/lib/StaticAnalyzer/Checkers/DivZeroChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/DivZeroChecker.cpp
@@ -69,7 +69,7 @@ void DivZeroChecker::reportTaintBug(
llvm::ArrayRef<SymbolRef> TaintedSyms) const {
if (!TaintedDivChecker.isEnabled())
return;
- if (ExplodedNode *N = C.generateNonFatalErrorNode(StateZero)) {
+ if (ExplodedNode *N = C.generateErrorNode(StateZero)) {
auto R =
std::make_unique<PathSensitiveBugReport>(TaintedDivChecker, Msg, N);
bugreporter::trackExpressionValue(N, getDenomExpr(N), *R);
@@ -113,9 +113,9 @@ void DivZeroChecker::checkPreStmt(const BinaryOperator *B,
if ((stateNotZero && stateZero)) {
std::vector<SymbolRef> taintedSyms = getTaintedSymbols(C.getState(), *DV);
if (!taintedSyms.empty()) {
- reportTaintBug("Division by a tainted value, possibly zero", stateNotZero,
- C, taintedSyms);
- return;
+ reportTaintBug("Division by a tainted value, possibly zero", stateZero, C,
+ taintedSyms);
+ // Fallthrough to continue analysis in case of non-zero denominator.
}
}
diff --git a/clang/test/Analysis/taint-generic.c b/clang/test/Analysis/taint-generic.c
index 3c520612c5d9b..9d6d2942df4a9 100644
--- a/clang/test/Analysis/taint-generic.c
+++ b/clang/test/Analysis/taint-generic.c
@@ -412,6 +412,19 @@ int testTaintedDivFP(void) {
return 5/x; // x cannot be 0, so no tainted warning either
}
+void clang_analyzer_warnIfReached();
+
+int testTaintDivZeroNonfatal() {
+ int x;
+ scanf("%d", &x);
+ int y = 5/x; // expected-warning {{Division by a tainted value, possibly zero}}
+ if (x == 0)
+ clang_analyzer_warnIfReached();
+ else
+ clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+ return y;
+}
+
// Zero-sized VLAs.
void testTaintedVLASize(void) {
int x;
|
ajaden-codes
pushed a commit
to Jaddyen/llvm-project
that referenced
this pull request
Jun 17, 2025
…ode (llvm#144491) This patch corrects the state of the error node generated by the core.DivideZero checker when it detects potential division by zero involving a tainted denominator. The checker split in llvm@91ac5ed started to introduce a conflicting assumption about the denominator into the error node: Node with the Bug Report "Division by a tainted value, possibly zero" has an assumption "denominator != 0". This has been done as a shortcut to continue analysis with the correct assumption *after* the division - if we proceed, we can only assume the denominator was not zero. However, this assumption is introduced one-node too soon, leading to a self-contradictory error node. In this patch, I make the error node with assumption of zero denominator fatal, but allow analysis to continue on the second half of the state split with the assumption of non-zero denominator. --- CPP-6376
fschlimb
pushed a commit
to fschlimb/llvm-project
that referenced
this pull request
Jun 18, 2025
…ode (llvm#144491) This patch corrects the state of the error node generated by the core.DivideZero checker when it detects potential division by zero involving a tainted denominator. The checker split in llvm@91ac5ed started to introduce a conflicting assumption about the denominator into the error node: Node with the Bug Report "Division by a tainted value, possibly zero" has an assumption "denominator != 0". This has been done as a shortcut to continue analysis with the correct assumption *after* the division - if we proceed, we can only assume the denominator was not zero. However, this assumption is introduced one-node too soon, leading to a self-contradictory error node. In this patch, I make the error node with assumption of zero denominator fatal, but allow analysis to continue on the second half of the state split with the assumption of non-zero denominator. --- CPP-6376
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This patch corrects the state of the error node generated by the core.DivideZero checker when it detects potential division by zero involving a tainted denominator.
The checker split in
91ac5ed started to introduce a conflicting assumption about the denominator into the error node:
Node with the Bug Report "Division by a tainted value, possibly zero" has an assumption "denominator != 0".
This has been done as a shortcut to continue analysis with the correct assumption after the division - if we proceed, we can only assume the denominator was not zero. However, this assumption is introduced one-node too soon, leading to a self-contradictory error node.
In this patch, I make the error node with assumption of zero denominator fatal, but allow analysis to continue on the second half of the state split with the assumption of non-zero denominator.
CPP-6376