[clang] 792be5d - [analyzer][solver] Fix CmpOpTable handling bug

[Gabor Marton via cfe-commits]

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}}
+  }
+}