From 792be5df92e8d068ca32444383bc4e9e7f024bd8 Mon Sep 17 00:00:00 2001 From: Gabor Marton Date: Thu, 30 Sep 2021 23:26:22 +0200 Subject: [PATCH] [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 --- .../lib/StaticAnalyzer/Core/RangeConstraintManager.cpp | 18 +++++++++++++----- clang/test/Analysis/constraint_manager_conditions.cpp | 14 ++++++++++++++ 2 files changed, 27 insertions(+), 5 deletions(-) diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp index c972494..b949237 100644 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1112,7 +1112,7 @@ private: 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 @@ private: 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'). // We treat `UnknownX2` column separately at the end of the loop body. @@ -1163,15 +1168,18 @@ private: 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 different 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 f148151..c0eb73e 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}} + } +} -- 2.7.4