[analyzer][solver][NFC] Introduce ConstraintAssignor

[vsavchenko]

Summary

The new component is a symmetric response to SymbolicRangeInferrer.
While the latter is the unified component, which answers all the
questions what does the solver knows about a particular symbolic
expression, assignor associates new constraints (aka "assumes")
with symbolic expressions and can imply additional knowledge that
the solver can extract and use later on.

• Why do we need it and why is SymbolicRangeInferrer not enough?

As it is noted before, the inferrer only helps us to get the most
precise range information based on the existing knowledge and on the
mathematical foundations of different operations that symbolic
expressions actually represent. It doesn't introduce new constraints.

The assignor, on the other hand, can impose constraints on other
symbols using the same domain knowledge.

• But for some expressions, SymbolicRangeInferrer looks into constraints for similar expressions, why can't we do that for all the cases?

That's correct! But in order to do something like this, we should
have a finite number of possible "similar expressions".

Let's say we are asked about $a - $b and we know something about
$b - $a. The inferrer can invert this expression and check
constraints for $b - $a. This is simple!
But let's say we are asked about $a and we know that $a * $b != 0.
In this situation, we can imply that $a != 0, but the inferrer shouldn't
try every possible symbolic expression X to check if $a * X or
X * $a is constrained to non-zero.

With the assignor mechanism, we can catch this implication right at
the moment we associate $a * $b with non-zero range, and set similar
constraints for $a and $b as well.

[martong]

Generally it looks okay to me. However, I have a question:
In SimpleSValBuilder::evalBinOpNN we do infer values to symbols. E.g. if we have an expression y / x and y is known to be 0 then we assign 0 to the division expression. On one hand, this logic is independent from whichever solver implementation we use. On the other hand, we do the value inferring based on the fact that y is a constrainted to be in [0, 0] so in this sense this infer logic should be in the solver.
What do you think, perhaps another round of refactoring should move that logic into the solver?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1388

New now, but it might be old after a while.

1394

typo, can.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1388

Whoops, this is how I first named the class. It is not new handler, but new constraint. Because of this ambiguity I actually renamed it 😅

[martong]

Uhh, what the hell happened with the Stack?

[vsavchenko]

Fix comments

[uabelho]

Hi,

When compiling with gcc I see the following new warnings with this patch:

[4/22] Building CXX object tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/obj.clangStaticAnalyzerCore.dir/RangeConstraintManager.cpp.o
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
 2395 | ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
      |                 ^~~~~~~~~~~~~~~~~~~~~~
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
 2384 | RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
      |          ^~~~~~~~~~~~~~~~~~~~~~

Will those methods be used or can they be removed?

[martong]

In D105692#2879186, @uabelho wrote:

Hi,

When compiling with gcc I see the following new warnings with this patch:

[4/22] Building CXX object tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/obj.clangStaticAnalyzerCore.dir/RangeConstraintManager.cpp.o
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
 2395 | ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
      |                 ^~~~~~~~~~~~~~~~~~~~~~
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
 2384 | RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
      |          ^~~~~~~~~~~~~~~~~~~~~~

Will those methods be used or can they be removed?

I think they can be removed, waiting for Valeriy's approval.
https://reviews.llvm.org/D106063

[uabelho]

In D105692#2879983, @martong wrote:

In D105692#2879186, @uabelho wrote:

Hi,

When compiling with gcc I see the following new warnings with this patch:

[4/22] Building CXX object tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/obj.clangStaticAnalyzerCore.dir/RangeConstraintManager.cpp.o
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
 2395 | ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
      |                 ^~~~~~~~~~~~~~~~~~~~~~
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
 2384 | RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
      |          ^~~~~~~~~~~~~~~~~~~~~~

Will those methods be used or can they be removed?

I think they can be removed, waiting for Valeriy's approval.
https://reviews.llvm.org/D106063

Thanks!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
   return State->get<ConstraintRange>(Class);
 }
 
 LLVM_NODISCARD inline const RangeSet *getConstraint(ProgramStateRef State,
                                                     SymbolRef Sym) {
   return getConstraint(State, EquivalenceClass::find(State, Sym));
 }
 
+LLVM_NODISCARD ProgramStateRef setConstraint(ProgramStateRef State,
+                                             EquivalenceClass Class,
+                                             RangeSet Constraint) {
+  return State->set<ConstraintRange>(Class, Constraint);
+}
+
+LLVM_NODISCARD ProgramStateRef setConstraints(ProgramStateRef State,
+                                              ConstraintRangeTy Constraints) {
+  return State->set<ConstraintRange>(Constraints);
+}
+
 //===----------------------------------------------------------------------===//
 //                       Equality/diseqiality abstraction
 //===----------------------------------------------------------------------===//
 
 /// A small helper structure representing symbolic equality.
 ///
 /// Equality check can have different forms (like a == b or a - b) and this
 /// class encapsulates those away if the only thing the user wants to check -
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
   }
 
   // Nevertheless, the symmetrical range for RHS is a conservative estimate
   // for any sign of either LHS, or RHS.
   return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
 }
 
 //===----------------------------------------------------------------------===//
+//                         Constraint assignment logic
+//===----------------------------------------------------------------------===//
+
+/// ConstraintAssignorBase is a small utility class that unifies visitor
+/// for ranges with a visitor for constraints (rangeset/range/constant).
+///
+/// It is designed to have one derived class, but generally it can have more.
+/// Derived class can control which types we handle by defining methods of the
+/// following form:
+///
+///   bool handle${SYMBOL}To${CONSTRAINT}(const SYMBOL *Sym,
+///                                       CONSTRAINT Constraint);
+///
+/// where SYMBOL is the type of the symbol (e.g. SymSymExpr, SymbolCast, etc.)
+///       CONSTRAINT is the type of constraint (RangeSet/Range/Const)
+///       return value signifies whether we should try other handle methods
+///          (i.e. false would mean to stop right after calling this method)
+template <class Derived> class ConstraintAssignorBase {
+public:
+  using Const = const llvm::APSInt &;
+
+#define DISPATCH(CLASS) return assign##CLASS##Impl(cast<CLASS>(Sym), Constraint)
+
+#define ASSIGN(CLASS, TO, SYM, CONSTRAINT)                                     \
+  if (!static_cast<Derived *>(this)->assign##CLASS##To##TO(SYM, CONSTRAINT))   \
+  return false
+
+  void assign(SymbolRef Sym, RangeSet Constraint) {
+    assignImpl(Sym, Constraint);
+  }
+
+  bool assignImpl(SymbolRef Sym, RangeSet Constraint) {
+    switch (Sym->getKind()) {
+#define SYMBOL(Id, Parent)                                                     \
+  case SymExpr::Id##Kind:                                                      \
+    DISPATCH(Id);
+#include "clang/StaticAnalyzer/Core/PathSensitive/Symbols.def"
+    }
+    llvm_unreachable("Unknown SymExpr kind!");
+  }
+
+#define DEFAULT_ASSIGN(Id)                                                     \
+  bool assign##Id##To##RangeSet(const Id *Sym, RangeSet Constraint) {          \
+    return true;                                                               \
+  }                                                                            \
+  bool assign##Id##To##Range(const Id *Sym, Range Constraint) { return true; } \
+  bool assign##Id##To##Const(const Id *Sym, Const Constraint) { return true; }
+
+  // When we dispatch for constraint types, we first try to check
+  // if the new constraint is the constant and try the corresponding
+  // assignor methods.  If it didn't interrupt, we can proceed to the
+  // range, and finally to the range set.
+#define CONSTRAINT_DISPATCH(Id)                                                \
+  if (const llvm::APSInt *Const = Constraint.getConcreteValue()) {             \
+    ASSIGN(Id, Const, Sym, *Const);                                            \
+  }                                                                            \
+  if (Constraint.size() == 1) {                                                \
+    ASSIGN(Id, Range, Sym, *Constraint.begin());                               \
+  }                                                                            \
+  ASSIGN(Id, RangeSet, Sym, Constraint)
+
+  // Our internal assign method first tries to call assignor methods for all
+  // constraint types that apply.  And if not interrupted, continues with its
+  // parent class.
+#define SYMBOL(Id, Parent)                                                     \
+  bool assign##Id##Impl(const Id *Sym, RangeSet Constraint) {                  \
+    CONSTRAINT_DISPATCH(Id);                                                   \
+    DISPATCH(Parent);                                                          \
+  }                                                                            \
+  DEFAULT_ASSIGN(Id)
+#define ABSTRACT_SYMBOL(Id, Parent) SYMBOL(Id, Parent)
+#include "clang/StaticAnalyzer/Core/PathSensitive/Symbols.def"
+
+  // Default implementations for the top class that doesn't have parents.
+  bool assignSymExprImpl(const SymExpr *Sym, RangeSet Constraint) {
+    CONSTRAINT_DISPATCH(SymExpr);
+    return true;
+  }
+  DEFAULT_ASSIGN(SymExpr);
+
+#undef DISPATCH
+#undef CONSTRAINT_DISPATCH
+#undef DEFAULT_ASSIGN
+#undef ASSIGN
+};
+
+/// A little component aggregating all of the reasoning we have about
+/// assigning new constraints to symbols.
+///
+/// The main purpose of this class is to associate constraints to symbols,
+/// and impose additional constraints on other symbols, when we can imply
+/// them.
+///
+/// It has a nice symmetry with SymbolicRangeInferrer.  When the latter
+/// can provide more precise ranges by looking into the operands of the
+/// expression in question, ConstraintAssignor looks into the operands
+/// to see if we can imply more from the new constraint.
+class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
+public:
+  template <class ClassOrSymbol>
+  LLVM_NODISCARD static ProgramStateRef
+  assign(ProgramStateRef State, SValBuilder &Builder, RangeSet::Factory &F,
+         ClassOrSymbol CoS, RangeSet NewConstraint) {
+    if (!State || NewConstraint.isEmpty())
+      return nullptr;
+
+    ConstraintAssignor Assignor{State, Builder, F};
+    return Assignor.assign(CoS, NewConstraint);
+  }
+
+  inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint);
+
+private:
+  ConstraintAssignor(ProgramStateRef State, SValBuilder &Builder,
+                     RangeSet::Factory &F)
+      : State(State), Builder(Builder), RangeFactory(F) {}
+  using Base = ConstraintAssignorBase<ConstraintAssignor>;
+
+  /// Base method for handling new constraints for symbols.
+  LLVM_NODISCARD ProgramStateRef assign(SymbolRef Sym, RangeSet NewConstraint) {
+    // All constraints are actually associated with equivalence classes, and
+    // that's what we are going to do first.
+    State = assign(EquivalenceClass::find(State, Sym), NewConstraint);
+    if (!State)
+      return nullptr;
+
+    // And after that we can check what other things we can get from this
+    // constraint.
+    Base::assign(Sym, NewConstraint);
+    return State;
+  }
+
+  /// Base method for handling new constraints for classes.
+  LLVM_NODISCARD ProgramStateRef assign(EquivalenceClass Class,
+                                        RangeSet NewConstraint) {
+    // There is a chance that we might need to update constraints for the
+    // classes that are known to be disequal to Class.
+    //
+    // In order for this to be even possible, the new constraint should
+    // be simply a constant because we can't reason about range disequalities.
+    if (const llvm::APSInt *Point = NewConstraint.getConcreteValue()) {
+
+      ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+      ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
+
+      // Add new constraint.
+      Constraints = CF.add(Constraints, Class, NewConstraint);
+
+      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;
+
+        Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
+      }
+      assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
+                                         "a state with infeasible constraints");
+
+      return setConstraints(State, Constraints);
+    }
+
+    return setConstraint(State, Class, NewConstraint);
+  }
+
+  ProgramStateRef State;
+  SValBuilder &Builder;
+  RangeSet::Factory &RangeFactory;
+};
+
+//===----------------------------------------------------------------------===//
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
 
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
       : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}
 
ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
 private:
   RangeSet::Factory F;
 
   RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
   RangeSet getRange(ProgramStateRef State, EquivalenceClass Class);
+  ProgramStateRef setRange(ProgramStateRef State, SymbolRef Sym,
+                           RangeSet Range);
+  ProgramStateRef setRange(ProgramStateRef State, EquivalenceClass Class,
+                           RangeSet Range);
 
   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
   RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
private:
   template <bool EQ>
   ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State,
                         SymbolRef Sym, const llvm::APSInt &Int,
                         const llvm::APSInt &Adjustment) {
     if (NewConstraint.isEmpty())
       // This is an infeasible assumption.
       return nullptr;
 
-    if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) {
+    if (ProgramStateRef NewState = setRange(State, Sym, NewConstraint)) {
       if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
         // If the original assumption is not Sym + Adjustment !=/</> Int,
         // we should invert IsEquality flag.
         Equality->IsEquality = Equality->IsEquality != EQ;
         return track(NewState, *Equality);
       }
 
       return NewState;
ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS,
                                    SymbolRef RHS) {
     return EquivalenceClass::markDisequal(F, State, LHS, RHS);
   }
 
   ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
                                 SymbolRef RHS) {
     return EquivalenceClass::merge(F, State, LHS, RHS);
   }
+};
 
-  LLVM_NODISCARD ProgramStateRef setConstraint(ProgramStateRef State,
-                                               EquivalenceClass Class,
-                                               RangeSet Constraint) {
-    ConstraintRangeTy Constraints = State->get<ConstraintRange>();
-    ConstraintRangeTy::Factory &CF = State->get_context<ConstraintRange>();
-
-    assert(!Constraint.isEmpty() && "New constraint should not be empty");
-
-    // Add new constraint.
-    Constraints = CF.add(Constraints, Class, Constraint);
-
-    // There is a chance that we might need to update constraints for the
-    // classes that are known to be disequal to Class.
-    //
-    // In order for this to be even possible, the new constraint should
-    // be simply a constant because we can't reason about range disequalities.
-    if (const llvm::APSInt *Point = Constraint.getConcreteValue())
-      for (EquivalenceClass DisequalClass : Class.getDisequalClasses(State)) {
-        RangeSet UpdatedConstraint = getRange(State, DisequalClass);
-        UpdatedConstraint = F.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;
-
-        Constraints = CF.add(Constraints, DisequalClass, UpdatedConstraint);
-      }
-
-    assert(areFeasible(Constraints) && "Constraint manager shouldn't produce "
-                                       "a state with infeasible constraints");
-
-    return State->set<ConstraintRange>(Constraints);
-  }
-
-  // Associate a constraint to a symbolic expression. First, we set the
-  // constraint in the State, then we try to simplify existing symbolic
-  // expressions based on the newly set constraint.
-  LLVM_NODISCARD inline ProgramStateRef
-  setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) {
-    assert(State);
-
-    State = setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
-    if (!State)
-      return nullptr;
-
-    // We have a chance to simplify existing symbolic values if the new
-    // constraint is a constant.
-    if (!Constraint.getConcreteValue())
-      return State;
-
-    llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
-    // Iterate over all equivalence classes and try to simplify them.
-    ClassMembersTy Members = State->get<ClassMembers>();
-    for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
-      EquivalenceClass Class = ClassToSymbolSet.first;
-      State = Class.simplify(getSValBuilder(), F, State);
-      if (!State)
-        return nullptr;
-      SimplifiedClasses.insert(Class);
-    }
+bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
+                                              const llvm::APSInt &Constraint) {
+    State = Class.simplify(Builder, RangeFactory, State);
+      return false;
 
-    // Trivial equivalence classes (those that have only one symbol member) are
-    // not stored in the State. Thus, we must skim through the constraints as
-    // well. And we try to simplify symbols in the constraints.
-    ConstraintRangeTy Constraints = State->get<ConstraintRange>();
-    for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
-      EquivalenceClass Class = ClassConstraint.first;
-      if (SimplifiedClasses.count(Class)) // Already simplified.
-        continue;
-      State = Class.simplify(getSValBuilder(), F, State);
-      if (!State)
-        return nullptr;
-    }
+    State = Class.simplify(Builder, RangeFactory, State);
+      return false;
 
-    return State;
-  }
-};
+  return true;
 
 } // end anonymous namespace
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
                                    ExprEngine *Eng) {
   return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
   return SymbolicRangeInferrer::inferRange(F, State, Sym);
 }
 
 RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
                                           EquivalenceClass Class) {
   return SymbolicRangeInferrer::inferRange(F, State, Class);
 }
 
+ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
+                                                 SymbolRef Sym,
+                                                 RangeSet Range) {
+  return ConstraintAssignor::assign(State, getSValBuilder(), F, Sym, Range);
+}
+
+ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
+                                                 EquivalenceClass Class,
+                                                 RangeSet Range) {
+  return ConstraintAssignor::assign(State, getSValBuilder(), F, Class, Range);
+}
+
 //===------------------------------------------------------------------------===
 // assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
 // and (x, y) for open ranges. These ranges are modular, corresponding with
 // a common treatment of C integer overflow. This means that these methods
 // do not have to worry about overflow; RangeSet::Intersect can handle such a
RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,
   return F.intersect(SymRange, Lower, Upper);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  return setRange(St, Sym, New);
 }
 
 RangeSet
 RangeConstraintManager::getSymLERange(llvm::function_ref<RangeSet()> RS,
                                       const llvm::APSInt &Int,
                                       const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St,
   return getSymLERange([&] { return getRange(St, Sym); }, Int, Adjustment);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  return setRange(St, Sym, New);
 }
 
 ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGERange(State, Sym, From, Adjustment);
   if (New.isEmpty())
     return nullptr;
   RangeSet Out = getSymLERange([&] { return New; }, To, Adjustment);
-  return Out.isEmpty() ? nullptr : setConstraint(State, Sym, Out);
+  return setRange(State, Sym, Out);
 }
 
 ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
   RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
   RangeSet New(F.add(RangeLT, RangeGT));
-  return New.isEmpty() ? nullptr : setConstraint(State, Sym, New);
+  return setRange(State, Sym, New);
 }
 
 //===----------------------------------------------------------------------===//
 // Pretty-printing.
 //===----------------------------------------------------------------------===//
 
 void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State,
                                        const char *NL, unsigned int Space,