[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-30 Thread Balázs Benics via Phabricator via cfe-commits 
steakhal added a comment.

In D88019#2303078 , @martong wrote:

> I like the second approach, i.e. to have a debug checker. But I don't see, 
> how would this checker validate all constraints at the moment when they are 
> added to the State.

`ProgramStateRef evalAssume(ProgramStateRef State, SVal Cond, bool Assumption)` 
checker callback is called **after** any assume call.
So, we would have a `State` which has all? the constraints stored in the 
appropriate GDM. I'm not sure if we should aggregate all the constraints till 
this node - like we do for refutation. I think, in this case, we should just 
make sure that the **current** state does not have any contradiction.

---

Here is my proof-of-concept:

I've  dumped the state and args of evalAssume for the repro example, pretending 
that we don't reach a code-path on the infeasable path to crash:

  void avoidInfeasibleConstraintforGT(int a, int b) {
int c = b - a;
if (c <= 0)
  return;
if (a != b) {
  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  return;
}
clang_analyzer_warnIfReached(); // eh, we will reach this..., #1
// These are commented out, to pretend that we don't find out that we are 
on an infeasable path...
// a == b
// if (c < 0)
//   ;
  }

We reach the `#1` line, but more importantly, we will have the following state 
dumps:

  evalAssume: assuming Cond: (reg_$1) != (reg_$0) to be true in 
state:
  "program_state": {
"constraints": [
  { "symbol": "(reg_$0) - (reg_$1)", "range": "{ [1, 
2147483647] }" },
  { "symbol": "(reg_$1) != (reg_$0)", "range": "{ 
[-2147483648, -1], [1, 2147483647] }" }
]
  }
  
  evalAssume: assuming Cond: (reg_$1) != (reg_$0) to be false in 
state:
  "program_state": {
"constraints": [
  { "symbol": "(reg_$0) - (reg_$1)", "range": "{ [1, 
2147483647] }" },
  { "symbol": "(reg_$1) != (reg_$0)", "range": "{ [0, 0] }" }
]
  }

As you can see, the **latter** is the //infeasable// path, and if we have had 
serialized the constraints and let the Z3 check it, we would have gotten that 
it's unfeasable.
At this point the checker can dump any useful data for debugging, and crash the 
analyzer to let us know that something really bad happened.

> [...] And that might be too slow, it would have the same speed as using z3 
> instead of the range based solver.

Yes, it will probably freaking slow, but at least we have something.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-30 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

In D88019#2296337 , @steakhal wrote:

> In D88019#2291953 , @steakhal wrote:
>
>> What are our options mitigating anything similar happening in the future?
>>
>> This way any change touching the `SymbolicRangeInferrer` and any related 
>> parts of the analyzer seems to be way too fragile.
>> Especially, since we might want to add support for comparing SymSyms, just 
>> like we try to do in D77792 .
>
> What about changing the EXPENSIVE_CHECKS 
> 
>  in the assume function in the following way:
> Convert all range constraints into a Z3 model and check if that is `UNSAT`.
> In that case, we would have returned a state with contradictions, so we would 
> prevent this particular bug from lurking around to bite us later.
>
> And another possibility could be to create a debug checker, which registers 
> to the assume callback and does the same conversion and check.
> This is more appealing to me in some way, like decouples the Z3 dependency 
> from the `ConstraintManager` header.
>
> Which approach should I prefer? @NoQ @vsavchenko @martong @xazax.hun 
> @Szelethus

I like the second approach, i.e. to have a debug checker. But I don't see, how 
would this checker validate all constraints at the moment when they are added 
to the State. And if we don't check all constraints then we might end up 
checking a state that is invalid for a while (i.e. that might became invalid 
previously and not because of the lastly added constraint.) So, essentially, my 
gut feeling is that both approaches should be validating all newly added 
constraints against Z3. And that might be too slow, it would have the same 
speed as using z3 instead of the range based solver.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-26 Thread Balázs Benics via Phabricator via cfe-commits 
steakhal added a comment.

In D88019#2291953 , @steakhal wrote:

> What are our options mitigating anything similar happening in the future?
>
> This way any change touching the `SymbolicRangeInferrer` and any related 
> parts of the analyzer seems to be way too fragile.
> Especially, since we might want to add support for comparing SymSyms, just 
> like we try to do in D77792 .

What about changing the EXPENSIVE_CHECKS 

 in the assume function in the following way:
Convert all range constraints into a Z3 model and check if that is `UNSAT`.
In that case, we would have returned a state with contradictions, so we would 
prevent this particular bug from lurking around to bite us later.

And another possibility could be to create a debug checker, which registers to 
the assume callback and does the same conversion and check.
This is more appealing to me in some way, like decouples the Z3 dependency from 
the `ConstraintManager` header.

Which approach should I prefer? @NoQ @vsavchenko @martong @xazax.hun @Szelethus


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-24 Thread Balázs Benics via Phabricator via cfe-commits 
steakhal added a comment.

What are our options mitigating anything similar happening in the future?

This way any change touching the `SymbolicRangeInferrer` and any related parts 
of the analyzer seems to be way too fragile.
Especially, since we might want to add support for comparing SymSyms, just like 
we try to do in D77792 .


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Gabor Marton via Phabricator via cfe-commits 
This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG0c4f91f84b2e: [analyzer][solver] Fix issue with symbol 
non-equality tracking (authored by martong).

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/equality_tracking.c

Index: clang/test/Analysis/equality_tracking.c
===
--- clang/test/Analysis/equality_tracking.c
+++ clang/test/Analysis/equality_tracking.c
@@ -185,3 +185,37 @@
 }
   }
 }
+
+void avoidInfeasibleConstraintforGT(int a, int b) {
+  int c = b - a;
+  if (c <= 0)
+return;
+  // c > 0
+  // b - a > 0
+  // b > a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
+
+void avoidInfeasibleConstraintforLT(int a, int b) {
+  int c = b - a;
+  if (c >= 0)
+return;
+  // c < 0
+  // b - a < 0
+  // b < a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1347,27 +1347,35 @@
   // Equality tracking implementation
   //===--===//
 
-  ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym,
-  const llvm::APSInt &Int,
+  ProgramStateRef trackEQ(RangeSet NewConstraint, ProgramStateRef State,
+  SymbolRef Sym, const llvm::APSInt &Int,
   const llvm::APSInt &Adjustment) {
-if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
-  // Extract function assumes that we gave it Sym + Adjustment != Int,
-  // so the result should be opposite.
-  Equality->invert();
-  return track(State, *Equality);
-}
-
-return State;
+return track(NewConstraint, State, Sym, Int, Adjustment);
   }
 
-  ProgramStateRef trackNE(ProgramStateRef State, SymbolRef Sym,
-  const llvm::APSInt &Int,
+  ProgramStateRef trackNE(RangeSet NewConstraint, ProgramStateRef State,
+  SymbolRef Sym, const llvm::APSInt &Int,
   const llvm::APSInt &Adjustment) {
+return track(NewConstraint, State, Sym, Int, Adjustment);
+  }
+
+  template 
+  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;
+
+ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint);
 if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
-  return track(State, *Equality);
+  // If the original assumption is not Sym + Adjustment !=/ Int,
+  // we should invert IsEquality flag.
+  Equality->IsEquality = Equality->IsEquality != EQ;
+  return track(NewState, *Equality);
 }
 
-return State;
+return NewState;
   }
 
   ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) {
@@ -2042,12 +2050,7 @@
 
   RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point);
 
-  if (New.isEmpty())
-// this is infeasible assumption
-return nullptr;
-
-  ProgramStateRef NewState = setConstraint(St, Sym, New);
-  return trackNE(NewState, Sym, Int, Adjustment);
+  return trackNE(New, St, Sym, Int, Adjustment);
 }
 
 ProgramStateRef
@@ -2063,12 +2066,7 @@
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
   RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
 
-  if (New.isEmpty())
-// this is infeasible assumption
-return nullptr;
-
-  ProgramStateRef NewState = setConstraint(St, Sym, New);
-  return trackEQ(NewState, Sym, Int, Adjustment);
+  return trackEQ(New, St, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
@@ -2104,7 +2102,7 @@
 const llvm::APSInt &Int,
 const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  return trackNE(New, St, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
@@ -2140,7 +2138,7 @@

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Valeriy Savchenko via Phabricator via cfe-commits 
vsavchenko accepted this revision.
vsavchenko added a comment.
This revision is now accepted and ready to land.

Amazing!


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

Thanks for the quick review!
I updated according to your suggestion, so we avoid the same pattern.




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1350-1371
   ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym,
   const llvm::APSInt &Int,
   const llvm::APSInt &Adjustment) {
 if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
   // Extract function assumes that we gave it Sym + Adjustment != Int,
   // so the result should be opposite.
   Equality->invert();

vsavchenko wrote:
> I suggest to change these two functions this way, so we can avoid the same 
> pattern in 4 different functions
> I suggest to change these two functions this way, so we can avoid the same 
> pattern in 4 different functions




Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Gabor Marton via Phabricator via cfe-commits 
martong updated this revision to Diff 293168.
martong marked an inline comment as done.
martong added a comment.

- Avoid same pattern when checking whether the assumption is infeasible


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/equality_tracking.c

Index: clang/test/Analysis/equality_tracking.c
===
--- clang/test/Analysis/equality_tracking.c
+++ clang/test/Analysis/equality_tracking.c
@@ -185,3 +185,37 @@
 }
   }
 }
+
+void avoidInfeasibleConstraintforGT(int a, int b) {
+  int c = b - a;
+  if (c <= 0)
+return;
+  // c > 0
+  // b - a > 0
+  // b > a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
+
+void avoidInfeasibleConstraintforLT(int a, int b) {
+  int c = b - a;
+  if (c >= 0)
+return;
+  // c < 0
+  // b - a < 0
+  // b < a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1347,27 +1347,35 @@
   // Equality tracking implementation
   //===--===//
 
-  ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym,
-  const llvm::APSInt &Int,
+  ProgramStateRef trackEQ(RangeSet NewConstraint, ProgramStateRef State,
+  SymbolRef Sym, const llvm::APSInt &Int,
   const llvm::APSInt &Adjustment) {
-if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
-  // Extract function assumes that we gave it Sym + Adjustment != Int,
-  // so the result should be opposite.
-  Equality->invert();
-  return track(State, *Equality);
-}
-
-return State;
+return track(NewConstraint, State, Sym, Int, Adjustment);
   }
 
-  ProgramStateRef trackNE(ProgramStateRef State, SymbolRef Sym,
-  const llvm::APSInt &Int,
+  ProgramStateRef trackNE(RangeSet NewConstraint, ProgramStateRef State,
+  SymbolRef Sym, const llvm::APSInt &Int,
   const llvm::APSInt &Adjustment) {
+return track(NewConstraint, State, Sym, Int, Adjustment);
+  }
+
+  template 
+  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;
+
+ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint);
 if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
-  return track(State, *Equality);
+  // If the original assumption is not Sym + Adjustment !=/ Int,
+  // we should invert IsEquality flag.
+  Equality->IsEquality = Equality->IsEquality != EQ;
+  return track(NewState, *Equality);
 }
 
-return State;
+return NewState;
   }
 
   ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) {
@@ -2042,12 +2050,7 @@
 
   RangeSet New = getRange(St, Sym).Delete(getBasicVals(), F, Point);
 
-  if (New.isEmpty())
-// this is infeasible assumption
-return nullptr;
-
-  ProgramStateRef NewState = setConstraint(St, Sym, New);
-  return trackNE(NewState, Sym, Int, Adjustment);
+  return trackNE(New, St, Sym, Int, Adjustment);
 }
 
 ProgramStateRef
@@ -2063,12 +2066,7 @@
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
   RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
 
-  if (New.isEmpty())
-// this is infeasible assumption
-return nullptr;
-
-  ProgramStateRef NewState = setConstraint(St, Sym, New);
-  return trackEQ(NewState, Sym, Int, Adjustment);
+  return trackEQ(New, St, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
@@ -2104,7 +2102,7 @@
 const llvm::APSInt &Int,
 const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  return trackNE(New, St, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
@@ -2140,7 +2138,7 @@
 const llvm::APSInt &Int,

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Valeriy Savchenko via Phabricator via cfe-commits 
vsavchenko added a comment.

After this "accepted" and a huge thank you 😄




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1350-1371
   ProgramStateRef trackEQ(ProgramStateRef State, SymbolRef Sym,
   const llvm::APSInt &Int,
   const llvm::APSInt &Adjustment) {
 if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
   // Extract function assumes that we gave it Sym + Adjustment != Int,
   // so the result should be opposite.
   Equality->invert();

I suggest to change these two functions this way, so we can avoid the same 
pattern in 4 different functions


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Valeriy Savchenko via Phabricator via cfe-commits 
vsavchenko added a comment.

I came up with exactly the same fix! Great job!
I just wanted to refactor it and not having

  if (New.isEmpty())
// this is infeasible assumption
return nullptr;
  
  ProgramStateRef NewState = setConstraint(St, Sym, New);
  return trackNE(NewState, Sym, Int, Adjustment);

repeated in different places


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Gabor Marton via Phabricator via cfe-commits 
martong added a comment.

@steakhal, thank you for your time and huge effort in debugging this!


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D88019/new/

https://reviews.llvm.org/D88019

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

2020-09-21 Thread Gabor Marton via Phabricator via cfe-commits 
martong created this revision.
martong added reviewers: vsavchenko, steakhal, NoQ.
Herald added subscribers: cfe-commits, ASDenysPetrov, Charusso, gamesh411, 
dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, 
baloghadamsoftware, xazax.hun, whisperity.
Herald added a reviewer: Szelethus.
Herald added a project: clang.
martong requested review of this revision.

We should track non-equivalency (disequality) in case of greater-then or
less-then assumptions.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D88019

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/equality_tracking.c


Index: clang/test/Analysis/equality_tracking.c
===
--- clang/test/Analysis/equality_tracking.c
+++ clang/test/Analysis/equality_tracking.c
@@ -185,3 +185,37 @@
 }
   }
 }
+
+void avoidInfeasibleConstraintforGT(int a, int b) {
+  int c = b - a;
+  if (c <= 0)
+return;
+  // c > 0
+  // b - a > 0
+  // b > a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
+
+void avoidInfeasibleConstraintforLT(int a, int b) {
+  int c = b - a;
+  if (c >= 0)
+return;
+  // c < 0
+  // b - a < 0
+  // b < a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2104,7 +2104,12 @@
 const llvm::APSInt &Int,
 const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  if (New.isEmpty())
+// this is infeasible assumption
+return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackNE(NewState, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
@@ -2140,7 +2145,12 @@
 const llvm::APSInt &Int,
 const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  if (New.isEmpty())
+// this is infeasible assumption
+return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackNE(NewState, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,


Index: clang/test/Analysis/equality_tracking.c
===
--- clang/test/Analysis/equality_tracking.c
+++ clang/test/Analysis/equality_tracking.c
@@ -185,3 +185,37 @@
 }
   }
 }
+
+void avoidInfeasibleConstraintforGT(int a, int b) {
+  int c = b - a;
+  if (c <= 0)
+return;
+  // c > 0
+  // b - a > 0
+  // b > a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
+
+void avoidInfeasibleConstraintforLT(int a, int b) {
+  int c = b - a;
+  if (c >= 0)
+return;
+  // c < 0
+  // b - a < 0
+  // b < a
+  if (a != b) {
+clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2104,7 +2104,12 @@
 const llvm::APSInt &Int,
 const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  if (New.isEmpty())
+// this is infeasible assumption
+return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackNE(NewState, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
@@ -2140,7 +2145,12 @@
 const llvm::APSInt &Int,
 const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  if (New.isEmpty())
+// this is infeasible assumption
+return nullptr;
+
+  ProgramS