r290505 - Fix for PR15623 (corrected r290413 reverted at 290415). The patch eliminates unwanted ProgramState checker data propagation from an operand of the logical operation to operation result.

Anton Yartsev via cfe-commits cfe-commits at lists.llvm.org
Sat Dec 24 16:57:51 PST 2016


Author: ayartsev
Date: Sat Dec 24 18:57:51 2016
New Revision: 290505

URL: http://llvm.org/viewvc/llvm-project?rev=290505&view=rev
Log:
Fix for PR15623 (corrected r290413 reverted at 290415). 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

Modified:
    cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
    cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
    cfe/trunk/test/Analysis/malloc.c
    cfe/trunk/test/Analysis/misc-ps.c

Modified: cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp?rev=290505&r1=290504&r2=290505&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp Sat Dec 24 18:57:51 2016
@@ -666,23 +666,13 @@ void ExprEngine::VisitLogicalExpr(const
     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));

Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp?rev=290505&r1=290504&r2=290505&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Sat Dec 24 18:57:51 2016
@@ -254,6 +254,19 @@ ProgramStateRef SimpleConstraintManager:
   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))
+      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
+        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 +278,6 @@ ProgramStateRef SimpleConstraintManager:
   // 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);
 

Modified: cfe/trunk/test/Analysis/malloc.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/malloc.c?rev=290505&r1=290504&r2=290505&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/malloc.c (original)
+++ cfe/trunk/test/Analysis/malloc.c Sat Dec 24 18:57:51 2016
@@ -1763,6 +1763,17 @@ void testConstEscapeThroughAnotherField(
   constEscape(&(s.x)); // could free s->p!
 } // no-warning
 
+// PR15623
+int testNoCheckerDataPropogationFromLogicalOpOperandToOpResult(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
+}
+
 // ----------------------------------------------------------------------------
 // False negatives.
 

Modified: cfe/trunk/test/Analysis/misc-ps.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/misc-ps.c?rev=290505&r1=290504&r2=290505&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/misc-ps.c (original)
+++ cfe/trunk/test/Analysis/misc-ps.c Sat Dec 24 18:57:51 2016
@@ -191,3 +191,13 @@ static void PR16131(int x) {
   clang_analyzer_eval(*ip == 42); // expected-warning{{TRUE}}
   clang_analyzer_eval(*(int *)&v == 42); // expected-warning{{TRUE}}
 }
+
+// PR15623: Currently the analyzer doesn't handle symbolic expressions of the
+// form "(exp comparison_op expr) != 0" very well. We perform a simplification
+// translating 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.
+void PR15623(int n) {
+  if ((n == 0) != 0) {
+    clang_analyzer_eval(n == 0); // expected-warning{{TRUE}}
+  }
+}




More information about the cfe-commits mailing list