[all-commits] [llvm/llvm-project] 20f873: [Analyzer][solver] Simplification: Do a fixpoint i...

[Gabor Marton via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 20f8733d4b8d5bdb93080b8824de57b7fae31785
      https://github.com/llvm/llvm-project/commit/20f8733d4b8d5bdb93080b8824de57b7fae31785
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2021-12-01 (Wed, 01 Dec 2021)

  Changed paths:
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    M clang/test/Analysis/expr-inspection-printState-eq-classes.c
    M clang/test/Analysis/symbol-simplification-disequality-info.cpp
    M clang/test/Analysis/symbol-simplification-fixpoint-one-iteration.cpp
    M clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

  Log Message:
  -----------
  [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