[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added a comment.

Thanks for the assiduous review guys!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

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

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[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 rG888af47095d5: [Analyzer][solver] Simplification: reorganize 
equalities with adjustment (authored by martong).

Changed prior to commit:
  https://reviews.llvm.org/D111642?vs=381536=382674#toc

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/solver-sym-simplification-adjustment.c

Index: clang/test/Analysis/solver-sym-simplification-adjustment.c
===
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-adjustment.c
@@ -0,0 +1,111 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_adjustment_concrete_int(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b != 0)  // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1 == 0 --> c == -1
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);   // expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+return;
+   // c: [-2,-1] is intersected with the
+   // already associated range which is [-1,1],
+   // thus we get c: [-1,-1]
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);// expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
+  if (b < 0 || b > 1) // b: [0,1]
+return;
+  if (c < 0 || c > 1) // c: [0,1]
+return;
+  if (c + b != 0) // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1) {   // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+clang_analyzer_eval(b == 0);  // expected-warning{{TRUE}}
+clang_analyzer_eval(c == 0);  // expected-warning{{TRUE}}
+// Keep the symbols and the constraints! alive.
+(void)(b * c);
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeassible_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < 0 || c > 1)  // c: [0,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1] contradiction
+return;
+  clang_analyzer_warnIfReached();  // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {
+  if (a == b)// a != b
+return;
+  if (c != 0)// c == 0
+return;
+
+  if (b != 0)// b == 0
+return;
+  // The above simplification of `b == 0` could result in an infinite loop
+  // unless we detect that the State is unchanged.
+  // The loop:
+  // 1) Simplification of the trivial equivalence class
+  //  "symbol": "(reg_$0) == (reg_$1)", "range": "{ [0, 0] }"
+  //results in
+  //  "symbol": "(reg_$0) == 0", "range": "{ [0, 0] }" }
+  //which in turn creates a non-trivial equivalence class
+  //  [ "(reg_$0) == (reg_$1)", "(reg_$0) == 0" ]
+  // 2) We call assumeSymInclusiveRange("(reg_$0) == 0")
+  //and that calls **simplify** on the associated non-trivial equivalence
+  //class. During the simplification the State does not change, we reached
+  //the fixpoint.
+
+  (void)(a * b * c);
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ 

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.

Awesome!
So clean, and I also like the tests.
Good job.




Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:58
+  if (b != 1) {   // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+clang_analyzer_eval(b == 0);  // expected-warning{{TRUE}}
+// Keep the symbols and the constraints! alive.

Please assert `clang_analyzer_eval(c == 0)` as well.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

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

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D111642#3059467 , @steakhal wrote:

> The coverage report of the test shows that L2124 is uncovered. Please add a 
> test demonstrating that path as well.

I've added such a test, thanks for the notice!




Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2126-2130
+  // Initiate the reorganization of the equality information. E.g., if we
+  // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes
+  // sense to do this only with `SymIntExpr`s.
+  // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle
+  // them.

steakhal wrote:
> Can the simplification of a `SymSymExpr` result in `IntSymExpr`? If it can 
> happen, then we could see such instances and we should do the right thing 
> with them as well.
> WDYT?
> Can the simplification of a `SymSymExpr` result in `IntSymExpr`?
Yes it can. However, in order to handle them we should extend 
`computeAdjustment` properly, which is absolutely not trivial - considering the 
test cases in `additive-folding.cpp` -  So, I'd rather address that in another 
patch.




Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:36
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+return;

steakhal wrote:
> Please express that `C: [-2,-1]` is then intersected with the already 
> associated range which is `[-1,1]`, thus we get `c: [-1,-1]`.
Ok, I've added that comment.



Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:55
+  if (b != 1) // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+return;
+  clang_analyzer_warnIfReached(); // no warning

steakhal wrote:
> Can we infer within this true branch that `b` must be `0` to make this path 
> feasible?
> If we already can infer this, can we put there the appropriate assertion?
> If not, an assertion would be justified with a FIXME.
> Can we infer within this true branch that `b` must be `0` to make this path 
> feasible?
Yes, we can.

> If we already can infer this, can we put there the appropriate assertion?
Ok, I've added the appropriate `clang_analyzer_eval` to check this.



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

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

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 381536.
martong added a comment.

- Add a test to cover `if (OldState == State)`


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/solver-sym-simplification-adjustment.c

Index: clang/test/Analysis/solver-sym-simplification-adjustment.c
===
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-adjustment.c
@@ -0,0 +1,110 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_adjustment_concrete_int(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b != 0)  // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1 == 0 --> c == -1
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);   // expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+return;
+   // c: [-2,-1] is intersected with the
+   // already associated range which is [-1,1],
+   // thus we get c: [-1,-1]
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);// expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
+  if (b < 0 || b > 1) // b: [0,1]
+return;
+  if (c < 0 || c > 1) // c: [0,1]
+return;
+  if (c + b != 0) // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1) {   // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+clang_analyzer_eval(b == 0);  // expected-warning{{TRUE}}
+// Keep the symbols and the constraints! alive.
+(void)(b * c);
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeassible_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < 0 || c > 1)  // c: [0,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1] contradiction
+return;
+  clang_analyzer_warnIfReached();  // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {
+  if (a == b)// a != b
+return;
+  if (c != 0)// c == 0
+return;
+
+  if (b != 0)// b == 0
+return;
+  // The above simplification of `b == 0` could result in an infinite loop
+  // unless we detect that the State is unchanged.
+  // The loop:
+  // 1) Simplification of the trivial equivalence class
+  //  "symbol": "(reg_$0) == (reg_$1)", "range": "{ [0, 0] }"
+  //results in
+  //  "symbol": "(reg_$0) == 0", "range": "{ [0, 0] }" }
+  //which in turn creates a non-trivial equivalence class
+  //  [ "(reg_$0) == (reg_$1)", "(reg_$0) == 0" ]
+  // 2) We call assumeSymInclusiveRange("(reg_$0) == 0")
+  //and that calls **simplify** on the associated non-trivial equivalence
+  //class. During the simplification the State does not change, we reached
+  //the fixpoint.
+
+  (void)(a * b * c);
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -602,10 +602,9 @@
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
   /// Iterate over all symbols and try to simplify them.
-  LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder ,
-   

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 381520.
martong marked 3 inline comments as done.
martong added a comment.

- Add comment about intersection in the test file
- Add check in the feasible case in the test file


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/solver-sym-simplification-adjustment.c

Index: clang/test/Analysis/solver-sym-simplification-adjustment.c
===
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-adjustment.c
@@ -0,0 +1,85 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_adjustment_concrete_int(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b != 0)  // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1 == 0 --> c == -1
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);   // expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+return;
+   // c: [-2,-1] is intersected with the
+   // already associated range which is [-1,1],
+   // thus we get c: [-1,-1]
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);// expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
+  if (b < 0 || b > 1) // b: [0,1]
+return;
+  if (c < 0 || c > 1) // c: [0,1]
+return;
+  if (c + b != 0) // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1) {   // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+clang_analyzer_eval(b == 0);  // expected-warning{{TRUE}}
+// Keep the symbols and the constraints! alive.
+(void)(b * c);
+return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeassible_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < 0 || c > 1)  // c: [0,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1] contradiction
+return;
+  clang_analyzer_warnIfReached();  // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -602,10 +602,9 @@
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
   /// Iterate over all symbols and try to simplify them.
-  LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder ,
-RangeSet::Factory ,
-ProgramStateRef State,
-EquivalenceClass Class);
+  LLVM_NODISCARD static inline ProgramStateRef
+  simplify(SValBuilder , RangeSet::Factory , RangedConstraintManager ,
+   ProgramStateRef State, EquivalenceClass Class);
 
   void dumpToStream(ProgramStateRef State, raw_ostream ) const;
   LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
@@ -1710,7 +1709,8 @@
   ClassMembersTy Members = State->get();
   for (std::pair ClassToSymbolSet : Members) {
 EquivalenceClass Class = ClassToSymbolSet.first;
-State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
+State =
+EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class);
 if 

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Balázs Benics via Phabricator via cfe-commits]

steakhal added inline comments.



Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2126-2130
+  // Initiate the reorganization of the equality information. E.g., if we
+  // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes
+  // sense to do this only with `SymIntExpr`s.
+  // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle
+  // them.

Can the simplification of a `SymSymExpr` result in `IntSymExpr`? If it can 
happen, then we could see such instances and we should do the right thing with 
them as well.
WDYT?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

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

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

The coverage report of the test shows that L2124 is uncovered. Please add a 
test demonstrating that path as well.
I'm gonna come back to this tomorrow.




Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:36
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+return;

Please express that `C: [-2,-1]` is then intersected with the already 
associated range which is `[-1,1]`, thus we get `c: [-1,-1]`.



Comment at: clang/test/Analysis/solver-sym-simplification-adjustment.c:55
+  if (b != 1) // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+return;
+  clang_analyzer_warnIfReached(); // no warning

Can we infer within this true branch that `b` must be `0` to make this path 
feasible?
If we already can infer this, can we put there the appropriate assertion?
If not, an assertion would be justified with a FIXME.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D111642

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

[PATCH] D111642: [Analyzer][solver] Simplification: reorganize equalities with adjustment

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: steakhal, ASDenysPetrov, NoQ.
Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, Szelethus, 
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun, 
whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Initiate the reorganization of the equality information during symbol
simplification. E.g., if we bump into `c + 1 == 0` during simplification
then we'd like to express that `c == -1`. It makes sense to do this only
with `SymIntExpr`s.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D111642

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/solver-sym-simplification-adjustment.c

Index: clang/test/Analysis/solver-sym-simplification-adjustment.c
===
--- /dev/null
+++ clang/test/Analysis/solver-sym-simplification-adjustment.c
@@ -0,0 +1,78 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_adjustment_concrete_int(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b != 0)  // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1 == 0 --> c == -1
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);   // expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < -1 || c > 1) // c: [-1,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);// expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
+  if (b < 0 || b > 1) // b: [0,1]
+return;
+  if (c < 0 || c > 1) // c: [0,1]
+return;
+  if (c + b != 0) // c + b == 0
+return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1) // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+return;
+  clang_analyzer_warnIfReached(); // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeassible_range(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+return;
+  if (c < 0 || c > 1)  // c: [0,1]
+return;
+  if (c + b < -1 || c + b > 0) // c + b: [-1,0]
+return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)  // b == 1  --> c + 1: [-1,0] --> c: [-2,-1] contradiction
+return;
+  clang_analyzer_warnIfReached();  // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -602,10 +602,9 @@
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
   /// Iterate over all symbols and try to simplify them.
-  LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder ,
-RangeSet::Factory ,
-ProgramStateRef State,
-EquivalenceClass Class);
+  LLVM_NODISCARD static inline ProgramStateRef
+  simplify(SValBuilder , RangeSet::Factory , RangedConstraintManager ,
+   ProgramStateRef State, EquivalenceClass Class);
 
   void dumpToStream(ProgramStateRef State, raw_ostream ) const;
   LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
@@ -1710,7 +1709,8 @@
   ClassMembersTy Members = State->get();
   for (std::pair ClassToSymbolSet : Members) {
 EquivalenceClass Class = ClassToSymbolSet.first;
-State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
+State =
+EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class);
 if