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

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko requested changes to this revision.
vsavchenko added a comment.
This revision now requires changes to proceed.

Hey, great job! This is really something that we need, but it's implemented not really correctly.
I tried to cover it in the inline comment.



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


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314