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