[analyzer] Use DisequalityMap while inferring constraints

[ASDenysPetrov]

Summary

Infer range using associated unequal symbols from DisequalityMap.
Example:

if(x == 42)
  if(x != y)
    y; // [-2147483648, 41]U[43, 2147483647]

NOTE: Currently, this revision causes test failure due to assertion in related to IteratorModeling.cpp in relateSymbols on line assert(isa<SymIntExpr>(CompSym) && "Symbol comparison must be a SymIntExpr`");`. It needs to be fixed in some way before loading. The revision is exposed to show the motivation for D130372.

[martong]

Awesome!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1512–1516

unite should be working with an empty set as well, shouldn't it?

clang/test/Analysis/range-inferring-from-disequality-map.cpp

10–11

Good point.

We should have an additional check in removeDeadBindings that goes through the disequality map of the dead symbol. And if any of the mapped classes are not dead then we shall not delete the dead symbol's equivalent class.

50–51

Why can't we return an empty set from getInvertedRangeFromDisequalityMap in this case? intersect should handle the rest then.

[martong]

clang/test/Analysis/range-inferring-from-disequality-map.cpp

10–11

Good point.

We should have an additional check in removeDeadBindings that goes through the disequality map of the dead symbol. And if any of the mapped classes are not dead then we shall not delete the dead symbol's equivalent class.

It would be better to address that in a child patch.

[ASDenysPetrov]

In D131006#3699017, @martong wrote:

Awesome!

Thank you!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1512–1516

You are right.

It's interesting that for some reason I was sure that unite returns empty if any given set is empty (mixed up with intersect). And this is at a time when I'm the author of unite :-P

clang/test/Analysis/range-inferring-from-disequality-map.cpp

50–51

Currently, we can't. At least, in this patch.
We produce infeasible branches (aka nullptr ProgramStateRef) when use ConstraintAssignor::assign.
But here we use SymbolicRangeInferrer which only produces a RangeSet. In other words, we don't store this range anywhere but infer it every time.

Basically, this is a work for the next patches. They should remove the TODOs.

[martong]

clang/test/Analysis/range-inferring-from-disequality-map.cpp

50–51

You mean this hunk?

for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
 RangeSet UpdatedConstraint = SymbolicRangeInferrer::inferRange(
     RangeFactory, State, DisequalClass);

 UpdatedConstraint = RangeFactory.deletePoint(UpdatedConstraint, *Point);

 // If we end up with at least one of the disequal classes to be
 // constrained with an empty range-set, the state is infeasible.
 if (UpdatedConstraint.isEmpty())
   return nullptr;

Yeah, I am not sure why do we infer a range here instead of simply getting the associated range from the constraint set. Inferring here might result with an inconsistent result. I think we should infer only in the SymbolicRangeInferrer.

[ASDenysPetrov]

@martong
This solution has an essential logical mistake. It relies on the erroneous assumption that
if x > 0 && x != y then y is in range [MIN, 0] but that's not true.
x and y could be 1 and 2 respectively.

My idea will only work with concrete ints but not ranges and it is already implemented in RangeConstraintManager in the snippet you mentioned (ConstraintAssignor::assign).

I'm sorry for the lost time.

P.S. The best I can do is just to add more tests for this. Created D131514 instead.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

RangeSet inferAs(SymbolRef Sym, QualType DestType) {
     return infer(DestType);
   }
 
   RangeSet infer(SymbolRef Sym) {
     return intersect(RangeFactory,
                      // Of course, we should take the constraint directly
                      // associated with this symbol into consideration.
                      getConstraint(State, Sym),
+                     // Use inverted ranges from DisequalityMap.
+                     getInvertedRangeFromDisequalityMap(State, Sym),
                      // Apart from the Sym itself, we can infer quite a lot if
                      // we look into subexpressions of Sym.
                      Visit(Sym));
   }
 
   RangeSet infer(EquivalenceClass Class) {
     if (const RangeSet *AssociatedConstraint = getConstraint(State, Class))
       return *AssociatedConstraint;
private:
   }
 
   /// Return a range set subtracting zero from \p Domain.
   RangeSet assumeNonZero(RangeSet Domain, QualType T) {
     APSIntType IntType = ValueFactory.getAPSIntType(T);
     return RangeFactory.deletePoint(Domain, IntType.getZeroValue());
   }
 
+  Optional<RangeSet> getInvertedRangeFromDisequalityMap(ProgramStateRef State,
+                                                        SymbolRef Sym) {
+    QualType T = Sym->getType();
+    // We only support integral types.
+    if (!T->isIntegralOrEnumerationType())
+      return llvm::None;
+
+    EquivalenceClass EC = EquivalenceClass::find(State, Sym);
+    const ClassSet *CS = State->get<DisequalityMap>(EC);
+
+    if (!CS)
+      return llvm::None;
+
+    bool IsFirst = true;
+    RangeSet RS = RangeFactory.getEmptySet();
+    for (EquivalenceClass EC : *CS) {
+      if (const RangeSet *RSPtr = getConstraint(State, EC)) {
+        if (IsFirst) {
+          IsFirst = false;
+          RS = *RSPtr;
+        } else
+          RS = RangeFactory.unite(RS, *RSPtr);
+      }
+    }
+
+    if (IsFirst)
+      return llvm::None;
+
+    RS = RangeFactory.castTo(RS, T);
+    RS = RangeFactory.invert(RS);
+    return RS;
+  }
+
   template <typename ProduceNegatedSymFunc>
   Optional<RangeSet> getRangeForNegatedExpr(ProduceNegatedSymFunc F,
                                             QualType T) {
     // Do not negate if the type cannot be meaningfully negated.
     if (!T->isUnsignedIntegerOrEnumerationType() &&
         !T->isSignedIntegerOrEnumerationType())
       return llvm::None;
 
void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State,
   printConstraints(Out, State, NL, Space, IsDot);
   printEquivalenceClasses(Out, State, NL, Space, IsDot);
   printDisequalities(Out, State, NL, Space, IsDot);
 }
 
 void RangeConstraintManager::printValue(raw_ostream &Out, ProgramStateRef State,
                                         SymbolRef Sym) {
   const RangeSet RS = getRange(State, Sym);
+  if (RS.isEmpty())
+    Out << "{ empty }";
+  else {
     Out << RS.getBitWidth() << (RS.isUnsigned() ? "u:" : "s:");
     RS.dump(Out);
   }
+}
 
 static std::string toString(const SymbolRef &Sym) {
   std::string S;
   llvm::raw_string_ostream O(S);
   Sym->dumpToStream(O);
   return O.str();
 }
 

clang/test/Analysis/range-inferring-from-disequality-map.cpp

+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+template<typename T>
+void clang_analyzer_value(T x);
+
+void test1(int x, int tmp) {
+  if(tmp != 0)
+    if(x != tmp)
+     clang_analyzer_value(x); // expected-warning {{32s:{ [0, 0] }}}
+  // TODO:  TODO: Keep x range correct even if associated disequalities are
+  // already dead.
+  (void)tmp; // Keep alive.
+}
+
+void test2(int x, int tmp) {
+  if(x != tmp)
+    if(tmp < 0)
+      clang_analyzer_value(x); // expected-warning {{32s:{ [0, 2147483647] }}}
+  // TODO:  TODO: Keep x range correct even if associated disequalities are
+  // already dead.
+  (void)tmp; // Keep alive.
+}
+
+void test3(int x, int tmp) {
+  if(x != tmp)
+    if(tmp > 42 && tmp < 87)
+      clang_analyzer_value(x); // expected-warning {{32s:{ [-2147483648, 42], [87, 2147483647] }}}
+  // TODO:  TODO: Keep x range correct even if associated disequalities are
+  // already dead.
+  (void)tmp; // Keep alive.
+}
+
+void test4(int x, int tmp1, int tmp2) {
+  if(x != tmp1) {
+    if (tmp1 < 0 && tmp2 > 0) {
+      clang_analyzer_value(x); // expected-warning {{32s:{ [0, 2147483647] }}}
+      if(x != tmp2)
+        clang_analyzer_value(x); // expected-warning {{32s:{ [0, 0] }}}
+    }
+  }
+  // TODO:  TODO: Keep x range correct even if associated disequalities are
+  // already dead.
+  (void)tmp1; // Keep alive.
+  (void)tmp2; // Keep alive.
+}
+
+void test5(int x, int tmp1, int tmp2) {
+  if (tmp1 < 42 && tmp2 >= 42) 
+    if(x != tmp1 && x != tmp2)
+      // TODO: This condition should be infeasible.
+      //       Thus, the branch should be unreachable.
+      clang_analyzer_value(x); // expected-warning {{{ empty }}}
+  // TODO:  TODO: Keep x range correct even if associated disequalities are
+  // already dead.
+  (void)tmp1; // Keep alive.
+  (void)tmp2; // Keep alive.
+}