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

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1561
+      return nullptr;
+
+    ConstraintMap CM = getConstraintMap(State);
----------------
vsavchenko wrote:
> Also I think we can introduce a simple, but efficient optimization of kicking off the simplification process only when `Constraint` is a constant.
Yes, good point.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1562-1578
+    ConstraintMap CM = getConstraintMap(State);
+    for (auto const &C : CM) {
+      const SymbolRef &ParentSym = C.first;
+      SValBuilder &SVB = getSValBuilder();
+
+      SVal SimplifiedParentVal =
+          SVB.simplifySVal(State, SVB.makeSymbolVal(ParentSym));
----------------
vsavchenko wrote:
> I tried to cover it in the comment to another patch.  This solution includes a lot of extra work and it will lose equality/disequality information for simplified expressions, and I think it's safe to say that if `a == b` then `simplify(a) == b`.
> 
> Let's start with `getConstraintMap`.  It is a completely artificial data structure (and function) that exists for Z3 refutation.  It's not what we keep in the state and it has a lot of duplicated constraints.  If we have an equivalence class `{a, b, c, d, e, f}`, we store only one constraint for all of them (thus when we update the class, or one of the members receives a new constraint, we can update all of them).  `getConstraintMap` returns a map where `a`, `b`, `c`, `d`, `e`, and `f` are mapped to the same constraint.  It's not **super** bad, but it's extra work constructing this map and then processing it.
> 
> Another, and more important aspect is that when you `setConstraint`, you lose information that this symbol is equal/disequal to other symbols.  One example here would be a situation where `x + y == z`, and we find out that `y == 0`, we should update equivalence class `{x + y, z}` to be a class `{x, z}`.  In order to do this, you need to update two maps: `ClassMap` (it's mapping `x + y` to `{x + y, z}`) and `ClassMembers` (it's mapping `{x + y, z}` to `x + y` and `z`).
> 
> Similar example can be made with `x + y != z`, but updating `ClassMap` and `ClassMembers` will fix it.  And you don't even need to touch the actual mapping with the actual constraints.
Absolutely, great findings!

I think the most straightforward and consistent implementation of updating `ClassMap` and `ClassMembers` is to directly use the `merge` method. I.e. we can merge the simplified symbol (as a trivial eq class) to the existing equivalence class. Using `merge`, however, would not remove the non-simplified original symbol. But this might not be a problem; rather it is a necessity (as the child patch demonstrates) it might be very useful if we can find the symbol (without simplification, i.e. as written) in the `ConstraintRange` map. Do you see any drawbacks of reusing `merge` here?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314