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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
