Page MenuHomePhabricator

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

Authored by martong on Nov 26 2021, 2:14 AM.



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.

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.

Diff Detail

Event Timeline

martong created this revision.Nov 26 2021, 2:14 AM
martong requested review of this revision.Nov 26 2021, 2:14 AM
Herald added a project: Restricted Project. · View Herald TranscriptNov 26 2021, 2:14 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript

I see. Simplification is always good. Let's measure and compare the runtime characteristics before moving forward.


Emphasize what you mean by relaxation. You meant probably something like not replacing the complex symbol, just adding the simplified version to the class.


nor memory consumption


Could you please elaborate on this in the review? I don't get the reasoning. I might miss something.


Please try to omit unnecessary changes.

martong updated this revision to Diff 390349.Nov 29 2021, 7:21 AM
martong marked 4 inline comments as done.
  • Update a comment





It's not a reasoning, just a guessing. Another reason could be that simply the time we spend here is negligible compared to the time we spend e.g. in removeDeadBindings. (Actually, removeDeadBindings is very hot and takes roughly 15-20 % of the runtime.) Perhaps I could do a measurement with a sampling profiler to be able to provide a precise explanation to this. But I think the point is that the runtime/memory consumption do not grow and the concrete reason is secondary.

However, you are right, I should not get into guessing here, I'll just remove this sentence.


I've made this change intentionally, so all hunks for each simplification steps are indented similarly. E.g., after the CHECK-NEXT: string comes 3 space characters until we the { character, see L16 and L34 and L51. Actually, I've made an indentation error in a previous patch, which I though I can correct now.

I see. Simplification is always good. Let's measure and compare the runtime characteristics before moving forward.

Here they are. Seems like the runtime and memory consumption are pretty much the same.

steakhal accepted this revision.Nov 29 2021, 9:04 AM

I think it looks great.


Fine by me.

This revision is now accepted and ready to land.Nov 29 2021, 9:04 AM

The test sometimes fails flakily:

Thanks @thakis for the report, I am aware of the issue and addressing that in

@thakis, if the issue is really disturbing and cannot wait until the review of D114887 finishes then please do a revert of this patch. But then the dependent child patch D103317 needs to be reverted as well.
I am trying my best to make D114887 reviewed in the next 24 hours.

I've had the confidence to commit D114887, the test should not be flaky anymore.

thakis added a comment.Dec 1 2021, 5:00 PM

Thanks for the fix!