[PATCH] D22862: [analyzer] Fix for PR15623: eliminate unwanted ProgramState checker data propagation.

[Anton Yartsev via cfe-commits]

ayartsev updated this revision to Diff 78810.
ayartsev added a comment.

The updated patch implements Devin's solution. Please review.


https://reviews.llvm.org/D22862

Files:
  lib/StaticAnalyzer/Core/ExprEngineC.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  test/Analysis/unwanted-programstate-data-propagation.c


Index: test/Analysis/unwanted-programstate-data-propagation.c
===================================================================
--- test/Analysis/unwanted-programstate-data-propagation.c
+++ test/Analysis/unwanted-programstate-data-propagation.c
@@ -0,0 +1,26 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,debug.ExprInspection,unix.Malloc -verify %s
+
+// test for PR15623
+#include "Inputs/system-header-simulator.h"
+
+void clang_analyzer_eval(int);
+
+typedef __typeof(sizeof(int)) size_t;
+void *malloc(size_t);
+void free(void *);
+
+int test1(void) {
+   char *param = malloc(10);
+   char *value = malloc(10);
+   int ok = (param && value);
+   free(param);
+   free(value);
+   // Previously we ended up with 'Use of memory after it is freed' on return.
+   return ok; // no warning
+}
+
+void test2(int n) {
+  if ((n == 0) != 0) {
+    clang_analyzer_eval(n == 0); // expected-warning{{TRUE}}
+  }
+}
Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -250,6 +250,21 @@
   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());
@@ -261,7 +276,6 @@
   // 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);
 
Index: lib/StaticAnalyzer/Core/ExprEngineC.cpp
===================================================================
--- lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -618,23 +618,13 @@
     if (RHSVal.isUndef()) {
       X = RHSVal;
     } else {
-      DefinedOrUnknownSVal DefinedRHS = RHSVal.castAs<DefinedOrUnknownSVal>();
-      ProgramStateRef StTrue, StFalse;
-      std::tie(StTrue, StFalse) = N->getState()->assume(DefinedRHS);
-      if (StTrue) {
-        if (StFalse) {
-          // We can't constrain the value to 0 or 1.
-          // The best we can do is a cast.
-          X = getSValBuilder().evalCast(RHSVal, B->getType(), RHS->getType());
-        } else {
-          // The value is known to be true.
-          X = getSValBuilder().makeIntVal(1, B->getType());
-        }
-      } else {
-        // The value is known to be false.
-        assert(StFalse && "Infeasible path!");
-        X = getSValBuilder().makeIntVal(0, B->getType());
-      }
+      // We evaluate "RHSVal != 0" expression which result in 0 if the value is
+      // known to be false, 1 if the value is known to be true and a new symbol
+      // when the assumption is unknown.
+      nonloc::ConcreteInt Zero(getBasicVals().getValue(0, B->getType()));
+      X = evalBinOp(N->getState(), BO_NE, 
+                    svalBuilder.evalCast(RHSVal, B->getType(), RHS->getType()),
+                    Zero, B->getType());
     }
   }
   Bldr.generateNode(B, Pred, state->BindExpr(B, Pred->getLocationContext(), X));


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D22862.78810.patch
Type: text/x-patch
Size: 4057 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20161122/545cac6d/attachment.bin>