martong created this revision.
martong added reviewers: ASDenysPetrov, steakhal, manas, vsavchenko, NoQ.
Herald added subscribers: gamesh411, dkrupp, donat.nagy, Szelethus,
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun,
whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
There is an error in the implementation of the logic of reaching the `Unknonw`
tristate in CmpOpTable.
void cmp_op_table_unknownX2(int x, int y, int z) {
if (x >= y) {
// x >= y [1, 1]
if (x + z < y)
return;
// x + z < y [0, 0]
if (z != 0)
return;
// x < y [0, 0]
clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
expected-warning{{FALSE}}
}
}
We miss the `FALSE` warning because the false branch is infeasible.
We have to exploit simplification to discover the bug. If we had `x < y`
as the second condition then the analyzer would return the parent state
on the false path and the new constraint would not be part of the State.
But adding `z` to the condition makes both paths feasible.
The root cause of the bug is that we reach the `Unknown` tristate
twice, but in both occasions we reach the same `Op` that is `>=` in the
test case. So, we reached `>=` twice, but we never reached `!=`, thus
querying the `Unknonw2x` column with `getCmpOpStateForUnknownX2` is
wrong.
The solution is to ensure that we reached both **different** `Op`s once.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D110910
Files:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constraint_manager_conditions.cpp
Index: clang/test/Analysis/constraint_manager_conditions.cpp
===================================================================
--- clang/test/Analysis/constraint_manager_conditions.cpp
+++ clang/test/Analysis/constraint_manager_conditions.cpp
@@ -211,3 +211,17 @@
clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
}
}
+
+// Test the logic of reaching the `Unknonw` tristate in CmpOpTable.
+void cmp_op_table_unknownX2(int x, int y, int z) {
+ if (x >= y) {
+ // x >= y [1, 1]
+ if (x + z < y)
+ return;
+ // x + z < y [0, 0]
+ if (z != 0)
+ return;
+ // x < y [0, 0]
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}}
expected-warning{{FALSE}}
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1126,7 +1126,7 @@
SymbolManager &SymMgr = State->getSymbolManager();
- int UnknownStates = 0;
+ llvm::SmallSet<BinaryOperatorKind, 2> QueriedToUnknown;
// Loop goes through all of the columns exept the last one ('UnknownX2').
// We treat `UnknownX2` column separately at the end of the loop body.
@@ -1163,7 +1163,8 @@
CmpOpTable.getCmpOpState(CurrentOP, QueriedOP);
if (BranchState == OperatorRelationsTable::Unknown) {
- if (++UnknownStates == 2)
+ QueriedToUnknown.insert(QueriedOP);
+ if (QueriedToUnknown.size() == 2)
// If we met both Unknown states.
// if (x <= y) // assume true
// if (x != y) // assume true
Index: clang/test/Analysis/constraint_manager_conditions.cpp
===================================================================
--- clang/test/Analysis/constraint_manager_conditions.cpp
+++ clang/test/Analysis/constraint_manager_conditions.cpp
@@ -211,3 +211,17 @@
clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
}
}
+
+// Test the logic of reaching the `Unknonw` tristate in CmpOpTable.
+void cmp_op_table_unknownX2(int x, int y, int z) {
+ if (x >= y) {
+ // x >= y [1, 1]
+ if (x + z < y)
+ return;
+ // x + z < y [0, 0]
+ if (z != 0)
+ return;
+ // x < y [0, 0]
+ clang_analyzer_eval(x > y); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1126,7 +1126,7 @@
SymbolManager &SymMgr = State->getSymbolManager();
- int UnknownStates = 0;
+ llvm::SmallSet<BinaryOperatorKind, 2> QueriedToUnknown;
// Loop goes through all of the columns exept the last one ('UnknownX2').
// We treat `UnknownX2` column separately at the end of the loop body.
@@ -1163,7 +1163,8 @@
CmpOpTable.getCmpOpState(CurrentOP, QueriedOP);
if (BranchState == OperatorRelationsTable::Unknown) {
- if (++UnknownStates == 2)
+ QueriedToUnknown.insert(QueriedOP);
+ if (QueriedToUnknown.size() == 2)
// If we met both Unknown states.
// if (x <= y) // assume true
// if (x != y) // assume true
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
