[PATCH] D114887: [Analyzer][solver] Simplification: Do a fixpoint iteration before the eq class merge

[Gabor Marton via Phabricator via cfe-commits]

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

This reverts commit f02c5f3478318075d1a469203900e452ba651421 <https://reviews.llvm.org/rGf02c5f3478318075d1a469203900e452ba651421> and
addresses the issue mentioned in D114619 <https://reviews.llvm.org/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 <https://reviews.llvm.org/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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D114887

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D114887.391057.patch
Type: text/x-patch
Size: 14673 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20211201/82d76e25/attachment-0001.bin>