[PATCH] D82445: [analyzer][solver] Track symbol equivalence

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko marked 4 inline comments as done.
vsavchenko added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:452
+  EquivalenceClass(const EquivalenceClass &) = default;
+  EquivalenceClass &operator=(const EquivalenceClass &) = default;
+  EquivalenceClass(EquivalenceClass &&) = default;
----------------
NoQ wrote:
> Assignment operator is currently the only thing that makes this class mutable (by allowing to change the `ID` after the class is constructed). Given that we want to put it into the program state, i don't think we want it to be mutable. Can we remove this operator?
Sure, that's a good point!


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:537
+  // true for equality and false for disequality.
+  bool IsEquality = true;
+
----------------
NoQ wrote:
> Do i understand correctly that this isn't used yet and it's for the later patches?
Not exactly, it is used in two symmetric cases:
  # We assumed a condition and we try to understand if what we assumed is an equality operation
  # We try understand something about a symbol and we want to understand if it is an equality operation

So, in the first case, the branch covering `IsEquality == false` does nothing and is designed for the later patches.

The second case, however, does work right now.  If we see an equality operation where operands are known to be a part of the same class, we can tell for sure the result of the comparison.  This way `a == b` is `true` and `a != b` is `false`.  You can find this logic in `getRangeForEqualities`.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1425
+  // merge the smaller class into the bigger one.
+  if (Members.getHeight() >= OtherMembers.getHeight()) {
+    return mergeImpl(BV, F, State, Members, Other, OtherMembers);
----------------
NoQ wrote:
> This makes me slightly worry about nondeterminism: height may depend on things like numeric values of pointers. I guess at the end of the day this will only manifest in choosing a different representative for the merged class, so it shouldn't be too bad, but i'd still rather double-check.
I agree, but as you pointed out correctly, it affects only which ID is used for the class.  Other ID is cease to exist after this function.  ID is used other than for comparison only for trivial classes, which is not going to happen because it is guaranteed to be non-trivial after the merge.  The only thing that it might affect is the ordering in the map, but we already have a problem with that as we use pointers for keys.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1603-1604
 ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef State,
                                            SymbolReaper &SymReaper) {
+  ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
----------------
NoQ wrote:
> Ok, this turned out to be much scarier than i expected. At least, can we somehow assert that our data structures remain internally consistent after these operations? I.e., things like "a symbol points to an equivalence class iff it belongs to the set of members of that class", etc.
Assertion like this might cost us double of what we have in this function right now.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D82445/new/

https://reviews.llvm.org/D82445