This is an archive of the discontinued LLVM Phabricator instance.

[Analyzer][solver] Add dump methods for (dis)equality classes.
ClosedPublic

Authored by martong on Jun 9 2021, 8:06 AM.

Diff Detail

Event Timeline

martong created this revision.Jun 9 2021, 8:06 AM
martong requested review of this revision.Jun 9 2021, 8:06 AM
Herald added a project: Restricted Project. · View Herald TranscriptJun 9 2021, 8:06 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
martong updated this revision to Diff 350905.Jun 9 2021, 8:09 AM
  • Change comment

This is definitely useful! Thanks!
I was just wondering if we should add it into the state printer instead. @NoQ what's your take on this?

NoQ added a comment.Jun 9 2021, 8:59 PM

Yes we should definitely have as much as possible in the state dump.

martong updated this revision to Diff 352464.Jun 16 2021, 9:32 AM
  • Extend printJson to handle equivalency info

Yes we should definitely have as much as possible in the state dump.

Okay, I've updated likewise and added two test files to check them in State->dump.

I suspect that the exploded-graph-rewriter should be updated as well so that the HTML dumps also carry this information.

I suspect that the exploded-graph-rewriter should be updated as well so that the HTML dumps also carry this information.

I've put that into a separate patch because that change has its own complexity. Plus, I think this patch is meaningful and useful by itself (without the exploded-graph-rewriter changes).
https://reviews.llvm.org/D104917

vsavchenko accepted this revision.Jun 25 2021, 7:38 AM

Awesome, thanks!

This revision is now accepted and ready to land.Jun 25 2021, 7:38 AM
thakis added a subscriber: thakis.Jun 28 2021, 5:16 AM

This breaks tests on Windows: http://45.33.8.238/win/40864/step_7.txt

Please take a look, and please revert if it takes a while to fix.

Thanks for the report @thakis ! This seems to be b/c of the different newline handling in windows. I've committed a change that disables the tests on windows.

Thanks. Looks like it flakily fails on mac too every now and then: http://45.33.8.238/mac/33005/step_7.txt

Maybe you print something in nondeterministic iteration order?

Thanks. Looks like it flakily fails on mac too every now and then: http://45.33.8.238/mac/33005/step_7.txt

Maybe you print something in nondeterministic iteration order?

Yes, I think that the problem is deeper. ClassMembers is llvm::ImmutableSet (i.e. sorted set), and it uses SymbolRef (e.g. pointer values) for sorting. So, it does look like the order can be nondeterministic.
However, when we print constraints, we should see similar problems, but we don't 🤔

Cool, can we revert this for now then? Flakily failing on my m1 bot too: http://45.33.8.238/macm1/12514/step_7.txt

(here's another flaky failure that was due to this: http://45.33.8.238/mac/33008/step_7.txt )

martong reopened this revision.Jul 5 2021, 7:19 AM

I have changed the dump methods to order the equivalence classes and the disequality info available before printing them out. The ordering is done based on their string representation. This comes necessarily with some performance penalty, though otherwise it is impossible (or practically way too cumbersome) to write deterministic tests. Also, the dump is used either from the debugger or from small test cases or when we create an exploded graph (which is again intended to be used during debugging), so I think that the penalty induced by the sorting won't be an issue.

This revision is now accepted and ready to land.Jul 5 2021, 7:19 AM
martong updated this revision to Diff 356502.Jul 5 2021, 7:20 AM
  • Change the dump methods to order the equivalence classes and the disequality info available before printing them out
martong added inline comments.Jul 5 2021, 7:31 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2537

Ah, SmallSet is not sorted :( I am gonna have to change this to either std::set or to a sorted vector :(

martong updated this revision to Diff 356504.Jul 5 2021, 7:38 AM
  • Use std::set for ordering

AFAICT this patch does not introduce significant overhead to the exploded graph DOT dumps.
Before the patch, an exploded graph took 12G and about 55 secs for a single top-level function.
After the patch, it increased to 13G, and the runtime remained the same as expected.

Which is about a 1.5 % increase in size in total. TBH I expected slightly higher numbers.

This benchmark was done using a release build with dumps, asserts, and expensive checks.

AFAICT this patch does not introduce significant overhead to the exploded graph DOT dumps.
Before the patch, an exploded graph took 12G and about 55 secs for a single top-level function.
After the patch, it increased to 13G, and the runtime remained the same as expected.

Which is about a 1.5 % increase in size in total. TBH I expected slightly higher numbers.

This benchmark was done using a release build with dumps, asserts, and expensive checks.

Thanks Balázs for the benchmark, this makes me confident to commit. Hopefully this time the tests won't be flaky.