[analyzer][solver] Fix CmpOpTable handling bug

[martong]

Summary

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 Ops once.

[martong]

@ASDenysPetrov Gentle ping

[ASDenysPetrov]

Thanks for mentioning me. I'll make a review of this tomorrow.

[ASDenysPetrov]

I see the problem. It appears when you meet, say, > in a true branch and <= in a false branch which then turns into > again and trigger the flag, but shouldn't. Your solution is correct and looks clear.
Here I propose you one more to not use additional abstruction in a favor of performance. See inlines.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1129–1134

1170–1173

1179–1182

[martong]

• Update to use a single variable to track the state
• Make CurrentOP const

[martong]

Thanks for the review Denys!

I've updated accordingly to your suggestion, it is certainly more efficient. However, I've found your solution more difficult to follow, thus I've added some more explanatory comments.

[ASDenysPetrov]

LGTM

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1129–1135

Perfect explanation. This is really worth to be here.

P.S. My nit. Disregard if you think it is unnecessary.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

private:
   // It covers all possible combinations (see CmpOpTable description).
   // Note that `x` and `y` can also stand for subexpressions,
   // not only for actual symbols.
   Optional<RangeSet> getRangeForComparisonSymbol(SymbolRef Sym) {
     const auto *SSE = dyn_cast<SymSymExpr>(Sym);
     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))
       return llvm::None;
 
     static const OperatorRelationsTable CmpOpTable{};
 
     const SymExpr *LHS = SSE->getLHS();
     const SymExpr *RHS = SSE->getRHS();
     QualType T = SSE->getType();
 
     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.
     for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
 
       // Let's find an expression e.g. (x < y).
       BinaryOperatorKind QueriedOP = OperatorRelationsTable::getOpFromIndex(i);
       const SymSymExpr *SymSym = SymMgr.getSymSymExpr(LHS, QueriedOP, RHS, T);
       const RangeSet *QueriedRangeSet = getConstraint(State, SymSym);
for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
       // because the table is made assuming we are in the true branch.
       // E.g. when (x <= y) is false, then (x > y) is true.
       if (isInFalseBranch)
         QueriedOP = BinaryOperator::negateComparisonOp(QueriedOP);
 
       OperatorRelationsTable::TriStateKind BranchState =
           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)
                                                            : getFalseRange(T);
     }
 
     return llvm::None;
   }
 

clang/test/Analysis/constraint_manager_conditions.cpp

void comparison_le_ge(int x, int y) {
   if (x <= y)
     if (x >= y) {
       clang_analyzer_eval(x == y); // expected-warning{{TRUE}}
       clang_analyzer_eval(y == x); // expected-warning{{TRUE}}
       clang_analyzer_eval(x != y); // 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}}
+  }
+}