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

[Gabor Marton via Phabricator via cfe-commits]

martong marked 5 inline comments as done.
martong added a comment.

In D103314#2789754 <https://reviews.llvm.org/D103314#2789754>, @vsavchenko wrote:

> I had another thought, `merge` is usually called in situations when we found out that two symbols should be marked equal (and checked that it's possible to begin with), which is not true in your case.
>
> If we update my case from before, we can get: `a + b == c` and `a != c` as given, and `b == 0` as a new constraint. In this situation, you will merge classes `{a + b, c}` and `{a}`, which contradicts our existing disequality information.

Yes, we must check the disequivalence classes to discover such a contradiction, I updated the code to do so.



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



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1576-1577
+          // Add the newly simplified symbol to the equivalence class.
+          State =
+              Class.merge(this->getBasicVals(), F, State,
+                          EquivalenceClass::find(State, SimplifiedMemberSym));
----------------
vsavchenko wrote:
> Uh-oh, almost let yet another null-state bug to happen!  During this iteration, `State` can become null, so we need to check for it.
Good catch!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314