[analyzer][solver] Introduce reasoning for not equal to operator

[manas]

Summary

Prior to this, the solver was only able to verify whether two symbols
are equal/unequal, only when constants were involved. This patch allows
the solver to work over ranges as well.

[vsavchenko]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1223–1225

I think it should be a specialization for another VisitBinaryOperator.
In the switch, you can see that we give range sets for LHS and RHS, so how does it work?
There is a function in between (also VisitBinaryOperator) that creates simple ranges out of range sets and ask to visit binary operator for those. You can specialize it instead since we can simply check for empty intersection of range sets.

1241

Empty range set means "This situation is IMPOSSIBLE". Is that what you want here?

clang/test/Analysis/constant-folding.c

286–320

Did you try it in debugger, do we get inside of your function?

[manas]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1223–1225

I went through the code and understood that part. I agree that this should be a specialized case for VisitBinaryOperator. So I understand it in this way:

1. Creating a new VisitBinaryOperator(Range,Range,QualType) which can check for empty intersections.
2. It will then call to appropriate functions (like VisittBinaryOperator<BO_NE> and others.)

1241

True! That's incorrect. We cannot find a good rangeset. Should I rather return the entire RangeSet inferred from T?

clang/test/Analysis/constant-folding.c

286–320

Yes, the function is being reached.

[martong]

This is promising! Gentle ping @manas @vsavchenko

[manas]

I haven't tried specializing that VisitBinaryOperator method which converts Ranges from RangeSets (as @vsavchenko mentioned). Should this case for NE stay here in the switch or move?

[manas]

Rebase

[martong]

In D106102#3019921, @manas wrote:

I haven't tried specializing that VisitBinaryOperator method which converts Ranges from RangeSets (as @vsavchenko mentioned). Should this case for NE stay here in the switch or move?

Please try what @vsavchenko mentioned, seems like with RangeSet::getMinValue and getMaxValue we can achieve the same before coersing to simple Ranges.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

1223–1225

No. You need the following specialization for RangeSet:

template <>
RangeSet VisitBinaryOperator<BO_NE>(RangeSet LHS, RangeSet RHS, QualType T) {
  // your original code here...
  return infer(T);
}

Besides, I think you should use getMaxValue() and getMinValue() instead of To() and From().

1241

True! That's incorrect. We cannot find a good rangeset. Should I rather return the entire RangeSet inferred from T?

Yes, that would work! Because the entire RangeSet implies both the logical True (non-zero values) and the logica False values.

[martong]

Adding @steakhal as reviewer because of other reviewers inactivity.

[manas]

Move method to a specialized template for VisitBinaryOperator

[manas]

Rebase

[manas]

The pre-merge checks fail due to the patch being unable to get applied. The troubleshooting suggest to update the patch via arc diff `git merge-base HEAD origin` --update D106102 and it would include all local changes into that patch. Shouldn't I avoid including all local changes, as some local changes are still WIP?

[martong]

LGTM! Thanks!

[martong]

In D106102#3028584, @manas wrote:

The pre-merge checks fail due to the patch being unable to get applied. The troubleshooting suggest to update the patch via arc diff `git merge-base HEAD origin` --update D106102 and it would include all local changes into that patch. Shouldn't I avoid including all local changes, as some local changes are still WIP?

I guess HEAD should refer to the commit that represents this patch, in this case that is ce82443c69be. And I believe you local changes that are not committed should not affect arc diff at all. But, as a precaution, you could first stash your local changes before calling arc. Hope this helps.

[steakhal]

This patch seems pretty straightforward, good job @manas, and for the folks giving review comments.
Aside from polishing the tests, I think it's good to go.

clang/test/Analysis/constant-folding.c

285

285

I would prefer u1, u2, s1, s2 respectively.
This way the name would signify the signess of the variable.

288

Isn't a != b enough? Why do you need the (..) != 0 part?

291–293

How is this different compared to the previous case? The difference I can see is that now we use different constants and the == operator in the outer expression. None of which should really change the behavior AFAICT.

296

You could have a comment that a: [20,50] b:[20,50].
It would be easier to comprehend than the chain of conjunctions.
Similarly, how at L464 does.

[manas]

In D106102#3029633, @martong wrote:

In D106102#3028584, @manas wrote:

The pre-merge checks fail due to the patch being unable to get applied. The troubleshooting suggest to update the patch via arc diff `git merge-base HEAD origin` --update D106102 and it would include all local changes into that patch. Shouldn't I avoid including all local changes, as some local changes are still WIP?

I guess HEAD should refer to the commit that represents this patch, in this case that is ce82443c69be. And I believe you local changes that are not committed should not affect arc diff at all. But, as a precaution, you could first stash your local changes before calling arc. Hope this helps.

Thanks. That was helpful.

clang/test/Analysis/constant-folding.c

285

Makes sense. I have amended it.

288

Sometime ago, Valeriy and I were discussing about how solver can't reason about sub-expressions containing logical operators with ranges. Currently, only ==/!= operators can reason about them, as they are trivial. So, this case is for != operator used with sub-expressions.

291–293

I wanted to put a signed case. Although I believe, I should have replaced == with !=.

296

Sure. I have amended.

[manas]

Apply mentioned edits in testcases

[steakhal]

Okay, I don't see any problems besides this typo.

BTW do you plan to implement other rules besides this in the future?
E.g. we currently miss this:
'x < y' is true if max(x) < min(y); and false if min(x) >= max(y)
'x > y', 'x <= y', etc. in a similar way.

clang/test/Analysis/constant-folding.c

293

[manas]

In D106102#3032888, @steakhal wrote:

Okay, I don't see any problems besides this typo.

Oops!

BTW do you plan to implement other rules besides this in the future?
E.g. we currently miss this:
'x < y' is true if max(x) < min(y); and false if min(x) >= max(y)
'x > y', 'x <= y', etc. in a similar way.

I think these cases need to be specialized as well. As, they aren't returning some complex RangeSet, so we can get away with a specialized template for BO_LT/BO_GT etc., instead of a class method (like BO_Rem has). I can work on this.

[manas]

Fix typo

[steakhal]

Good work. Land it.

[manas]

In D106102#3035598, @steakhal wrote:

Good work. Land it.

I do not have landing rights.

[steakhal]

In D106102#3036220, @manas wrote:

I do not have landing rights.

Please add your name and email on whom behalf I should commit this patch. Mine is Balazs Benics<[e-mail]>

[steakhal]

🛬

[manas]

In D106102#3036474, @steakhal wrote:

In D106102#3036220, @manas wrote:

I do not have landing rights.

Please add your name and email on whom behalf I should commit this patch. Mine is Balazs Benics<[e-mail]>

It is Manas <[e-mail]>

Thanks!

[steakhal]

It seems like it doesn't build with GCC 8.3.0 on a Debian system.
Could you investigate?

llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1029:13: error: explicit specialization in non-namespace scope 'class {anonymous}::SymbolicRangeInferrer'
   template <>
             ^
llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1030:77: error: template-id 'VisitBinaryOperator<BO_NE>' in declaration of primary template
   RangeSet VisitBinaryOperator<BO_NE>(RangeSet LHS, RangeSet RHS, QualType T) {
                                                                             ^

I think the issue is this: https://stackoverflow.com/questions/3052579/explicit-specialization-in-non-namespace-scope

[manas]

I'll take a look at this over the weekend.

[martong]

I've fixed the compilation error and pushed.

[manas]

I have received a failed build on clang-ppc64be-linux (https://lab.llvm.org/buildbot/#/builders/52/builds/11704). Although, I haven't verified the commit. Is there something wrong with this commit? Is the function VisitBinaryOperator<BO_NE> reachable?

[martong]

In D106102#3080339, @manas wrote:

I have received a failed build on clang-ppc64be-linux (https://lab.llvm.org/buildbot/#/builders/52/builds/11704). Although, I haven't verified the commit. Is there something wrong with this commit? Is the function VisitBinaryOperator<BO_NE> reachable?

No worries, that seems to be a test suite python error that is unrelated:

Traceback (most recent call last):
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/llvm/llvm/utils/lit/lit.py", line 6, in <module>
    main()
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/llvm/llvm/utils/lit/lit/main.py", line 44, in main
    opts.indirectlyRunCheck)
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/llvm/llvm/utils/lit/lit/discovery.py", line 279, in find_tests_for_inputs
    local_config_cache, indirectlyRunCheck)[1])
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/llvm/llvm/utils/lit/lit/discovery.py", line 130, in getTests
    ts,path_in_suite = getTestSuite(path, litConfig, testSuiteCache)
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/llvm/llvm/utils/lit/lit/discovery.py", line 91, in getTestSuite
    ts, relative = search(item)
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/llvm/llvm/utils/lit/lit/discovery.py", line 75, in search
    cache[real_path] = res = search1(path)
  File "/home/buildbots/ppc64be-clang-test/clang-ppc64be/l

[bjope]

I get failures after having merged this patch:

/llvm/build-all/bin/clang -Xanalyzer -analyzer-output=text -Xanalyzer -analyzer-checker='nullability,optin.portability.UnixAPI,security,valist' -Xanalyzer -analyzer-disable-checker='security.insecureAPI.strcpy' --analyze crash.c
clang: ../include/llvm/ADT/APSInt.h:148: bool llvm::APSInt::operator<(const llvm::APSInt &) const: Assertion `IsUnsigned == RHS.IsUnsigned && "Signedness mismatch!"' failed.
PLEASE submit a bug report to https://bugs.llvm.org/ and include the crash backtrace, preprocessed source, and associated run script.
Stack dump:
0.      Program arguments: /llvm/build-all/bin/clang -Xanalyzer -analyzer-output=text -Xanalyzer -analyzer-checker=nullability,optin.portability.UnixAPI,security,valist -Xanalyzer -analyzer-disable-checker=security.insecureAPI.strcpy --analyze crash.c
1.      <eof> parser at end of file
2.      While analyzing stack: 
        #0 Calling func_59
3.      build-all/runtest/csmith/csmith-3790728623.c:1368:79: Error evaluating statement
4.      build-all/runtest/csmith/csmith-3790728623.c:1368:79: Error evaluating statement
 #0 0x0000000002cd99a3 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/llvm/build-all/bin/clang+0x2cd99a3)
 #1 0x0000000002cd761e llvm::sys::RunSignalHandlers() (/llvm/build-all/bin/clang+0x2cd761e)
 #2 0x0000000002cd8d42 llvm::sys::CleanupOnSignal(unsigned long) (/llvm/build-all/bin/clang+0x2cd8d42)
 #3 0x0000000002c4c893 (anonymous namespace)::CrashRecoveryContextImpl::HandleCrash(int, unsigned long) CrashRecoveryContext.cpp:0:0
 #4 0x0000000002c4ca3d CrashRecoverySignalHandler(int) CrashRecoveryContext.cpp:0:0
 #5 0x00007f877102c630 __restore_rt sigaction.c:0:0
 #6 0x00007f876e75f387 raise (/lib64/libc.so.6+0x36387)
 #7 0x00007f876e760a78 abort (/lib64/libc.so.6+0x37a78)
 #8 0x00007f876e7581a6 __assert_fail_base (/lib64/libc.so.6+0x2f1a6)
 #9 0x00007f876e758252 (/lib64/libc.so.6+0x2f252)
#10 0x000000000435bd4f (anonymous namespace)::SymbolicRangeInferrer::VisitBinaryOperator(clang::ento::RangeSet, clang::BinaryOperatorKind, clang::ento::RangeSet, clang::QualType) RangeConstraintManager.cpp:0:0
#11 0x000000000435a757 (anonymous namespace)::SymbolicRangeInferrer::infer(clang::ento::SymExpr const*) RangeConstraintManager.cpp:0:0
#12 0x000000000434e7b5 (anonymous namespace)::RangeConstraintManager::assumeSymNE(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::SymExpr const*, llvm::APSInt const&, llvm::APSInt const&) RangeConstraintManager.cpp:0:0
#13 0x0000000004361e52 clang::ento::RangedConstraintManager::assumeSymUnsupported(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::SymExpr const*, bool) (/llvm/build-all/bin/clang+0x4361e52)
#14 0x000000000437e419 clang::ento::SimpleConstraintManager::assumeAux(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool) (/llvm/build-all/bin/clang+0x437e419)
#15 0x000000000437e278 clang::ento::SimpleConstraintManager::assume(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool) (/llvm/build-all/bin/clang+0x437e278)
#16 0x000000000437e18b clang::ento::SimpleConstraintManager::assume(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::DefinedSVal, bool) (/llvm/build-all/bin/clang+0x437e18b)
#17 0x0000000003f4967c clang::ento::ConstraintManager::assumeDual(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::DefinedSVal) crtstuff.c:0:0
#18 0x00000000042ed7cf clang::ento::ExprEngine::evalEagerlyAssumeBinOpBifurcation(clang::ento::ExplodedNodeSet&, clang::ento::ExplodedNodeSet&, clang::Expr const*) (/llvm/build-all/bin/clang+0x42ed7cf)
#19 0x00000000042ea5db clang::ento::ExprEngine::Visit(clang::Stmt const*, clang::ento::ExplodedNode*, clang::ento::ExplodedNodeSet&) (/llvm/build-all/bin/clang+0x42ea5db)
#20 0x00000000042e58ee clang::ento::ExprEngine::ProcessStmt(clang::Stmt const*, clang::ento::ExplodedNode*) (/llvm/build-all/bin/clang+0x42e58ee)
#21 0x00000000042e5609 clang::ento::ExprEngine::processCFGElement(clang::CFGElement, clang::ento::ExplodedNode*, unsigned int, clang::ento::NodeBuilderContext*) (/llvm/build-all/bin/clang+0x42e5609)
#22 0x00000000042cd850 clang::ento::CoreEngine::HandlePostStmt(clang::CFGBlock const*, unsigned int, clang::ento::ExplodedNode*) (/llvm/build-all/bin/clang+0x42cd850)
#23 0x00000000042cc8e4 clang::ento::CoreEngine::ExecuteWorkList(clang::LocationContext const*, unsigned int, llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>) (/llvm/build-all/bin/clang+0x42cc8e4)
#24 0x0000000003f1fa5c (anonymous namespace)::AnalysisConsumer::HandleCode(clang::Decl*, unsigned int, clang::ento::ExprEngine::InliningModes, llvm::DenseSet<clang::Decl const*, llvm::DenseMapInfo<clang::Decl const*> >*) AnalysisConsumer.cpp:0:0
#25 0x0000000003f035c7 (anonymous namespace)::AnalysisConsumer::HandleTranslationUnit(clang::ASTContext&) AnalysisConsumer.cpp:0:0

Here is the crash.c input

crash.c194 KBDownload

I see lots of these. Probably worth a revert.

[bjope]

I actually see lots of these as well:

clang: ../lib/Support/APInt.cpp:284: int llvm::APInt::compareSigned(const llvm::APInt &) const: Assertion `BitWidth == RHS.BitWidth && "Bit widths must be same for comparison"' failed.

[steakhal]

In D106102#3081178, @bjope wrote:

I get failures after having merged this patch:
[...]
Here is the crash.c input

crash.c194 KBDownload

I see lots of these. Probably worth a revert.

Yeah, actually our nightlies are also crying for the same reason, thus I'm reverting this.
@martong, we should have run some measurement jobs. We definitely need tighter integration with the upstream changes, regarding our build jobs.

@bjope, thanks for the quick report.

[manas]

Based on the information from debugger, the logs show RangeSets [0, 255] and [INT_MIN, 0] from different types are causing the failure.
I tried producing a compact test case. The essential part is the comparison between different types, as in this case unsigned int and int. In other binary operators (BO_And, BO_Rem, etc.), this gets handled by coarsing RangeSets to Ranges and converting those Ranges to resulting type for comparison. This is missing in BO_NE. I suppose, this may be the reason behind the signedness mismatch.

One way to solve this would be to let the specialization of VisitBinaryOperator (definition here) handle the coarse/convert, and then VisitBinaryOperator<BO_NE> checking for any reasonable result which can be inferred from those Ranges.

[steakhal]

In D106102#3082399, @manas wrote:

Based on the information from debugger, the logs show RangeSets [0, 255] and [INT_MIN, 0] from different types are causing the failure.
I tried producing a compact test case. The essential part is the comparison between different types, as in this case unsigned int and int. In other binary operators (BO_And, BO_Rem, etc.), this gets handled by coarsing RangeSets to Ranges and converting those Ranges to resulting type for comparison. This is missing in BO_NE. I suppose, this may be the reason behind the signedness mismatch.

One way to solve this would be to let the specialization of VisitBinaryOperator (definition here) handle the coarse/convert, and then VisitBinaryOperator<BO_NE> checking for any reasonable result which can be inferred from those Ranges.

I think you are right. I'm gonna have a deeper look at this tomorrow. Until then you shouls figure out how this was avoided in other operations. Dealing with this for one and all seems promising. Ive seen multiple fixup commits resolving similar issues, so it seems to bite back regularly.

[martong]

Thanks for the report @bjope and thanks for the action @manas and @steakhal !
Sorry guys, I should have run our CI safety net jobs for this patch. I tend to do that with all my solver related patches, I really don't know why I thought this was different.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/ADT/STLExtras.h"
-#include "llvm/ADT/StringExtras.h"
 #include "llvm/ADT/SmallSet.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/Compiler.h"
 #include "llvm/Support/raw_ostream.h"
 #include <algorithm>
 #include <iterator>
 
 using namespace clang;
 using namespace ento;
 
RangeSet VisitBinaryOperator(const BinarySymExprTy *Sym) {
     // in here.
     QualType ResultType = Sym->getType();
     return VisitBinaryOperator(inferAs(Sym->getLHS(), ResultType),
                                Sym->getOpcode(),
                                inferAs(Sym->getRHS(), ResultType), ResultType);
   }
 
   RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
-                               RangeSet RHS, QualType T) {
-    switch (Op) {
-    case BO_Or:
-      return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
-    case BO_And:
-      return VisitBinaryOperator<BO_And>(LHS, RHS, T);
-    case BO_Rem:
-      return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
-    default:
-      return infer(T);
-    }
-  }
+                               RangeSet RHS, QualType T);
 
   //===----------------------------------------------------------------------===//
   //                         Ranges and operators
   //===----------------------------------------------------------------------===//
 
   /// Return a rough approximation of the given range set.
   ///
   /// For the range set:
private:
   RangeSet::Factory &RangeFactory;
   ProgramStateRef State;
 };
 
 //===----------------------------------------------------------------------===//
 //               Range-based reasoning about symbolic operations
 //===----------------------------------------------------------------------===//
 
 template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_NE>(RangeSet LHS,
+                                                           RangeSet RHS,
+                                                           QualType T) {
+  // When both the RangeSets are non-overlapping then all possible pairs of
+  // (x, y) in LHS, RHS respectively, will satisfy expression (x != y).
+  if ((LHS.getMaxValue() < RHS.getMinValue()) ||
+      (LHS.getMinValue() > RHS.getMaxValue())) {
+    return getTrueRange(T);
+  }
+
+  // If both RangeSets contain only one Point which is equal then the
+  // expression will always return true.
+  if ((LHS.getMinValue() == RHS.getMaxValue()) &&
+      (LHS.getMaxValue() == RHS.getMaxValue()) &&
+      (LHS.getMinValue() == RHS.getMinValue())) {
+    return getFalseRange(T);
+  }
+
+  // In all other cases, the resulting range cannot be deduced.
+  return infer(T);
+}
+
+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)};
 }
 
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator(RangeSet LHS,
+                                                    BinaryOperator::Opcode Op,
+                                                    RangeSet RHS, QualType T) {
+  switch (Op) {
+  case BO_NE:
+    return VisitBinaryOperator<BO_NE>(LHS, RHS, T);
+  case BO_Or:
+    return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
+  case BO_And:
+    return VisitBinaryOperator<BO_And>(LHS, RHS, T);
+  case BO_Rem:
+    return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
+  default:
+    return infer(T);
+  }
+}
+
 //===----------------------------------------------------------------------===//
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
 
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
       : RangedConstraintManager(EE, SVB), F(getBasicVals()) {}

clang/test/Analysis/constant-folding.c

void testRemainderRules(unsigned int a, unsigned int b, int c, int d) {
 
   // Check that we work correctly when minimal unsigned value from a range is
   // equal to the signed minimum for the same bit width.
   unsigned int x = INT_MIN;
   if (a >= x && a <= x + 10) {
     clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
   }
 }
+
+void testDisequalityRules(unsigned int u1, unsigned int u2, int s1, int s2) {
+  // Checks when ranges are not overlapping
+  if (u1 <= 10 && u2 >= 20) {
+    // u1: [0,10], u2: [20,UINT_MAX]
+    clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{TRUE}}
+  }
+
+  if (s1 <= INT_MIN + 10 && s2 >= INT_MAX - 10) {
+    // s1: [INT_MIN,INT_MIN + 10], s2: [INT_MAX - 10,INT_MAX]
+    clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{FALSE}}
+  }
+
+  // Checks when ranges are completely overlapping and have more than one point
+  if (u1 >= 20 && u1 <= 50 && u2 >= 20 && u2 <= 50) {
+    // u1: [20,50], u2: [20,50]
+    clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (s1 >= -20 && s1 <= 20 && s2 >= -20 && s2 <= 20) {
+    // s1: [-20,20], s2: [-20,20]
+    clang_analyzer_eval((s1 != s2) != 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks when ranges are partially overlapping
+  if (u1 >= 100 && u1 <= 200 && u2 >= 150 && u2 <= 300) {
+    // u1: [100,200], u2: [150,300]
+    clang_analyzer_eval((u1 != u2) != 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (s1 >= -80 && s1 <= -50 && s2 >= -100 && s2 <= -75) {
+    // s1: [-80,-50], s2: [-100,-75]
+    clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks for ranges which are subset of one-another
+  if (u1 >= 500 && u1 <= 1000 && u2 >= 750 && u2 <= 1000) {
+    // u1: [500,1000], u2: [750,1000]
+    clang_analyzer_eval((u1 != u2) == 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (s1 >= -1000 && s1 <= -500 && s2 <= -500 && s2 >= -750) {
+    // s1: [-1000,-500], s2: [-500,-750]
+    clang_analyzer_eval((s1 != s2) == 0); // expected-warning{{UNKNOWN}}
+  }
+}