[analyzer] Introduce small improvements to the solver infra

[vsavchenko]

Summary

• Add a new function to delete points from range sets.
• Introduce an internal generic interface for range set intersections.
• Remove unnecessary bits from a couple of solver functions.
• Add in-code sections.

[vsavchenko]

Remove hunk that is meant for the next commmit

[vsavchenko]

Fix comment

[vsavchenko]

Add forgotten nodiscards

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

558–567

I'm a bit confused, why aren't these invocations of getRangeForInvertedSub() and getRangeForComparisonSymbol() implemented simply as steps in Visit()? What's so different about them, other then our desire not to go into infinite recursion (which should probably be addressed via memoization)?

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

558–567

I even had a patch that moves these two functions inside of the Visit, but then I reverted that change.
Right now the logic for each symbol is like this: let's try to find anything on this symbol in the existing constraints and if we did find something - return it. And only if that didn't work, we try to figure out something from the sub-tree on its own.

So what does that mean in here: that we will need to make a performance impacting [probably nothing serious, but still a functional] change - to intersect the range assigned to the symbol and whatever we can infer from its subtrees. It would be good to have when we support binary operators +/-/==/<=/etc. because it can help narrowing it down.

As of now, it will give no information, only possible overhead of traversing a tree. For this reason, I suggest to move those separately and AFTER we support more operators, because that will also have a couple of good motivation examples.

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

467–470

Why do we have these representations in the first place?

It sounds like you're treating null pointers / empty optionals equivalently to full ranges (i.e., intersecting with them has no effect). How hard would it be to simply construct an actual full range in all the places in which we currently have empty optionals?

[xazax.hun]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

373

Sorry if my question is dumb, but I do not really have a mental model at this point about where do we actually handle types and overflows. Will this method work when we delete the last or the first element of the full range of a type?

I think having unit tests would be a great way to make this clear. I always felt that the solver is actually something that should be really easy to test separately and those tests would also help a lot to understand how the solver is actually working.

467–470

+1

I also find this confusing. Should I interpret a None as a full or empty range? Does this depend on the context or a general rule? Is there any reason we need to handle nullable pointers or could we actually make call sites more uniform to get rid of some of the complexity here?

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

467–470

It sounds like you're treating null pointers / empty optionals equivalently to full ranges (i.e., intersecting with them has no effect)

It is not actually true. Empty optionals is the information that "this range information is not available for this symbol". It is true that intersecting with them has no effect, but they are semantically different in other aspects.

Currently solver RELIES on the information that whether the range is available or not (see my previous comment), and we simply couldn't get rid of this behavior as part of NFC.

How hard would it be to simply construct an actual full range in all the places in which we currently have empty optionals?

It is not hard architecturally, but it WILL make the change functional and possibly impact the performance.

Should I interpret a None as a full or empty range?

Neither of those. That is the problem right now, that we rely on different sources of information for the ranges and behave differently depending on whether one piece of information is available or not.

Does this depend on the context or a general rule?

Semantics are always the same - this info is not available.

Is there any reason we need to handle nullable pointers?

State->get<XYZ>(abc) returns a nullable pointer meaning optional object, it is hard to avoid it especially because we currently behave very differently when this information is not available.

...could we actually make call sites more uniform to get rid of some of the complexity here?

Yes we can, but later on. See the explanations above and in my other comment.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

373

Sorry if my question is dumb...

No problem at all, I also had this question when I looked at that.

where do we actually handle types and overflows

APInt class basically does it all for us in terms of overflows, number of bits, and signedness.

I think having unit tests would be a great way to make this clear

I am onboard! I will add a framework for testing the solver in later patches.

[vsavchenko]

Rebase

[ASDenysPetrov]

Hi @vsavchenko , sorry for the late review.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

367–378

Useful function. But I'd better rename it to subtract as we are working with sets (as a mathimatical collection). We should have a such one for the Ranges not only for Points.
We have intersect, delete aka subtract. And we also need to have functions union and symmetricDifference to cover full palette of common operations on sets.

734

As for me, I'd call this like getRangeForNegatedSymSymExpr, since you do Negate operation inside.

841–844

Don't you think this is too complicated for such a simple getter?
Maybe we can just construct the range using smth about RangeSet(RangeFactory, ++Zero, --Zero); ?

[vsavchenko]

Hi @ASDenysPetrov no problem at all! Thanks for taking your time and checking it.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

367–378

I agree that we should have a full set of functions. I don't agree however, that this function is a subtract. Subtract is an operation on two sets and here we have a set and a point. One might argue that a point is just a very simple set, that's true, but real subtract would be more complex in its implementation.

Naming it delete, on the other hand, I was coming from a notion of deleting points or neighbourhoods (https://en.wikipedia.org/wiki/Neighbourhood_(mathematics)#Deleted_neighbourhood).

734

I'm not super happy about my name either, but I feel like it describes it better than the previous name and your version. That function doesn't work for any SymSymExpr and it doesn't simply negate whatever we gave it. It works specifically for symbolic subtractions and this is the information I want to be reflected in the name.

841–844

It is more complex than a false range but there is a reason for it.

First of all, RangeSet can't have ranges where the end is greater than its start. Only Intersect can handle such ranges correctly. Another thing is that ranges like that mean [MIN, --Zero], [++Zero, MAX] and without a type we can't really say what MIN and MAX are, so such constructor for RangeSet simply cannot exist.

Another point is that we do need to have [MIN, -1], [+1, MAX] as opposed to [-1, -1], [+1, +1] because of C language (it doesn't have boolean type), and because of the cases like a - b where we know that a != b.

I hope that answers the question.

[ASDenysPetrov]

@vsavchenko
Thank you.
Despite of all of my nits, LGTM!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

367–378

One might argue that a point is just a very simple set

That's actually what I mean :) and for this particular case you may leave the implementation as is. And for me it still does what subtract does. But I'm OK, I don't insist.

734

Oh, I just assumed ...Sub at the end as a subexpression but you mean subtraction. What I'm trying to say is that we can rename it like getRangeFor...the expression which this function can handle. E.g. getRangeForNegatedSubtractionSymSymExpr. My point is in a speaking name.

I think invertion is not something appropriate in terms of applying minus operator. I think invertion of zero should be something opposite but not a zero. Because when you would like to implement the function which turns [A, B] into [MIN, A)U(B, MAX], what would be the name of it? I think this is an invertion.

But this is not a big deal, it's just my thoughts.

841–844

I just want this function has low complexity and be more lightweight as getFalseRange. And if we have any chance to simplify it (and you have all the data to get MIN and MAX), it'd be cool.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

734

My thought process here was that we are trying to get range for A - B and there is also information on B - A, so we can get something for A - B based on that. So, it doesn't really matter what it does under the hood with ranges, it matters what its semantics are. Here I called B - A an inverted subtraction.
I don't really know what would be the best name, but I thought that this one makes more sense.

841–844

infer(QualType T) does just that ☺️ So it is a pretty low complexity.

[ASDenysPetrov]

@vsavchenko
OK, let it be. )

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

467–470

it WILL make the change functional and possibly impact the performance

Mmm, yeah, i guess the necessity to construct a full range and then do the possibly O(N) intersection when it'll do nothing most of the time is indeed daunting.

Maybe we should implement full ranges as a special case in the RangeSet class? Like, don't actually construct the single range, just remember the type; special-case all operations on such sets to perform trivially in O(1), etc.?

734

Because when you would like to implement the function which turns [A, B] into [MIN, A)U(B, MAX], what would be the name of it? I think this is an invertion.

https://en.wikipedia.org/wiki/Complement_(set_theory)
https://en.wikipedia.org/wiki/Inverse_function

"Negated subtraction" is definitely my favorite so far. "Mirrored" might be a good layman term as well.

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

734

https://en.wikipedia.org/wiki/Complement_(set_theory)
https://en.wikipedia.org/wiki/Inverse_function

Thanks for the links, @NoQ. That's much definite now.

[vsavchenko]

Rename function

clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

private:
   bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const;
 
 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;
+  RangeSet Delete(BasicValueFactory &BV, Factory &F,
+                  const llvm::APSInt &Point) const;
 
   void print(raw_ostream &os) const;
 
   bool operator==(const RangeSet &other) const {
     return ranges == other.ranges;
   }
 };
 
 class ConstraintRange {};
 using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
 
 template <>
 struct ProgramStateTrait<ConstraintRange>
     : public ProgramStatePartialTrait<ConstraintRangeTy> {
   static void *GDMIndex();
 };
 
-
 class RangedConstraintManager : public SimpleConstraintManager {
 public:
   RangedConstraintManager(ExprEngine *EE, SValBuilder &SB)
       : SimpleConstraintManager(EE, SB) {}
 
   ~RangedConstraintManager() override;
 
   //===------------------------------------------------------------------===//
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
                                           bool InRange) override;
 
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                        bool Assumption) override;
 
 protected:
   /// Assume a constraint between a symbolic expression and a concrete integer.
   virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
                                        BinaryOperator::Opcode op,
                                        const llvm::APSInt &Int);
 
   //===------------------------------------------------------------------===//
   // Interface that subclasses must implement.
   //===------------------------------------------------------------------===//
 
   // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
   // operation for the method being invoked.
 
protected:
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 private:
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
-} // end GR namespace
-
-} // end clang namespace
+} // namespace ento
+} // namespace clang
 
 #endif

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 public:
   constexpr size_t getCmpOpCount() const { return CmpOpCount; }
 
   static BinaryOperatorKind getOpFromIndex(size_t Index) {
     return static_cast<BinaryOperatorKind>(Index + BO_LT);
   }
 
   TriStateKind getCmpOpState(BinaryOperatorKind CurrentOP,
                              BinaryOperatorKind QueriedOP) const {
     return CmpOpTable[getIndexFromOp(CurrentOP)][getIndexFromOp(QueriedOP)];
   }
 
   TriStateKind getCmpOpStateForUnknownX2(BinaryOperatorKind CurrentOP) const {
     return CmpOpTable[getIndexFromOp(CurrentOP)][CmpOpCount];
   }
 };
 //===----------------------------------------------------------------------===//
if (iter1->To() == MIN && (iter2->From() - 1) == MIN) {
     newRanges = F.remove(newRanges, *newRanges.begin());
     // add united range
     newRanges = F.add(newRanges, Range(MIN, to));
   }
 
   return newRanges;
 }
 
+RangeSet RangeSet::Delete(BasicValueFactory &BV, Factory &F,
+                          const llvm::APSInt &Point) const {
+  llvm::APSInt Upper = Point;
+  llvm::APSInt Lower = Point;
+
+  ++Upper;
+  --Lower;
+
+  // Notice that the lower bound is greater than the upper bound.
+  return Intersect(BV, F, Upper, Lower);
+}
+
 void RangeSet::print(raw_ostream &os) const {
   bool isFirst = true;
   os << "{ ";
   for (iterator i = begin(), e = end(); i != e; ++i) {
     if (isFirst)
       isFirst = false;
     else
       os << ", ";
 
     os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
        << ']';
   }
   os << " }";
 }
 
 namespace {
 
+//===----------------------------------------------------------------------===//
+//                            Intersection functions
+//===----------------------------------------------------------------------===//
+
+template <class SecondTy, class... RestTy>
+LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV,
+                                         RangeSet::Factory &F, RangeSet Head,
+                                         SecondTy Second, RestTy... Tail);
+
+template <class... RangeTy> struct IntersectionTraits;
+
+template <class... TailTy> struct IntersectionTraits<RangeSet, TailTy...> {
+  // Found RangeSet, no need to check any further
+  using Type = RangeSet;
+};
+
+template <> struct IntersectionTraits<> {
+  // We ran out of types, and we didn't find any RangeSet, so the result should
+  // be optional.
+  using Type = Optional<RangeSet>;
+};
+
+template <class OptionalOrPointer, class... TailTy>
+struct IntersectionTraits<OptionalOrPointer, TailTy...> {
+  // If current type is Optional or a raw pointer, we should keep looking.
+  using Type = typename IntersectionTraits<TailTy...>::Type;
+};
+
+template <class EndTy>
+LLVM_NODISCARD inline EndTy intersect(BasicValueFactory &BV,
+                                      RangeSet::Factory &F, EndTy End) {
+  // If the list contains only RangeSet or Optional<RangeSet>, simply return
+  // that range set.
+  return End;
+}
+
+LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED inline Optional<RangeSet>
+intersect(BasicValueFactory &BV, RangeSet::Factory &F, const RangeSet *End) {
+  // This is an extraneous conversion from a raw pointer into Optional<RangeSet>
+  if (End) {
+    return *End;
+  }
+  return llvm::None;
+}
+
+template <class... RestTy>
+LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV,
+                                         RangeSet::Factory &F, RangeSet Head,
+                                         RangeSet Second, RestTy... Tail) {
+  // Here we call either the <RangeSet,RangeSet,...> or <RangeSet,...> version
+  // of the function and can be sure that the result is RangeSet.
+  return intersect(BV, F, Head.Intersect(BV, F, Second), Tail...);
+}
+
+template <class SecondTy, class... RestTy>
+LLVM_NODISCARD inline RangeSet intersect(BasicValueFactory &BV,
+                                         RangeSet::Factory &F, RangeSet Head,
+                                         SecondTy Second, RestTy... Tail) {
+  if (Second) {
+    // Here we call the <RangeSet,RangeSet,...> version of the function...
+    return intersect(BV, F, Head, *Second, Tail...);
+  }
+  // ...and here it is either <RangeSet,RangeSet,...> or <RangeSet,...>, which
+  // means that the result is definitely RangeSet.
+  return intersect(BV, F, Head, Tail...);
+}
+
+/// Main generic intersect function.
+/// It intersects all of the given range sets.  If some of the given arguments
+/// don't hold a range set (nullptr or llvm::None), the function will skip them.
+///
+/// Available representations for the arguments are:
+///   * RangeSet
+///   * Optional<RangeSet>
+///   * RangeSet *
+/// Pointer to a RangeSet is automatically assumed to be nullable and will get
+/// checked as well as the optional version.  If this behaviour is undesired,
+/// please dereference the pointer in the call.
+///
+/// Return type depends on the arguments' types.  If we can be sure in compile
+/// time that there will be a range set as a result, the returning type is
+/// simply RangeSet, in other cases we have to back off to Optional<RangeSet>.
+///
+/// Please, prefer optional range sets to raw pointers.  If the last argument is
+/// a raw pointer and all previous arguments are None, it will cost one
+/// additional check to convert RangeSet * into Optional<RangeSet>.
+template <class HeadTy, class SecondTy, class... RestTy>
+LLVM_NODISCARD inline
+    typename IntersectionTraits<HeadTy, SecondTy, RestTy...>::Type
+    intersect(BasicValueFactory &BV, RangeSet::Factory &F, HeadTy Head,
+              SecondTy Second, RestTy... Tail) {
+  if (Head) {
+    return intersect(BV, F, *Head, Second, Tail...);
+  }
+  return intersect(BV, F, Second, Tail...);
+}
+
+//===----------------------------------------------------------------------===//
+//                           Symbolic reasoning logic
+//===----------------------------------------------------------------------===//
+
 /// A little component aggregating all of the reasoning we have about
 /// the ranges of symbolic expressions.
 ///
 /// Even when we don't know the exact values of the operands, we still
 /// can get a pretty good estimate of the result's range.
 class SymbolicRangeInferrer
     : public SymExprVisitor<SymbolicRangeInferrer, RangeSet> {
 public:
if (ActualType->isIntegralOrEnumerationType() ||
       return infer(Sym);
     }
     // Otherwise, let's simply infer from the destination type.
     // We couldn't figure out nothing else about that expression.
     return infer(DestType);
   }
 
   RangeSet infer(SymbolRef Sym) {
-    const RangeSet *AssociatedRange = State->get<ConstraintRange>(Sym);
-
-    // If Sym is a difference of symbols A - B, then maybe we have range set
-    // stored for B - A.
-    const RangeSet *RangeAssociatedWithNegatedSym =
-        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 (AssociatedRange && RangeAssociatedWithNegatedSym)
-      return AssociatedRange->Intersect(
-          ValueFactory, RangeFactory,
-          RangeAssociatedWithNegatedSym->Negate(ValueFactory, RangeFactory));
-
-    if (AssociatedRange)
-      return *AssociatedRange;
-
-    if (RangeAssociatedWithNegatedSym)
-      return RangeAssociatedWithNegatedSym->Negate(ValueFactory, RangeFactory);
+    if (Optional<RangeSet> ConstraintBasedRange = intersect(
+            ValueFactory, RangeFactory, State->get<ConstraintRange>(Sym),
+            // If Sym is a difference of symbols A - B, then maybe we have range
+            // set stored for B - A.
+            //
+            // 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.
+            getRangeForNegatedSub(Sym)))
+      return *ConstraintBasedRange;
 
     // If Sym is a comparison expression (except <=>),
     // find any other comparisons with the same operands.
     // See function description.
-    const RangeSet CmpRangeSet = getRangeForComparisonSymbol(State, Sym);
-    if (!CmpRangeSet.isEmpty())
-      return CmpRangeSet;
+    if (Optional<RangeSet> CmpRangeSet = getRangeForComparisonSymbol(Sym))
+      return *CmpRangeSet;
 
     return Visit(Sym);
   }
 
   /// Infer range information solely from the type.
   RangeSet infer(QualType T) {
     // Lazily generate a new RangeSet representing all possible values for the
     // given symbol type.
Range getSymmetricalRange(Range Origin, QualType T) {
 
     // Intersection is guaranteed to be non-empty.
     return {ValueFactory.getValue(-AbsMax), ValueFactory.getValue(AbsMax)};
   }
 
   /// Return a range set subtracting zero from \p Domain.
   RangeSet assumeNonZero(RangeSet Domain, QualType T) {
     APSIntType IntType = ValueFactory.getAPSIntType(T);
-    return Domain.Intersect(ValueFactory, RangeFactory,
-                            ++IntType.getZeroValue(), --IntType.getZeroValue());
+    return Domain.Delete(ValueFactory, RangeFactory, IntType.getZeroValue());
   }
 
   // FIXME: Once SValBuilder supports unary minus, we should use SValBuilder to
   //        obtain the negated symbolic expression instead of constructing the
   //        symbol manually. This will allow us to support finding ranges of not
   //        only negated SymSymExpr-type expressions, but also of other, simpler
   //        expressions which we currently do not know how to negate.
-  const RangeSet *getRangeForMinusSymbol(ProgramStateRef State, SymbolRef Sym) {
+  Optional<RangeSet> getRangeForNegatedSub(SymbolRef Sym) {
     if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
       if (SSE->getOpcode() == BO_Sub) {
         QualType T = Sym->getType();
+
+        // Do not negate unsigned ranges
+        if (!T->isUnsignedIntegerOrEnumerationType() &&
+            !T->isSignedIntegerOrEnumerationType())
+          return llvm::None;
+
         SymbolManager &SymMgr = State->getSymbolManager();
-        SymbolRef negSym =
+        SymbolRef NegatedSym =
             SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), T);
 
-        if (const RangeSet *negV = State->get<ConstraintRange>(negSym)) {
-          // Unsigned range set cannot be negated, unless it is [0, 0].
-          if (T->isUnsignedIntegerOrEnumerationType() ||
-              T->isSignedIntegerOrEnumerationType())
-            return negV;
+        if (const RangeSet *NegatedRange =
+                State->get<ConstraintRange>(NegatedSym)) {
+          return NegatedRange->Negate(ValueFactory, RangeFactory);
         }
       }
     }
-    return nullptr;
+    return llvm::None;
   }
 
   // Returns ranges only for binary comparison operators (except <=>)
   // when left and right operands are symbolic values.
   // Finds any other comparisons with the same operands.
   // Then do logical calculations and refuse impossible branches.
   // E.g. (x < y) and (x > y) at the same time are impossible.
   // E.g. (x >= y) and (x != y) at the same time makes (x > y) true only.
   // E.g. (x == y) and (y == x) are just reversed but the same.
   // It covers all possible combinations (see CmpOpTable description).
   // Note that `x` and `y` can also stand for subexpressions,
   // not only for actual symbols.
-  RangeSet getRangeForComparisonSymbol(ProgramStateRef State, SymbolRef Sym) {
-    const RangeSet EmptyRangeSet = RangeFactory.getEmptySet();
-
-    auto SSE = dyn_cast<SymSymExpr>(Sym);
+  Optional<RangeSet> getRangeForComparisonSymbol(SymbolRef Sym) {
+    const auto *SSE = dyn_cast<SymSymExpr>(Sym);
     if (!SSE)
-      return EmptyRangeSet;
+      return llvm::None;
 
     BinaryOperatorKind CurrentOP = SSE->getOpcode();
 
     // We currently do not support <=> (C++20).
     if (!BinaryOperator::isComparisonOp(CurrentOP) || (CurrentOP == BO_Cmp))
-      return EmptyRangeSet;
+      return llvm::None;
 
     static const OperatorRelationsTable CmpOpTable{};
 
     const SymExpr *LHS = SSE->getLHS();
     const SymExpr *RHS = SSE->getRHS();
     QualType T = SSE->getType();
 
     SymbolManager &SymMgr = State->getSymbolManager();
-    const llvm::APSInt &Zero = ValueFactory.getValue(0, T);
-    const llvm::APSInt &One = ValueFactory.getValue(1, T);
-    const RangeSet TrueRangeSet(RangeFactory, One, One);
-    const RangeSet FalseRangeSet(RangeFactory, Zero, Zero);
 
     int UnknownStates = 0;
 
     // Loop goes through all of the columns exept the last one ('UnknownX2').
     // We treat `UnknownX2` column separately at the end of the loop body.
     for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
 
       // Let's find an expression e.g. (x < y).
for (size_t i = 0; i < CmpOpTable.getCmpOpCount(); ++i) {
           //   if (x != y)  // assume true
           //     if (x < y) // would be also true
           // Get a state from `UnknownX2` column.
           BranchState = CmpOpTable.getCmpOpStateForUnknownX2(CurrentOP);
         else
           continue;
       }
 
-      return (BranchState == OperatorRelationsTable::True) ? TrueRangeSet
-                                                           : FalseRangeSet;
-    }
+      return (BranchState == OperatorRelationsTable::True) ? getTrueRange(T)
+                                                           : getFalseRange(T);
+    }
+
+    return llvm::None;
+  }
+
+  RangeSet getTrueRange(QualType T) {
+    RangeSet TypeRange = infer(T);
+    return assumeNonZero(TypeRange, T);
 
-    return EmptyRangeSet;
+  RangeSet getFalseRange(QualType T) {
+    const llvm::APSInt &Zero = ValueFactory.getValue(0, T);
+    return RangeSet(RangeFactory, Zero);
   }
 
   BasicValueFactory &ValueFactory;
   RangeSet::Factory &RangeFactory;
   ProgramStateRef State;
 };
 
+//===----------------------------------------------------------------------===//
+//               Range-based reasoning about symbolic operations
+//===----------------------------------------------------------------------===//
+
 template <>
 RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Or>(Range LHS, Range RHS,
                                                            QualType T) {
   APSIntType ResultType = ValueFactory.getAPSIntType(T);
   llvm::APSInt Zero = ResultType.getZeroValue();
 
   bool IsLHSPositiveOrZero = LHS.From() >= Zero;
   bool IsRHSPositiveOrZero = RHS.From() >= Zero;
if (IsLHSPositiveOrZero && IsRHSPositiveOrZero) {
     Min = LHS.To() < RHS.From() ? LHS.From() : Zero;
   }
 
   // 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 manager implementation details
+//===----------------------------------------------------------------------===//
+
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
       : RangedConstraintManager(EE, SVB) {}
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//

 } // end anonymous namespace
 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr,
                                    ExprEngine *Eng) {
   return std::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
+//===----------------------------------------------------------------------===//
+//                    RangeConstraintManager implementation
+//===----------------------------------------------------------------------===//
+
 bool RangeConstraintManager::canReasonAbout(SVal X) const {
   Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
   if (SymVal && SymVal->isExpression()) {
     const SymExpr *SE = SymVal->getSymbol();
 
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
       switch (SIE->getOpcode()) {
       // We don't reason yet about bitwise-constraints on symbolic values.

 }
 
 const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
                                                       SymbolRef Sym) const {
   const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
   return T ? T->getConcreteValue() : nullptr;
 }
 
+//===----------------------------------------------------------------------===//
+//                Remove dead symbols from existing constraints
+//===----------------------------------------------------------------------===//
+
 /// Scan all symbols referenced by the constraints. If the symbol is not alive
 /// as marked in LSymbols, mark it as dead in DSymbols.
 ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef State,
                                            SymbolReaper &SymReaper) {
   bool Changed = false;
   ConstraintRangeTy CR = State->get<ConstraintRange>();
   ConstraintRangeTy::Factory &CRFactory = State->get_context<ConstraintRange>();

 RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
                                     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);
   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
     return St;
 
-  llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
-  llvm::APSInt Upper = Lower;
-  --Lower;
-  ++Upper;
+  llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
 
-  // [Int-Adjustment+1, Int-Adjustment-1]
-  // Notice that the lower bound is greater than the upper bound.
-  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
+  RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef
 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.