[PATCH] D103314: [Analyzer][solver] Simplify existing constraints when a new constraint is added

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

Awesome!
I know, I said that we are ready to land, but I think I was too excited about this change. We probably should have some data on how it performs on real-life codebases.



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1559
+  // absolute minimum.
+  LLVM_NODISCARD ProgramStateRef simplifyEquivalenceClass(
+      ProgramStateRef State, EquivalenceClass Class, SymbolSet ClassMembers) {
----------------
Maybe it should be a `simplify` method of the class itself?


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1568-1573
+        EquivalenceClass ClassOfSimplifiedSym =
+            EquivalenceClass::find(State, SimplifiedMemberSym);
+        // We are about to add the newly simplified symbol to the existing
+        // equivalence class, but they are known to be non-equal. This is a
+        // contradiction.
+        if (DisequalClasses.contains(ClassOfSimplifiedSym))
----------------
I think we can add a method `isDisequalTo` or just use `areEqual` in a this way:
are equal?
  [Yes] -> nothing to do here
  [No]  -> return nullptr
  [Don't know] -> merge


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1566-1569
+    ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+    for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
+      EquivalenceClass Class = ClassConstraint.first;
+      SymbolSet ClassMembers = Class.getClassMembers(State);
----------------
martong wrote:
> vsavchenko wrote:
> > You don't actually use constraints here, so (let me write it in python) instead of:
> > ```
> > [update(classMap[class]) for class, constraint in constraints.items()]
> > ```
> > you can use
> > ```
> > [update(members) for class, members in classMap.items()]
> > ```
> Actually, trivial equivalence classes (those that have only one symbol member) are not stored in the State. Thus, we must skim through the constraints as well in order to be able to simplify symbols in the constraints.
> In short, we have to iterate both collections.
> 
Ah, I see.  Then I would say that your previous solution is more readable (if we keep `simplify`, of course).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314