sgatev added a comment.
> Are there plans to get a model/assignment of the variables from the solver?
> That could be helpful for generating warning messages in the future :)
Absolutely! That was only discussed briefly so far. One challenge would be
distilling this model to present only relevant information to the user. That
could also be best effort, of course. It's certainly something I think we
should provide at some point.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:159
+ /// Adds the 3-literal `L1 v L2 v L3` clause to the formula.
+ void addClause(Literal L1, Literal L2, Literal L3) {
+ // The literals are guaranteed to be distinct from properties of BoolValue
----------------
xazax.hun wrote:
> Shouldn't we make this function variadic (or taking a container) instead of
> having multiple overloads?
I'd like to avoid containers here to minimize allocations. I'd love to use a
fold expression, but that's C++ 17. I opted for setting default values for the
last two arguments.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:213
+ // Visit the sub-values of `Val`.
+ if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+ UnprocessedSubVals.push(&C->getLeftSubValue());
----------------
xazax.hun wrote:
> Switch on the kind instead? That way `DisjunctionValue` and
> `ConjunctionValue` could be handled by the same case.
Unfortunately, I don't think we can handle them in the same case because they
don't share a parent that represents a binary operation. Perhaps an improvement
worth considering, as we discussed in one of the previous patches.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:241
+ for (BoolValue *Val : Vals)
+ UnprocessedSubVals.push(Val);
+ while (!UnprocessedSubVals.empty()) {
----------------
xazax.hun wrote:
> While I get that this should be empty before this loop due to the loop
> condition at the previous use, but I find such code confusing. I'd prefer to
> either use a separate queue or have at least an assert to remind us that this
> one should be a clean container before the loop.
I agree that this would be an improvement. I opted for narrowing the scope of
the first container and adding a second container for this operation.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:355
+
+ LevelVars.resize(Formula.LargestVar + 1);
+
----------------
xazax.hun wrote:
> Shouldn't we call the right ctor directly in the initialization list instead
> of resizing a default constructed vector?
Makes complete sense. Updated.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D120289/new/
https://reviews.llvm.org/D120289
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
