patches/cherry/20f8733d4b8d5bdb93080b8824de57b7fae31785.patch - toolchain/llvm_android - Git at Google

 From 16ae0cfa1e8e07e17fdc7ad93e544a828d933072 Mon Sep 17 00:00:00 2001
 From: Gabor Marton <gabor.marton@ericsson.com>
 Date: Wed, 1 Dec 2021 16:47:22 +0100
 Subject: [PATCH] [Analyzer][solver] Simplification: Do a fixpoint iteration
  before the eq class merge

 This reverts commit f02c5f3478318075d1a469203900e452ba651421 and
 addresses the issue mentioned in D114619 differently.

 Repeating the issue here:
 Currently, during symbol simplification we remove the original member
 symbol from the equivalence class (`ClassMembers` trait). However, we
 keep the reverse link (`ClassMap` trait), in order to be able the query
 the related constraints even for the old member. This asymmetry can lead
 to a problem when we merge equivalence classes:
 ```
 ClassA: [a, b]   // ClassMembers trait,
 a->a, b->a       // ClassMap trait, a is the representative symbol
 ```
 Now let,s delete `a`:
 ```
 ClassA: [b]
 a->a, b->a
 ```
 Let's merge ClassA into the trivial class `c`:
 ```
 ClassA: [c, b]
 c->c, b->c, a->a
 ```
 Now, after the merge operation, `c` and `a` are actually in different
 equivalence classes, which is inconsistent.

 This issue manifests in a test case (added in D103317):
 ```
 void recurring_symbol(int b) {
   if (b * b != b)
     if ((b * b) * b * b != (b * b) * b)
       if (b * b == 1)
 }
 ```
 Before the simplification we have these equivalence classes:
 ```
 trivial EQ1: [b * b != b]
 trivial EQ2: [(b * b) * b * b != (b * b) * b]
 ```

 During the simplification with `b * b == 1`, EQ1 is merged with `1 != b`
 `EQ1: [b * b != b, 1 != b]` and we remove the complex symbol, so
 `EQ1: [1 != b]`
 Then we start to simplify the only symbol in EQ2:
 `(b * b) * b * b != (b * b) * b --> 1 * b * b != 1 * b --> b * b != b`
 But `b * b != b` is such a symbol that had been removed previously from
 EQ1, thus we reach the above mentioned inconsistency.

 This patch addresses the issue by making it impossible to synthesise a
 symbol that had been simplified before. We achieve this by simplifying
 the given symbol to the absolute simplest form.

 Differential Revision: https://reviews.llvm.org/D114887
 ---
  .../Core/RangeConstraintManager.cpp           | 93 ++++++++++++++++---
  .../expr-inspection-printState-eq-classes.c   |  4 +-
  ...symbol-simplification-disequality-info.cpp | 57 ++++++------
  ...-simplification-fixpoint-one-iteration.cpp | 17 ++--
  ...simplification-fixpoint-two-iterations.cpp | 25 +++--
  5 files changed, 128 insertions(+), 68 deletions(-)

 diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
 index 3f8d9e4298a0..23c67c64f975 100644
 --- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
 +++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
 @@ -601,6 +601,10 @@ public:
    LLVM_NODISCARD static inline Optional<bool>
    areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);

 +  /// Remove one member from the class.
 +  LLVM_NODISCARD ProgramStateRef removeMember(ProgramStateRef State,
 +                                              const SymbolRef Old);
 +
    /// Iterate over all symbols and try to simplify them.
    LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB,
                                                          RangeSet::Factory &F,
 @@ -2132,6 +2136,34 @@ inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
    return llvm::None;
  }

 +LLVM_NODISCARD ProgramStateRef
 +EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
 +
 +  SymbolSet ClsMembers = getClassMembers(State);
 +  assert(ClsMembers.contains(Old));
 +
 +  // We don't remove `Old`'s Sym->Class relation for two reasons:
 +  // 1) This way constraints for the old symbol can still be found via it's
 +  // equivalence class that it used to be the member of.
 +  // 2) Performance and resource reasons. We can spare one removal and thus one
 +  // additional tree in the forest of `ClassMap`.
 +
 +  // Remove `Old`'s Class->Sym relation.
 +  SymbolSet::Factory &F = getMembersFactory(State);
 +  ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>();
 +  ClsMembers = F.remove(ClsMembers, Old);
 +  // Ensure another precondition of the removeMember function (we can check
 +  // this only with isEmpty, thus we have to do the remove first).
 +  assert(!ClsMembers.isEmpty() &&
 +         "Class should have had at least two members before member removal");
 +  // Overwrite the existing members assigned to this class.
 +  ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
 +  ClassMembersMap = EMFactory.add(ClassMembersMap, *this, ClsMembers);
 +  State = State->set<ClassMembers>(ClassMembersMap);
 +
 +  return State;
 +}
 +
  // Re-evaluate an SVal with top-level `State->assume` logic.
  LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
                                          const RangeSet *Constraint,
 @@ -2159,6 +2191,42 @@ LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
                                       Constraint->getMaxValue(), true);
  }

 +// Simplify the given symbol with the help of the SValBuilder. In
 +// SValBuilder::symplifySval, we traverse the symbol tree and query the
 +// constraint values for the sub-trees and if a value is a constant we do the
 +// constant folding. Compound symbols might collapse to simpler symbol tree
 +// that is still possible to further simplify. Thus, we do the simplification on
 +// a new symbol tree until we reach the simplest form, i.e. the fixpoint.
 +//
 +// Consider the following symbol `(b * b) * b * b` which has this tree:
 +//       *
 +//      / \
 +//     *   b
 +//    /  \
 +//   /    b
 +// (b * b)
 +// Now, if the `b * b == 1` new constraint is added then during the first
 +// iteration we have the following transformations:
 +//       *                  *
 +//      / \                / \
 +//     *   b     -->      b   b
 +//    /  \
 +//   /    b
 +//  1
 +// We need another iteration to reach the final result `1`.
 +LLVM_NODISCARD
 +static SVal simplifyUntilFixpoint(SValBuilder &SVB, ProgramStateRef State,
 +                                  const SymbolRef Sym) {
 +  SVal Val = SVB.makeSymbolVal(Sym);
 +  SVal SimplifiedVal = SVB.simplifySVal(State, Val);
 +  // Do the simplification until we can.
 +  while (SimplifiedVal != Val) {
 +    Val = SimplifiedVal;
 +    SimplifiedVal = SVB.simplifySVal(State, Val);
 +  }
 +  return SimplifiedVal;
 +}
 +
  // Iterate over all symbols and try to simplify them. Once a symbol is
  // simplified then we check if we can merge the simplified symbol's equivalence
  // class to this class. This way, we simplify not just the symbols but the
 @@ -2170,7 +2238,8 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
    SymbolSet ClassMembers = Class.getClassMembers(State);
    for (const SymbolRef &MemberSym : ClassMembers) {

 -    const SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym);
 +    const SVal SimplifiedMemberVal =
 +        simplifyUntilFixpoint(SVB, State, MemberSym);
      const SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();

      // The symbol is collapsed to a constant, check if the current State is
 @@ -2196,6 +2265,8 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
          continue;

        assert(find(State, MemberSym) == find(State, SimplifiedMemberSym));
 +      // Remove the old and more complex symbol.
 +      State = find(State, MemberSym).removeMember(State, MemberSym);

        // Query the class constraint again b/c that may have changed during the
        // merge above.
 @@ -2207,25 +2278,19 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
        // About performance and complexity: Let us assume that in a State we
        // have N non-trivial equivalence classes and that all constraints and
        // disequality info is related to non-trivial classes. In the worst case,
 -      // we can simplify only one symbol of one class in each iteration.
 +      // we can simplify only one symbol of one class in each iteration. The
 +      // number of symbols in one class cannot grow b/c we replace the old
 +      // symbol with the simplified one. Also, the number of the equivalence
 +      // classes can decrease only, b/c the algorithm does a merge operation
 +      // optionally. We need N iterations in this case to reach the fixpoint.
 +      // Thus, the steps needed to be done in the worst case is proportional to
 +      // N*N.
        //
 -      // The number of the equivalence classes can decrease only, because the
 -      // algorithm does a merge operation optionally.
 -      // ASSUMPTION G: Let us assume that the
 -      // number of symbols in one class cannot grow because we replace the old
 -      // symbol with the simplified one.
 -      // If assumption G holds then we need N iterations in this case to reach
 -      // the fixpoint. Thus, the steps needed to be done in the worst case is
 -      // proportional to N*N.
        // This worst case scenario can be extended to that case when we have
        // trivial classes in the constraints and in the disequality map. This
        // case can be reduced to the case with a State where there are only
        // non-trivial classes. This is because a merge operation on two trivial
        // classes results in one non-trivial class.
 -      //
 -      // Empirical measurements show that if we relax assumption G (i.e. if we
 -      // do not replace the complex symbol just add the simplified one) then
 -      // the runtime and memory consumption does not grow noticeably.
        State = reAssume(State, ClassConstraint, SimplifiedMemberVal);
        if (!State)
          return nullptr;
 diff --git a/clang/test/Analysis/expr-inspection-printState-eq-classes.c b/clang/test/Analysis/expr-inspection-printState-eq-classes.c
 index c56fcd627b0a..08a1c6cbd60b 100644
 --- a/clang/test/Analysis/expr-inspection-printState-eq-classes.c
 +++ b/clang/test/Analysis/expr-inspection-printState-eq-classes.c
 @@ -16,6 +16,6 @@ void test_equivalence_classes(int a, int b, int c, int d) {
  }

  // CHECK:      "equivalence_classes": [
 -// CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ],
 -// CHECK-NEXT:   [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$0<int a>", "reg_$2<int c>", "reg_$3<int d>" ]
 +// CHECK-NEXT:     [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
 +// CHECK-NEXT:     [ "reg_$0<int a>", "reg_$2<int c>", "reg_$3<int d>" ]
  // CHECK-NEXT: ],
 diff --git a/clang/test/Analysis/symbol-simplification-disequality-info.cpp b/clang/test/Analysis/symbol-simplification-disequality-info.cpp
 index 45d8c05bcfc5..69238b583eb8 100644
 --- a/clang/test/Analysis/symbol-simplification-disequality-info.cpp
 +++ b/clang/test/Analysis/symbol-simplification-disequality-info.cpp
 @@ -12,18 +12,18 @@ void test(int a, int b, int c, int d) {
    if (a + b + c == d)
      return;
    clang_analyzer_printState();
 -  // CHECK:      "disequality_info": [
 -  // CHECK-NEXT:   {
 -  // CHECK-NEXT:     "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ],
 -  // CHECK-NEXT:     "disequal_to": [
 -  // CHECK-NEXT:       [ "reg_$3<int d>" ]]
 -  // CHECK-NEXT:   },
 -  // CHECK-NEXT:   {
 -  // CHECK-NEXT:     "class": [ "reg_$3<int d>" ],
 -  // CHECK-NEXT:     "disequal_to": [
 -  // CHECK-NEXT:       [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ]]
 -  // CHECK-NEXT:   }
 -  // CHECK-NEXT: ],
 +  // CHECK:       "disequality_info": [
 +  // CHECK-NEXT:    {
 +  // CHECK-NEXT:      "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ],
 +  // CHECK-NEXT:      "disequal_to": [
 +  // CHECK-NEXT:        [ "reg_$3<int d>" ]]
 +  // CHECK-NEXT:    },
 +  // CHECK-NEXT:    {
 +  // CHECK-NEXT:      "class": [ "reg_$3<int d>" ],
 +  // CHECK-NEXT:      "disequal_to": [
 +  // CHECK-NEXT:        [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ]]
 +  // CHECK-NEXT:    }
 +  // CHECK-NEXT:  ],


    // Simplification starts here.
 @@ -32,33 +32,32 @@ void test(int a, int b, int c, int d) {
    clang_analyzer_printState();
    // CHECK:      "disequality_info": [
    // CHECK-NEXT:   {
 -  // CHECK-NEXT:     "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)" ],
 +  // CHECK-NEXT:     "class": [ "(reg_$0<int a>) + (reg_$2<int c>)" ],
    // CHECK-NEXT:     "disequal_to": [
    // CHECK-NEXT:       [ "reg_$3<int d>" ]]
    // CHECK-NEXT:   },
    // CHECK-NEXT:   {
    // CHECK-NEXT:     "class": [ "reg_$3<int d>" ],
    // CHECK-NEXT:     "disequal_to": [
 -  // CHECK-NEXT:       [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)" ]]
 -  // CHECK-NEXT:   }
 -  // CHECK-NEXT: ],
 +  // CHECK-NEXT:        [ "(reg_$0<int a>) + (reg_$2<int c>)" ]]
 +  // CHECK-NEXT:    }
 +  // CHECK-NEXT:  ],

    if (c != 0)
      return;
    clang_analyzer_printState();
 -
 -  // CHECK:      "disequality_info": [
 -  // CHECK-NEXT:   {
 -  // CHECK-NEXT:     "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>" ],
 -  // CHECK-NEXT:     "disequal_to": [
 -  // CHECK-NEXT:       [ "reg_$3<int d>" ]]
 -  // CHECK-NEXT:   },
 -  // CHECK-NEXT:   {
 -  // CHECK-NEXT:     "class": [ "reg_$3<int d>" ],
 -  // CHECK-NEXT:     "disequal_to": [
 -  // CHECK-NEXT:       [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>" ]]
 -  // CHECK-NEXT:   }
 -  // CHECK-NEXT: ],
 +  // CHECK:       "disequality_info": [
 +  // CHECK-NEXT:    {
 +  // CHECK-NEXT:      "class": [ "reg_$0<int a>" ],
 +  // CHECK-NEXT:      "disequal_to": [
 +  // CHECK-NEXT:        [ "reg_$3<int d>" ]]
 +  // CHECK-NEXT:    },
 +  // CHECK-NEXT:    {
 +  // CHECK-NEXT:      "class": [ "reg_$3<int d>" ],
 +  // CHECK-NEXT:      "disequal_to": [
 +  // CHECK-NEXT:        [ "reg_$0<int a>" ]]
 +  // CHECK-NEXT:    }
 +  // CHECK-NEXT:  ],

    // Keep the symbols and the constraints! alive.
    (void)(a * b * c * d);
 diff --git a/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp b/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
 index aec0da1b82f1..73922d420a8c 100644
 --- a/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
 +++ b/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
 @@ -24,15 +24,14 @@ void test(int a, int b, int c) {
    if (b != 0)
      return;
    clang_analyzer_printState();
 -  // CHECK:      "constraints": [
 -  // CHECK-NEXT:   { "symbol": "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
 -  // CHECK-NEXT: ],
 -  // CHECK-NEXT: "equivalence_classes": [
 -  // CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ],
 -  // CHECK-NEXT:   [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$0<int a>", "reg_$2<int c>" ]
 -  // CHECK-NEXT: ],
 +  // CHECK:        "constraints": [
 +  // CHECK-NEXT:     { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
 +  // CHECK-NEXT:     { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
 +  // CHECK-NEXT:   ],
 +  // CHECK-NEXT:   "equivalence_classes": [
 +  // CHECK-NEXT:     [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
 +  // CHECK-NEXT:     [ "reg_$0<int a>", "reg_$2<int c>" ]
 +  // CHECK-NEXT:   ],
    // CHECK-NEXT: "disequality_info": null,

    // Keep the symbols and the constraints! alive.
 diff --git a/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp b/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
 index f1b057be3abd..679ed3fda7a7 100644
 --- a/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
 +++ b/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
 @@ -27,20 +27,17 @@ void test(int a, int b, int c, int d) {
    if (b != 0)
      return;
    clang_analyzer_printState();
 -  // CHECK:      "constraints": [
 -  // CHECK-NEXT:   { "symbol": "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "(reg_$2<int c>) + (reg_$1<int b>)", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
 -  // CHECK-NEXT:   { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
 -  // CHECK-NEXT: ],
 -  // CHECK-NEXT: "equivalence_classes": [
 -  // CHECK-NEXT:   [ "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "(reg_$0<int a>) != (reg_$3<int d>)" ],
 -  // CHECK-NEXT:   [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>", "reg_$3<int d>" ],
 -  // CHECK-NEXT:   [ "(reg_$2<int c>) + (reg_$1<int b>)", "reg_$2<int c>" ]
 -  // CHECK-NEXT: ],
 -  // CHECK-NEXT: "disequality_info": null,
 +  // CHECK:       "constraints": [
 +  // CHECK-NEXT:    { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
 +  // CHECK-NEXT:    { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
 +  // CHECK-NEXT:    { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
 +  // CHECK-NEXT:  ],
 +  // CHECK-NEXT:  "equivalence_classes": [
 +  // CHECK-NEXT:    [ "(reg_$0<int a>) != (reg_$3<int d>)" ],
 +  // CHECK-NEXT:    [ "reg_$0<int a>", "reg_$3<int d>" ],
 +  // CHECK-NEXT:    [ "reg_$2<int c>" ]
 +  // CHECK-NEXT:  ],
 +  // CHECK-NEXT:  "disequality_info": null,

    // Keep the symbols and the constraints! alive.
    (void)(a * b * c * d);
 --
 2.35.0.rc0.227.g00780c9af4-goog
	From 16ae0cfa1e8e07e17fdc7ad93e544a828d933072 Mon Sep 17 00:00:00 2001
	From: Gabor Marton <gabor.marton@ericsson.com>
	Date: Wed, 1 Dec 2021 16:47:22 +0100
	Subject: [PATCH] [Analyzer][solver] Simplification: Do a fixpoint iteration
	before the eq class merge

	This reverts commit f02c5f3478318075d1a469203900e452ba651421 and
	addresses the issue mentioned in D114619 differently.

	Repeating the issue here:
	Currently, during symbol simplification we remove the original member
	symbol from the equivalence class (`ClassMembers` trait). However, we
	keep the reverse link (`ClassMap` trait), in order to be able the query
	the related constraints even for the old member. This asymmetry can lead
	to a problem when we merge equivalence classes:
	```
	ClassA: [a, b] // ClassMembers trait,
	a->a, b->a // ClassMap trait, a is the representative symbol
	```
	Now let,s delete `a`:
	```
	ClassA: [b]
	a->a, b->a
	```
	Let's merge ClassA into the trivial class `c`:
	```
	ClassA: [c, b]
	c->c, b->c, a->a
	```
	Now, after the merge operation, `c` and `a` are actually in different
	equivalence classes, which is inconsistent.

	This issue manifests in a test case (added in D103317):
	```
	void recurring_symbol(int b) {
	if (b * b != b)
	if ((b * b) * b * b != (b * b) * b)
	if (b * b == 1)
	}
	```
	Before the simplification we have these equivalence classes:
	```
	trivial EQ1: [b * b != b]
	trivial EQ2: [(b * b) * b * b != (b * b) * b]
	```

	During the simplification with `b * b == 1`, EQ1 is merged with `1 != b`
	`EQ1: [b * b != b, 1 != b]` and we remove the complex symbol, so
	`EQ1: [1 != b]`
	Then we start to simplify the only symbol in EQ2:
	`(b * b) * b * b != (b * b) * b --> 1 * b * b != 1 * b --> b * b != b`
	But `b * b != b` is such a symbol that had been removed previously from
	EQ1, thus we reach the above mentioned inconsistency.

	This patch addresses the issue by making it impossible to synthesise a
	symbol that had been simplified before. We achieve this by simplifying
	the given symbol to the absolute simplest form.

	Differential Revision: https://reviews.llvm.org/D114887
	---
	.../Core/RangeConstraintManager.cpp \| 93 ++++++++++++++++---
	.../expr-inspection-printState-eq-classes.c \| 4 +-
	...symbol-simplification-disequality-info.cpp \| 57 ++++++------
	...-simplification-fixpoint-one-iteration.cpp \| 17 ++--
	...simplification-fixpoint-two-iterations.cpp \| 25 +++--
	5 files changed, 128 insertions(+), 68 deletions(-)

	diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
	index 3f8d9e4298a0..23c67c64f975 100644
	--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
	+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
	@@ -601,6 +601,10 @@ public:
	LLVM_NODISCARD static inline Optional<bool>
	areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);

	+ /// Remove one member from the class.
	+ LLVM_NODISCARD ProgramStateRef removeMember(ProgramStateRef State,
	+ const SymbolRef Old);
	+
	/// Iterate over all symbols and try to simplify them.
	LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB,
	RangeSet::Factory &F,
	@@ -2132,6 +2136,34 @@ inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
	return llvm::None;
	}

	+LLVM_NODISCARD ProgramStateRef
	+EquivalenceClass::removeMember(ProgramStateRef State, const SymbolRef Old) {
	+
	+ SymbolSet ClsMembers = getClassMembers(State);
	+ assert(ClsMembers.contains(Old));
	+
	+ // We don't remove `Old`'s Sym->Class relation for two reasons:
	+ // 1) This way constraints for the old symbol can still be found via it's
	+ // equivalence class that it used to be the member of.
	+ // 2) Performance and resource reasons. We can spare one removal and thus one
	+ // additional tree in the forest of `ClassMap`.
	+
	+ // Remove `Old`'s Class->Sym relation.
	+ SymbolSet::Factory &F = getMembersFactory(State);
	+ ClassMembersTy::Factory &EMFactory = State->get_context<ClassMembers>();
	+ ClsMembers = F.remove(ClsMembers, Old);
	+ // Ensure another precondition of the removeMember function (we can check
	+ // this only with isEmpty, thus we have to do the remove first).
	+ assert(!ClsMembers.isEmpty() &&
	+ "Class should have had at least two members before member removal");
	+ // Overwrite the existing members assigned to this class.
	+ ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
	+ ClassMembersMap = EMFactory.add(ClassMembersMap, *this, ClsMembers);
	+ State = State->set<ClassMembers>(ClassMembersMap);
	+
	+ return State;
	+}
	+
	// Re-evaluate an SVal with top-level `State->assume` logic.
	LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
	const RangeSet *Constraint,
	@@ -2159,6 +2191,42 @@ LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
	Constraint->getMaxValue(), true);
	}

	+// Simplify the given symbol with the help of the SValBuilder. In
	+// SValBuilder::symplifySval, we traverse the symbol tree and query the
	+// constraint values for the sub-trees and if a value is a constant we do the
	+// constant folding. Compound symbols might collapse to simpler symbol tree
	+// that is still possible to further simplify. Thus, we do the simplification on
	+// a new symbol tree until we reach the simplest form, i.e. the fixpoint.
	+//
	+// Consider the following symbol `(b * b) * b * b` which has this tree:
	+// *
	+// / \
	+// * b
	+// / \
	+// / b
	+// (b * b)
	+// Now, if the `b * b == 1` new constraint is added then during the first
	+// iteration we have the following transformations:
	+// * *
	+// / \ / \
	+// * b --> b b
	+// / \
	+// / b
	+// 1
	+// We need another iteration to reach the final result `1`.
	+LLVM_NODISCARD
	+static SVal simplifyUntilFixpoint(SValBuilder &SVB, ProgramStateRef State,
	+ const SymbolRef Sym) {
	+ SVal Val = SVB.makeSymbolVal(Sym);
	+ SVal SimplifiedVal = SVB.simplifySVal(State, Val);
	+ // Do the simplification until we can.
	+ while (SimplifiedVal != Val) {
	+ Val = SimplifiedVal;
	+ SimplifiedVal = SVB.simplifySVal(State, Val);
	+ }
	+ return SimplifiedVal;
	+}
	+
	// Iterate over all symbols and try to simplify them. Once a symbol is
	// simplified then we check if we can merge the simplified symbol's equivalence
	// class to this class. This way, we simplify not just the symbols but the
	@@ -2170,7 +2238,8 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
	SymbolSet ClassMembers = Class.getClassMembers(State);
	for (const SymbolRef &MemberSym : ClassMembers) {

	- const SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym);
	+ const SVal SimplifiedMemberVal =
	+ simplifyUntilFixpoint(SVB, State, MemberSym);
	const SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();

	// The symbol is collapsed to a constant, check if the current State is
	@@ -2196,6 +2265,8 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
	continue;

	assert(find(State, MemberSym) == find(State, SimplifiedMemberSym));
	+ // Remove the old and more complex symbol.
	+ State = find(State, MemberSym).removeMember(State, MemberSym);

	// Query the class constraint again b/c that may have changed during the
	// merge above.
	@@ -2207,25 +2278,19 @@ EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
	// About performance and complexity: Let us assume that in a State we
	// have N non-trivial equivalence classes and that all constraints and
	// disequality info is related to non-trivial classes. In the worst case,
	- // we can simplify only one symbol of one class in each iteration.
	+ // we can simplify only one symbol of one class in each iteration. The
	+ // number of symbols in one class cannot grow b/c we replace the old
	+ // symbol with the simplified one. Also, the number of the equivalence
	+ // classes can decrease only, b/c the algorithm does a merge operation
	+ // optionally. We need N iterations in this case to reach the fixpoint.
	+ // Thus, the steps needed to be done in the worst case is proportional to
	+ // N*N.
	//
	- // The number of the equivalence classes can decrease only, because the
	- // algorithm does a merge operation optionally.
	- // ASSUMPTION G: Let us assume that the
	- // number of symbols in one class cannot grow because we replace the old
	- // symbol with the simplified one.
	- // If assumption G holds then we need N iterations in this case to reach
	- // the fixpoint. Thus, the steps needed to be done in the worst case is
	- // proportional to N*N.
	// This worst case scenario can be extended to that case when we have
	// trivial classes in the constraints and in the disequality map. This
	// case can be reduced to the case with a State where there are only
	// non-trivial classes. This is because a merge operation on two trivial
	// classes results in one non-trivial class.
	- //
	- // Empirical measurements show that if we relax assumption G (i.e. if we
	- // do not replace the complex symbol just add the simplified one) then
	- // the runtime and memory consumption does not grow noticeably.
	State = reAssume(State, ClassConstraint, SimplifiedMemberVal);
	if (!State)
	return nullptr;
	diff --git a/clang/test/Analysis/expr-inspection-printState-eq-classes.c b/clang/test/Analysis/expr-inspection-printState-eq-classes.c
	index c56fcd627b0a..08a1c6cbd60b 100644
	--- a/clang/test/Analysis/expr-inspection-printState-eq-classes.c
	+++ b/clang/test/Analysis/expr-inspection-printState-eq-classes.c
	@@ -16,6 +16,6 @@ void test_equivalence_classes(int a, int b, int c, int d) {
	}

	// CHECK: "equivalence_classes": [
	-// CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ],
	-// CHECK-NEXT: [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$0<int a>", "reg_$2<int c>", "reg_$3<int d>" ]
	+// CHECK-NEXT: [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
	+// CHECK-NEXT: [ "reg_$0<int a>", "reg_$2<int c>", "reg_$3<int d>" ]
	// CHECK-NEXT: ],
	diff --git a/clang/test/Analysis/symbol-simplification-disequality-info.cpp b/clang/test/Analysis/symbol-simplification-disequality-info.cpp
	index 45d8c05bcfc5..69238b583eb8 100644
	--- a/clang/test/Analysis/symbol-simplification-disequality-info.cpp
	+++ b/clang/test/Analysis/symbol-simplification-disequality-info.cpp
	@@ -12,18 +12,18 @@ void test(int a, int b, int c, int d) {
	if (a + b + c == d)
	return;
	clang_analyzer_printState();
	- // CHECK: "disequality_info": [
	- // CHECK-NEXT: {
	- // CHECK-NEXT: "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ],
	- // CHECK-NEXT: "disequal_to": [
	- // CHECK-NEXT: [ "reg_$3<int d>" ]]
	- // CHECK-NEXT: },
	- // CHECK-NEXT: {
	- // CHECK-NEXT: "class": [ "reg_$3<int d>" ],
	- // CHECK-NEXT: "disequal_to": [
	- // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ]]
	- // CHECK-NEXT: }
	- // CHECK-NEXT: ],
	+ // CHECK: "disequality_info": [
	+ // CHECK-NEXT: {
	+ // CHECK-NEXT: "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ],
	+ // CHECK-NEXT: "disequal_to": [
	+ // CHECK-NEXT: [ "reg_$3<int d>" ]]
	+ // CHECK-NEXT: },
	+ // CHECK-NEXT: {
	+ // CHECK-NEXT: "class": [ "reg_$3<int d>" ],
	+ // CHECK-NEXT: "disequal_to": [
	+ // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)" ]]
	+ // CHECK-NEXT: }
	+ // CHECK-NEXT: ],


	// Simplification starts here.
	@@ -32,33 +32,32 @@ void test(int a, int b, int c, int d) {
	clang_analyzer_printState();
	// CHECK: "disequality_info": [
	// CHECK-NEXT: {
	- // CHECK-NEXT: "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)" ],
	+ // CHECK-NEXT: "class": [ "(reg_$0<int a>) + (reg_$2<int c>)" ],
	// CHECK-NEXT: "disequal_to": [
	// CHECK-NEXT: [ "reg_$3<int d>" ]]
	// CHECK-NEXT: },
	// CHECK-NEXT: {
	// CHECK-NEXT: "class": [ "reg_$3<int d>" ],
	// CHECK-NEXT: "disequal_to": [
	- // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)" ]]
	- // CHECK-NEXT: }
	- // CHECK-NEXT: ],
	+ // CHECK-NEXT: [ "(reg_$0<int a>) + (reg_$2<int c>)" ]]
	+ // CHECK-NEXT: }
	+ // CHECK-NEXT: ],

	if (c != 0)
	return;
	clang_analyzer_printState();
	-
	- // CHECK: "disequality_info": [
	- // CHECK-NEXT: {
	- // CHECK-NEXT: "class": [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>" ],
	- // CHECK-NEXT: "disequal_to": [
	- // CHECK-NEXT: [ "reg_$3<int d>" ]]
	- // CHECK-NEXT: },
	- // CHECK-NEXT: {
	- // CHECK-NEXT: "class": [ "reg_$3<int d>" ],
	- // CHECK-NEXT: "disequal_to": [
	- // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>" ]]
	- // CHECK-NEXT: }
	- // CHECK-NEXT: ],
	+ // CHECK: "disequality_info": [
	+ // CHECK-NEXT: {
	+ // CHECK-NEXT: "class": [ "reg_$0<int a>" ],
	+ // CHECK-NEXT: "disequal_to": [
	+ // CHECK-NEXT: [ "reg_$3<int d>" ]]
	+ // CHECK-NEXT: },
	+ // CHECK-NEXT: {
	+ // CHECK-NEXT: "class": [ "reg_$3<int d>" ],
	+ // CHECK-NEXT: "disequal_to": [
	+ // CHECK-NEXT: [ "reg_$0<int a>" ]]
	+ // CHECK-NEXT: }
	+ // CHECK-NEXT: ],

	// Keep the symbols and the constraints! alive.
	(void)(a * b * c * d);
	diff --git a/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp b/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
	index aec0da1b82f1..73922d420a8c 100644
	--- a/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
	+++ b/clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
	@@ -24,15 +24,14 @@ void test(int a, int b, int c) {
	if (b != 0)
	return;
	clang_analyzer_printState();
	- // CHECK: "constraints": [
	- // CHECK-NEXT: { "symbol": "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
	- // CHECK-NEXT: ],
	- // CHECK-NEXT: "equivalence_classes": [
	- // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "(reg_$0<int a>) != (reg_$2<int c>)" ],
	- // CHECK-NEXT: [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$0<int a>", "reg_$2<int c>" ]
	- // CHECK-NEXT: ],
	+ // CHECK: "constraints": [
	+ // CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
	+ // CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
	+ // CHECK-NEXT: ],
	+ // CHECK-NEXT: "equivalence_classes": [
	+ // CHECK-NEXT: [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
	+ // CHECK-NEXT: [ "reg_$0<int a>", "reg_$2<int c>" ]
	+ // CHECK-NEXT: ],
	// CHECK-NEXT: "disequality_info": null,

	// Keep the symbols and the constraints! alive.
	diff --git a/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp b/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
	index f1b057be3abd..679ed3fda7a7 100644
	--- a/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
	+++ b/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp
	@@ -27,20 +27,17 @@ void test(int a, int b, int c, int d) {
	if (b != 0)
	return;
	clang_analyzer_printState();
	- // CHECK: "constraints": [
	- // CHECK-NEXT: { "symbol": "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "(reg_$2<int c>) + (reg_$1<int b>)", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
	- // CHECK-NEXT: { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
	- // CHECK-NEXT: ],
	- // CHECK-NEXT: "equivalence_classes": [
	- // CHECK-NEXT: [ "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "(reg_$0<int a>) != (reg_$3<int d>)" ],
	- // CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>", "reg_$3<int d>" ],
	- // CHECK-NEXT: [ "(reg_$2<int c>) + (reg_$1<int b>)", "reg_$2<int c>" ]
	- // CHECK-NEXT: ],
	- // CHECK-NEXT: "disequality_info": null,
	+ // CHECK: "constraints": [
	+ // CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
	+ // CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
	+ // CHECK-NEXT: { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
	+ // CHECK-NEXT: ],
	+ // CHECK-NEXT: "equivalence_classes": [
	+ // CHECK-NEXT: [ "(reg_$0<int a>) != (reg_$3<int d>)" ],
	+ // CHECK-NEXT: [ "reg_$0<int a>", "reg_$3<int d>" ],
	+ // CHECK-NEXT: [ "reg_$2<int c>" ]
	+ // CHECK-NEXT: ],
	+ // CHECK-NEXT: "disequality_info": null,

	// Keep the symbols and the constraints! alive.
	(void)(a * b * c * d);
	--
	2.35.0.rc0.227.g00780c9af4-goog