Page MenuHomePhabricator

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

Authored by martong on Dec 1 2021, 9:12 AM.

Details

Summary

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.

Diff Detail

Event Timeline

martong created this revision.Dec 1 2021, 9:12 AM
martong requested review of this revision.Dec 1 2021, 9:12 AM
Herald added a project: Restricted Project. · View Herald TranscriptDec 1 2021, 9:12 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
martong added inline comments.Dec 1 2021, 12:16 PM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2218

Perhaps this should be done in SimpleSValbuilder::simplifySVal, I think this should be the responsibility of the SValBuilder compoment.

I am attaching the performance measurement results:

There is no any noticeable difference.

I am going to commit this as is because there is a push to revert D114619 (because of a flaky test) and this commit does that. On the other hand this is not a pure revert, so I apologize for the reviewers. If we were to purely revert D114619 then we'd have to revert its dependent child patch as well.

I have a strong confidence in this patch since I had a verbal discussion about this with @steakhal and he verified the basic idea. I am going to address my comment about simplifyUntilFixpoint in a follow-up patch.

This revision was not accepted when it landed; it landed in state Needs Review.Dec 1 2021, 1:23 PM
This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.

I think I'm in favor of this change. However, Im also slightly in favor of reverting stuff instead of rushing things. Let's hope it will resolve the issue of the previous offending commit.

Accepted.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2218

My thought was the same.

2220

Couldnt we just create an SVal from a SymExpr? Why do we need the SVB foe this?

2222

Nit: It doesnt seem to be grammatically correct.

Also, please provide the coverage of the new test case (only excercising the new test case not the whole test file) I really want to make sure that it will cover the loop as it supposed to.

Oh, I just now see that there is no test. Now I'm really courious.

Also, please provide the coverage of the new test case (only excercising the new test case not the whole test file) I really want to make sure that it will cover the loop as it supposed to.

Oh, I just now see that there is no test. Now I'm really courious.

There is a test case in D103317 (with the so many bs) which covers the loop. That patch is the dependent patch of the reverted patch.

Also, please provide the coverage of the new test case (only excercising the new test case not the whole test file) I really want to make sure that it will cover the loop as it supposed to.

Oh, I just now see that there is no test. Now I'm really courious.

There is a test case in D103317 (with the so many bs) which covers the loop. That patch is the dependent patch of the reverted patch.

I'm still curious to see which lines are covered by tests.
Pragmatically, this patch changes some behavior, thus we need to know what lines become uncovered due to this change.
I suspect it won't change much, but better be on the safe side.