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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

That's awesome, just a few stylistic tweaks and tests and we are to land!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1561-1562
+
+    if (!Constraint.getConcreteValue())
+      return State;
+
----------------
I think we need a comment why we care about this early exit.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1564
+
+    // Simplify existing constraints.
+    SValBuilder &SVB = getSValBuilder();
----------------
Here I also think that we need to give more context to the readers, so they understand what simplification you are talking about here.


================
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);
----------------
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()]
```


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1575
+        if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
+          // Add the newly simplified symbol to the equivalence class.
+          State =
----------------
It would be great if we provide some justification why we do merge here.


================
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));
----------------
martong wrote:
> 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?
Oh, that's actually even better!

If we consider the following example.
Let `a + b == c` and `a == d` be known and `b == 0` to be a new constraint. Then your approach will help us to figure out that `c == d`.

So, you found a great way!

I think that we should still add the test cases I briefly described in my previous comment and that one from above.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314