forked from OSchip/llvm-project
[analyzer][solver] Fix CmpOpTable handling bug
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. Differential Revision: https://reviews.llvm.org/D110910
This commit is contained in:
parent
b2c906da19
commit
792be5df92
|
@ -1112,7 +1112,7 @@ private:
|
||||||
if (!SSE)
|
if (!SSE)
|
||||||
return llvm::None;
|
return llvm::None;
|
||||||
|
|
||||||
BinaryOperatorKind CurrentOP = SSE->getOpcode();
|
const BinaryOperatorKind CurrentOP = SSE->getOpcode();
|
||||||
|
|
||||||
// We currently do not support <=> (C++20).
|
// We currently do not support <=> (C++20).
|
||||||
if (!BinaryOperator::isComparisonOp(CurrentOP) || (CurrentOP == BO_Cmp))
|
if (!BinaryOperator::isComparisonOp(CurrentOP) || (CurrentOP == BO_Cmp))
|
||||||
|
@ -1126,7 +1126,12 @@ private:
|
||||||
|
|
||||||
SymbolManager &SymMgr = State->getSymbolManager();
|
SymbolManager &SymMgr = State->getSymbolManager();
|
||||||
|
|
||||||
int UnknownStates = 0;
|
// We use this variable to store the last queried operator (`QueriedOP`)
|
||||||
|
// for which the `getCmpOpState` returned with `Unknown`. If there are two
|
||||||
|
// different OPs that returned `Unknown` then we have to query the special
|
||||||
|
// `UnknownX2` column. We assume that `getCmpOpState(CurrentOP, CurrentOP)`
|
||||||
|
// never returns `Unknown`, so `CurrentOP` is a good initial value.
|
||||||
|
BinaryOperatorKind LastQueriedOpToUnknown = CurrentOP;
|
||||||
|
|
||||||
// Loop goes through all of the columns exept the last one ('UnknownX2').
|
// Loop goes through all of the columns exept the last one ('UnknownX2').
|
||||||
// We treat `UnknownX2` column separately at the end of the loop body.
|
// We treat `UnknownX2` column separately at the end of the loop body.
|
||||||
|
@ -1163,16 +1168,19 @@ private:
|
||||||
CmpOpTable.getCmpOpState(CurrentOP, QueriedOP);
|
CmpOpTable.getCmpOpState(CurrentOP, QueriedOP);
|
||||||
|
|
||||||
if (BranchState == OperatorRelationsTable::Unknown) {
|
if (BranchState == OperatorRelationsTable::Unknown) {
|
||||||
if (++UnknownStates == 2)
|
if (LastQueriedOpToUnknown != CurrentOP &&
|
||||||
// If we met both Unknown states.
|
LastQueriedOpToUnknown != QueriedOP) {
|
||||||
|
// If we got the Unknown state for both different operators.
|
||||||
// if (x <= y) // assume true
|
// if (x <= y) // assume true
|
||||||
// if (x != y) // assume true
|
// if (x != y) // assume true
|
||||||
// if (x < y) // would be also true
|
// if (x < y) // would be also true
|
||||||
// Get a state from `UnknownX2` column.
|
// Get a state from `UnknownX2` column.
|
||||||
BranchState = CmpOpTable.getCmpOpStateForUnknownX2(CurrentOP);
|
BranchState = CmpOpTable.getCmpOpStateForUnknownX2(CurrentOP);
|
||||||
else
|
} else {
|
||||||
|
LastQueriedOpToUnknown = QueriedOP;
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T)
|
return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T)
|
||||||
: getFalseRange(T);
|
: getFalseRange(T);
|
||||||
|
|
|
@ -211,3 +211,17 @@ void comparison_le_ge(int x, int y) {
|
||||||
clang_analyzer_eval(y != x); // expected-warning{{FALSE}}
|
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}}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
Loading…
Reference in New Issue