Author: Gabor Marton Date: 2021-10-06T18:28:03+02:00 New Revision: 792be5df92e8d068ca32444383bc4e9e7f024bd8
URL: https://github.com/llvm/llvm-project/commit/792be5df92e8d068ca32444383bc4e9e7f024bd8 DIFF: https://github.com/llvm/llvm-project/commit/792be5df92e8d068ca32444383bc4e9e7f024bd8.diff LOG: [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 Added: Modified: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp clang/test/Analysis/constraint_manager_conditions.cpp Removed: ################################################################################ diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index c972494f4262..b9492370c404 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1112,7 +1112,7 @@ class SymbolicRangeInferrer if (!SSE) return llvm::None; - BinaryOperatorKind CurrentOP = SSE->getOpcode(); + const BinaryOperatorKind CurrentOP = SSE->getOpcode(); // We currently do not support <=> (C++20). if (!BinaryOperator::isComparisonOp(CurrentOP) || (CurrentOP == BO_Cmp)) @@ -1126,7 +1126,12 @@ class SymbolicRangeInferrer 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 + // diff erent 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'). // We treat `UnknownX2` column separately at the end of the loop body. @@ -1163,15 +1168,18 @@ class SymbolicRangeInferrer CmpOpTable.getCmpOpState(CurrentOP, QueriedOP); if (BranchState == OperatorRelationsTable::Unknown) { - if (++UnknownStates == 2) - // If we met both Unknown states. + if (LastQueriedOpToUnknown != CurrentOP && + LastQueriedOpToUnknown != QueriedOP) { + // If we got the Unknown state for both diff erent operators. // if (x <= y) // assume true // if (x != y) // assume true // if (x < y) // would be also true // Get a state from `UnknownX2` column. BranchState = CmpOpTable.getCmpOpStateForUnknownX2(CurrentOP); - else + } else { + LastQueriedOpToUnknown = QueriedOP; continue; + } } return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T) diff --git a/clang/test/Analysis/constraint_manager_conditions.cpp b/clang/test/Analysis/constraint_manager_conditions.cpp index f148151ab357..c0eb73ef2470 100644 --- a/clang/test/Analysis/constraint_manager_conditions.cpp +++ b/clang/test/Analysis/constraint_manager_conditions.cpp @@ -211,3 +211,17 @@ void comparison_le_ge(int x, int y) { 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}} + } +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
