Fix for PR15623. The patch eliminates unwanted ProgramState checker data propagation from an operand of the logical operation to operation result.

The patch also simplifies an assume of a constraint of the form: "(exp comparison_op expr) != 0" to true into an assume of "exp comparison_op expr" to true. (And similarly, an assume of the form "(exp comparison_op expr) == 0" to true as an assume of exp comparison_op expr to false.) which improves precision overall.
https://reviews.llvm.org/D22862

llvm-svn: 290413

1 files changed, 15 insertions, 1 deletions

diff --git a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index c5e0f9b8626..ef2fcefb052 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -254,6 +254,21 @@ ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
   assert(BinaryOperator::isComparisonOp(Op) &&
          "Non-comparison ops should be rewritten as comparisons to zero.");
 
+  SymbolRef Sym = LHS;
+
+  // Simplification: translate an assume of a constraint of the form
+  // "(exp comparison_op expr) != 0" to true into an assume of 
+  // "exp comparison_op expr" to true. (And similarly, an assume of the form
+  // "(exp comparison_op expr) == 0" to true into an assume of
+  // "exp comparison_op expr" to false.)
+  if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
+    if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym)) {
+      BinaryOperator::Opcode Op = SE->getOpcode();
+      if (BinaryOperator::isComparisonOp(Op))
+        return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false));
+    }
+  }
+
   // Get the type used for calculating wraparound.
   BasicValueFactory &BVF = getBasicVals();
   APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
@@ -265,7 +280,6 @@ ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
   // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
   // the subclasses of SimpleConstraintManager to handle the adjustment.
-  SymbolRef Sym = LHS;
   llvm::APSInt Adjustment = WraparoundType.getZeroValue();
   computeAdjustment(Sym, Adjustment);