[PATCH] D114619: [Analyzer][solver] Do not remove the simplified symbol from the eq class

[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.

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 lets delete `a`:

  ClassA: [b]
  a->a, b->a

Let's merge the trivial class `c` into ClassA:

  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.

One solution to this problem is to simply avoid removing the original
member and this is what this patch does.

Other options I have considered:

1. Always merge the trivial class into the non-trivial class. This might work most of the time, however, will fail if we have to merge two non-trivial classes (in that case we no longer can track equivalences precisely).
2. In `removeMember`, update the reverse link as well. This would cease the inconsistency, but we'd loose precision since we could not query the constraints for the removed member.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D114619

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: D114619.389955.patch
Type: text/x-patch
Size: 12575 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20211126/1c7bafb8/attachment.bin>