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