[analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[baloghadamsoftware]

Summary

This patch extends the constraint manager to be able to reason about trivial sym-sym comparisons.

We all know that a < b if the maximum value of a is still less than the minimum value of b.
This reasoning can be applied for the <,<=,>,>= relation operators.
This patch solely implements this functionality.

This patch does not address transitity like:
If a < b and b < c than a < c.

This patch is necessary to be able to express hidden function preconditions.
For example, with the D69726 we could express the connection between the
extent size of src and the size (n) parameter of the function.

#define ANALYZER_ASSERT assert

void my_memcpy(char *dst, char *src, int n) {
  ANALYZER_ASSERT(clang_analyzer_getExtent(src) >= n)
  ANALYZER_ASSERT(clang_analyzer_getExtent(dst) >= n)
  
  for (int i = 0; i < n; ++i) {
    // The extent of dst would be compared to the index i.
    dst[i] = src[i]; // each memory access in-bound, no-warning
  }
}

[Szelethus]

You seem to have forgotten -U9999 :^)

[martong]

I like it, nice work!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

774

Is it possible to ever return with None? Other assume functions usually just return with nullptr on infeasible state as you do. What would be the meaning if None is returned, is that another kind of infeasibility?

797

Perhaps this hunk could be greatly simplified if CompareResult was actually BinaryOperator::Opcode.

Maybe (?):

if (Res == Op)
  return State;
return InfeasibleState;

clang/test/Analysis/constraint-manager-sym-sym.c

71

How is it different than // [0,5] and [5,10]?

173

I think we could benefit from tests for cases like this:

{[0,1],[5,6]} < {[9,9],[11,42],[44,44]}

[steakhal]

• add full diff context
• NFC refactored RangeSet comparison function
• add tests for compund RangeSets like: {[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
• NFC clang-format test file

[steakhal]

In D77792#1971921, @Szelethus wrote:

You seem to have forgotten -U9999 :^)

Nice catch!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

774

The rest of the functions there is no maybe answer. There is always yes or no, returning the State or the nullptr.
In our case, we don't know in advance that we know a definitive answer.

Imagine the following:
When the analyzer sees the a < b comparison.
It queries whether it canReasonAbout(). In our case that would return true due to my change.
When tries to reason about the given SymSymExpr (a < b), we don't know if the corresponding value ranges of a and b are disjunct or not, we need to check that.
If we can prove that the ranges are disjunct (or just connected: a: [a1,x] and b: [x,b2]) then we know an answer. That can be true (State) or false (nullptr). Otherwise the result should be UNKNOWN (llvm::None).

797

Honestly, I had exactly the same thoughts.

I think an Opcode is a different thing than a result of a comparison.
Here, we have a partial ordering among RangeSets.
But you can convince me :)

But I agree, it looks clunky, looking forward to a better solution. Any idea?

clang/test/Analysis/constraint-manager-sym-sym.c

71

It covers the same. I just wanted a full and clear showcase of the possible intervals.
I can be convinced to remove this testcase.

173

Really good idea.

I added tests for these. But I'm not really sure what's going on there :D
I'm sure that these test cases are not testing what I meant to test.
(The exploded graphs are showing that each subrange is assumed for a given value (l and r) on a given path)

Any idea of how to express the proper value ranges?

[steakhal]

• rewritten the RangeSet::compare function and checked the assumptions on WolframAlpha
• moved the RangeSet::compare function to a cpp file
• added comments to the RangeSet::compare function
• fixed the comment in RangeConstraintManager::canReasonAbout function
• introduced the RangeSet::CompareResult::identical enum value to be complete
• updated the RangeConstraintManager::tryAssumeSymSymOp accoding the identical CompareResult.
• omited testing the [2,5] < [5,10] testcase, since that is covered by [0,5] < [5,10]

[ASDenysPetrov]

@steakhal
What about unsigneds? Does it work for unsigned values as well?

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2293

I believe you don't need to return an optional here. The method simply acknowledges any assumptions it could make in the existing state and returns the updated state. Therefore, if it wasn't able to record any assumptions, it returns the existing state. Because the only reasonable behavior the caller could implement when the current implementation returns None is to roll back to the existing state anyway.

clang/test/Analysis/constraint-manager-sym-sym.c

183

You can also explicitly create a single path with disconnected ranges (as opposed to like 3 different paths on each of which the range is a single segment) like this:

assert(r >= 9 && r <= 44 && r != 10 && r != 43);

[ASDenysPetrov]

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

110–117

Can we use Optional<BinaryOperatorKind> instead, to reduce similar enums? Or you want to separate the meaning in a such way?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

31–34

As you use here getMaxValue twice which is not O(1), it'd better to use a buffer variable.

199–206

Can we improve llvm::ImmutableSet this to make getMaxValue complexity O(1)?

clang/test/Analysis/constraint-manager-sym-sym.c

182

Could you add some tests for unsigned, unsigned and signed, unsigned?

[steakhal]

I no longer think that we should support Symbol to Symbol comparisons.
It would introduce certain anomalies, like Why could the CM reason about this and that comparisons wile could not in others.

As of now, it's clear that we can not compare Symbols to Symbols - preventing such confusing questions to arise in the future.
If we were to implement Symbol to Symbol comparisons, we should cover a lot more cases than this patch could.

So I decided to abandon this patch.

[baloghadamsoftware]

We found use cases which can be solved using this improvement. That is why I commandeer this patch now.

[baloghadamsoftware]

Crash fixed and new tests added.

[baloghadamsoftware]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2293

Actually, tryAssumeSymSymOp() does not assume anything and therefore it does not return a new state. What it actually returns is a ternary logical value: the assumption is either valid, invalid or we cannot reason about it. Maybe Optional<bool> would be better here and we should also chose a less misleading name, because it does not "try to assume" anything, but tries to reason about the existing assumption.

[baloghadamsoftware]

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

110–117

Good question. @NoQ?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

31–34

getMaxValue() for the current and other.getMaxValue() are different.

199–206

llvm::ImmutableSet seems to me a heap-like structure, a tree optimized for minimum-search: the mininum is in the root of the tree. Maximum is linear.

clang/test/Analysis/constraint-manager-sym-sym.c

182

I will do it.

[baloghadamsoftware]

Tests updated: some execution paths merged by refactoring assertions.

[martong]

Adding Valeriy as a reviewer. He's been working with the solver recently, so his insights might be really useful here.

[vsavchenko]

Hi @baloghadamsoftware

Great job! I also wanted to support more operations for range-based logic.

However, I don't think that this is the right place to make this kind of assumptions. A couple months ago, I added the SymbolicRangeInferrer component to aggregate all of the reasoning we have about range constraints and I strongly believe that the logic from this patch should be integrated in that component.

[NoQ]

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

110–117

The meaning is obviously completely different even when the names actually match. BO_LT is not a "result", it's the operation itself. It gets even worse for other opcodes (what kind of comparison result is BO_PtrMemI???).

The idea to re-use the enum is noble but we definitely need to find some other enum.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2293

I dislike this design because it turns the code into a spaghetti in which every facility in the constraint manager has to be aware of any other facility in the constraint manager and agree on who's responsible for what. It's too easy to miss something and missing something isn't as bad as doing double work.

Like, should different facilities in the constraint manager try to record as *much* information in the program state ("fat constraints") as possible or as *little* as possible ("thin constraints")? Eg., in this example, if we know that the range for $x is strictly below the range for $y, should we also add the opaque constraint $x < $y to the program state, or should we instead teach every facility to infer that $x < $y by looking at their ranges?

I feel we should go with fat constraints.

1. Con: They're fat. They eat more memory, cause more immutable tree rebalances, etc.
2. Con: It's easy to accidentally make two similar states look different. Eg., { $x: [1, 2], $y: [3, 4] } and { $x : [1, 2], $y: [3, 4], $x < $y: true } are the same state but they won't be deduplicated and if they appear on different paths at the same program point these paths won't get merged.
3. Pro: They minimize the amount of false positives by giving every facility in the constraint manager as much data as possible to conclude that the state is infeasible.
4. Pro: As i said above, they're easier to implement and to get right. In case of thin constraints, every facility has to actively let other facilites know that they don't need to handle the assumption anymore because this facility has "consumed" it. In our example it means returning an Optional<ProgramStateRef> which would be empty if the constraint wasn't consumed and needs to be handled by another facility (namely, assumeSymUnsupported). In case of fat constraints you simply add your information and you don't care if other facilities ever read it or not.

Con 1. should be dismissed as a premature optimization: we can always add some thinness to fat constraints if we have a proof that their fatness is an actual problem. Con 2. is a real issue but it's a fairly minor issue; path merges are fairly rare anyway; mergeability is a nice goal to pursue but not at the cost of having false positives. So i think pros outweight the cons here.

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

public:
 
   /// getConcreteValue - If a symbol is contrained to equal a specific integer
   ///  constant then this method returns that value.  Otherwise, it returns
   ///  NULL.
   const llvm::APSInt *getConcreteValue() const {
     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
   }
 
+  enum class CompareResult {
+    unknown,
+    identical,
+    less,
+    less_equal,
+    greater,
+    greater_equal
+  };
+
+  // 'a < b' is true if the maximum value of 'a' is still (strictly) less than
+  // the minimum value of 'b'. The same logic applies for <=,>,>=,== operators.
+  // If there is no clear relation between the two RangeSet returns unknown.
+  CompareResult compare(const RangeSet &other) const;
+
   /// Get a minimal value covered by the ranges in the set
   const llvm::APSInt &getMinValue() const;
   /// Get a maximal value covered by the ranges in the set
   const llvm::APSInt &getMaxValue() const;
 
 private:
   void IntersectInRange(BasicValueFactory &BV, Factory &F,
                         const llvm::APSInt &Lower, const llvm::APSInt &Upper,
protected:
   virtual ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
   virtual ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
+  virtual Optional<ProgramStateRef>
+  tryAssumeSymSymOp(ProgramStateRef State, BinaryOperator::Opcode Op,
+                    SymbolRef LHSSym, SymbolRef RHSSym, bool Assumption) = 0;
+
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 private:
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
 } // namespace ento
 } // namespace clang
 
 REGISTER_FACTORY_WITH_PROGRAMSTATE(ConstraintMap)
 
 #endif

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/Support/raw_ostream.h"
 
 using namespace clang;
 using namespace ento;
 
+RangeSet::CompareResult RangeSet::compare(const RangeSet &other) const {
+  if (isEmpty() || other.isEmpty())
+    return CompareResult::unknown;
+
+  const int LMaxRMin =
+      llvm::APSInt::compareValues(getMaxValue(), other.getMinValue());
+  const int LMinRMax =
+      llvm::APSInt::compareValues(getMinValue(), other.getMaxValue());
+
+  // {-1,0,1}x{-1,0,1} has 9 combinations, so we will enumerate all of them.
+  // Given [a0,a1] and [b0,b1] ranges.
+  // Assuming that a0 <= a1 and b0 <= b1 (since ranges...)
+  // Than we examine the 'a1 <? b0' and the 'a0 <? b1' comparisons.
+  // Eg. if a1 <? b0 is -1, that means that a1 < b0; zero for equality; etc.
+  // Solving these 9 inequality systems we draw some conclusion and find some
+  // impossible cases (which are not satisfiable with any valid ranges).
+  if (LMaxRMin == -1 && LMinRMax == -1)
+    return CompareResult::less;
+  if (LMaxRMin == -1 && LMinRMax == 0)
+    llvm_unreachable("Impossible.");
+  if (LMaxRMin == -1 && LMinRMax == 1)
+    llvm_unreachable("Impossible.");
+
+  if (LMaxRMin == 0 && LMinRMax == -1)
+    return CompareResult::less_equal;
+  if (LMaxRMin == 0 && LMinRMax == 0)
+    return CompareResult::identical;
+  if (LMaxRMin == 0 && LMinRMax == 1)
+    llvm_unreachable("Impossible.");
+
+  if (LMaxRMin == 1 && LMinRMax == -1)
+    return CompareResult::unknown;
+  if (LMaxRMin == 1 && LMinRMax == 0)
+    return CompareResult::greater_equal;
+  assert(LMaxRMin == 1 && LMinRMax == 1);
+  return CompareResult::greater;
+}
+
+
 // This class can be extended with other tables which will help to reason
 // about ranges more precisely.
 class OperatorRelationsTable {
   static_assert(BO_LT < BO_GT && BO_GT < BO_LE && BO_LE < BO_GE &&
                     BO_GE < BO_EQ && BO_EQ < BO_NE,
                 "This class relies on operators order. Rework it otherwise.");
 
 public:
const llvm::APSInt &RangeSet::getMaxValue() const {
   //       llvm::ImmutableSet should support decrement for 'end' iterators
   //       or reverse order iteration.
   auto It = begin();
   for (auto End = end(); std::next(It) != End; ++It) {
   }
   return It->To();
 }
 
 bool RangeSet::pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
   if (isEmpty()) {
     // This range is already infeasible.
     return false;
   }
 
   // This function has nine cases, the cartesian product of range-testing
   // both the upper and lower bounds against the symbol's type.
   // Each case requires a different pinning operation.
   // The function returns false if the described range is entirely outside
   // the range of values for the associated symbol.
   APSIntType Type(getMinValue());
   APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true);
   APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
 
   switch (LowerTest) {
public:
   RangeSet VisitSymIntExpr(const SymIntExpr *Sym) {
     return VisitBinaryOperator(Sym);
   }
 
   RangeSet VisitIntSymExpr(const IntSymExpr *Sym) {
     return VisitBinaryOperator(Sym);
   }
 
   RangeSet VisitSymSymExpr(const SymSymExpr *Sym) {
     return VisitBinaryOperator(Sym);
   }
 
 private:
   SymbolicRangeInferrer(BasicValueFactory &BV, RangeSet::Factory &F,
                         ProgramStateRef S)
       : ValueFactory(BV), RangeFactory(F), State(S) {}
 
   /// Infer range information from the given integer constant.
   ///
   /// It's not a real "inference", but is here for operating with
   /// sub-expressions in a more polymorphic manner.
   RangeSet inferAs(const llvm::APSInt &Val, QualType) {
     return {RangeFactory, Val};
   }
 
   /// Infer range information from symbol in the context of the given type.
   RangeSet inferAs(SymbolRef Sym, QualType DestType) {
     QualType ActualType = Sym->getType();
     // Check that we can reason about the symbol at all.
     if (ActualType->isIntegralOrEnumerationType() ||
         Loc::isLocType(ActualType)) {
       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) {
     if (Optional<RangeSet> ConstraintBasedRange = intersect(
public:
   ProgramStateRef assumeSymWithinInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
   ProgramStateRef assumeSymOutsideInclusiveRange(
       ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
+  Optional<ProgramStateRef> tryAssumeSymSymOp(ProgramStateRef State,
+                                              BinaryOperator::Opcode Op,
+                                              SymbolRef LHSSym,
+                                              SymbolRef RHSSym,
+                                              bool Assumption) override;
+
 private:
   RangeSet::Factory F;
 
   RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
   RangeSet getRange(ProgramStateRef State, EquivalenceClass Class);
 
   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
         return true;
       }
     }
 
     if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
       // FIXME: Handle <=> here.
       if (BinaryOperator::isEqualityOp(SSE->getOpcode()) ||
           BinaryOperator::isRelationalOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        // We've recently started producing Loc <> NonLoc comparisons (that
-        // result from casts of one of the operands between eg. intptr_t and
-        // void *), but we can't reason about them yet.
+        // We handle Loc <> Loc comparisons.
         if (Loc::isLocType(SSE->getLHS()->getType())) {
           return Loc::isLocType(SSE->getRHS()->getType());
         }
+
+        // We can handle certain NonLoc <> NonLoc comparisons, when the
+        // corresponding RangeSets are non-overlapping.
+        // We've recently started producing Loc <> NonLoc comparisons (that
+        // result from casts of one of the operands between eg. intptr_t and
+        // void *), but we can't reason about them yet.
+        return true;
       }
     }
 
     return false;
   }
 
   return true;
 }
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(RangeLT.addRange(F, RangeGT));
   return New.isEmpty() ? nullptr : setConstraint(State, Sym, New);
 }
 
+Optional<ProgramStateRef> RangeConstraintManager::tryAssumeSymSymOp(
+    ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,
+    SymbolRef RHSSym, bool Assumption) {
+  // FIXME: In C++20? replace with 'using RangeSet::CompareResult;'
+  using CR = RangeSet::CompareResult;
+  constexpr auto unknown = CR::unknown;
+  constexpr auto identical = CR::identical;
+  constexpr auto less = CR::less;
+  constexpr auto greater = CR::greater;
+  constexpr auto less_equal = CR::less_equal;
+  constexpr auto greater_equal = CR::greater_equal;
+
+  const auto InfeasibleState = Optional<ProgramStateRef>{nullptr};
+
+  const RangeSet LHSRange = getRange(State, LHSSym);
+  const RangeSet RHSRange = getRange(State, RHSSym);
+  const RangeSet::CompareResult Res = LHSRange.compare(RHSRange);
+
+  if (Res == unknown)
+    return llvm::None;
+
+  if (!Assumption)
+    Op = BinaryOperator::negateComparisonOp(Op);
+
+  switch (Op) {
+  case BO_LT:
+    if (Res == less)
+      return State;
+    if (Res == identical || Res == greater_equal || Res == greater)
+      return InfeasibleState;
+    assert(Res == less_equal);
+    return llvm::None;
+  case BO_GT:
+    if (Res == greater)
+      return State;
+    if (Res == identical || Res == less_equal || Res == less)
+      return InfeasibleState;
+    assert(Res == greater_equal);
+    return llvm::None;
+  case BO_LE:
+    if (Res == identical || Res == less_equal || Res == less)
+      return State;
+    if (Res == greater)
+      return InfeasibleState;
+    assert(Res == greater_equal);
+    return llvm::None;
+  case BO_GE:
+    if (Res == identical || Res == greater_equal || Res == greater)
+      return State;
+    if (Res == less)
+      return InfeasibleState;
+    assert(Res == less_equal);
+    return llvm::None;
+  default:
+    llvm_unreachable("Should not reach this with any other operators.");
+  }
+}
+
 //===----------------------------------------------------------------------===//
 // Pretty-printing.
 //===----------------------------------------------------------------------===//
 
 void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State,
                                        const char *NL, unsigned int Space,
                                        bool IsDot) const {
   ConstraintRangeTy Constraints = State->get<ConstraintRange>();

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
 
       return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
     }
 
   } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
     BinaryOperator::Opcode Op = SSE->getOpcode();
     assert(BinaryOperator::isComparisonOp(Op));
 
-    // We convert equality operations for pointers only.
+    // We support comparing pointers and... (TODO!!!)
     if (Loc::isLocType(SSE->getLHS()->getType()) &&
         Loc::isLocType(SSE->getRHS()->getType())) {
       // Translate "a != b" to "(b - a) != 0".
       // We invert the order of the operands as a heuristic for how loop
       // conditions are usually written ("begin != end") as compared to length
       // calculations ("end - begin"). The more correct thing to do would be to
       // canonicalize "a - b" and "b - a", which would allow us to treat
       // "a != b" and "b != a" the same.
if (BinaryOperator::isEqualityOp(Op)) {
       const llvm::APSInt &Zero = getBasicVals().getValue(0, ExprType);
 
       if (IsExpectedEqual) {
         return assumeSymNE(State, CanonicalEquality, Zero, Zero);
       }
 
       return assumeSymEQ(State, CanonicalEquality, Zero, Zero);
     }
+
+    // We also support constrained symbols, which don't have any overlapping
+    // range intervals. Eg. {[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
+    if (SSE->getLHS()->getType()->isIntegralOrEnumerationType() &&
+        SSE->getRHS()->getType()->isIntegralOrEnumerationType()) {
+      if (auto OptionalState = tryAssumeSymSymOp(State, Op, SSE->getLHS(),
+                                                 SSE->getRHS(), Assumption))
+        return OptionalState.getValue();
+    }
   }
 
   // If we get here, there's nothing else we can do but treat the symbol as
   // opaque.
   return assumeSymUnsupported(State, Sym, Assumption);
 }
 
 ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(

clang/test/Analysis/constraint-manager-sym-sym.c

+// RUN: %clang_analyze_cc1 -verify -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false %s
+
+void clang_analyzer_eval(int);
+
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+                          unsigned int __line, __const char *__function)
+    __attribute__((__noreturn__));
+#define assert(expr) \
+  ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+// Given [a1,a2] and [b1,b2] intervals.
+// Pin the [b1,b2] interval to eg. [5,10]
+// Choose the a1,a2 points from 0,2,5,7,10,12 where a1 < a2.
+// There will be 5+4+3+2+1 cases.
+
+// [0,2] and [5,10]
+void test_range1(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 2);
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// [0,5] and [5,10]
+void test_range2(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 5);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,7] and [5,10]
+void test_range3(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,10] and [5,10]
+void test_range4(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [0,12] and [5,10]
+void test_range5(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(0 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,5] and [5,10] omitted because it is the same as the '[0,5] and [5,10]'
+
+// [2,7] and [5,10]
+void test_range7(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,10] and [5,10]
+void test_range8(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [2,12] and [5,10]
+void test_range9(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(2 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,7] and [5,10]
+void test_range10(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 7);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,10] and [5,10]
+void test_range11(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [5,12] and [5,10]
+void test_range12(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(5 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [7,10] and [5,10]
+void test_range13(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(7 <= l && l <= 10);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [7,12] and [5,10]
+void test_range14(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(7 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// [10,12] and [5,10]
+void test_range15(int l, int r) {
+  assert(5 <= r && r <= 10);
+  assert(7 <= l && l <= 12);
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}}
+}
+
+// {[0,1],[5,6]} and {[9,9],[11,42],[44,44]}
+void test_range16(int l, int r) {
+  assert(r >= 9 && r <= 44 && r != 10 && r != 43);
+  assert((0 <= l && l <= 1) || (5 <= l && l <= 6));
+  clang_analyzer_eval(l < r);  // expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{FALSE}}
+}
+
+// {[0,1],[5,10]} and {[9,9],[11,42],[44,44]}
+void test_range17(int l, int r) {
+  assert(r >= 9 && r <= 44 && r != 10 && r != 43);
+  assert((0 <= l && l <= 1) || (5 <= l && l <= 10));
+
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+}
+
+// {[0,1],[20,20]} and {[9,9],[11,42],[44,44]}
+void test_range18(int l, int r) {
+  assert(r >= 9 && r <= 44 && r != 10 && r != 43);
+  assert((0 <= l && l <= 1) || l == 20);
+
+  clang_analyzer_eval(l < r);  // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+  clang_analyzer_eval(l <= r); // expected-warning{{UNKNOWN}} expected-warning{{TRUE}}
+  clang_analyzer_eval(l > r);  // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+  clang_analyzer_eval(l >= r); // expected-warning{{UNKNOWN}} expected-warning{{FALSE}}
+}
+
+
+#define INT_MIN (- (int)(((unsigned) 0 - 1) / 2) - 1)
+
+void test_difference1(int k, int l, int m, int n) {
+  assert(k - l > INT_MIN && k - l <= 10);
+  assert(l - k <= 0);
+  // This means that k - l is from [0..10], l - k is from [-10..0]
+  assert(m - n >= -20);
+  assert(n - m > 10);
+  // This means that m - n is from [-20..-11], n - m is from [11..20]
+  clang_analyzer_eval(k - l < n - m); // expected-warning{{TRUE}}
+  clang_analyzer_eval(l - k < n - m); // expected-warning{{TRUE}}
+  clang_analyzer_eval(k - l < m - n); // expected-warning{{FALSE}}
+  clang_analyzer_eval(l - k < m - n); // expected-warning{{FALSE}}
+}