r357167 - [Analyzer] Constraint Manager - Calculate Effective Range for Differences

[Adam Balogh via cfe-commits]

Author: baloghadamsoftware
Date: Thu Mar 28 06:05:59 2019
New Revision: 357167

URL: http://llvm.org/viewvc/llvm-project?rev=357167&view=rev
Log:
[Analyzer] Constraint Manager - Calculate Effective Range for Differences

Since rL335814, if the constraint manager cannot find a range set for `A - B`
(where `A` and `B` are symbols) it looks for a range for `B - A` and returns
it negated if it exists. However, if a range set for both `A - B` and `B - A`
is stored then it only returns the first one. If we both use `A - B` and
`B - A`, these expressions behave as two totally unrelated symbols. This way
we miss some useful deductions which may lead to false negatives or false
positives.

This tiny patch changes this behavior: if the symbolic expression the
constraint manager is looking for is a difference `A - B`, it tries to
retrieve the range for both `A - B` and `B - A` and if both exists it returns
the intersection of range `A - B` and the negated range of `B - A`. This way
every time a checker applies new constraints to the symbolic difference or to
its negated it always affects both the original difference and its negated.

Differential Revision: https://reviews.llvm.org/D55007


Modified:
    cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
    cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    cfe/trunk/test/Analysis/constraint_manager_negate_difference.c

Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h?rev=357167&r1=357166&r2=357167&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h Thu Mar 28 06:05:59 2019
@@ -113,7 +113,8 @@ private:
 public:
   RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
                      llvm::APSInt Upper) const;
-
+  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
+                     const RangeSet &Other) const;
   RangeSet Negate(BasicValueFactory &BV, Factory &F) const;
 
   void print(raw_ostream &os) const;

Modified: cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp?rev=357167&r1=357166&r2=357167&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp Thu Mar 28 06:05:59 2019
@@ -173,6 +173,22 @@ RangeSet RangeSet::Intersect(BasicValueF
   return newRanges;
 }
 
+// Returns a set containing the values in the receiving set, intersected with
+// the range set passed as parameter.
+RangeSet RangeSet::Intersect(BasicValueFactory &BV, Factory &F,
+                             const RangeSet &Other) const {
+  PrimRangeSet newRanges = F.getEmptySet();
+
+  for (iterator i = Other.begin(), e = Other.end(); i != e; ++i) {
+    RangeSet newPiece = Intersect(BV, F, i->From(), i->To());
+    for (iterator j = newPiece.begin(), ee = newPiece.end(); j != ee; ++j) {
+      newRanges = F.add(newRanges, *j);
+    }
+  }
+
+  return newRanges;
+}
+
 // Turn all [A, B] ranges to [-B, -A]. Ranges [MIN, B] are turned to range set
 // [MIN, MIN] U [-B, MAX], when MIN and MAX are the minimal and the maximal
 // signed values of the type.
@@ -461,14 +477,21 @@ static RangeSet applyBitwiseConstraints(
 
 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
                                           SymbolRef Sym) {
-  if (ConstraintRangeTy::data_type *V = State->get<ConstraintRange>(Sym))
-    return *V;
-
-  BasicValueFactory &BV = getBasicVals();
+  ConstraintRangeTy::data_type *V = State->get<ConstraintRange>(Sym);
 
   // If Sym is a difference of symbols A - B, then maybe we have range set
   // stored for B - A.
-  if (const RangeSet *R = getRangeForMinusSymbol(State, Sym))
+  BasicValueFactory &BV = getBasicVals();
+  const RangeSet *R = getRangeForMinusSymbol(State, Sym);
+
+  // If we have range set stored for both A - B and B - A then calculate the
+  // effective range set by intersecting the range set for A - B and the
+  // negated range set of B - A.
+  if (V && R)
+    return V->Intersect(BV, F, R->Negate(BV, F));
+  if (V)
+    return *V;
+  if (R)
     return R->Negate(BV, F);
 
   // Lazily generate a new RangeSet representing all possible values for the

Modified: cfe/trunk/test/Analysis/constraint_manager_negate_difference.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/constraint_manager_negate_difference.c?rev=357167&r1=357166&r2=357167&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/constraint_manager_negate_difference.c (original)
+++ cfe/trunk/test/Analysis/constraint_manager_negate_difference.c Thu Mar 28 06:05:59 2019
@@ -96,3 +96,17 @@ void negate_mixed(int m, int n) {
     return;
   clang_analyzer_eval(n - m <= 0); // expected-warning{{TRUE}}
 }
+
+void effective_range(int m, int n) {
+  assert(m - n >= 0);
+  assert(n - m >= 0);
+  clang_analyzer_eval(m - n == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(n - m == 0); // expected-warning{{TRUE}}
+}
+
+void effective_range_2(int m, int n) {
+  assert(m - n <= 0);
+  assert(n - m <= 0);
+  clang_analyzer_eval(m - n == 0); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+  clang_analyzer_eval(n - m == 0); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+}