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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:452
+  EquivalenceClass(const EquivalenceClass &) = default;
+  EquivalenceClass &operator=(const EquivalenceClass &) = default;
+  EquivalenceClass(EquivalenceClass &&) = default;
----------------
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?


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:537
+  // true for equality and false for disequality.
+  bool IsEquality = true;
+
----------------
Do i understand correctly that this isn't used yet and it's for the later patches?


================
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);
----------------
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.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1603-1604
 ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef State,
                                            SymbolReaper &SymReaper) {
+  ClassMembersTy ClassMembersMap = State->get<ClassMembers>();
----------------
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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D82445